Revision ca7ff3f7
Added by Lélio Brun 8 months 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