Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_cex.ml @ 57d61d67

History | View | Annotate | Download (7.53 KB)

1
(* Rebuilding Cex *)
2
(* In order to properly rebuild the Cex, one needsthe unsliced model. Otherwise
3
   some input or state variables are removed.
4

    
5
*)
6

    
7

    
8
open Lustre_types
9
open Machine_code_types
10
(* open Machine_code_common *)
11
open Zustre_common
12

    
13
open Zustre_data
14

    
15
let get_conjuncts e =
16
  assert (Z3.Boolean.is_bool e);
17
  if Z3.Boolean.is_and e then
18
    Z3.Expr.get_args e
19
  else
20
    [e]
21

    
22
let build_cex machine machines decl_err =
23
  (* Recovering associated top machine (to build full traces) and property *) 
24
  (* TODO: for example extract top node and ok prop. We may have multiple
25
     MAIN/ERR loaded at the same time. Each of them should be assocaited with a
26
     CEX/Inv/Timeout.*)
27
  
28
  let node_id = machine.mname.node_id in
29

    
30
  let cex = match Z3.Fixedpoint.get_answer !fp with Some e -> e | None -> raise Not_found in
31
  (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
32

    
33
  let stats = Z3.Fixedpoint.get_statistics !fp in
34
  
35
  let conjuncts = List.rev (get_conjuncts cex) in
36

    
37
  Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@."
38
    (Z3.Expr.to_string cex)
39
    (List.length conjuncts)
40
    (Utils.fprintf_list ~sep:"@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) conjuncts;
41

    
42
  (* Checking size *)
43
  let inputs = machine.mstep.step_inputs in
44
  let nb_inputs = List.length inputs in
45
  let outputs = machine.mstep.step_outputs in
46
  let nb_outputs = List.length inputs in
47
  let nb_mems = List.length (full_memory_vars machines machine) in
48
  
49
  let main =
50
    List.fold_left (fun accu conj ->
51
    (* Filtering out non MAIN decls *)
52
    let func_decl = Z3.Expr.get_func_decl conj in
53
    let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
54
    (* Focusing only on MAIN_nodeid predicates *)
55
    if node_name = "MAIN_" ^ node_id then
56
      (* Extracting info *)
57
      (* Recall that MAIN args are 
58
	 main_input @ 
59
	 (full_memory_vars machines machine) @
60
	 main_output   *)
61
      let args = Z3.Expr.get_args conj in
62
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
63
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
64
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
65
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
66
	(id, (input_values, output_values))::accu
67
      else
68
	assert false
69
    else
70
      accu 
71
  ) [] conjuncts
72
  in
73
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
74
  List.iter (
75
    fun (id, expr) ->
76
      Format.eprintf "Id %i: %a@."
77
	(id)
78
	(Utils.fprintf_list ~sep:", "
79
	   (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
80
	(fst expr)
81
  ) main;		    
82
   (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
83

    
84
   (* We recover the Zustre XML format, projecting each cex on each input/output
85
      signal *)
86
  let in_signals, out_signals =
87
    List.fold_right (
88
      fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->
89
	let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in
90
	let sigs_in_id = add sigs_in res_sigs_in in
91
	let sigs_out_id = add sigs_out res_sigs_out in
92
	sigs_in_id, sigs_out_id
93
    ) main (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs)
94
  in
95

    
96
  (* let _ = List.mapi (fun k conj -> *)
97
  (*   (\* k-iterate *\) *)
98
  (*   let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
99
  (*   let func_decl = Z3.Expr.get_func_decl conj in *)
100
  (*   if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl); *)
101
  (*   let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *)
102

    
103
   
104
  (*   if !debug then Format.eprintf "Node %s, args %a@." node_name  (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *)
105
    
106
  (*   () *)
107
  (*   (\*  ground_pair = [] *)
108
  (*           try: *)
109
  (*               ground_vars = pred_dict[node_name] *)
110
  (*               ground_pair = zip(ground_vars,ground_val) *)
111
  (*               if "_reset" in node_name: *)
112
  (*                   # this condition is to remove the node nodename_reset added by lustrec *)
113
  (*                   continue *)
114
  (*                   # node = node_name.split("_reset")[0] *)
115
  (*                   # cex_dict.update({node:{k:ground_pair}}) *)
116
  (*               elif "_step" in node_name: *)
117
  (*                   node = node_name.split("_step")[0] *)
118
  (*                   try: *)
119
  (*                       # case in which we already have the node in dict *)
120
  (*                       d = cex_dict[node] *)
121
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
122
  (*                       d.update({(max_key+1):ground_pair}) *)
123
  (*                   except Exception as e: *)
124
  (*                       self._log.warning("Adding a new node cex " + str(e)) *)
125
  (*                       cex_dict.update({node:{k:ground_pair}}) *)
126
  (*               else: *)
127
  (*                   node = node_name *)
128
  (*                   try: *)
129
  (*                       d = cex_dict[node] *)
130
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
131
  (*                       d.update({(max_key+1):ground_pair}) *)
132
  (*                   except Exception as e: *)
133
  (*                       if node not in ["MAIN", "ERR"]: *)
134
  (*                           self._log.warning("Adding a new node cex " + str(e)) *)
135
  (*                           cex_dict.update({node:{k:ground_pair}}) *)
136
  (*           except Exception as e: *)
137
  (*               self._log.warning("Problem with getting a node name: " + str(e)) *)
138
  (*   *\) *)
139
  (* ) conjuncts in *)
140
  (*   let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
141
  (*   if !debug then *)
142
  (*     Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
143
  (* 	(Utils.fprintf_list ~sep:"@ " *)
144
  (*   	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
145
  (* 	rules_expr; *)
146
  (*   if !debug then *)
147
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
148

    
149
  let stats_entries =   Z3.Statistics.get_entries stats in
150
  List.iter (fun e -> Format.eprintf "%s@.@?"
151
    (Z3.Statistics.Entry.to_string e)
152
    
153
  ) stats_entries;
154
  let json : Yojson.json =
155
    `Assoc [
156
      "Results",
157
      `Assoc [
158
	"Property",
159
	`Assoc [
160
	  "name", `String node_id;
161
	  "date", `String (Utils.get_date ());
162
	  "query", `Assoc ["unit", `String "sec";
163
			   "value", `Float (
164
			     let time_opt = Z3.Statistics.get stats "time.spacer.solve" in
165
			     match time_opt with None -> -1.
166
			     | Some f -> Z3.Statistics.Entry.get_float f)
167
			  ];
168
	  "answer", `String "CEX";
169
	  "counterexample",
170
	  `Assoc [
171
	    node_id, `Assoc
172
	      (
173
		List.map (fun (vardecl, values) ->
174
		  vardecl.var_id,
175
		  `Assoc [
176
		    "type", (let _ = Format.fprintf Format.str_formatter "%a" Printers.pp_var_type vardecl in
177
			    let s = Format.flush_str_formatter () in
178
			    `String s);
179
		    "values", `Assoc (List.map (fun (id, v) ->
180
		      string_of_int id, `String (Z3.Expr.to_string v))
181
					values)
182
		  ]   
183
		) in_signals
184
	      )
185
	  ]
186
	]
187
      ]
188
     ]
189
  in
190
  Format.eprintf "JSON: %s@."
191
    (Yojson.to_string json);
192
  ()
193
  (* Results *)
194
  (*   Property *)
195
  (*   Date *)
196
  (*   Query time *)
197
  (*   Answer CEX *)
198
  (*   Counterexample *)
199
  (*     Node name="nodeid" *)
200
  (*       Stream name="opt.x" type="unk" *)
201
  (* 	  Value instant="0">xxx</Value>		       *)
202
  (* () *)
203
	(* ordered_by_signal = self.reorder(cex_dict) *)
204
        (* return self.mk_cex_xml(ordered_by_signal) *)
205

    
206
(* Local Variables: *)
207
(* compile-command:"make -C ../.. lustrev" *)
208
(* End: *)
209

    
210