Revision e4edf171 src/tools/zustre_verifier.ml
src/tools/zustre_verifier.ml  

1 
open LustreSpec 

2 
open Machine_code 

1 
open Lustre_types 

2 
open Machine_code_types 

3 
open Machine_code_common 

3  4 
open Format 
4  5 
(* open Horn_backend_common 
5  6 
* open Horn_backend *) 
...  ...  
16  17 
let rename_mid_list = HBC.rename_mid_list 
17  18 
let rename_next_list = HBC.rename_next_list 
18  19 
let full_memory_vars = HBC.full_memory_vars 
19 


20 
let active = ref false 

21 
let ctx = ref (Z3.mk_context []) 

20 
let inout_vars = HBC.inout_vars 

21 
let reset_vars = HBC.reset_vars 

22 
let step_vars = HBC.step_vars 

23 
let local_memory_vars = HBC.local_memory_vars 

24 


22  25 
let machine_reset_name = HBC.machine_reset_name 
23  26 
let machine_stateless_name = HBC.machine_stateless_name 
24  27  
28 
let rename_mid = HBC.rename_mid 

29  
30 
let preprocess = Horn_backend.preprocess 

31 


32 
let active = ref false 

33 
let ctx = ref (Z3.mk_context []) 

34 
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx) 

35  
25  36 
(** Sorts 
26  37  
27  38 
A sort is introduced for each basic type and each enumerated type. 
...  ...  
105  116 

106  117  
107  118  
108 
(** conversion functions


119 
(** Conversion functions


109  120  
110  121 
The following is similar to the Horn backend. Each printing function 
111  122 
is rephrased from pp_xx to xx_to_expr and produces a Z3 value. 
...  ...  
168  179 
*  Types.Ttuple(l) > assert false 
169  180 
* _ > *) assert false 
170  181  
171  
182 
(* Conversion of basic library functions *) 

183 


172  184 
let horn_basic_app i val_to_expr vl = 
173  185 
match i, vl with 
174  186 
 "ite", [v1; v2; v3] > 
...  ...  
445  457 
in 
446  458 
[expr] 
447  459 
) 
460  
461  
462 


463 
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *) 

464 
(* let rec value_suffix_to_expr self value = *) 

465 
(* match value.value_desc with *) 

466 
(*  Fun (n, vl) > *) 

467 
(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *) 

448  468 

469 
(*  _ > *) 

470 
(* horn_val_to_expr self value *) 

471  
449  472  
473 
(* type_directed assignment: array vs. statically sized type 

474 
 [var_type]: type of variable to be assigned 

475 
 [var_name]: name of variable to be assigned 

476 
 [value]: assigned value 

477 
 [pp_var]: printer for variables 

478 
*) 

479 
let assign_to_exprs m var_name value = 

480 
let self = m.mname.node_id in 

481 
let e = 

482 
Z3.Boolean.mk_eq 

483 
!ctx 

484 
(horn_val_to_expr ~is_lhs:true self var_name) 

485 
(horn_val_to_expr self value) 

486 
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *) 

487 
in 

488 
[e] 

489  
490 


450  491 
(* Convert instruction to Z3.Expr and update the set of reset instances *) 
451 
let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = 

492 
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =


452  493 
match Corelang.get_instr_desc instr with 
453  494 
 MComment _ > [], reset_instances 
454  495 
 MNoReset i > (* we assign middle_mem with mem_m. And declare i as reset *) 
...  ...  
459  500 
i::reset_instances 
460  501 
 MLocalAssign (i,v) > 
461  502 
assign_to_exprs 
462 
m (horn_var_to_expr)


503 
m 

463  504 
(mk_val (LocalVar i) i.var_type) v, 
464  505 
reset_instances 
465  506 
 MStateAssign (i,v) > 
466  507 
assign_to_exprs 
467 
m (horn_var_to_expr)


508 
m 

468  509 
(mk_val (StateVar i) i.var_type) v, 
469  510 
reset_instances 
470  511 
 MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 
...  ...  
487  528 
statement. *) 
488  529 
let self = m.mname.node_id in 
489  530 
let branch_to_expr (tag, instrs) = 
490 
Z3.Boolean.mk_implies 

