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
|
|