Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/zustre/zustre_cex.ml | ||
---|---|---|
1 | 1 |
(* Rebuilding Cex *) |
2 | 2 |
(* In order to properly rebuild the Cex, one needsthe unsliced model. Otherwise |
3 |
some input or state variables are removed. |
|
4 |
|
|
5 |
*) |
|
6 |
|
|
3 |
some input or state variables are removed. *) |
|
7 | 4 |
|
8 | 5 |
open Lustre_types |
9 | 6 |
open Machine_code_types |
7 |
|
|
10 | 8 |
(* open Machine_code_common *) |
11 | 9 |
open Zustre_common |
12 |
|
|
13 | 10 |
open Zustre_data |
14 | 11 |
|
15 | 12 |
let get_conjuncts e = |
16 | 13 |
assert (Z3.Boolean.is_bool e); |
17 |
if Z3.Boolean.is_and e then |
|
18 |
Z3.Expr.get_args e |
|
19 |
else |
|
20 |
[e] |
|
14 |
if Z3.Boolean.is_and e then Z3.Expr.get_args e else [ e ] |
|
21 | 15 |
|
22 | 16 |
let build_cex machine machines _decl_err = |
23 |
(* Recovering associated top machine (to build full traces) and property *)
|
|
17 |
(* Recovering associated top machine (to build full traces) and property *) |
|
24 | 18 |
(* TODO: for example extract top node and ok prop. We may have multiple |
25 | 19 |
MAIN/ERR loaded at the same time. Each of them should be assocaited with a |
26 | 20 |
CEX/Inv/Timeout.*) |
27 |
|
|
28 | 21 |
let node_id = machine.mname.node_id in |
29 | 22 |
|
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 *) |
|
23 |
let cex = |
|
24 |
match Z3.Fixedpoint.get_answer !fp with |
|
25 |
| Some e -> |
|
26 |
e |
|
27 |
| None -> |
|
28 |
raise Not_found |
|
29 |
in |
|
32 | 30 |
|
31 |
(* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *) |
|
33 | 32 |
let stats = Z3.Fixedpoint.get_statistics !fp in |
34 |
|
|
33 |
|
|
35 | 34 |
let conjuncts = List.rev (get_conjuncts cex) in |
36 | 35 |
|
37 |
Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@." |
|
38 |
(Z3.Expr.to_string cex) |
|
36 |
Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@." (Z3.Expr.to_string cex) |
|
39 | 37 |
(List.length conjuncts) |
40 |
(Utils.fprintf_list ~sep:"@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) conjuncts; |
|
38 |
(Utils.fprintf_list ~sep:"@ " (fun fmt e -> |
|
39 |
Format.fprintf fmt "%s" (Z3.Expr.to_string e))) |
|
40 |
conjuncts; |
|
41 | 41 |
|
42 | 42 |
(* Checking size *) |
43 | 43 |
let inputs = machine.mstep.step_inputs in |
... | ... | |
45 | 45 |
let outputs = machine.mstep.step_outputs in |
46 | 46 |
let nb_outputs = List.length inputs in |
47 | 47 |
let nb_mems = List.length (full_memory_vars machines machine) in |
48 |
|
|
48 |
|
|
49 | 49 |
let main, _ = |
50 |
List.fold_left (fun (main, funs) 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 in@mems@out *) |
|
58 |
let args = Z3.Expr.get_args conj in |
|
59 |
if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then |
|
60 |
(* Should be done with get_int but that function vanished from the opam Z3 API *) |
|
61 |
let id = Z.to_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) in |
|
62 |
let input_values = Utils.List.extract args 1 (1 + nb_inputs) in |
|
63 |
let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in |
|
64 |
(id, (input_values, output_values))::main, funs |
|
65 |
else |
|
66 |
assert false |
|
67 |
else |
|
68 |
let reg = Str.regexp_string "[a-z]*_step" in |
|
69 |
if Str.string_match reg node_name 0 then ( |
|
70 |
let actual_name = Str.matched_group 0 node_name in |
|
71 |
Format.eprintf "Name %s@." actual_name; |
|
72 |
main, funs |
|
73 |
) |
|
74 |
else ( |
|
75 |
Format.eprintf "pas matché %s@." node_name; |
|
76 |
main, funs |
|
77 |
) |
|
78 |
) ((* main*) [],(* other functions *) []) conjuncts |
|
50 |
List.fold_left |
|
51 |
(fun (main, funs) conj -> |
|
52 |
(* Filtering out non MAIN decls *) |
|
53 |
let func_decl = Z3.Expr.get_func_decl conj in |
|
54 |
let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in |
|
55 |
(* Focusing only on MAIN_nodeid predicates *) |
|
56 |
if node_name = "MAIN_" ^ node_id then |
|
57 |
(* Extracting info *) |
|
58 |
(* Recall that MAIN args are in@mems@out *) |
|
59 |
let args = Z3.Expr.get_args conj in |
|
60 |
if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then |
|
61 |
(* Should be done with get_int but that function vanished from the |
|
62 |
opam Z3 API *) |
|
63 |
let id = |
|
64 |
Z.to_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) |
|
65 |
in |
|
66 |
let input_values = Utils.List.extract args 1 (1 + nb_inputs) in |
|
67 |
let output_values = |
|
68 |
Utils.List.extract args |
|
69 |
(1 + nb_inputs + nb_mems) |
|
70 |
(1 + nb_inputs + nb_mems + nb_outputs) |
|
71 |
in |
|
72 |
(id, (input_values, output_values)) :: main, funs |
|
73 |
else assert false |
|
74 |
else |
|
75 |
let reg = Str.regexp_string "[a-z]*_step" in |
|
76 |
if Str.string_match reg node_name 0 then ( |
|
77 |
let actual_name = Str.matched_group 0 node_name in |
|
78 |
Format.eprintf "Name %s@." actual_name; |
|
79 |
main, funs) |
|
80 |
else ( |
|
81 |
Format.eprintf "pas matché %s@." node_name; |
|
82 |
main, funs)) |
|
83 |
((* main*) |
|
84 |
[], (* other functions *) |
|
85 |
[]) |
|
86 |
conjuncts |
|
79 | 87 |
in |
80 | 88 |
let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in |
81 |
List.iter ( |
|
82 |
fun (id, expr) -> |
|
83 |
Format.eprintf "Id %i: %a@." |
|
84 |
(id) |
|
85 |
(Utils.fprintf_list ~sep:", " |
|
86 |
(fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) |
|
87 |
(fst expr) |
|
88 |
) main; |
|
89 |
(* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *) |
|
90 |
|
|
91 |
(* We recover the Zustre XML format, projecting each cex on each input/output |
|
92 |
signal *) |
|
89 |
List.iter |
|
90 |
(fun (id, expr) -> |
|
91 |
Format.eprintf "Id %i: %a@." id |
|
92 |
(Utils.fprintf_list ~sep:", " (fun fmt e -> |
|
93 |
Format.fprintf fmt "%s" (Z3.Expr.to_string e))) |
|
94 |
(fst expr)) |
|
95 |
main; |
|
96 |
|
|
97 |
(* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args |
|
98 |
conj) in *) |
|
99 |
|
|
100 |
(* We recover the Zustre XML format, projecting each cex on each input/output |
|
101 |
signal *) |
|
93 | 102 |
let in_signals, _ = |
94 |
List.fold_right ( |
|
95 |
fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) -> |
|
96 |
let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in |
|
97 |
let sigs_in_id = add sigs_in res_sigs_in in |
|
98 |
let sigs_out_id = add sigs_out res_sigs_out in |
|
99 |
sigs_in_id, sigs_out_id |
|
100 |
) main (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs) |
|
103 |
List.fold_right |
|
104 |
(fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) -> |
|
105 |
let add l1 l2 = |
|
106 |
List.map2 (fun e1 e2 -> fst e2, (id, e1) :: snd e2) l1 l2 |
|
107 |
in |
|
108 |
let sigs_in_id = add sigs_in res_sigs_in in |
|
109 |
let sigs_out_id = add sigs_out res_sigs_out in |
|
110 |
sigs_in_id, sigs_out_id) |
|
111 |
main |
|
112 |
(List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs) |
|
101 | 113 |
in |
102 | 114 |
|
103 | 115 |
(* let _ = List.mapi (fun k conj -> *) |
104 | 116 |
(* (\* k-iterate *\) *) |
105 |
(* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *) |
|
106 |
(* let func_decl = Z3.Expr.get_func_decl conj in *) |
|
107 |
(* if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl); *) |
|
108 |
(* let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *) |
|
109 |
|
|
110 |
|
|
111 |
(* if !debug then Format.eprintf "Node %s, args %a@." node_name (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *) |
|
112 |
|
|
117 |
(* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args |
|
118 |
conj) in *) |
|
119 |
(* let func_decl = Z3.Expr.get_func_decl conj in *) |
|
120 |
(* if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string |
|
121 |
func_decl); *) |
|
122 |
(* let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *) |
|
123 |
|
|
124 |
(* if !debug then Format.eprintf "Node %s, args %a@." node_name |
|
125 |
(Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *) |
|
126 |
|
|
113 | 127 |
(* () *) |
114 | 128 |
(* (\* ground_pair = [] *) |
115 | 129 |
(* try: *) |
116 | 130 |
(* ground_vars = pred_dict[node_name] *) |
117 | 131 |
(* ground_pair = zip(ground_vars,ground_val) *) |
118 | 132 |
(* if "_reset" in node_name: *) |
119 |
(* # this condition is to remove the node nodename_reset added by lustrec *)
|
|
133 |
(* # this condition is to remove the node nodename_reset added by lustrec *) |
|
120 | 134 |
(* continue *) |
121 | 135 |
(* # node = node_name.split("_reset")[0] *) |
122 | 136 |
(* # cex_dict.update({node:{k:ground_pair}}) *) |
... | ... | |
125 | 139 |
(* try: *) |
126 | 140 |
(* # case in which we already have the node in dict *) |
127 | 141 |
(* d = cex_dict[node] *) |
128 |
(* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *) |
|
142 |
(* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key |
|
143 |
value and add 1 *) |
|
129 | 144 |
(* d.update({(max_key+1):ground_pair}) *) |
130 | 145 |
(* except Exception as e: *) |
131 | 146 |
(* self._log.warning("Adding a new node cex " + str(e)) *) |
... | ... | |
134 | 149 |
(* node = node_name *) |
135 | 150 |
(* try: *) |
136 | 151 |
(* d = cex_dict[node] *) |
137 |
(* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *) |
|
152 |
(* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key |
|
153 |
value and add 1 *) |
|
138 | 154 |
(* d.update({(max_key+1):ground_pair}) *) |
139 | 155 |
(* except Exception as e: *) |
140 | 156 |
(* if node not in ["MAIN", "ERR"]: *) |
141 |
(* self._log.warning("Adding a new node cex " + str(e)) *)
|
|
157 |
(* self._log.warning("Adding a new node cex " + str(e)) *) |
|
142 | 158 |
(* cex_dict.update({node:{k:ground_pair}}) *) |
143 | 159 |
(* except Exception as e: *) |
144 |
(* self._log.warning("Problem with getting a node name: " + str(e)) *)
|
|
160 |
(* self._log.warning("Problem with getting a node name: " + str(e)) *) |
|
145 | 161 |
(* *\) *) |
146 | 162 |
(* ) conjuncts in *) |
147 | 163 |
(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *) |
... | ... | |
156 | 172 |
(* let _ (*stats_entries*) = Z3.Statistics.get_entries stats in *) |
157 | 173 |
(* List.iter (fun e -> Format.eprintf "%s@.@?" *) |
158 | 174 |
(* (Z3.Statistics.Entry.to_string e) *) |
159 |
|
|
175 |
|
|
160 | 176 |
(* ) stats_entries; *) |
161 | 177 |
let json : Yojson.t = |
162 |
`Assoc [ |
|
163 |
"Results", |
|
164 |
`Assoc [ |
|
165 |
"Property", |
|
166 |
`Assoc [ |
|
167 |
"name", `String node_id; |
|
168 |
"date", `String (Utils.get_date ()); |
|
169 |
"query", `Assoc ["unit", `String "sec"; |
|
170 |
"value", `Float ( |
|
171 |
let time_opt = Z3.Statistics.get stats "time.spacer.solve" in |
|
172 |
match time_opt with None -> -1. |
|
173 |
| Some f -> Z3.Statistics.Entry.get_float f) |
|
174 |
]; |
|
175 |
"answer", `String "CEX"; |
|
176 |
"counterexample", |
|
177 |
`Assoc [ |
|
178 |
node_id, `Assoc |
|
179 |
( |
|
180 |
List.map (fun (vardecl, values) -> |
|
181 |
vardecl.var_id, |
|
182 |
`Assoc [ |
|
183 |
"type", (let _ = Format.fprintf Format.str_formatter "%a" Printers.pp_var_type vardecl in |
|
184 |
let s = Format.flush_str_formatter () in |
|
185 |
`String s); |
|
186 |
"values", `Assoc (List.map (fun (id, v) -> |
|
187 |
string_of_int id, `String (Z3.Expr.to_string v)) |
|
188 |
values) |
|
189 |
] |
|
190 |
) in_signals |
|
191 |
) |
|
192 |
] |
|
193 |
] |
|
178 |
`Assoc |
|
179 |
[ |
|
180 |
( "Results", |
|
181 |
`Assoc |
|
182 |
[ |
|
183 |
( "Property", |
|
184 |
`Assoc |
|
185 |
[ |
|
186 |
"name", `String node_id; |
|
187 |
"date", `String (Utils.get_date ()); |
|
188 |
( "query", |
|
189 |
`Assoc |
|
190 |
[ |
|
191 |
"unit", `String "sec"; |
|
192 |
( "value", |
|
193 |
`Float |
|
194 |
(let time_opt = |
|
195 |
Z3.Statistics.get stats "time.spacer.solve" |
|
196 |
in |
|
197 |
match time_opt with |
|
198 |
| None -> |
|
199 |
-1. |
|
200 |
| Some f -> |
|
201 |
Z3.Statistics.Entry.get_float f) ); |
|
202 |
] ); |
|
203 |
"answer", `String "CEX"; |
|
204 |
( "counterexample", |
|
205 |
`Assoc |
|
206 |
[ |
|
207 |
( node_id, |
|
208 |
`Assoc |
|
209 |
(List.map |
|
210 |
(fun (vardecl, values) -> |
|
211 |
( vardecl.var_id, |
|
212 |
`Assoc |
|
213 |
[ |
|
214 |
( "type", |
|
215 |
let _ = |
|
216 |
Format.fprintf Format.str_formatter |
|
217 |
"%a" Printers.pp_var_type vardecl |
|
218 |
in |
|
219 |
let s = |
|
220 |
Format.flush_str_formatter () |
|
221 |
in |
|
222 |
`String s ); |
|
223 |
( "values", |
|
224 |
`Assoc |
|
225 |
(List.map |
|
226 |
(fun (id, v) -> |
|
227 |
( string_of_int id, |
|
228 |
`String |
|
229 |
(Z3.Expr.to_string v) )) |
|
230 |
values) ); |
|
231 |
] )) |
|
232 |
in_signals) ); |
|
233 |
] ); |
|
234 |
] ); |
|
235 |
] ); |
|
194 | 236 |
] |
195 |
] |
|
196 | 237 |
in |
197 |
Format.eprintf "JSON: %s@." |
|
198 |
(Yojson.to_string json); |
|
238 |
Format.eprintf "JSON: %s@." (Yojson.to_string json); |
|
199 | 239 |
() |
200 |
(* Results *)
|
|
201 |
(* Property *)
|
|
202 |
(* Date *)
|
|
203 |
(* Query time *)
|
|
204 |
(* Answer CEX *)
|
|
205 |
(* Counterexample *)
|
|
206 |
(* Node name="nodeid" *)
|
|
207 |
(* Stream name="opt.x" type="unk" *)
|
|
208 |
(* Value instant="0">xxx</Value> *)
|
|
209 |
(* () *)
|
|
210 |
(* ordered_by_signal = self.reorder(cex_dict) *)
|
|
211 |
(* return self.mk_cex_xml(ordered_by_signal) *)
|
|
240 |
(* Results *) |
|
241 |
(* Property *) |
|
242 |
(* Date *) |
|
243 |
(* Query time *) |
|
244 |
(* Answer CEX *) |
|
245 |
(* Counterexample *) |
|
246 |
(* Node name="nodeid" *) |
|
247 |
(* Stream name="opt.x" type="unk" *) |
|
248 |
(* Value instant="0">xxx</Value> *) |
|
249 |
(* () *) |
|
250 |
(* ordered_by_signal = self.reorder(cex_dict) *) |
|
251 |
(* return self.mk_cex_xml(ordered_by_signal) *) |
|
212 | 252 |
|
213 | 253 |
(* Local Variables: *) |
214 | 254 |
(* compile-command:"make -C ../.. lustrev" *) |
215 | 255 |
(* End: *) |
216 |
|
|
217 |
|
Also available in: Unified diff
reformatting