491 
(Z3.Boolean.mk_eq !ctx 

492 
(horn_val_to_expr self g) 

493 
(horn_tag_to_expr tag)) 

494 
(machine_instrs_to_exprs machines reset_instances m instrs) 

531 
let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in 

532 
let e = 

533 
Z3.Boolean.mk_implies !ctx 

534 
(Z3.Boolean.mk_eq !ctx 

535 
(horn_val_to_expr self g) 

536 
(horn_tag_to_expr tag)) 

537 
branch_def in 

538  
539 
[e], branch_resets 

540 


495  541 
in 
496 
List.map branch_to_expr hl, 

497 
reset_instances 

542 
List.fold_left (fun (instrs, resets) b > 

543 
let b_instrs, b_resets = branch_to_expr b in 

544 
instrs@b_instrs, resets@b_resets 

545 
) ([], reset_instances) hl 

498  546  
499  547 
and instrs_to_expr machines reset_instances m instrs = 
500 
let instr_to_expr rs i = instr_to_expr machines rs m i in 

501 
match instrs with 

502 
 [x] > instr_to_expres reset_instances x 

503 
 _::_ > (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *) 

504  
505 
List.fold_left (fun (exprs, rs) i > 

506 
let exprs_i, rs = ppi rs i in 

507 
expr@exprs_i, rs 

508 
) 

509 
([], reset_instances) instrs 

510 


511 


512 
 [] > [], reset_instances 

513  
514  
515 
let basic_library_to_horn_expr i vl = 

516 
match i, vl with 

517 
 "ite", [v1; v2; v3] > Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 

518  
519 
 "uminus", [v] > Format.fprintf fmt "( %a)" pp_val v 

520 
 "not", [v] > Format.fprintf fmt "(not %a)" pp_val v 

521 
 "=", [v1; v2] > Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 

522 
 "&&", [v1; v2] > Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 

523 
 "", [v1; v2] > Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 

524 
 "impl", [v1; v2] > Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 

525 
 "mod", [v1; v2] > Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 

526 
 "equi", [v1; v2] > Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 

527 
 "xor", [v1; v2] > Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 

528 
 "!=", [v1; v2] > Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 

529 
 "/", [v1; v2] > Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 

530 
 _, [v1; v2] > Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 

531 
 _ > (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false) 

532 
(*  "mod", [v1; v2] > Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 

533  
534 
*) 

548 
let instr_to_exprs rs i = instr_to_exprs machines rs m i in 

549 
let e_list, rs = 

550 
match instrs with 

551 
 [x] > instr_to_exprs reset_instances x 

552 
 _::_ > (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *) 

553 


554 
List.fold_left (fun (exprs, rs) i > 

555 
let exprs_i, rs_i = instr_to_exprs rs i in 

556 
exprs@exprs_i, rs@rs_i 

557 
) 

558 
([], reset_instances) instrs 

559 


560 


561 
 [] > [], reset_instances 

562 
in 

563 
let e = 

564 
match e_list with 

565 
 [e] > e 

566 
 [] > Z3.Boolean.mk_true !ctx 

567 
 _ > Z3.Boolean.mk_and !ctx e_list 

568 
in 

569 
e, rs 

535  570  
536  571 

537 
(* Prints a [value] indexed by the suffix list [loop_vars] *) 

538 
let rec value_suffix_to_expr self value = 

539 
match value.value_desc with 

540 
 Fun (n, vl) > 

541 
basic_library_to_horn_expr n (value_suffix_to_expr self vl) 

542 
 _ > 

543 
horn_val_to_expr self value 

572 
let machine_reset machines m = 

573 
let locals = local_memory_vars machines m in 

574 


575 
(* print "x_m = x_c" for each local memory *) 

576 
let mid_mem_def = 

577 
List.map (fun v > 

578 
Z3.Boolean.mk_eq !ctx 

579 
(horn_var_to_expr (rename_mid v)) 

580 
(horn_var_to_expr (rename_current v)) 

581 
) locals 

582 
in 

544  583  
545 


