Project

General

Profile

Revision f4cba4b8 src/normalization.ml

View differences:

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