Project

General

Profile

Revision 2d2144c0 src/backends/Horn/horn_backend_traces.ml

View differences:

src/backends/Horn/horn_backend_traces.ml
23 23
open Horn_backend_common
24 24
open Horn_backend_printers
25 25

  
26
let pp_traces = (Utils.fprintf_list ~sep:", " (fun fmt (v,e) -> Format.fprintf fmt "%s -> %a"
27
                                                         v
28
                                                         Printers.pp_expr e))
29

  
26 30
(* Compute memories associated to each machine *)
27 31
let compute_mems machines m =
28 32
  let rec aux fst prefix m =
......
46 50
      let filtered =
47 51
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
48 52
      in
53
      (* List.iter (Format.eprintf "Annots: %a@." Printers.pp_expr_annot) (m.mannot); *)
49 54
      let content = List.map snd filtered in
50 55
      (* Elements are supposed to be a pair (tuple): variable, expression *)
51 56
      List.map (fun ee ->
......
57 62
	| _ -> assert false)
58 63
	content
59 64
    in
60

  
65
    (* Format.eprintf "Build traces: %a@." pp_traces traces; *)
61 66
    m, traces
62 67

  
63 68
  ) machines
......
71 76
	(* We take the expression associated to variable v in the trace
72 77
	   info *)
73 78

  
74
	(* eprintf "Found variable %a in traces: %a@."  pp_var v
75
	   Printers.pp_expr (List.assoc v.var_id traces); *)
79
	 (* eprintf "Found variable %a in traces: %a@."  Printers.pp_var v
80
	  *   Printers.pp_expr (List.assoc v.var_id traces);  *)
76 81
	p, List.assoc v.var_id traces
77 82
      )
78 83
    else 
......
80 85

  
81 86
	(* We keep the variable as is: we create an expression v *)
82 87

  
83
	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v
84
	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
85
	   traces); *)	    
88
	 (* eprintf "Unable to found variable %a in traces (%a)@."  Printers.pp_var v
89
	  *   pp_traces traces;  *)
86 90

  
87 91
	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
88 92
      end
......
92 96
let memories_next  machines m = (* We remove the topest pre in each expression *)
93 97
  List.map
94 98
    (fun (prefix, ee) ->
99
      let m = match prefix with | [] -> m | (_,m')::_ -> m' in
95 100
      match ee.expr_desc with
96 101
      | Expr_pre e -> prefix, e
97
      | _ -> eprintf
98
      	"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
99
      	(Utils.fprintf_list ~sep:","
100
      	   (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
101
      	(List.rev prefix)
102
      	Printers.pp_expr ee;
103
      	assert false)
102
      | Expr_ident var_id -> (
103
        (* This memory was not introduced through
104
           normalization. It shall then be a regular x = pre y
105
           expression. Otherwise it would have been rewritten. We
106
           have to get its definition and extract the argument of
107
           the pre *)
108
        
109
        let selected_def =
110
          try  
111
            List.find
112
              (fun def ->
113
                match def with
114
                | Eq eq -> (match eq.eq_lhs with
115
                            | [v] -> v = var_id 
116
                           )
117
                | _ -> false)
118
              m.mname.node_stmts
119
          with _ -> (Format.eprintf
120
                       "Unable to find definition of %s in stmts %a@.prefix=%a@.@?"
121
                       var_id
122
                       Printers.pp_node_stmts m.mname.node_stmts
123
                       (Utils.fprintf_list ~sep:","
124
      	                  (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
125
      	               (List.rev prefix)
126
      	            
127
                    ;
128
                      assert false)
129
        in
130
        let def = match selected_def with
131
          | Eq eq -> (
132
            match eq.eq_lhs, eq.eq_rhs.expr_desc with
133
            | [single_var], Expr_pre e -> if single_var = var_id then e else assert false
134
            | _ -> assert false
135
          )
136
          | _ -> assert false
137
        in
138
        prefix, def
139
      )
140
                           
141
      | _ ->
142
         eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
143
      	   (Utils.fprintf_list ~sep:","
144
      	      (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
145
      	   (List.rev prefix)
146
      	   Printers.pp_expr ee;
147
      	 assert false
148
    )
104 149
    (memories_old machines m)
105 150
      
106 151

  

Also available in: Unified diff