1
|
m.mstep.step_instrs
|
2
|
pp_machine_stateless_name m.mname.node_id
|
3
|
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
|
4
|
end
|
5
|
else
|
6
|
begin
|
7
|
(* Declaring predicate *)
|
8
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
9
|
pp_machine_init_name m.mname.node_id
|
10
|
(Utils.fprintf_list ~sep:" " pp_type)
|
11
|
(List.map (fun v -> v.var_type) (init_vars machines m));
|
12
|
|
13
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
14
|
pp_machine_step_name m.mname.node_id
|
15
|
(Utils.fprintf_list ~sep:" " pp_type)
|
16
|
(List.map (fun v -> v.var_type) (step_vars machines m));
|
17
|
|
18
|
Format.pp_print_newline fmt ();
|
19
|
|
20
|
(* Rule for init *)
|
21
|
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
22
|
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
23
|
pp_machine_init_name m.mname.node_id
|
24
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
25
|
|
26
|
(* (\* Rule for step *\) *)
|
27
|
(* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
|
28
|
(* (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
|
29
|
(* pp_machine_step_name m.mname.node_id *)
|
30
|
(* (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
|
31
|
|
32
|
|
33
|
(* Adding assertions *)
|
34
|
(match m.mstep.step_asserts with
|
35
|
| [] ->
|
36
|
begin
|
37
|
(* Rule for init *)
|
38
|
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
39
|
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
40
|
pp_machine_init_name m.mname.node_id
|
41
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
42
|
(* Rule for step*)
|
43
|
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
44
|
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
45
|
pp_machine_step_name m.mname.node_id
|
46
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
|
47
|
end
|
48
|
| assertsl ->
|
49
|
begin
|
50
|
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
|
51
|
(* print_string pp_val; *)
|
52
|
let instrs_concat = m.mstep.step_instrs in
|
53
|
Format.fprintf fmt "; with Assertions @.";
|
54
|
(*Rule for init*)
|
55
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
|
56
|
(pp_conj (pp_instr true m.mname.node_id)) instrs_concat
|
57
|
(pp_conj pp_val) assertsl
|
58
|
pp_machine_init_name m.mname.node_id
|
59
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
60
|
(*Rule for step*)
|
61
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
|
62
|
(pp_conj (pp_instr false m.mname.node_id)) instrs_concat
|
63
|
(pp_conj pp_val) assertsl
|
64
|
pp_machine_step_name m.mname.node_id
|
65
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
|
66
|
(* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
|
67
|
(* (pp_conj pp_val) assertsl; *)
|
68
|
|
69
|
end
|
70
|
);
|
71
|
|
72
|
|
73
|
end
|
74
|
end
|
75
|
|
76
|
|
77
|
|
78
|
let collecting_semantics machines fmt node machine =
|
79
|
Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
|
80
|
(* We print the types of the main node "memory tree" TODO: add the output *)
|
81
|
let main_output =
|
82
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
83
|
in
|
84
|
let main_output_dummy =
|
85
|
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
|
86
|
in
|
87
|
let main_memory_next =
|
88
|
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
|
89
|
main_output
|
90
|
in
|
91
|
let main_memory_current =
|
92
|
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
|
93
|
main_output_dummy
|
94
|
in
|
95
|
|
96
|
(* Special case when the main node is stateless *)
|
97
|
let init_name, step_name =
|
98
|
if is_stateless machine then
|
99
|
pp_machine_stateless_name, pp_machine_stateless_name
|
100
|
else
|
101
|
pp_machine_init_name, pp_machine_step_name
|
102
|
in
|
103
|
|
104
|
Format.fprintf fmt "(declare-rel MAIN (%a))@."
|
105
|
(Utils.fprintf_list ~sep:" " pp_type)
|
106
|
(List.map (fun v -> v.var_type) main_memory_next);
|
107
|
|
108
|
Format.fprintf fmt "; Initial set@.";
|
109
|
Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
|
110
|
Format.fprintf fmt "(rule INIT_STATE)@.";
|
111
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
112
|
init_name node
|
113
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
|
114
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
|
115
|
|
116
|
Format.fprintf fmt "; Inductive def@.";
|
117
|
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
|
118
|
Format.fprintf fmt
|
119
|
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
120
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current
|
121
|
step_name node
|
122
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
|
123
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
|
124
|
|
125
|
let check_prop machines fmt node machine =
|
126
|
let main_output =
|
127
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
128
|
in
|
129
|
let main_memory_next =
|
130
|
(rename_next_list (full_memory_vars machines machine)) @ main_output
|
131
|
in
|
132
|
Format.fprintf fmt "; Property def@.";
|
133
|
Format.fprintf fmt "(declare-rel ERR ())@.";
|
134
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
|
135
|
(pp_conj pp_var) main_output
|
136
|
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
|
137
|
;
|
138
|
Format.fprintf fmt "(query ERR)@."
|
139
|
|
140
|
|
141
|
let cex_computation machines fmt node machine =
|
142
|
Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
|
143
|
(* We print the types of the cex node "memory tree" TODO: add the output *)
|
144
|
let cex_input =
|
145
|
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
|
146
|
in
|
147
|
let cex_input_dummy =
|
148
|
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
|
149
|
in
|
150
|
let cex_output =
|
151
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
152
|
in
|
153
|
let cex_output_dummy =
|
154
|
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
|
155
|
in
|
156
|
let cex_memory_next =
|
157
|
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
|
158
|
in
|
159
|
let cex_memory_current =
|
160
|
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
|
161
|
in
|
162
|
|
163
|
(* Special case when the cex node is stateless *)
|
164
|
let init_name, step_name =
|
165
|
if is_stateless machine then
|
166
|
pp_machine_stateless_name, pp_machine_stateless_name
|
167
|
else
|
168
|
pp_machine_init_name, pp_machine_step_name
|
169
|
in
|
170
|
|
171
|
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
|
172
|
(Utils.fprintf_list ~sep:" " pp_type)
|
173
|
(List.map (fun v -> v.var_type) cex_memory_next);
|
174
|
|
175
|
Format.fprintf fmt "; Initial set@.";
|
176
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
|
177
|
init_name node
|
178
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
|
179
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
|
180
|
|
181
|
Format.fprintf fmt "; Inductive def@.";
|
182
|
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
|
183
|
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
|
184
|
Format.fprintf fmt "(declare-var cexcpt Int)@.";
|
185
|
Format.fprintf fmt
|
186
|
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
|
187
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
|
188
|
step_name node
|
189
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
|
190
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
|
191
|
|
192
|
let get_cex machines fmt node machine =
|
193
|
let cex_input =
|
194
|
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
|
195
|
in
|
196
|
let cex_output =
|
197
|
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
|
198
|
in
|
199
|
let cex_memory_next =
|
200
|
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
|
201
|
in
|
202
|
Format.fprintf fmt "; Property def@.";
|
203
|
Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
|
204
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
|
205
|
(pp_conj pp_var) cex_output
|
206
|
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
|
207
|
;
|
208
|
Format.fprintf fmt "(query CEXTRACE)@."
|
209
|
|
210
|
|
211
|
let main_print machines fmt =
|
212
|
if !Options.main_node <> "" then
|
213
|
begin
|
214
|
let node = !Options.main_node in
|
215
|
let machine = get_machine machines node in
|
216
|
|
217
|
|
218
|
collecting_semantics machines fmt node machine;
|
219
|
check_prop machines fmt node machine;
|
220
|
if !Options.horn_cex then(
|
221
|
cex_computation machines fmt node machine;
|
222
|
get_cex machines fmt node machine)
|
223
|
end
|
224
|
|
225
|
|
226
|
let translate fmt basename prog machines =
|
227
|
List.iter (print_machine machines fmt) (List.rev machines);
|
228
|
main_print machines fmt
|
229
|
|
230
|
|
231
|
let traces_file fmt basename prog machines =
|
232
|
Format.fprintf fmt
|
233
|
"; Horn code traceability generated by %s@.; SVN version number %s@.@."
|
234
|
(Filename.basename Sys.executable_name)
|
235
|
Version.number;
|
236
|
|
237
|
(* We extract the annotation dealing with traceability *)
|
238
|
let machines_traces = List.map (fun m ->
|
239
|
let traces : (ident * expr) list=
|
240
|
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
|
241
|
let filtered =
|
242
|
List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
|
243
|
in
|
244
|
let content = List.map snd filtered in
|
245
|
(* Elements are supposed to be a pair (tuple): variable, expression *)
|
246
|
List.map (fun ee ->
|
247
|
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
|
248
|
| [], Expr_tuple [v;e] -> (
|
249
|
match v.expr_desc with
|
250
|
| Expr_ident vid -> vid, e
|
251
|
| _ -> assert false )
|
252
|
| _ -> assert false)
|
253
|
content
|
254
|
in
|
255
|
|
256
|
m, traces
|
257
|
|
258
|
) machines
|
259
|
in
|
260
|
|
261
|
(* Compute memories associated to each machine *)
|
262
|
let compute_mems m =
|
263
|
let rec aux fst prefix m =
|
264
|
(List.map (fun mem -> (prefix, mem)) m.mmemory) @
|
265
|
List.fold_left (fun accu (id, (n, _)) ->
|
266
|
let name = node_name n in
|
267
|
if name = "_arrow" then accu else
|
268
|
let machine_n = get_machine machines name in
|
269
|
( aux false ((id,machine_n)::prefix) machine_n )
|
270
|
@ accu
|
271
|
) [] m.minstances
|
272
|
in
|
273
|
aux true [] m
|
274
|
in
|
275
|
|
276
|
List.iter (fun m ->
|
277
|
Format.fprintf fmt "; Node %s@." m.mname.node_id;
|
278
|
|
279
|
let memories_old =
|
280
|
List.map (fun (p, v) ->
|
281
|
let machine = match p with | [] -> m | (_,m')::_ -> m' in
|
282
|
let traces = List.assoc machine machines_traces in
|
283
|
if List.mem_assoc v.var_id traces then (
|
284
|
(* We take the expression associated to variable v in the trace info *)
|
285
|
(* Format.eprintf "Found variable %a in traces: %a@." pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
|
286
|
p, List.assoc v.var_id traces
|
287
|
)
|
288
|
else (
|
289
|
(* We keep the variable as is: we create an expression v *)
|
290
|
(* Format.eprintf "Unable to found variable %a in traces (%a)@." pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *)
|
291
|
p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
|
292
|
)
|
293
|
|
294
|
) (compute_mems m)
|
295
|
in
|
296
|
let memories_next = (* We remove the topest pre in each expression *)
|
297
|
List.map
|
298
|
(fun (prefix, ee) ->
|
299
|
match ee.expr_desc with
|
300
|
| Expr_pre e -> prefix, e
|
301
|
| _ -> Format.eprintf
|
302
|
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
|
303
|
(Utils.fprintf_list ~sep:","
|
304
|
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
|
305
|
(List.rev prefix)
|
306
|
Printers.pp_expr ee;
|
307
|
assert false)
|
308
|
memories_old
|
309
|
in
|
310
|
|
311
|
let pp_prefix_rev fmt prefix =
|
312
|
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
|
313
|
in
|
314
|
|
315
|
Format.fprintf fmt "; Init predicate@.";
|
316
|
|
317
|
Format.fprintf fmt "; horn encoding@.";
|
318
|
Format.fprintf fmt "(%a %a)@."
|
319
|
pp_machine_init_name m.mname.node_id
|
320
|
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
321
|
|
322
|
Format.fprintf fmt "; original expressions@.";
|
323
|
Format.fprintf fmt "(%a %a%t%a)@."
|
324
|
pp_machine_init_name m.mname.node_id
|
325
|
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
|
326
|
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
|
327
|
(Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
|
328
|
|
329
|
Format.pp_print_newline fmt ();
|
330
|
Format.fprintf fmt "; Step predicate@.";
|
331
|
|
332
|
Format.fprintf fmt "; horn encoding@.";
|
333
|
Format.fprintf fmt "(%a %a)@."
|
334
|
pp_machine_step_name m.mname.node_id
|
335
|
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
|
336
|
Format.fprintf fmt "; original expressions@.";
|
337
|
Format.fprintf fmt "(%a %a%t%a)@."
|
338
|
pp_machine_step_name m.mname.node_id
|
339
|
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
|
340
|
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
|
341
|
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
|
342
|
Format.pp_print_newline fmt ();
|
343
|
) (List.rev machines);
|
344
|
|
345
|
|
346
|
(* Local Variables: *)
|
347
|
(* compile-command:"make -C ../.." *)
|
348
|
(* End: *)
|