Revision 86ae18b7 src/backends/Horn/horn_backend_traces.ml
src/backends/Horn/horn_backend_traces.ml | ||
---|---|---|
39 | 39 |
|
40 | 40 |
|
41 | 41 |
(* We extract the annotation dealing with traceability *) |
42 |
let machines_traces machines =
|
|
42 |
let machines_traces machines = |
|
43 | 43 |
List.map (fun m -> |
44 | 44 |
let traces : (ident * expr) list= |
45 | 45 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
... | ... | |
61 | 61 |
m, traces |
62 | 62 |
|
63 | 63 |
) machines |
64 |
|
|
64 |
|
|
65 | 65 |
let memories_old machines m = |
66 | 66 |
List.map (fun (p, v) -> |
67 | 67 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
68 | 68 |
let traces = List.assoc machine (machines_traces machines) in |
69 |
if List.mem_assoc v.var_id traces then
|
|
69 |
if List.mem_assoc v.var_id traces then |
|
70 | 70 |
( |
71 | 71 |
(* We take the expression associated to variable v in the trace |
72 | 72 |
info *) |
... | ... | |
75 | 75 |
Printers.pp_expr (List.assoc v.var_id traces); *) |
76 | 76 |
p, List.assoc v.var_id traces |
77 | 77 |
) |
78 |
else
|
|
78 |
else |
|
79 | 79 |
begin |
80 | 80 |
|
81 | 81 |
(* We keep the variable as is: we create an expression v *) |
82 | 82 |
|
83 | 83 |
(* eprintf "Unable to found variable %a in traces (%a)@." pp_var v |
84 | 84 |
(Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst |
85 |
traces); *)
|
|
85 |
traces); *) |
|
86 | 86 |
|
87 | 87 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
88 | 88 |
end |
89 | 89 |
|
90 | 90 |
) (compute_mems machines m) |
91 |
|
|
91 |
|
|
92 | 92 |
let memories_next machines m = (* We remove the topest pre in each expression *) |
93 | 93 |
List.map |
94 | 94 |
(fun (prefix, ee) -> |
... | ... | |
102 | 102 |
Printers.pp_expr ee; |
103 | 103 |
assert false) |
104 | 104 |
(memories_old machines m) |
105 |
|
|
105 |
|
|
106 | 106 |
|
107 | 107 |
|
108 | 108 |
let pp_prefix_rev fmt prefix = |
109 |
Utils.fprintf_list ~sep:"."
|
|
110 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
|
|
111 |
fmt
|
|
109 |
Utils.fprintf_list ~sep:"." |
|
110 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) |
|
111 |
fmt |
|
112 | 112 |
(List.rev prefix) |
113 |
|
|
113 |
|
|
114 | 114 |
|
115 | 115 |
let traces_file fmt basename prog machines = |
116 | 116 |
fprintf fmt "<?xml version=\"1.0\"?>@."; |
... | ... | |
120 | 120 |
let pp_var = pp_horn_var m in |
121 | 121 |
let memories_old = memories_old machines m in |
122 | 122 |
let memories_next = memories_next machines m in |
123 |
|
|
123 |
|
|
124 | 124 |
(* fprintf fmt "; Node %s@." m.mname.node_id; *) |
125 | 125 |
fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id; |
126 |
|
|
126 |
|
|
127 | 127 |
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in |
128 | 128 |
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in |
129 | 129 |
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ " |
... | ... | |
135 | 135 |
(Utils.fprintf_list ~sep:" | " pp_var) output_vars |
136 | 136 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars |
137 | 137 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
138 |
|
|
139 |
let init_local_vars =
|
|
140 |
|
|
141 |
(rename_next_list (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
|
|
142 |
|
|
138 |
|
|
139 |
let init_local_vars = |
|
140 |
(rename_next_list |
|
141 |
(try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
|
|
142 |
|
|
143 | 143 |
|
144 | 144 |
in |
145 | 145 |
let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in |
... | ... | |
160 | 160 |
fprintf fmt "@]@ </Node>"; |
161 | 161 |
)) (List.rev machines); |
162 | 162 |
fprintf fmt "</Traces>@." |
163 |
|
|
163 |
|
|
164 | 164 |
|
165 | 165 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt |
166 | 166 |
"%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) |
Also available in: Unified diff