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
|
open Lustre_types
|
6
|
open Machine_code_types
|
7
|
|
8
|
(* open Machine_code_common *)
|
9
|
open Zustre_common
|
10
|
open Zustre_data
|
11
|
|
12
|
let get_conjuncts e =
|
13
|
assert (Z3.Boolean.is_bool e);
|
14
|
if Z3.Boolean.is_and e then Z3.Expr.get_args e else [ e ]
|
15
|
|
16
|
let build_cex machine machines _decl_err =
|
17
|
(* Recovering associated top machine (to build full traces) and property *)
|
18
|
(* TODO: for example extract top node and ok prop. We may have multiple
|
19
|
MAIN/ERR loaded at the same time. Each of them should be assocaited with a
|
20
|
CEX/Inv/Timeout.*)
|
21
|
let node_id = machine.mname.node_id in
|
22
|
|
23
|
let cex =
|
24
|
match Z3.Fixedpoint.get_answer !fp with
|
25
|
| Some e ->
|
26
|
e
|
27
|
| None ->
|
28
|
raise Not_found
|
29
|
in
|
30
|
|
31
|
(* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
|
32
|
let stats = Z3.Fixedpoint.get_statistics !fp in
|
33
|
|
34
|
let conjuncts = List.rev (get_conjuncts cex) in
|
35
|
|
36
|
Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@." (Z3.Expr.to_string cex)
|
37
|
(List.length conjuncts)
|
38
|
(Utils.fprintf_list ~sep:"@ " (fun fmt e ->
|
39
|
Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
|
40
|
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
|
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
|
87
|
in
|
88
|
let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
|
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 *)
|
102
|
let in_signals, _ =
|
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)
|
113
|
in
|
114
|
|
115
|
(* let _ = List.mapi (fun k conj -> *)
|
116
|
(* (\* k-iterate *\) *)
|
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
|
|
127
|
(* () *)
|
128
|
(* (\* ground_pair = [] *)
|
129
|
(* try: *)
|
130
|
(* ground_vars = pred_dict[node_name] *)
|
131
|
(* ground_pair = zip(ground_vars,ground_val) *)
|
132
|
(* if "_reset" in node_name: *)
|
133
|
(* # this condition is to remove the node nodename_reset added by lustrec *)
|
134
|
(* continue *)
|
135
|
(* # node = node_name.split("_reset")[0] *)
|
136
|
(* # cex_dict.update({node:{k:ground_pair}}) *)
|
137
|
(* elif "_step" in node_name: *)
|
138
|
(* node = node_name.split("_step")[0] *)
|
139
|
(* try: *)
|
140
|
(* # case in which we already have the node in dict *)
|
141
|
(* d = cex_dict[node] *)
|
142
|
(* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key
|
143
|
value and add 1 *)
|
144
|
(* d.update({(max_key+1):ground_pair}) *)
|
145
|
(* except Exception as e: *)
|
146
|
(* self._log.warning("Adding a new node cex " + str(e)) *)
|
147
|
(* cex_dict.update({node:{k:ground_pair}}) *)
|
148
|
(* else: *)
|
149
|
(* node = node_name *)
|
150
|
(* try: *)
|
151
|
(* d = cex_dict[node] *)
|
152
|
(* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key
|
153
|
value and add 1 *)
|
154
|
(* d.update({(max_key+1):ground_pair}) *)
|
155
|
(* except Exception as e: *)
|
156
|
(* if node not in ["MAIN", "ERR"]: *)
|
157
|
(* self._log.warning("Adding a new node cex " + str(e)) *)
|
158
|
(* cex_dict.update({node:{k:ground_pair}}) *)
|
159
|
(* except Exception as e: *)
|
160
|
(* self._log.warning("Problem with getting a node name: " + str(e)) *)
|
161
|
(* *\) *)
|
162
|
(* ) conjuncts in *)
|
163
|
(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
|
164
|
(* if !debug then *)
|
165
|
(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
|
166
|
(* (Utils.fprintf_list ~sep:"@ " *)
|
167
|
(* (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
|
168
|
(* rules_expr; *)
|
169
|
(* if !debug then *)
|
170
|
(* Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
|
171
|
|
172
|
(* let _ (*stats_entries*) = Z3.Statistics.get_entries stats in *)
|
173
|
(* List.iter (fun e -> Format.eprintf "%s@.@?" *)
|
174
|
(* (Z3.Statistics.Entry.to_string e) *)
|
175
|
|
176
|
(* ) stats_entries; *)
|
177
|
let json : Yojson.t =
|
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
|
] );
|
236
|
]
|
237
|
in
|
238
|
Format.eprintf "JSON: %s@." (Yojson.to_string json);
|
239
|
()
|
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) *)
|
252
|
|
253
|
(* Local Variables: *)
|
254
|
(* compile-command:"make -C ../.. lustrev" *)
|
255
|
(* End: *)
|