546 
(* type_directed assignment: array vs. statically sized type 

547 
 [var_type]: type of variable to be assigned 

548 
 [var_name]: name of variable to be assigned 

549 
 [value]: assigned value 

550 
 [pp_var]: printer for variables 

551 
*) 

552 
let assign_to_exprs m var_name value = 

553 
let self = m.mname.node_id in 

554 
let e = 

555 
Z3.Boolean.mk_eq 

556 
!ctx 

557 
(horn_val_to_expr ~is_lhs:true self var_name) 

558 
(value_suffix_to_expr self value) 

584 
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. 

585 
Special treatment for _arrow: _first = true 

586 
*) 

587  
588 
let reset_instances = 

589 


590 
List.map (fun (id, (n, _)) > 

591 
let name = node_name n in 

592 
if name = "_arrow" then ( 

593 
Z3.Boolean.mk_eq !ctx 

594 
( 

595 
let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in 

596 
Z3.Expr.mk_const_f !ctx vdecl 

597 
) 

598 
(Z3.Boolean.mk_true !ctx) 

599 


600 
) else ( 

601 
let machine_n = get_machine machines name in 

602 


603 
Z3.Expr.mk_app 

604 
!ctx 

605 
(get_fdecl (name ^ "_reset")) 

606 
(List.map (horn_var_to_expr) 

607 
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) 

608 
) 

609 


610 
) 

611 
) m.minstances 

612 


613 


559  614 
in 
560 
[e] 

615 


616 
Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances) 

617 


618 


561  619  
562 
(* TODO: empty list means true statement *)


620 
(* TODO: empty list means true statement *) 

563  621 
let decl_machine machines m = 
564 
if m.Machine_code.mname.node_id = Machine_code.arrow_id then


565 
(* We don't print arrow function *)


622 
if m.mname.node_id = Arrow.arrow_id then


623 
(* We don't do arrow function *)


566  624 
() 
567  625 
else 
568  626 
begin 
...  ...  
571  629 
( 
572  630 
(inout_vars machines m)@ 
573  631 
(rename_current_list (full_memory_vars machines m)) @ 
574 
(rename_mid_list (full_memory_vars machines m)) @


575 
(rename_next_list (full_memory_vars machines m)) @


576 
(rename_machine_list m.mname.node_id m.mstep.step_locals)


632 
(rename_mid_list (full_memory_vars machines m)) @ 

633 
(rename_next_list (full_memory_vars machines m)) @ 

634 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 

577  635 
) 
578  636 
in 
579  637 

580  638 
if is_stateless m then 
581  639 
begin 
582  640 
(* Declaring single predicate *) 
583 
let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in 

584 
match m.mstep.step_asserts with 

641 
let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in 

642 
let horn_body, _ (* don't care for reset here *) = 

643 
instrs_to_expr 

644 
machines 

645 
([] (* No reset info for stateless nodes *) ) 

646 
m 

647 
m.mstep.step_instrs 

648 
in 

649 
let horn_head = 

650 
Z3.Expr.mk_app 

651 
!ctx 

652 
(get_fdecl (machine_stateless_name m.mname.node_id)) 

653 
(List.map (horn_var_to_expr) (inout_vars machines m)) 

654 
in 

655 
match m.mstep.step_asserts with 

585  656 
 [] > 
586  657 
begin 
587  
588 
(* Rule for single predicate *) 

589 
fprintf fmt "; Stateless step rule @."; 

590 
fprintf fmt "@[<v 2>(rule (=> @ "; 

591 
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs); 

592 
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." 

593 
pp_machine_stateless_name m.mname.node_id 

594 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m); 

658 
(* Rule for single predicate : "; Stateless step rule @." *) 

659 
Z3.Fixedpoint.add_rule !fp 

660 
(Z3.Boolean.mk_implies !ctx horn_body horn_head) 

661 
None 

595  662 
end 
596  663 
 assertsl > 
597  664 
begin 
598 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in 

599 


600 
fprintf fmt "; Stateless step rule with Assertions @."; 

601 
(*Rule for step*) 

602 
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; 

603 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 

604 
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl 

605 
pp_machine_stateless_name m.mname.node_id 

606 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m); 

