Revision c7c6ef4c
Added by Teme Kahsai over 9 years ago
| src/backends/Horn/horn_backend.ml | ||
|---|---|---|
| 65 | 65 |
let get_machine machines node_name = |
| 66 | 66 |
List.find (fun m -> m.mname.node_id = node_name) machines |
| 67 | 67 |
|
| 68 |
|
|
| 68 | 69 |
let full_memory_vars machines machine = |
| 69 | 70 |
let rec aux fst prefix m = |
| 70 | 71 |
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @ |
| ... | ... | |
| 77 | 78 |
in |
| 78 | 79 |
aux true machine.mname.node_id machine |
| 79 | 80 |
|
| 81 |
|
|
| 80 | 82 |
let stateless_vars machines m = |
| 81 | 83 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
| 82 | 84 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs) |
| ... | ... | |
| 338 | 340 |
(* (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *) |
| 339 | 341 |
|
| 340 | 342 |
|
| 341 |
(* Adding assertions *)
|
|
| 343 |
(* Adding assertions *) |
|
| 342 | 344 |
(match m.mstep.step_asserts with |
| 343 | 345 |
| [] -> |
| 344 | 346 |
begin |
| 347 |
(* Rule for init *) |
|
| 348 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
| 349 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
| 350 |
pp_machine_init_name m.mname.node_id |
|
| 351 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
| 352 |
(* Rule for step*) |
|
| 345 | 353 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
| 346 | 354 |
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
| 347 | 355 |
pp_machine_step_name m.mname.node_id |
| ... | ... | |
| 349 | 357 |
end |
| 350 | 358 |
| assertsl -> |
| 351 | 359 |
begin |
| 352 |
|
|
| 353 | 360 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in |
| 354 | 361 |
(* print_string pp_val; *) |
| 355 | 362 |
let instrs_concat = m.mstep.step_instrs in |
| 356 |
Format.fprintf fmt "; with Invariants @."; |
|
| 363 |
Format.fprintf fmt "; with Assertions @."; |
|
| 364 |
(*Rule for init*) |
|
| 365 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@." |
|
| 366 |
(pp_conj (pp_instr true m.mname.node_id)) instrs_concat |
|
| 367 |
(pp_conj pp_val) assertsl |
|
| 368 |
pp_machine_init_name m.mname.node_id |
|
| 369 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
| 370 |
(*Rule for step*) |
|
| 357 | 371 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@." |
| 358 | 372 |
(pp_conj (pp_instr false m.mname.node_id)) instrs_concat |
| 359 | 373 |
(pp_conj pp_val) assertsl |
| 360 | 374 |
pp_machine_step_name m.mname.node_id |
| 361 | 375 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
| 362 |
|
|
| 363 |
|
|
| 364 | 376 |
(* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *) |
| 365 | 377 |
(* (pp_conj pp_val) assertsl; *) |
| 366 | 378 |
|
| 367 | 379 |
end |
| 368 | 380 |
); |
| 369 | 381 |
|
| 370 |
(* (\* Adding assertions *\) *) |
|
| 371 |
(* (match m.mstep.step_asserts with *) |
|
| 372 |
(* | [] -> () *) |
|
| 373 |
(* | assertsl -> begin *) |
|
| 374 |
(* let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in *) |
|
| 375 |
|
|
| 376 |
(* Format.fprintf fmt "; Asserts@."; *) |
|
| 377 |
(* Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." *) |
|
| 378 |
(* (pp_conj pp_val) assertsl; *) |
|
| 379 |
|
|
| 380 |
(* (\** TEME: the following code is the one we described. But it generates a segfault in z3 *) |
|
| 381 |
(* Format.fprintf fmt "; Asserts for init@."; *) |
|
| 382 |
(* Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." *) |
|
| 383 |
(* (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs *) |
|
| 384 |
(* pp_machine_init_name m.mname.node_id *) |
|
| 385 |
(* (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) *) |
|
| 386 |
(* (pp_conj pp_val) assertsl; *) |
|
| 387 |
|
|
| 388 |
(* Format.fprintf fmt "; Asserts for step@."; *) |
|
| 389 |
(* Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." *) |
|
| 390 |
(* (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs *) |
|
| 391 |
|
|
| 392 |
(* pp_machine_step_name m.mname.node_id *) |
|
| 393 |
(* (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) *) |
|
| 394 |
(* (pp_conj pp_val) assertsl *) |
|
| 395 |
(* *\) *) |
|
| 396 |
(* end *) |
|
| 397 |
(* ); *) |
|
| 398 |
|
|
| 399 |
(* |
|
| 400 |
match m.mspec with |
|
| 401 |
None -> () (* No node spec; we do nothing *) |
|
| 402 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
|
|
| 403 |
( |
|
| 404 |
(* For the moment, we only deal with simple case: single ensures, no other parameters *) |
|
| 405 |
() |
|
| 406 | 382 |
|
| 407 |
) |
|
| 408 |
| _ -> () (* Other cases give nothing *) |
|
| 409 |
*) |
|
| 410 | 383 |
end |
| 411 | 384 |
end |
| 412 | 385 |
|
| ... | ... | |
| 472 | 445 |
(pp_conj pp_var) main_output |
| 473 | 446 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
| 474 | 447 |
; |
| 475 |
if !Options.horn_queries then |
|
| 476 |
Format.fprintf fmt "(query ERR)@." |
|
| 448 |
Format.fprintf fmt "(query ERR)@." |
|
| 477 | 449 |
|
| 478 | 450 |
|
| 479 | 451 |
let cex_computation machines fmt node machine = |
| ... | ... | |
| 543 | 515 |
(pp_conj pp_var) cex_output |
| 544 | 516 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
| 545 | 517 |
; |
| 546 |
if !Options.horn_queries then |
|
| 547 |
Format.fprintf fmt "(query CEXTRACE)@." |
|
| 518 |
Format.fprintf fmt "(query CEXTRACE)@." |
|
| 548 | 519 |
|
| 549 | 520 |
|
| 550 | 521 |
let main_print machines fmt = |
Also available in: Unified diff
Fixed conflict with the svn trunk version
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@417 041b043f-8d7c-46b2-b46e-ef0dd855326e