lustrec / src / inliner.ml @ fc886259
History  View  Annotate  Download (14.1 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(********************************************************************) 
11  
12 
open LustreSpec 
13 
open Corelang 
14 
open Utils 
15  
16 
(* Local annotations are declared with the following key /inlining/: true *) 
17 
let keyword = ["inlining"] 
18  
19 
let is_inline_expr expr = 
20 
match expr.expr_annot with 
21 
 Some ann > 
22 
List.exists (fun (key, value) > key = keyword) ann.annots 
23 
 None > false 
24  
25 
let check_node_name id = (fun t > 
26 
match t.top_decl_desc with 
27 
 Node nd > nd.node_id = id 
28 
 _ > false) 
29  
30 
let get_static_inputs node args = 
31 
List.fold_right2 (fun vdecl arg static > 
32 
if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static) 
33 
node.node_inputs 
34 
(Corelang.expr_list_of_expr args) 
35 
[] 
36  
37 
let get_carrier_inputs node args = 
38 
List.fold_right2 (fun vdecl arg carrier > 
39 
if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier) 
40 
node.node_inputs 
41 
(Corelang.expr_list_of_expr args) 
42 
[] 
43  
44 
let is_node_var node v = 
45 
try 
46 
ignore (Corelang.get_node_var v node); true 
47 
with Not_found > false 
48  
49 
let rename_expr rename expr = expr_replace_var rename expr 
50  
51 
let rename_eq rename eq = 
52 
{ eq with 
53 
eq_lhs = List.map rename eq.eq_lhs; 
54 
eq_rhs = rename_expr rename eq.eq_rhs 
55 
} 
56  
57 
(* 
58 
expr, locals', eqs = inline_call id args' reset locals node nodes 
59  
60 
We select the called node equations and variables. 
61 
renamed_inputs = args 
62 
renamed_eqs 
63  
64 
the resulting expression is tuple_of_renamed_outputs 
65 

66 
TODO: convert the specification/annotation/assert and inject them 
67 
TODO: deal with reset 
68 
*) 
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 
72 
let rename v = 
73 
if v = tag_true  v = tag_false  not (is_node_var node v) then v else 
74 
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) 
75 
in 
76 
let eqs' = List.map (rename_eq rename) (get_node_eqs node) 
77 
in 
78 
let static_inputs = get_static_inputs node args in 
79 
let carrier_inputs = get_carrier_inputs node args in 
80 
let rename_static v = 
81 
try 
82 
List.assoc v static_inputs 
83 
with Not_found > Dimension.mkdim_ident loc v 
84 
(*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*) 
85 
in 
86 
let rename_carrier v = 
87 
try 
88 
List.assoc v carrier_inputs 
89 
with Not_found > v in 
90 
let rename_var v = 
91 
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) 
92 
{ v with 
93 
var_id = rename v.var_id; 
94 
var_type = Types.rename_static rename_static v.var_type; 
95 
var_clock = Clocks.rename_static rename_carrier v.var_clock; 
96 
} in 
97 
let inputs' = List.map rename_var node.node_inputs in 
98 
let outputs' = List.map rename_var node.node_outputs in 
99 
let locals' = List.map rename_var node.node_locals in 
100 
(* checking we are at the appropriate (early) step: node_checks and 
101 
node_gencalls should be empty (not yet assigned) *) 
102 
assert (node.node_checks = []); 
103 
assert (node.node_gencalls = []); 
104  
105 
(* Bug included: todo deal with reset *) 
106 
assert (reset = None); 
107  
108 
let assign_inputs = mkeq loc (List.map (fun v > v.var_id) inputs', args) in 
109 
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') 
110 
in 
111 
let asserts' = (* We rename variables in assert expressions *) 
112 
List.map 
113 
(fun a > 
114 
{a with assert_expr = 
115 
let expr = a.assert_expr in 
116 
rename_expr rename expr 
117 
}) 
118 
node.node_asserts 
119 
in 
120 
expr, 
121 
inputs'@outputs'@locals'@locals, 
122 
assign_inputs::eqs', 
123 
asserts' 
124  
125  
126  
127 
let inline_table = Hashtbl.create 23 
128  
129 
(* 
130 
new_expr, new_locals, new_eqs = inline_expr expr locals node nodes 
131 

132 
Each occurence of a node in nodes in the expr should be replaced by fresh 
133 
variables and the code of called node instance added to new_eqs 
134  
135 
*) 
136 
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes = 
137 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
138 
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in 
139 
let inline_tuple el = 
140 
List.fold_right (fun e (el_tail, locals, eqs, asserts) > 
141 
let e', locals', eqs', asserts' = inline_expr e locals node nodes in 
142 
e'::el_tail, locals', eqs'@eqs, asserts@asserts' 
143 
) el ([], locals, [], []) 
144 
in 
145 
let inline_pair e1 e2 = 
146 
let el', l', eqs', asserts' = inline_tuple [e1;e2] in 
147 
match el' with 
148 
 [e1'; e2'] > e1', e2', l', eqs', asserts' 
149 
 _ > assert false 
150 
in 
151 
let inline_triple e1 e2 e3 = 
152 
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in 
153 
match el' with 
154 
 [e1'; e2'; e3'] > e1', e2', e3', l', eqs', asserts' 
155 
 _ > assert false 
156 
in 
157 

158 
match expr.expr_desc with 
159 
 Expr_appl (id, args, reset) > 
160 
let args', locals', eqs', asserts' = inline_expr args locals node nodes in 
161 
if List.exists (check_node_name id) nodes && (* the current node call is provided 
162 
as arguments nodes *) 
163 
(not selection_on_annotation  is_inline_expr expr) (* and if selection on annotation is activated, 
164 
it is explicitely inlined here *) 
165 
then 
166 
(* The node should be inlined *) 
167 
(* let _ = Format.eprintf "Inlining call to %s@." id in *) 
168 
let called = try List.find (check_node_name id) nodes 
169 
with Not_found > (assert false) in 
170 
let called = node_of_top called in 
171 
let called' = inline_node called nodes in 
172 
let expr, locals', eqs'', asserts'' = 
173 
inline_call called' expr args' reset locals' node in 
174 
expr, locals', eqs'@eqs'', asserts'@asserts'' 
175 
else 
176 
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) 
177 
{ expr with expr_desc = Expr_appl(id, args', reset)}, 
178 
locals', 
179 
eqs', 
180 
asserts' 
181  
182 
(* For other cases, we just keep the structure, but convert subexpressions *) 
183 
 Expr_const _ 
184 
 Expr_ident _ > expr, locals, [], [] 
185 
 Expr_tuple el > 
186 
let el', l', eqs', asserts' = inline_tuple el in 
187 
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts' 
188 
 Expr_ite (g, t, e) > 
189 
let g', t', e', l', eqs', asserts' = inline_triple g t e in 
190 
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts' 
191 
 Expr_arrow (e1, e2) > 
192 
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in 
193 
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts' 
194 
 Expr_fby (e1, e2) > 
195 
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in 
196 
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts' 
197 
 Expr_array el > 
198 
let el', l', eqs', asserts' = inline_tuple el in 
199 
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts' 
200 
 Expr_access (e, dim) > 
201 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 
202 
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts' 
203 
 Expr_power (e, dim) > 
204 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 
205 
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts' 
206 
 Expr_pre e > 
207 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 
208 
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts' 
209 
 Expr_when (e, id, label) > 
210 
let e', l', eqs', asserts' = inline_expr e locals node nodes in 
211 
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts' 
212 
 Expr_merge (id, branches) > 
213 
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in 
214 
let branches' = List.map2 (fun (label, _) v > label, v) branches el in 
215 
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts' 
216  
217 
and inline_node ?(selection_on_annotation=false) node nodes = 
218 
try Hashtbl.find inline_table node.node_id 
219 
with Not_found > 
220 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
221 
let new_locals, eqs, asserts = 
222 
List.fold_left (fun (locals, eqs, asserts) eq > 
223 
let eq_rhs', locals', new_eqs', asserts' = 
224 
inline_expr eq.eq_rhs locals node nodes 
225 
in 
226 
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts 
227 
) (node.node_locals, [], node.node_asserts) (get_node_eqs node) 
228 
in 
229 
let inlined = 
230 
{ node with 
231 
node_locals = new_locals; 
232 
node_stmts = List.map (fun eq > Eq eq) eqs; 
233 
node_asserts = asserts; 
234 
} 
235 
in 
236 
begin 
237 
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) 
238 
Hashtbl.add inline_table node.node_id inlined; 
239 
inlined 
240 
end 
241  
242 
let inline_all_calls node nodes = 
243 
let nd = match node.top_decl_desc with Node nd > nd  _ > assert false in 
244 
{ node with top_decl_desc = Node (inline_node nd nodes) } 
245 

246  
247  
248  
249  
250 
let witness filename main_name orig inlined type_env clock_env = 
251 
let loc = Location.dummy_loc in 
252 
let rename_local_node nodes prefix id = 
253 
if List.exists (check_node_name id) nodes then 
254 
prefix ^ id 
255 
else 
256 
id 
257 
in 
258 
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with 
259 
Node nd > nd  _ > assert false in 
260 

261 
let orig_rename = rename_local_node orig "orig_" in 
262 
let inlined_rename = rename_local_node inlined "inlined_" in 
263 
let identity = (fun x > x) in 
264 
let is_node top = match top.top_decl_desc with Node _ > true  _ > false in 
265 
let orig = rename_prog orig_rename identity identity orig in 
266 
let inlined = rename_prog inlined_rename identity identity inlined in 
267 
let nodes_origs, others = List.partition is_node orig in 
268 
let nodes_inlined, _ = List.partition is_node inlined in 
269  
270 
(* One ok_i boolean variable per output var *) 
271 
let nb_outputs = List.length main_orig_node.node_outputs in 
272 
let ok_i = List.map (fun id > 
273 
mkvar_decl 
274 
loc 
275 
("OK" ^ string_of_int id, 
276 
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, 
277 
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, 
278 
false) 
279 
) (Utils.enumerate nb_outputs) 
280 
in 
281  
282 
(* OK = ok_1 and ok_2 and ... ok_n1 *) 
283 
let ok_ident = "OK" in 
284 
let ok_output = mkvar_decl 
285 
loc 
286 
(ok_ident, 
287 
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, 
288 
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, 
289 
false) 
290 
in 
291 
let main_ok_expr = 
292 
let mkv x = mkexpr loc (Expr_ident x) in 
293 
match ok_i with 
294 
 [] > assert false 
295 
 [x] > mkv x.var_id 
296 
 hd::tl > 
297 
List.fold_left (fun accu elem > 
298 
mkpredef_call loc "&&" [mkv elem.var_id; accu] 
299 
) (mkv hd.var_id) tl 
300 
in 
301  
302 
(* Building main node *) 
303  
304 
let ok_i_eq = 
305 
{ eq_loc = loc; 
306 
eq_lhs = List.map (fun v > v.var_id) ok_i; 
307 
eq_rhs = 
308 
let inputs = expr_of_expr_list loc (List.map (fun v > mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in 
309 
let call_orig = 
310 
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in 
311 
let call_inlined = 
312 
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in 
313 
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
314 
mkexpr loc (Expr_appl ("=", args, None)) 
315 
} in 
316 
let ok_eq = 
317 
{ eq_loc = loc; 
318 
eq_lhs = [ok_ident]; 
319 
eq_rhs = main_ok_expr; 
320 
} in 
321 
let main_node = { 
322 
node_id = "check"; 
323 
node_type = Types.new_var (); 
324 
node_clock = Clocks.new_var true; 
325 
node_inputs = main_orig_node.node_inputs; 
326 
node_outputs = [ok_output]; 
327 
node_locals = ok_i; 
328 
node_gencalls = []; 
329 
node_checks = []; 
330 
node_asserts = []; 
331 
node_stmts = [Eq ok_i_eq; Eq ok_eq]; 
332 
node_dec_stateless = false; 
333 
node_stateless = None; 
334 
node_spec = Some 
335 
{requires = []; 
336 
ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; 
337 
behaviors = []; 
338 
spec_loc = loc 
339 
}; 
340 
node_annot = []; 
341 
} 
342 
in 
343 
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in 
344 
let new_prog = others@nodes_origs@nodes_inlined@main in 
345  
346 
let _ = Typing.type_prog type_env new_prog in 
347 
let _ = Clock_calculus.clock_prog clock_env new_prog in 
348  
349 

350 
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in 
351 
let witness_out = open_out witness_file in 
352 
let witness_fmt = Format.formatter_of_out_channel witness_out in 
353 
Format.fprintf witness_fmt 
354 
"(* Generated lustre file to check validity of inlining process *)@."; 
355 
Printers.pp_prog witness_fmt new_prog; 
356 
Format.fprintf witness_fmt "@."; 
357 
() (* xx *) 
358  
359 
let global_inline basename prog type_env clock_env = 
360 
(* We select the main node desc *) 
361 
let main_node, other_nodes, other_tops = 
362 
List.fold_left 
363 
(fun (main_opt, nodes, others) top > 
364 
match top.top_decl_desc with 
365 
 Node nd when nd.node_id = !Options.main_node > 
366 
Some top, nodes, others 
367 
 Node _ > main_opt, top::nodes, others 
368 
 _ > main_opt, nodes, top::others) 
369 
(None, [], []) prog 
370 
in 
371 
(* Recursively each call of a node in the top node is replaced *) 
372 
let main_node = Utils.desome main_node in 
373 
let main_node' = inline_all_calls main_node other_nodes in 
374 
let res = main_node'::other_tops in 
375 
if !Options.witnesses then ( 
376 
witness 
377 
basename 
378 
(match main_node.top_decl_desc with Node nd > nd.node_id  _ > assert false) 
379 
prog res type_env clock_env 
380 
); 
381 
res 
382  
383 
let local_inline basename prog type_env clock_env = 
384 
let local_anns = Annotations.get_expr_annotations keyword in 
385 
if local_anns != [] then ( 
386 
let nodes_with_anns = List.fold_left (fun accu (k, _) > ISet.add k accu) ISet.empty local_anns in 
387 
ISet.iter (fun node_id > Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns; 
388 
List.fold_right (fun top accu > 
389 
( match top.top_decl_desc with 
390 
 Node nd when ISet.mem nd.node_id nodes_with_anns > 
391 
{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) } 
392 
 _ > top 
393 
)::accu) prog [] 
394 

395 
) 
396 
else 
397 
prog 
398  
399  
400 
(* Local Variables: *) 
401 
(* compilecommand:"make C .." *) 
402 
(* End: *) 