Revision a7062da6
Added by LĂ©lio Brun over 3 years ago
src/backends/Horn/horn_backend_traces.ml | ||
---|---|---|
14 | 14 |
|
15 | 15 |
This is a modified version that handle reset *) |
16 | 16 |
|
17 |
open Utils |
|
17 | 18 |
open Format |
18 | 19 |
open Lustre_types |
19 | 20 |
open Corelang |
... | ... | |
22 | 23 |
open Horn_backend_printers |
23 | 24 |
|
24 | 25 |
let pp_traces = |
25 |
Utils.fprintf_list ~sep:", " (fun fmt (v, e) -> |
|
26 |
Format.fprintf fmt "%s -> %a" v Printers.pp_expr e) |
|
26 |
pp_comma_list (fun fmt (v, e) -> fprintf fmt "%s -> %a" v Printers.pp_expr e) |
|
27 | 27 |
|
28 | 28 |
(* Compute memories associated to each machine *) |
29 | 29 |
let compute_mems machines m = |
... | ... | |
51 | 51 |
let filtered = |
52 | 52 |
List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots |
53 | 53 |
in |
54 |
(* List.iter (Format.eprintf "Annots: %a@." Printers.pp_expr_annot)
|
|
54 |
(* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot) |
|
55 | 55 |
(m.mannot); *) |
56 | 56 |
let content = List.map snd filtered in |
57 | 57 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
... | ... | |
68 | 68 |
assert false) |
69 | 69 |
content |
70 | 70 |
in |
71 |
(* Format.eprintf "Build traces: %a@." pp_traces traces; *)
|
|
71 |
(* eprintf "Build traces: %a@." pp_traces traces; *) |
|
72 | 72 |
m, traces) |
73 | 73 |
machines |
74 | 74 |
|
... | ... | |
90 | 90 |
(* eprintf "Unable to found variable %a in traces (%a)@." |
91 | 91 |
Printers.pp_var v * pp_traces traces; *) |
92 | 92 |
p, |
93 |
mkexpr Location.dummy_loc (Expr_ident v.var_id) ))
|
|
93 |
mkexpr Location.dummy (Expr_ident v.var_id) )) |
|
94 | 94 |
(compute_mems machines m) |
95 | 95 |
|
96 | 96 |
let memories_next machines m = |
... | ... | |
117 | 117 |
false) |
118 | 118 |
m.mname.node_stmts |
119 | 119 |
with _ -> |
120 |
Format.eprintf
|
|
120 |
eprintf |
|
121 | 121 |
"Unable to find definition of %s in stmts %a@.prefix=%a@.@?" |
122 | 122 |
var_id Printers.pp_node_stmts m.mname.node_stmts |
123 |
(Utils.fprintf_list ~sep:"," (fun fmt (id, n) ->
|
|
123 |
(pp_comma_list (fun fmt (id, n) ->
|
|
124 | 124 |
fprintf fmt "(%s,%s)" id n.mname.node_id)) |
125 | 125 |
(List.rev prefix); |
126 | 126 |
|
... | ... | |
140 | 140 |
prefix, def |
141 | 141 |
| _ -> |
142 | 142 |
eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
143 |
(Utils.fprintf_list ~sep:"," (fun fmt (id, n) ->
|
|
143 |
(pp_comma_list (fun fmt (id, n) ->
|
|
144 | 144 |
fprintf fmt "(%s,%s)" id n.mname.node_id)) |
145 | 145 |
(List.rev prefix) Printers.pp_expr ee; |
146 | 146 |
assert false) |
147 | 147 |
(memories_old machines m) |
148 | 148 |
|
149 | 149 |
let pp_prefix_rev fmt prefix = |
150 |
Utils.fprintf_list ~sep:"."
|
|
150 |
pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ".")
|
|
151 | 151 |
(fun fmt (id, n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) |
152 | 152 |
fmt (List.rev prefix) |
153 | 153 |
|
154 | 154 |
let traces_file fmt machines = |
155 |
let pp_l = pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " | ") in |
|
155 | 156 |
fprintf fmt "<?xml version=\"1.0\"?>@."; |
156 | 157 |
fprintf fmt |
157 | 158 |
"<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@."; |
158 | 159 |
fprintf fmt "@[<v 5>@ %a@ @]@." |
159 |
(Utils.fprintf_list ~sep:"@ " (fun fmt m ->
|
|
160 |
(pp_print_list (fun fmt m ->
|
|
160 | 161 |
let pp_var = pp_horn_var m in |
161 | 162 |
let memories_old = memories_old machines m in |
162 | 163 |
let memories_next = memories_next machines m in |
... | ... | |
171 | 172 |
rename_machine_list m.mname.node_id m.mstep.step_outputs |
172 | 173 |
in |
173 | 174 |
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ " |
174 |
(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) |
|
175 |
input_vars |
|
176 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> |
|
177 |
pp_type fmt id.var_type)) |
|
178 |
input_vars |
|
179 |
(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) |
|
180 |
m.mstep.step_inputs; |
|
175 |
(pp_l (pp_horn_var m)) input_vars |
|
176 |
(pp_l (fun fmt id -> pp_type fmt id.var_type)) input_vars |
|
177 |
(pp_l (pp_horn_var m)) m.mstep.step_inputs; |
|
181 | 178 |
|
182 | 179 |
fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ " |
183 |
(Utils.fprintf_list ~sep:" | " pp_var) |
|
184 |
output_vars |
|
185 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> |
|
186 |
pp_type fmt id.var_type)) |
|
187 |
output_vars |
|
188 |
(Utils.fprintf_list ~sep:" | " pp_var) |
|
189 |
m.mstep.step_outputs; |
|
180 |
(pp_l pp_var) output_vars |
|
181 |
(pp_l (fun fmt id -> pp_type fmt id.var_type)) output_vars |
|
182 |
(pp_l pp_var) m.mstep.step_outputs; |
|
190 | 183 |
|
191 | 184 |
let local_vars = |
192 | 185 |
try full_memory_vars ~without_arrow:true machines m |
193 | 186 |
with Not_found -> |
194 |
Format.eprintf "machine %s@.@?" m.mname.node_id;
|
|
187 |
eprintf "machine %s@.@?" m.mname.node_id; |
|
195 | 188 |
assert false |
196 | 189 |
in |
197 | 190 |
let init_local_vars = rename_next_list local_vars in |
198 | 191 |
let step_local_vars = rename_current_list local_vars in |
199 | 192 |
|
200 | 193 |
fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ " |
201 |
(Utils.fprintf_list ~sep:" | " pp_var) |
|
202 |
init_local_vars |
|
203 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> |
|
204 |
pp_type fmt id.var_type)) |
|
194 |
(pp_l pp_var) |
|
205 | 195 |
init_local_vars |
196 |
(pp_l (fun fmt id -> pp_type fmt id.var_type)) init_local_vars |
|
206 | 197 |
(fun fmt -> |
207 | 198 |
match memories_next with [] -> () | _ -> fprintf fmt "") |
208 |
(Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) -> |
|
209 |
fprintf fmt "%a" pp_xml_expr ee)) |
|
199 |
(pp_l (fun fmt (_, ee) -> fprintf fmt "%a" pp_xml_expr ee)) |
|
210 | 200 |
memories_next; |
211 | 201 |
|
212 | 202 |
fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ " |
213 |
(Utils.fprintf_list ~sep:" | " pp_var) |
|
214 |
step_local_vars |
|
215 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> |
|
216 |
pp_type fmt id.var_type)) |
|
217 |
step_local_vars |
|
203 |
(pp_l pp_var) step_local_vars |
|
204 |
(pp_l (fun fmt id -> pp_type fmt id.var_type)) step_local_vars |
|
218 | 205 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "") |
219 |
(Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) -> |
|
220 |
fprintf fmt "(%a)" pp_xml_expr ee)) |
|
206 |
(pp_l (fun fmt (_, ee) -> fprintf fmt "(%a)" pp_xml_expr ee)) |
|
221 | 207 |
memories_old; |
222 | 208 |
|
223 | 209 |
let arrow_vars = arrow_vars machines m in |
224 | 210 |
let arrow_vars_curr = rename_current_list arrow_vars |
225 | 211 |
and arrow_vars_mid = rename_mid_list arrow_vars |
226 | 212 |
and arrow_vars_next = rename_next_list arrow_vars in |
227 |
Utils.fprintf_list ~sep:"@ " |
|
228 |
(fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v) |
|
213 |
pp_print_list (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v) |
|
229 | 214 |
fmt |
230 | 215 |
(arrow_vars_curr @ arrow_vars_mid @ arrow_vars_next); |
231 | 216 |
fprintf fmt "@]@ </Node>")) |
Also available in: Unified diff
another step towards refactoring