Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/Horn/horn_backend_traces.ml | ||
---|---|---|
12 | 12 |
(* The compilation presented here was first defined in Garoche, Gurfinkel, |
13 | 13 |
Kahsai, HCSV'14. |
14 | 14 |
|
15 |
This is a modified version that handle reset |
|
16 |
*) |
|
15 |
This is a modified version that handle reset *) |
|
17 | 16 |
|
18 | 17 |
open Format |
19 | 18 |
open Lustre_types |
20 | 19 |
open Corelang |
21 | 20 |
open Machine_code_types |
22 |
|
|
23 | 21 |
open Horn_backend_common |
24 | 22 |
open Horn_backend_printers |
25 | 23 |
|
26 |
let pp_traces = (Utils.fprintf_list ~sep:", " (fun fmt (v,e) -> Format.fprintf fmt "%s -> %a"
|
|
27 |
v
|
|
28 |
Printers.pp_expr e))
|
|
24 |
let pp_traces = |
|
25 |
Utils.fprintf_list ~sep:", " (fun fmt (v, e) ->
|
|
26 |
Format.fprintf fmt "%s -> %a" v Printers.pp_expr e)
|
|
29 | 27 |
|
30 | 28 |
(* Compute memories associated to each machine *) |
31 | 29 |
let compute_mems machines m = |
32 | 30 |
let rec aux fst prefix m = |
33 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
|
34 |
List.fold_left (fun accu (id, (n, _)) -> |
|
35 |
let name = node_name n in |
|
36 |
if name = "_arrow" then accu else |
|
37 |
let machine_n = get_machine machines name in |
|
38 |
( aux false ((id,machine_n)::prefix) machine_n ) |
|
39 |
@ accu |
|
40 |
) [] m.minstances |
|
31 |
List.map (fun mem -> prefix, mem) m.mmemory |
|
32 |
@ List.fold_left |
|
33 |
(fun accu (id, (n, _)) -> |
|
34 |
let name = node_name n in |
|
35 |
if name = "_arrow" then accu |
|
36 |
else |
|
37 |
let machine_n = get_machine machines name in |
|
38 |
aux false ((id, machine_n) :: prefix) machine_n @ accu) |
|
39 |
[] m.minstances |
|
41 | 40 |
in |
42 | 41 |
aux true [] m |
43 | 42 |
|
44 |
|
|
45 | 43 |
(* We extract the annotation dealing with traceability *) |
46 |
let machines_traces machines = |
|
47 |
List.map (fun m -> |
|
48 |
let traces : (ident * expr) list= |
|
49 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
|
50 |
let filtered = |
|
51 |
List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots |
|
44 |
let machines_traces machines = |
|
45 |
List.map |
|
46 |
(fun m -> |
|
47 |
let traces : (ident * expr) list = |
|
48 |
let all_annots = |
|
49 |
List.flatten (List.map (fun ann -> ann.annots) m.mannot) |
|
50 |
in |
|
51 |
let filtered = |
|
52 |
List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots |
|
53 |
in |
|
54 |
(* List.iter (Format.eprintf "Annots: %a@." Printers.pp_expr_annot) |
|
55 |
(m.mannot); *) |
|
56 |
let content = List.map snd filtered in |
|
57 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
|
58 |
List.map |
|
59 |
(fun ee -> |
|
60 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
|
61 |
| [], Expr_tuple [ v; e ] -> ( |
|
62 |
match v.expr_desc with |
|
63 |
| Expr_ident vid -> |
|
64 |
vid, e |
|
65 |
| _ -> |
|
66 |
assert false) |
|
67 |
| _ -> |
|
68 |
assert false) |
|
69 |
content |
|
52 | 70 |
in |
53 |
(* List.iter (Format.eprintf "Annots: %a@." Printers.pp_expr_annot) (m.mannot); *) |
|
54 |
let content = List.map snd filtered in |
|
55 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
|
56 |
List.map (fun ee -> |
|
57 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
|
58 |
| [], Expr_tuple [v;e] -> ( |
|
59 |
match v.expr_desc with |
|
60 |
| Expr_ident vid -> vid, e |
|
61 |
| _ -> assert false ) |
|
62 |
| _ -> assert false) |
|
63 |
content |
|
64 |
in |
|
65 |
(* Format.eprintf "Build traces: %a@." pp_traces traces; *) |
|
66 |
m, traces |
|
67 |
|
|
68 |
) machines |
|
69 |
|
|
71 |
(* Format.eprintf "Build traces: %a@." pp_traces traces; *) |
|
72 |
m, traces) |
|
73 |
machines |
|
74 |
|
|
70 | 75 |
let memories_old machines m = |
71 |
List.map (fun (p, v) -> |
|
72 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
|
73 |
let traces = List.assoc machine (machines_traces machines) in |
|
74 |
if List.mem_assoc v.var_id traces then |
|
75 |
( |
|
76 |
(* We take the expression associated to variable v in the trace |
|
77 |
info *) |
|
78 |
|
|
79 |
(* eprintf "Found variable %a in traces: %a@." Printers.pp_var v |
|
80 |
* Printers.pp_expr (List.assoc v.var_id traces); *) |
|
81 |
p, List.assoc v.var_id traces |
|
82 |
) |
|
83 |
else |
|
84 |
begin |
|
85 |
|
|
86 |
(* We keep the variable as is: we create an expression v *) |
|
87 |
|
|
88 |
(* eprintf "Unable to found variable %a in traces (%a)@." Printers.pp_var v |
|
89 |
* pp_traces traces; *) |
|
90 |
|
|
91 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
|
92 |
end |
|
93 |
|
|
94 |
) (compute_mems machines m) |
|
95 |
|
|
96 |
let memories_next machines m = (* We remove the topest pre in each expression *) |
|
76 |
List.map |
|
77 |
(fun (p, v) -> |
|
78 |
let machine = match p with [] -> m | (_, m') :: _ -> m' in |
|
79 |
let traces = List.assoc machine (machines_traces machines) in |
|
80 |
if List.mem_assoc v.var_id traces then |
|
81 |
( (* We take the expression associated to variable v in the trace info *) |
|
82 |
|
|
83 |
(* eprintf "Found variable %a in traces: %a@." Printers.pp_var v * |
|
84 |
Printers.pp_expr (List.assoc v.var_id traces); *) |
|
85 |
p, |
|
86 |
List.assoc v.var_id traces ) |
|
87 |
else |
|
88 |
( (* We keep the variable as is: we create an expression v *) |
|
89 |
|
|
90 |
(* eprintf "Unable to found variable %a in traces (%a)@." |
|
91 |
Printers.pp_var v * pp_traces traces; *) |
|
92 |
p, |
|
93 |
mkexpr Location.dummy_loc (Expr_ident v.var_id) )) |
|
94 |
(compute_mems machines m) |
|
95 |
|
|
96 |
let memories_next machines m = |
|
97 |
(* We remove the topest pre in each expression *) |
|
97 | 98 |
List.map |
98 | 99 |
(fun (prefix, ee) -> |
99 |
let m = match prefix with | [] -> m | (_,m')::_ -> m' in
|
|
100 |
let m = match prefix with [] -> m | (_, m') :: _ -> m' in
|
|
100 | 101 |
match ee.expr_desc with |
101 |
| Expr_pre e -> prefix, e
|
|
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 |
|
102 |
| Expr_pre e -> |
|
103 |
prefix, e
|
|
104 |
| Expr_ident var_id ->
|
|
105 |
(* This memory was not introduced through normalization. It shall then
|
|
106 |
be a regular x = pre y expression. Otherwise it would have been
|
|
107 |
rewritten. We have to get its definition and extract the argument of
|
|
107 | 108 |
the pre *) |
108 |
|
|
109 | 109 |
let selected_def = |
110 |
try
|
|
110 |
try |
|
111 | 111 |
List.find |
112 | 112 |
(fun def -> |
113 | 113 |
match def with |
114 |
| Eq eq -> (match eq.eq_lhs with |
|
115 |
| [v] -> v = var_id |
|
116 |
| _ -> assert false |
|
117 |
) |
|
118 |
| _ -> false) |
|
114 |
| Eq eq -> ( |
|
115 |
match eq.eq_lhs with [ v ] -> v = var_id | _ -> assert false) |
|
116 |
| _ -> |
|
117 |
false) |
|
119 | 118 |
m.mname.node_stmts |
120 |
with _ -> (Format.eprintf |
|
121 |
"Unable to find definition of %s in stmts %a@.prefix=%a@.@?" |
|
122 |
var_id |
|
123 |
Printers.pp_node_stmts m.mname.node_stmts |
|
124 |
(Utils.fprintf_list ~sep:"," |
|
125 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
126 |
(List.rev prefix) |
|
127 |
|
|
128 |
; |
|
129 |
assert false) |
|
119 |
with _ -> |
|
120 |
Format.eprintf |
|
121 |
"Unable to find definition of %s in stmts %a@.prefix=%a@.@?" |
|
122 |
var_id Printers.pp_node_stmts m.mname.node_stmts |
|
123 |
(Utils.fprintf_list ~sep:"," (fun fmt (id, n) -> |
|
124 |
fprintf fmt "(%s,%s)" id n.mname.node_id)) |
|
125 |
(List.rev prefix); |
|
126 |
|
|
127 |
assert false |
|
130 | 128 |
in |
131 |
let def = match selected_def with |
|
129 |
let def = |
|
130 |
match selected_def with |
|
132 | 131 |
| Eq eq -> ( |
133 | 132 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
134 |
| [single_var], Expr_pre e -> if single_var = var_id then e else assert false |
|
135 |
| _ -> assert false |
|
136 |
) |
|
137 |
| _ -> assert false |
|
133 |
| [ single_var ], Expr_pre e -> |
|
134 |
if single_var = var_id then e else assert false |
|
135 |
| _ -> |
|
136 |
assert false) |
|
137 |
| _ -> |
|
138 |
assert false |
|
138 | 139 |
in |
139 | 140 |
prefix, def |
140 |
) |
|
141 |
|
|
142 | 141 |
| _ -> |
143 |
eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
144 |
(Utils.fprintf_list ~sep:"," |
|
145 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
146 |
(List.rev prefix) |
|
147 |
Printers.pp_expr ee; |
|
148 |
assert false |
|
149 |
) |
|
142 |
eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
143 |
(Utils.fprintf_list ~sep:"," (fun fmt (id, n) -> |
|
144 |
fprintf fmt "(%s,%s)" id n.mname.node_id)) |
|
145 |
(List.rev prefix) Printers.pp_expr ee; |
|
146 |
assert false) |
|
150 | 147 |
(memories_old machines m) |
151 |
|
|
152 |
|
|
153 | 148 |
|
154 | 149 |
let pp_prefix_rev fmt prefix = |
155 |
Utils.fprintf_list ~sep:"." |
|
156 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) |
|
157 |
fmt |
|
158 |
(List.rev prefix) |
|
159 |
|
|
150 |
Utils.fprintf_list ~sep:"." |
|
151 |
(fun fmt (id, n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) |
|
152 |
fmt (List.rev prefix) |
|
160 | 153 |
|
161 | 154 |
let traces_file fmt machines = |
162 | 155 |
fprintf fmt "<?xml version=\"1.0\"?>@."; |
163 |
fprintf fmt "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@."; |
|
156 |
fprintf fmt |
|
157 |
"<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@."; |
|
164 | 158 |
fprintf fmt "@[<v 5>@ %a@ @]@." |
165 | 159 |
(Utils.fprintf_list ~sep:"@ " (fun fmt m -> |
166 |
let pp_var = pp_horn_var m in |
|
167 |
let memories_old = memories_old machines m in |
|
168 |
let memories_next = memories_next machines m in |
|
169 |
|
|
170 |
(* fprintf fmt "; Node %s@." m.mname.node_id; *) |
|
171 |
fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id; |
|
172 |
|
|
173 |
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in |
|
174 |
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in |
|
175 |
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ " |
|
176 |
(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) input_vars |
|
177 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) input_vars |
|
178 |
(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) (m.mstep.step_inputs); |
|
179 |
|
|
180 |
fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ " |
|
181 |
(Utils.fprintf_list ~sep:" | " pp_var) output_vars |
|
182 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars |
|
183 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
|
184 |
|
|
185 |
let local_vars = |
|
186 |
(try |
|
187 |
full_memory_vars ~without_arrow:true machines m |
|
188 |
with Not_found -> Format.eprintf "machine %s@.@?" m.mname.node_id; assert false |
|
189 |
) |
|
190 |
in |
|
191 |
let init_local_vars = rename_next_list local_vars in |
|
192 |
let step_local_vars = rename_current_list local_vars in |
|
193 |
|
|
194 |
fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ " |
|
195 |
(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars |
|
196 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) init_local_vars |
|
197 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "") |
|
198 |
(Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) -> fprintf fmt "%a" pp_xml_expr ee)) memories_next; |
|
199 |
|
|
200 |
fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ " |
|
201 |
(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars |
|
202 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) step_local_vars |
|
203 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "") |
|
204 |
(Utils.fprintf_list ~sep:" | " (fun fmt (_,ee) -> fprintf fmt "(%a)" |
|
205 |
pp_xml_expr ee)) (memories_old); |
|
206 |
|
|
207 |
let arrow_vars = arrow_vars machines m in |
|
208 |
let arrow_vars_curr = rename_current_list arrow_vars and |
|
209 |
arrow_vars_mid = rename_mid_list arrow_vars and |
|
210 |
arrow_vars_next = rename_next_list arrow_vars |
|
211 |
in |
|
212 |
Utils.fprintf_list ~sep:"@ " |
|
213 |
(fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v) |
|
214 |
fmt (arrow_vars_curr@arrow_vars_mid@arrow_vars_next); |
|
215 |
fprintf fmt "@]@ </Node>"; |
|
216 |
)) (List.rev machines); |
|
160 |
let pp_var = pp_horn_var m in |
|
161 |
let memories_old = memories_old machines m in |
|
162 |
let memories_next = memories_next machines m in |
|
163 |
|
|
164 |
(* fprintf fmt "; Node %s@." m.mname.node_id; *) |
|
165 |
fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id; |
|
166 |
|
|
167 |
let input_vars = |
|
168 |
rename_machine_list m.mname.node_id m.mstep.step_inputs |
|
169 |
in |
|
170 |
let output_vars = |
|
171 |
rename_machine_list m.mname.node_id m.mstep.step_outputs |
|
172 |
in |
|
173 |
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; |
|
181 |
|
|
182 |
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; |
|
190 |
|
|
191 |
let local_vars = |
|
192 |
try full_memory_vars ~without_arrow:true machines m |
|
193 |
with Not_found -> |
|
194 |
Format.eprintf "machine %s@.@?" m.mname.node_id; |
|
195 |
assert false |
|
196 |
in |
|
197 |
let init_local_vars = rename_next_list local_vars in |
|
198 |
let step_local_vars = rename_current_list local_vars in |
|
199 |
|
|
200 |
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)) |
|
205 |
init_local_vars |
|
206 |
(fun fmt -> |
|
207 |
match memories_next with [] -> () | _ -> fprintf fmt "") |
|
208 |
(Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) -> |
|
209 |
fprintf fmt "%a" pp_xml_expr ee)) |
|
210 |
memories_next; |
|
211 |
|
|
212 |
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 |
|
218 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "") |
|
219 |
(Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) -> |
|
220 |
fprintf fmt "(%a)" pp_xml_expr ee)) |
|
221 |
memories_old; |
|
222 |
|
|
223 |
let arrow_vars = arrow_vars machines m in |
|
224 |
let arrow_vars_curr = rename_current_list arrow_vars |
|
225 |
and arrow_vars_mid = rename_mid_list arrow_vars |
|
226 |
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) |
|
229 |
fmt |
|
230 |
(arrow_vars_curr @ arrow_vars_mid @ arrow_vars_next); |
|
231 |
fprintf fmt "@]@ </Node>")) |
|
232 |
(List.rev machines); |
|
217 | 233 |
fprintf fmt "</Traces>@." |
218 |
|
|
219 | 234 |
|
220 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt |
|
221 |
"%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) |
|
222 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt |
|
223 |
"%a(%a)" *) |
|
235 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" |
|
236 |
pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) |
|
237 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *) |
|
224 | 238 |
(* pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *) |
225 | 239 |
|
226 |
|
|
227 | 240 |
(* Local Variables: *) |
228 | 241 |
(* compile-command:"make -C ../.." *) |
229 | 242 |
(* End: *) |
Also available in: Unified diff
reformatting