607 


665 
(*Rule for step "; Stateless step rule with Assertions @.";*) 

666 
let body_with_asserts = 

667 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 

668 
in 

669 
Z3.Fixedpoint.add_rule !fp 

670 
(Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) 

671 
None 

608  672 
end 
609 


610  673 
end 
611  674 
else 
612  675 
begin 
...  ...  
615  678 
let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in 
616  679  
617  680 
(* Rule for reset *) 
618 
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." 

619 
(pp_machine_reset machines) m 

620 
pp_machine_reset_name m.mname.node_id 

621 
(Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m); 

622  681  
623 
match m.mstep.step_asserts with 

682 
let horn_reset_body = machine_reset machines m in 

683 
let horn_reset_head = 

684 
Z3.Expr.mk_app 

685 
!ctx 

686 
(get_fdecl (machine_reset_name m.mname.node_id)) 

687 
(List.map (horn_var_to_expr) (reset_vars machines m)) 

688 
in 

689 


690 
let _ = 

691 
Z3.Fixedpoint.add_rule !fp 

692 
(Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) 

693 
None 

694 
in 

695  
696 
(* Rule for step*) 

697 
let horn_step_body, _ (* don't care for reset here *) = 

698 
instrs_to_expr 

699 
machines 

700 
[] 

701 
m 

702 
m.mstep.step_instrs 

703 
in 

704 
let horn_step_head = 

705 
Z3.Expr.mk_app 

706 
!ctx 

707 
(get_fdecl (machine_step_name m.mname.node_id)) 

708 
(List.map (horn_var_to_expr) (step_vars machines m)) 

709 
in 

710 
match m.mstep.step_asserts with 

624  711 
 [] > 
625  712 
begin 
626 
fprintf fmt "; Step rule @."; 

627 
(* Rule for step*) 

628 
fprintf fmt "@[<v 2>(rule (=> @ "; 

629 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 

630 
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." 

631 
pp_machine_step_name m.mname.node_id 

632 
(Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m); 

713 
(* Rule for single predicate *) 

714 
Z3.Fixedpoint.add_rule !fp 

715 
(Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head) 

716 
None 

633  717 
end 
634 
 assertsl >


718 
 assertsl > 

635  719 
begin 
636 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in 

637 
(* print_string pp_val; *) 

638 
fprintf fmt "; Step rule with Assertions @."; 

639 


640 
(*Rule for step*) 

641 
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; 

642 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 

643 
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl 

644 
pp_machine_step_name m.mname.node_id 

645 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m); 

720 
(* Rule for step Assertions @.; *) 

721 
let body_with_asserts = 

722 
Z3.Boolean.mk_and !ctx 

723 
(horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 

724 
in 

725 
Z3.Fixedpoint.add_rule !fp 

726 
(Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) 

727 
None 

646  728 
end 
647 


648  729 

649  730 
end 
650  731 
end 
...  ...  
679  760 
Backends.get_normalization_params () 
680  761  
681  762 
let setup_solver () = 
682 
let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in


763 
fp := Z3.Fixedpoint.mk_fixedpoint !ctx;


683  764 
(* let help = Z3.Fixedpoint.get_help fp in 
684  765 
* Format.eprintf "Fp help : %s@." help; 
685  766 
* 
...  ...  
744  825 
P.add_bool params (mks "xform.inline_linear") false; 
745  826 
P.add_bool params (mks "xform.inline_eager") false 
746  827 
); 
747 
Z3.Fixedpoint.set_parameters fp params 

748 


828 
Z3.Fixedpoint.set_parameters !fp params


829 


749  830 

750  831 
let run basename prog machines = 
751 
let machines = Machine_code.arrow_machine::machines in 

832 
let machines = Machine_code_common.arrow_machine::machines in


752  833 
let machines = preprocess machines in 
753  834 
setup_solver (); 
754  835 
decl_sorts (); 
755  836 
List.iter (decl_machine machines) (List.rev machines); 
756  
757 


758  837 
() 
838 


839 


759  840  
760  841 
end: VerifierType.S) 
761  842 

Also available in: Unified diff