Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
src/inliner.ml | ||
---|---|---|
39 | 39 |
eq_lhs = List.map rename eq.eq_lhs; |
40 | 40 |
eq_rhs = rename_expr rename eq.eq_rhs |
41 | 41 |
} |
42 |
|
|
43 |
let rec add_expr_reset_cond cond expr = |
|
44 |
let aux = add_expr_reset_cond cond in |
|
45 |
let new_desc = |
|
46 |
match expr.expr_desc with |
|
47 |
| Expr_const _ |
|
48 |
| Expr_ident _ -> expr.expr_desc |
|
49 |
| Expr_tuple el -> Expr_tuple (List.map aux el) |
|
50 |
| Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e) |
|
51 |
|
|
52 |
| Expr_arrow (e1, e2) -> |
|
53 |
(* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *) |
|
54 |
let e1 = aux e1 and e2 = aux e2 in |
|
55 |
(* inlining is performed before typing. we can leave the fields free *) |
|
56 |
let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in |
|
57 |
Expr_arrow (e1, new_e2) |
|
58 |
|
|
59 |
| Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *) |
|
60 |
|
|
61 |
| Expr_array el -> Expr_array (List.map aux el) |
|
62 |
| Expr_access (e, dim) -> Expr_access (aux e, dim) |
|
63 |
| Expr_power (e, dim) -> Expr_power (aux e, dim) |
|
64 |
| Expr_pre e -> Expr_pre (aux e) |
|
65 |
| Expr_when (e, id, l) -> Expr_when (aux e, id, l) |
|
66 |
| Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases) |
|
67 |
|
|
68 |
| Expr_appl (id, args, reset_opt) -> |
|
69 |
(* we "add" cond to the reset field. *) |
|
70 |
let new_reset = match reset_opt with |
|
71 |
None -> cond |
|
72 |
| Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond'] |
|
73 |
in |
|
74 |
Expr_appl (id, args, Some new_reset) |
|
75 |
|
|
76 |
|
|
77 |
in |
|
78 |
{ expr with expr_desc = new_desc } |
|
79 |
|
|
80 |
let add_eq_reset_cond cond eq = |
|
81 |
{ eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs } |
|
42 | 82 |
(* |
43 | 83 |
let get_static_inputs input_arg_list = |
44 | 84 |
List.fold_right (fun (vdecl, arg) res -> |
... | ... | |
54 | 94 |
else res) |
55 | 95 |
input_arg_list [] |
56 | 96 |
*) |
97 |
|
|
98 |
|
|
57 | 99 |
(* |
58 | 100 |
expr, locals', eqs = inline_call id args' reset locals node nodes |
59 | 101 |
|
... | ... | |
64 | 106 |
the resulting expression is tuple_of_renamed_outputs |
65 | 107 |
|
66 | 108 |
TODO: convert the specification/annotation/assert and inject them |
67 |
TODO: deal with reset |
|
68 | 109 |
*) |
69 |
let inline_call node orig_expr args reset locals caller = |
|
70 |
let loc = orig_expr.expr_loc in |
|
71 |
let uid = orig_expr.expr_tag in |
|
110 |
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr, |
|
111 |
locals, eqs, asserts) |
|
112 |
*) |
|
113 |
let inline_call node loc uid args reset locals caller = |
|
72 | 114 |
let rename v = |
73 | 115 |
if v = tag_true || v = tag_false || not (is_node_var node v) then v else |
74 | 116 |
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) |
... | ... | |
96 | 138 |
v.var_dec_const, |
97 | 139 |
Utils.option_map (rename_expr rename) v.var_dec_value) in |
98 | 140 |
begin |
99 |
(* |
|
100 |
(try
|
|
101 |
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
|
|
102 |
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
|
|
103 |
with Not_found -> ());
|
|
104 |
(try
|
|
105 |
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) |
|
106 |
with Not_found -> ());
|
|
107 |
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*) |
|
108 |
*) |
|
141 |
(*
|
|
142 |
(try
|
|
143 |
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs); |
|
144 |
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ())) |
|
145 |
with Not_found -> ());
|
|
146 |
(try
|
|
147 |
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
|
|
148 |
with Not_found -> ());
|
|
149 |
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
|
|
150 |
*)
|
|
109 | 151 |
vdecl |
110 | 152 |
end |
111 |
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
|
|
153 |
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) |
|
112 | 154 |
in |
113 | 155 |
let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in |
114 | 156 |
let outputs' = List.map rename_var node.node_outputs in |
115 | 157 |
let locals' = |
116 |
(List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
|
|
158 |
(List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) |
|
117 | 159 |
@ (List.map rename_var node.node_locals) |
118 |
in |
|
160 |
in
|
|
119 | 161 |
(* checking we are at the appropriate (early) step: node_checks and |
120 | 162 |
node_gencalls should be empty (not yet assigned) *) |
121 | 163 |
assert (node.node_checks = []); |
122 | 164 |
assert (node.node_gencalls = []); |
123 | 165 |
|
124 |
(* Bug included: todo deal with reset *) |
|
125 |
assert (reset = None); |
|
126 |
|
|
127 |
let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in |
|
166 |
(* Expressing reset locally in equations *) |
|
167 |
let eqs_r' = |
|
168 |
match reset with |
|
169 |
None -> eqs' |
|
170 |
| Some cond -> List.map (add_eq_reset_cond cond) eqs' |
|
171 |
in |
|
172 |
let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', |
|
173 |
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in |
|
128 | 174 |
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') |
129 | 175 |
in |
130 | 176 |
let asserts' = (* We rename variables in assert expressions *) |
... | ... | |
133 | 179 |
{a with assert_expr = |
134 | 180 |
let expr = a.assert_expr in |
135 | 181 |
rename_expr rename expr |
136 |
})
|
|
182 |
})
|
|
137 | 183 |
node.node_asserts |
138 | 184 |
in |
185 |
let annots' = |
|
186 |
Plugins.inline_annots rename node.node_annot |
|
187 |
in |
|
139 | 188 |
expr, |
140 | 189 |
inputs'@outputs'@locals'@locals, |
141 |
assign_inputs::eqs', |
|
142 |
asserts' |
|
190 |
assign_inputs::eqs_r', |
|
191 |
asserts', |
|
192 |
annots' |
|
143 | 193 |
|
144 | 194 |
|
145 | 195 |
|
... | ... | |
156 | 206 |
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
157 | 207 |
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in |
158 | 208 |
let inline_tuple el = |
159 |
List.fold_right (fun e (el_tail, locals, eqs, asserts) -> |
|
160 |
let e', locals', eqs', asserts' = inline_expr e locals node nodes in |
|
161 |
e'::el_tail, locals', eqs'@eqs, asserts@asserts' |
|
162 |
) el ([], locals, [], []) |
|
209 |
List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) ->
|
|
210 |
let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
211 |
e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'
|
|
212 |
) el ([], locals, [], [], [])
|
|
163 | 213 |
in |
164 | 214 |
let inline_pair e1 e2 = |
165 |
let el', l', eqs', asserts' = inline_tuple [e1;e2] in |
|
215 |
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
|
|
166 | 216 |
match el' with |
167 |
| [e1'; e2'] -> e1', e2', l', eqs', asserts' |
|
217 |
| [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
|
|
168 | 218 |
| _ -> assert false |
169 | 219 |
in |
170 | 220 |
let inline_triple e1 e2 e3 = |
171 |
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in |
|
221 |
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
|
|
172 | 222 |
match el' with |
173 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts' |
|
223 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots'
|
|
174 | 224 |
| _ -> assert false |
175 | 225 |
in |
176 | 226 |
|
177 | 227 |
match expr.expr_desc with |
178 | 228 |
| Expr_appl (id, args, reset) -> |
179 |
let args', locals', eqs', asserts' = inline_expr args locals node nodes in |
|
229 |
let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in
|
|
180 | 230 |
if List.exists (check_node_name id) nodes && (* the current node call is provided |
181 | 231 |
as arguments nodes *) |
182 | 232 |
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, |
... | ... | |
188 | 238 |
with Not_found -> (assert false) in |
189 | 239 |
let called = node_of_top called in |
190 | 240 |
let called' = inline_node called nodes in |
191 |
let expr, locals', eqs'', asserts'' = |
|
192 |
inline_call called' expr args' reset locals' node in |
|
193 |
expr, locals', eqs'@eqs'', asserts'@asserts'' |
|
241 |
let expr, locals', eqs'', asserts'', annots'' =
|
|
242 |
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
|
|
243 |
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
|
|
194 | 244 |
else |
195 | 245 |
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
196 | 246 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, |
197 | 247 |
locals', |
198 | 248 |
eqs', |
199 |
asserts' |
|
249 |
asserts', |
|
250 |
annots' |
|
200 | 251 |
|
201 | 252 |
(* For other cases, we just keep the structure, but convert sub-expressions *) |
202 | 253 |
| Expr_const _ |
203 |
| Expr_ident _ -> expr, locals, [], [] |
|
254 |
| Expr_ident _ -> expr, locals, [], [], []
|
|
204 | 255 |
| Expr_tuple el -> |
205 |
let el', l', eqs', asserts' = inline_tuple el in |
|
206 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts' |
|
256 |
let el', l', eqs', asserts', annots' = inline_tuple el in
|
|
257 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
|
|
207 | 258 |
| Expr_ite (g, t, e) -> |
208 |
let g', t', e', l', eqs', asserts' = inline_triple g t e in |
|
209 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts' |
|
259 |
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
|
|
260 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
|
|
210 | 261 |
| Expr_arrow (e1, e2) -> |
211 |
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in |
|
212 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts' |
|
262 |
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
|
|
263 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
|
|
213 | 264 |
| Expr_fby (e1, e2) -> |
214 |
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in |
|
215 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts' |
|
265 |
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
|
|
266 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
|
|
216 | 267 |
| Expr_array el -> |
217 |
let el', l', eqs', asserts' = inline_tuple el in |
|
218 |
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts' |
|
268 |
let el', l', eqs', asserts', annots' = inline_tuple el in
|
|
269 |
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
|
|
219 | 270 |
| Expr_access (e, dim) -> |
220 |
let e', l', eqs', asserts' = inline_expr e locals node nodes in |
|
221 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts' |
|
271 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
272 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
|
|
222 | 273 |
| Expr_power (e, dim) -> |
223 |
let e', l', eqs', asserts' = inline_expr e locals node nodes in |
|
224 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts' |
|
274 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
275 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
|
|
225 | 276 |
| Expr_pre e -> |
226 |
let e', l', eqs', asserts' = inline_expr e locals node nodes in |
|
227 |
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts' |
|
277 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
278 |
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
|
|
228 | 279 |
| Expr_when (e, id, label) -> |
229 |
let e', l', eqs', asserts' = inline_expr e locals node nodes in |
|
230 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts' |
|
280 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
281 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
|
|
231 | 282 |
| Expr_merge (id, branches) -> |
232 |
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in |
|
283 |
let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
|
|
233 | 284 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
234 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts' |
|
285 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
|
|
235 | 286 |
|
236 | 287 |
and inline_node ?(selection_on_annotation=false) node nodes = |
237 | 288 |
try copy_node (Hashtbl.find inline_table node.node_id) |
238 | 289 |
with Not_found -> |
239 | 290 |
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
240 |
let new_locals, eqs, asserts = |
|
241 |
List.fold_left (fun (locals, eqs, asserts) eq -> |
|
242 |
let eq_rhs', locals', new_eqs', asserts' = |
|
291 |
let new_locals, eqs, asserts, annots =
|
|
292 |
List.fold_left (fun (locals, eqs, asserts, annots) eq ->
|
|
293 |
let eq_rhs', locals', new_eqs', asserts', annots' =
|
|
243 | 294 |
inline_expr eq.eq_rhs locals node nodes |
244 | 295 |
in |
245 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts |
|
246 |
) (node.node_locals, [], node.node_asserts) (get_node_eqs node) |
|
296 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots
|
|
297 |
) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node)
|
|
247 | 298 |
in |
248 | 299 |
let inlined = |
249 | 300 |
{ node with |
250 | 301 |
node_locals = new_locals; |
251 | 302 |
node_stmts = List.map (fun eq -> Eq eq) eqs; |
252 | 303 |
node_asserts = asserts; |
304 |
node_annot = annots; |
|
253 | 305 |
} |
254 | 306 |
in |
255 | 307 |
begin |
... | ... | |
363 | 415 |
in |
364 | 416 |
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in |
365 | 417 |
let new_prog = others@nodes_origs@nodes_inlined@main in |
418 |
(* |
|
419 |
let _ = Typing.type_prog type_env new_prog in |
|
420 |
let _ = Clock_calculus.clock_prog clock_env new_prog in |
|
421 |
*) |
|
422 |
|
|
366 | 423 |
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |
367 | 424 |
let witness_out = open_out witness_file in |
368 | 425 |
let witness_fmt = Format.formatter_of_out_channel witness_out in |
... | ... | |
387 | 444 |
| _ -> main_opt, nodes, top::others) |
388 | 445 |
prog (None, [], []) |
389 | 446 |
in |
390 |
|
|
391 | 447 |
(* Recursively each call of a node in the top node is replaced *) |
392 | 448 |
let main_node = Utils.desome main_node in |
393 | 449 |
let main_node' = inline_all_calls main_node other_nodes in |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04