Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/horn_backend.ml | ||
---|---|---|
20 | 20 |
| Types.Tarrow _ |
21 | 21 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
22 | 22 |
Types.print_ty t; assert false |
23 |
|
|
24 | 23 |
|
25 | 24 |
let pp_decl_var fmt id = |
26 | 25 |
Format.fprintf fmt "(declare-var %s %a)" |
... | ... | |
30 | 29 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
31 | 30 |
|
32 | 31 |
|
32 |
let pp_conj pp fmt l = |
|
33 |
match l with |
|
34 |
[] -> assert false |
|
35 |
| [x] -> pp fmt x |
|
36 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l |
|
37 |
|
|
38 |
|
|
39 |
|
|
33 | 40 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
34 | 41 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
35 | 42 |
let rename_machine p = rename (fun n -> concat p n) |
... | ... | |
134 | 141 |
let (n,_) = List.assoc i m.minstances in |
135 | 142 |
match node_name n, inputs, outputs with |
136 | 143 |
| "_arrow", [i1; i2], [o] -> begin |
137 |
if init then |
|
138 |
pp_assign |
|
139 |
m |
|
140 |
self |
|
141 |
(pp_horn_var m) |
|
142 |
(* (pp_horn_val self (pp_horn_var m) fmt o) *) |
|
143 |
fmt |
|
144 |
o.var_type (LocalVar o) i1 |
|
145 |
else |
|
146 |
pp_assign |
|
147 |
m self (pp_horn_var m) fmt |
|
148 |
o.var_type (LocalVar o) i2 |
|
149 |
|
|
144 |
if init then |
|
145 |
pp_assign |
|
146 |
m |
|
147 |
self |
|
148 |
(pp_horn_var m) |
|
149 |
fmt |
|
150 |
o.var_type (LocalVar o) i1 |
|
151 |
else |
|
152 |
pp_assign |
|
153 |
m self (pp_horn_var m) fmt |
|
154 |
o.var_type (LocalVar o) i2 |
|
155 |
|
|
150 | 156 |
end |
151 | 157 |
| name, _, _ -> |
152 | 158 |
begin |
153 | 159 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
154 | 160 |
if init then |
155 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
156 |
pp_machine_init_name (node_name n) |
|
157 |
(* inputs *) |
|
158 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
159 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
160 |
(* outputs *) |
|
161 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
|
162 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
163 |
(* memories (next) *) |
|
164 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
165 |
rename_machine_list |
|
166 |
(concat m.mname.node_id i) |
|
167 |
(rename_next_list (* concat m.mname.node_id i *) |
|
168 |
(full_memory_vars machines target_machine) |
|
169 |
) |
|
170 |
) |
|
161 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
162 |
pp_machine_init_name (node_name n) |
|
163 |
(* inputs *) |
|
164 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
165 |
inputs |
|
166 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
167 |
(* outputs *) |
|
168 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
169 |
(List.map (fun v -> LocalVar v) outputs) |
|
170 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
171 |
(* memories (next) *) |
|
172 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
173 |
rename_machine_list |
|
174 |
(concat m.mname.node_id i) |
|
175 |
(rename_next_list (full_memory_vars machines target_machine) |
|
176 |
) |
|
177 |
) |
|
171 | 178 |
else |
172 | 179 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
173 | 180 |
pp_machine_step_name (node_name n) |
174 | 181 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
175 | 182 |
(Utils.pp_final_char_if_non_empty " " inputs) |
176 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
|
183 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
184 |
(List.map (fun v -> LocalVar v) outputs) |
|
177 | 185 |
(Utils.pp_final_char_if_non_empty " " outputs) |
178 | 186 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
179 | 187 |
(rename_machine_list |
180 | 188 |
(concat m.mname.node_id i) |
181 |
(rename_current_list (* concat m.mname.node_id i *) |
|
182 |
(full_memory_vars machines target_machine)) |
|
189 |
(rename_current_list (full_memory_vars machines target_machine)) |
|
183 | 190 |
) @ |
184 | 191 |
(rename_machine_list |
185 | 192 |
(concat m.mname.node_id i) |
186 |
(rename_next_list (* concat m.mname.node_id i *) |
|
187 |
(full_memory_vars machines target_machine)) |
|
193 |
(rename_next_list (full_memory_vars machines target_machine)) |
|
188 | 194 |
) |
189 | 195 |
) |
190 | 196 |
|
... | ... | |
194 | 200 |
let (n,_) = List.assoc i m.mcalls in |
195 | 201 |
Format.fprintf fmt "(%s %a%t%a)" |
196 | 202 |
(node_name n) |
197 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
203 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
204 |
inputs |
|
198 | 205 |
(Utils.pp_final_char_if_non_empty " " inputs) |
199 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
|
|
200 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs *)
|
|
206 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
207 |
(List.map (fun v -> LocalVar v) outputs)
|
|
201 | 208 |
) |
202 | 209 |
|
203 | 210 |
let pp_machine_init (m: machine_t) self fmt inst = |
... | ... | |
229 | 236 |
pp_assign |
230 | 237 |
m self (pp_horn_var m) fmt |
231 | 238 |
i.var_type (StateVar i) v |
232 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> assert false (* This should not happen anymore *)
|
|
233 |
(* pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl))) *)
|
|
239 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
240 |
assert false (* This should not happen anymore *)
|
|
234 | 241 |
| MStep (il, i, vl) -> |
235 | 242 |
pp_instance_call machines ~init:init m self fmt i vl il |
236 | 243 |
| MBranch (g,hl) -> |
237 | 244 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
238 | 245 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
239 |
(* may disappear if we optimize code by replacing last branch test with default *)
|
|
246 |
(* may disappear if we optimize code by replacing last branch test with default *)
|
|
240 | 247 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
241 | 248 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
242 | 249 |
pp_conditional machines ~init:init m self fmt g tl el |
... | ... | |
279 | 286 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
280 | 287 |
|
281 | 288 |
(* Rule for single predicate *) |
282 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
|
283 |
(Utils.fprintf_list ~sep:"@ " |
|
284 |
(pp_instr |
|
285 |
true (* In this case, the boolean init can be set to true or false. |
|
286 |
The node is stateless. *) |
|
287 |
m.mname.node_id) |
|
288 |
) |
|
289 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
290 |
(pp_conj (pp_instr |
|
291 |
true (* In this case, the boolean init can be set to true or false. |
|
292 |
The node is stateless. *) |
|
293 |
m.mname.node_id) |
|
294 |
) |
|
289 | 295 |
m.mstep.step_instrs |
290 | 296 |
pp_machine_stateless_name m.mname.node_id |
291 | 297 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
... | ... | |
295 | 301 |
(* Declaring predicate *) |
296 | 302 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
297 | 303 |
pp_machine_init_name m.mname.node_id |
298 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m)); |
|
304 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
305 |
(List.map (fun v -> v.var_type) (init_vars machines m)); |
|
299 | 306 |
|
300 | 307 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
301 | 308 |
pp_machine_step_name m.mname.node_id |
302 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m)); |
|
309 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
310 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
311 |
|
|
303 | 312 |
Format.pp_print_newline fmt (); |
304 | 313 |
|
305 |
(* Rule for init *) |
|
306 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
|
|
307 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
314 |
(* Rule for init *)
|
|
315 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
316 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
308 | 317 |
pp_machine_init_name m.mname.node_id |
309 | 318 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
310 | 319 |
|
311 |
(* Rule for step *) |
|
312 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
|
|
313 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
|
320 |
(* Rule for step *)
|
|
321 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
322 |
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
|
314 | 323 |
pp_machine_step_name m.mname.node_id |
315 | 324 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
325 |
|
|
326 |
(* Adding assertions *) |
|
327 |
(match m.mstep.step_asserts with |
|
328 |
| [] -> () |
|
329 |
| assertsl -> begin |
|
330 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in |
|
331 |
|
|
332 |
Format.fprintf fmt "; Asserts@."; |
|
333 |
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." |
|
334 |
(pp_conj pp_val) assertsl; |
|
335 |
|
|
336 |
(** TEME: the following code is the one we described. But it generates a segfault in z3 |
|
337 |
Format.fprintf fmt "; Asserts for init@."; |
|
338 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." |
|
339 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
340 |
pp_machine_init_name m.mname.node_id |
|
341 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) |
|
342 |
(pp_conj pp_val) assertsl; |
|
343 |
|
|
344 |
Format.fprintf fmt "; Asserts for step@."; |
|
345 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." |
|
346 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
|
347 |
|
|
348 |
pp_machine_step_name m.mname.node_id |
|
349 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) |
|
350 |
(pp_conj pp_val) assertsl |
|
351 |
*) |
|
352 |
end |
|
353 |
); |
|
354 |
|
|
316 | 355 |
(* |
317 | 356 |
match m.mspec with |
318 | 357 |
None -> () (* No node spec; we do nothing *) |
... | ... | |
329 | 368 |
|
330 | 369 |
|
331 | 370 |
|
332 |
let main_print machines fmt = |
|
333 |
if !Options.main_node <> "" then |
|
334 |
begin |
|
335 |
let node = !Options.main_node in |
|
336 |
let machine = get_machine machines node in |
|
337 |
|
|
371 |
let collecting_semantics machines fmt node machine = |
|
338 | 372 |
Format.fprintf fmt "; Collecting semantics for node %s@.@." node; |
339 | 373 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
340 | 374 |
let main_output = |
... | ... | |
359 | 393 |
else |
360 | 394 |
pp_machine_init_name, pp_machine_step_name |
361 | 395 |
in |
362 |
|
|
396 |
|
|
363 | 397 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
364 | 398 |
(Utils.fprintf_list ~sep:" " pp_type) |
365 | 399 |
(List.map (fun v -> v.var_type) main_memory_next); |
... | ... | |
379 | 413 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
380 | 414 |
step_name node |
381 | 415 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
382 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
|
|
416 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
383 | 417 |
|
384 |
Format.fprintf fmt "; Property def@."; |
|
385 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
|
386 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@." |
|
387 |
(Utils.fprintf_list ~sep:" " pp_var) main_output |
|
388 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
418 |
let check_prop machines fmt node machine = |
|
419 |
let main_output = |
|
420 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
421 |
in |
|
422 |
let main_memory_next = |
|
423 |
(rename_next_list (full_memory_vars machines machine)) @ main_output |
|
424 |
in |
|
425 |
Format.fprintf fmt "; Property def@."; |
|
426 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
|
427 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
|
428 |
(pp_conj pp_var) main_output |
|
429 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
389 | 430 |
; |
390 |
Format.fprintf fmt "(query ERR)@."; |
|
431 |
if !Options.horn_queries then |
|
432 |
Format.fprintf fmt "(query ERR)@." |
|
391 | 433 |
|
392 |
() |
|
434 |
|
|
435 |
let cex_computation machines fmt node machine = |
|
436 |
Format.fprintf fmt "; CounterExample computation for node %s@.@." node; |
|
437 |
(* We print the types of the cex node "memory tree" TODO: add the output *) |
|
438 |
let cex_input = |
|
439 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
440 |
in |
|
441 |
let cex_input_dummy = |
|
442 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
|
443 |
in |
|
444 |
let cex_output = |
|
445 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
446 |
in |
|
447 |
let cex_output_dummy = |
|
448 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
|
449 |
in |
|
450 |
let cex_memory_next = |
|
451 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
452 |
in |
|
453 |
let cex_memory_current = |
|
454 |
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
|
455 |
in |
|
456 |
|
|
457 |
(* Special case when the cex node is stateless *) |
|
458 |
let init_name, step_name = |
|
459 |
if is_stateless machine then |
|
460 |
pp_machine_stateless_name, pp_machine_stateless_name |
|
461 |
else |
|
462 |
pp_machine_init_name, pp_machine_step_name |
|
463 |
in |
|
464 |
|
|
465 |
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@." |
|
466 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
467 |
(List.map (fun v -> v.var_type) cex_memory_next); |
|
468 |
|
|
469 |
Format.fprintf fmt "; Initial set@."; |
|
470 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@." |
|
471 |
init_name node |
|
472 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
|
473 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ; |
|
474 |
|
|
475 |
Format.fprintf fmt "; Inductive def@."; |
|
476 |
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
|
477 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
|
478 |
Format.fprintf fmt "(declare-var cexcpt Int)@."; |
|
479 |
Format.fprintf fmt |
|
480 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
|
481 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current |
|
482 |
step_name node |
|
483 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
|
484 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
485 |
|
|
486 |
let get_cex machines fmt node machine = |
|
487 |
let cex_input = |
|
488 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
489 |
in |
|
490 |
let cex_output = |
|
491 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
492 |
in |
|
493 |
let cex_memory_next = |
|
494 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
495 |
in |
|
496 |
Format.fprintf fmt "; Property def@."; |
|
497 |
Format.fprintf fmt "(declare-rel CEXTRACE ())@."; |
|
498 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
|
499 |
(pp_conj pp_var) cex_output |
|
500 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
501 |
; |
|
502 |
if !Options.horn_queries then |
|
503 |
Format.fprintf fmt "(query CEXTRACE)@." |
|
504 |
|
|
505 |
|
|
506 |
let main_print machines fmt = |
|
507 |
if !Options.main_node <> "" then |
|
508 |
begin |
|
509 |
let node = !Options.main_node in |
|
510 |
let machine = get_machine machines node in |
|
511 |
|
|
512 |
|
|
513 |
collecting_semantics machines fmt node machine; |
|
514 |
check_prop machines fmt node machine; |
|
515 |
|
|
516 |
cex_computation machines fmt node machine; |
|
517 |
get_cex machines fmt node machine |
|
393 | 518 |
end |
394 | 519 |
|
395 | 520 |
|
... | ... | |
399 | 524 |
main_print machines fmt |
400 | 525 |
|
401 | 526 |
|
527 |
let traces_file fmt basename prog machines = |
|
528 |
Format.fprintf fmt |
|
529 |
"; Horn code traceability generated by %s@.; SVN version number %s@.@." |
|
530 |
(Filename.basename Sys.executable_name) |
|
531 |
Version.number; |
|
532 |
|
|
533 |
(* We extract the annotation dealing with traceability *) |
|
534 |
let machines_traces = List.map (fun m -> |
|
535 |
let traces : (ident * expr) list= |
|
536 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
|
537 |
let filtered = |
|
538 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots |
|
539 |
in |
|
540 |
let content = List.map snd filtered in |
|
541 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
|
542 |
List.map (fun ee -> |
|
543 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
|
544 |
| [], Expr_tuple [v;e] -> ( |
|
545 |
match v.expr_desc with |
|
546 |
| Expr_ident vid -> vid, e |
|
547 |
| _ -> assert false ) |
|
548 |
| _ -> assert false) |
|
549 |
content |
|
550 |
in |
|
551 |
|
|
552 |
m, traces |
|
553 |
|
|
554 |
) machines |
|
555 |
in |
|
556 |
|
|
557 |
(* Compute memories associated to each machine *) |
|
558 |
let compute_mems m = |
|
559 |
let rec aux fst prefix m = |
|
560 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
|
561 |
List.fold_left (fun accu (id, (n, _)) -> |
|
562 |
let name = node_name n in |
|
563 |
if name = "_arrow" then accu else |
|
564 |
let machine_n = get_machine machines name in |
|
565 |
( aux false ((id,machine_n)::prefix) machine_n ) |
|
566 |
@ accu |
|
567 |
) [] m.minstances |
|
568 |
in |
|
569 |
aux true [] m |
|
570 |
in |
|
571 |
|
|
572 |
List.iter (fun m -> |
|
573 |
Format.fprintf fmt "; Node %s@." m.mname.node_id; |
|
574 |
|
|
575 |
let memories_old = |
|
576 |
List.map (fun (p, v) -> |
|
577 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
|
578 |
let traces = List.assoc machine machines_traces in |
|
579 |
if List.mem_assoc v.var_id traces then |
|
580 |
(* We take the expression associated to variable v in the trace info *) |
|
581 |
p, List.assoc v.var_id traces |
|
582 |
else |
|
583 |
(* We keep the variable as is: we create an expression v *) |
|
584 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
|
585 |
|
|
586 |
) (compute_mems m) |
|
587 |
in |
|
588 |
let memories_next = (* We remove the topest pre in each expression *) |
|
589 |
List.map |
|
590 |
(fun (prefix, ee) -> |
|
591 |
match ee.expr_desc with |
|
592 |
| Expr_pre e -> prefix, e |
|
593 |
| _ -> Format.eprintf |
|
594 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
595 |
(Utils.fprintf_list ~sep:"," |
|
596 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
597 |
(List.rev prefix) |
|
598 |
Printers.pp_expr ee; |
|
599 |
assert false) |
|
600 |
memories_old |
|
601 |
in |
|
602 |
|
|
603 |
let pp_prefix_rev fmt prefix = |
|
604 |
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) |
|
605 |
in |
|
606 |
|
|
607 |
Format.fprintf fmt "; Init predicate@."; |
|
608 |
|
|
609 |
Format.fprintf fmt "; horn encoding@."; |
|
610 |
Format.fprintf fmt "(%a %a)@." |
|
611 |
pp_machine_init_name m.mname.node_id |
|
612 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
613 |
|
|
614 |
Format.fprintf fmt "; original expressions@."; |
|
615 |
Format.fprintf fmt "(%a %a%t%a)@." |
|
616 |
pp_machine_init_name m.mname.node_id |
|
617 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
|
618 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ") |
|
619 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; |
|
620 |
|
|
621 |
Format.pp_print_newline fmt (); |
|
622 |
Format.fprintf fmt "; Step predicate@."; |
|
623 |
|
|
624 |
Format.fprintf fmt "; horn encoding@."; |
|
625 |
Format.fprintf fmt "(%a %a)@." |
|
626 |
pp_machine_step_name m.mname.node_id |
|
627 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
|
628 |
Format.fprintf fmt "; original expressions@."; |
|
629 |
Format.fprintf fmt "(%a %a%t%a)@." |
|
630 |
pp_machine_step_name m.mname.node_id |
|
631 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
|
632 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ") |
|
633 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next); |
|
634 |
Format.pp_print_newline fmt (); |
|
635 |
) (List.rev machines); |
|
636 |
|
|
637 |
|
|
402 | 638 |
(* Local Variables: *) |
403 | 639 |
(* compile-command:"make -C .." *) |
404 | 640 |
(* End: *) |
Also available in: Unified diff
Merged horn_traces branch