Revision f4cba4b8 src/normalization.ml
src/normalization.ml  

554  554  
555  555 
(* We use node local vars to make sure we are creating fresh variables *) 
556  556 
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s = 
557 
(* Original set of variables actually visible from here: iun/out and


557 
(* Original set of variables actually visible from here: in/out and 

558  558 
spec locals (no node locals) *) 
559  559 
let orig_vars = in_vars @ out_vars @ s.locals in 
560  560 
let not_is_orig_var v = 
...  ...  
593  593 
in 
594  594 

595  595 
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) 
596 


597 


596 
new_locals, defs, 

598  597 
{s with 
599  598 
locals = s.locals @ new_locals; 
600 
stmts = List.map (fun eq > Eq eq) defs;


599 
stmts = [];


601  600 
assume = assume'; 
602  601 
guarantees = guarantees'; 
603  602 
modes = modes' 
...  ...  
644  643 
is_output = (fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs); 
645  644 
} 
646  645 
in 
647 


646  
647 
let eqs, auts = get_node_eqs node in 

648 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

649 
let spec, new_vars, eqs = 

650 
begin 

651 
(* Update mutable fields of eexpr to perform normalization of 

652 
specification. 

653  
654 
Careful: we do not normalize annotations, since they can have the form 

655 
x = (a, b, c) *) 

656 
match node.node_spec with 

657 
 None 

658 
 Some (NodeSpec _) > node.node_spec, [], eqs 

659 
 Some (Contract s) > 

660 
let new_locals, new_stmts, s' = normalize_spec 

661 
decls 

662 
node.node_id 

663 
(node.node_inputs, node.node_outputs, node.node_locals) 

664 
s 

665 
in 

666 
Some (Contract s'), new_locals, new_stmts@eqs 

667 
end 

668 
in 

648  669 
let defs, vars = 
649 
let eqs, auts = get_node_eqs node in 

650 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

651 
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in 

670 
List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in 

652  671 
(* Normalize the asserts *) 
653  672 
let vars, assert_defs, asserts = 
654  673 
List.fold_left ( 
655 
fun (vars, def_accu, assert_accu) assert_ > 

674 
fun (vars, def_accu, assert_accu) assert_ >


656  675 
let assert_expr = assert_.assert_expr in 
657  676 
let (defs, vars'), expr = 
658  677 
normalize_expr 
...  ...  
662  681 
([], vars) (* defvar only contains vars *) 
663  682 
assert_expr 
664  683 
in 
665 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 

684 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)


666  685 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
667 
) (vars, [], []) node.node_asserts in 

686 
) (vars, [], []) node.node_asserts in


668  687 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
669  688 
vars and initial locals ones *) 
670  689 

...  ...  
679  698 
(* Compute traceability info: 
680  699 
 gather newly bound variables 
681  700 
 compute the associated expression without aliases 
682 
*) 

701 
*)


683  702 
let new_annots = 
684  703 
if !Options.traces then 
685  704 
begin 
686  705 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
687  706 
let norm_traceability = { 
688 
annots = List.map (fun v > 

689 
let eq = 

690 
try 

691 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 

692 
with Not_found > 

693 
( 

694 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 

695 
assert false 

696 
) 

697 
in 

698 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 

699 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 

700 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 

701 
(["traceability"], pair) 

702 
) diff_vars; 

703 
annot_loc = Location.dummy_loc 

704 
} 

707 
annots = List.map (fun v >


708 
let eq =


709 
try


710 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs)


711 
with Not_found >


712 
(


713 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id;


714 
assert false


715 
)


716 
in


717 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in


718 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in


719 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];


720 
(["traceability"], pair)


721 
) diff_vars;


722 
annot_loc = Location.dummy_loc


723 
}


705  724 
in 
706  725 
norm_traceability::node.node_annot 
707  726 
end 
...  ...  
711  730  
712  731 
let new_annots = 
713  732 
List.fold_left (fun annots v > 
714 
if Machine_types.is_active && Machine_types.is_exportable v then 

715 
let typ = Machine_types.get_specified_type v in 

716 
let typ_name = Machine_types.type_name typ in 

717  
718 
let loc = v.var_loc in 

719 
let typ_as_string = 

720 
mkexpr 

721 
loc 

722 
(Expr_const 

723 
(Const_string typ_name)) 

724 
in 

725 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 

726 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 

727 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 

728 
else 

729 
annots 

730 
) new_annots new_locals 

731 
in 

732 
let spec = 

733 
begin 

734 
(* Update mutable fields of eexpr to perform normalization of 

735 
specification. 

736  
737 
Careful: we do not normalize annotations, since they can have the form 

738 
x = (a, b, c) *) 

739 
match node.node_spec with None > None  Some s > Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 

740 
end 

733 
if Machine_types.is_active && Machine_types.is_exportable v then 

734 
let typ = Machine_types.get_specified_type v in 

735 
let typ_name = Machine_types.type_name typ in 

736  
737 
let loc = v.var_loc in 

738 
let typ_as_string = 

739 
mkexpr 

740 
loc 

741 
(Expr_const 

742 
(Const_string typ_name)) 

743 
in 

744 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 

745 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 

746 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 

747 
else 

748 
annots 

749 
) new_annots new_locals 

741  750 
in 
742  751 

743  752 

...  ...  
750  759 
node_spec = spec; 
751  760 
} 
752  761 
in ((*Printers.pp_node Format.err_formatter node;*) 
753 
node 

754 
) 

762 
node


763 
)


755  764  
756  765 
let normalize_inode decls nd = 
757  766 
reset_cpt_fresh (); 
758  767 
match nd.nodei_spec with 
759 
None > nd 

760 
 Some s > 

761 
let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in 

762 
{ nd with nodei_spec = Some s } 

763 


768 
None  Some (NodeSpec _) > nd 

769 
 Some (Contract _) > assert false 

770 


764  771 
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl = 
765  772 
match decl.top_decl_desc with 
766  773 
 Node nd > 
Also available in: Unified diff