lustrec / src / inliner.ml @ 70df2f87
History  View  Annotate  Download (11.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  
15 
let check_node_name id = (fun t > 
16 
match t.top_decl_desc with 
17 
 Node nd > nd.node_id = id 
18 
 _ > false) 
19  
20  
21 
let rename_expr rename expr = expr_replace_var rename expr 
22 
let rename_eq rename eq = 
23 
{ eq with 
24 
eq_lhs = List.map rename eq.eq_lhs; 
25 
eq_rhs = rename_expr rename eq.eq_rhs 
26 
} 
27  
28 
(* 
29 
expr, locals', eqs = inline_call id args' reset locals nodes 
30  
31 
We select the called node equations and variables. 
32 
renamed_inputs = args 
33 
renamed_eqs 
34  
35 
the resulting expression is tuple_of_renamed_outputs 
36 

37 
TODO: convert the specification/annotation/assert and inject them 
38 
TODO: deal with reset 
39 
*) 
40 
let inline_call orig_expr args reset locals node = 
41 
let loc = orig_expr.expr_loc in 
42 
let uid = orig_expr.expr_tag in 
43 
let rename v = 
44 
if v = tag_true  v = tag_false then v else 
45 
(Format.fprintf Format.str_formatter "%s_%i_%s" 
46 
node.node_id uid v; 
47 
Format.flush_str_formatter ()) 
48 
in 
49 
let eqs' = List.map (rename_eq rename) node.node_eqs 
50 
in 
51 
let rename_var v = { v with var_id = rename v.var_id } in 
52 
let inputs' = List.map rename_var node.node_inputs in 
53 
let outputs' = List.map rename_var node.node_outputs in 
54 
let locals' = List.map rename_var node.node_locals in 
55  
56 
(* checking we are at the appropriate (early) step: node_checks and 
57 
node_gencalls should be empty (not yet assigned) *) 
58 
assert (node.node_checks = []); 
59 
assert (node.node_gencalls = []); 
60  
61 
(* Bug included: todo deal with reset *) 
62 
assert (reset = None); 
63  
64 
let assign_inputs = mkeq loc (List.map (fun v > v.var_id) inputs', args) in 
65 
let assign_inputs = Splitting.tuple_split_eq assign_inputs in 
66 
let expr = expr_of_expr_list 
67 
loc 
68 
(List.map (fun v > mkexpr loc (Expr_ident v.var_id)) outputs') 
69 
in 
70 
let asserts' = (* We rename variables in assert expressions *) 
71 
List.map 
72 
(fun a > 
73 
{a with assert_expr = 
74 
let expr = a.assert_expr in 
75 
rename_expr rename expr 
76 
}) 
77 
node.node_asserts 
78 
in 
79 
expr, 
80 
inputs'@outputs'@locals'@locals, 
81 
assign_inputs@eqs', 
82 
asserts' 
83  
84  
85  
86  
87 
(* 
88 
new_expr, new_locals, new_eqs = inline_expr expr locals nodes 
89 

90 
Each occurence of a node in nodes in the expr should be replaced by fresh 
91 
variables and the code of called node instance added to new_eqs 
92  
93 
*) 
94 
let rec inline_expr expr locals nodes = 
95 
let inline_tuple el = 
96 
List.fold_right (fun e (el_tail, locals, eqs, asserts) > 
97 
let e', locals', eqs', asserts' = inline_expr e locals nodes in 
98 
e'::el_tail, locals', eqs'@eqs, asserts@asserts' 
99 
) el ([], locals, [], []) 
100 
in 
101 
let inline_pair e1 e2 = 
102 
let el', l', eqs', asserts' = inline_tuple [e1;e2] in 
103 
match el' with 
104 
 [e1'; e2'] > e1', e2', l', eqs', asserts' 
105 
 _ > assert false 
106 
in 
107 
let inline_triple e1 e2 e3 = 
108 
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in 
109 
match el' with 
110 
 [e1'; e2'; e3'] > e1', e2', e3', l', eqs', asserts' 
111 
 _ > assert false 
112 
in 
113 

114 
match expr.expr_desc with 
115 
 Expr_appl (id, args, reset) > 
116 
let args', locals', eqs', asserts' = inline_expr args locals nodes in 
117 
if List.exists (check_node_name id) nodes then 
118 
(* The node should be inlined *) 
119 
(* let _ = Format.eprintf "Inlining call to %s@." id in *) 
120 
let node = try List.find (check_node_name id) nodes 
121 
with Not_found > (assert false) in 
122 
let node = node_of_top node in 
123 
let node = inline_node node nodes in 
124 
let expr, locals', eqs'', asserts'' = 
125 
inline_call expr args' reset locals' node in 
126 
expr, locals', eqs'@eqs'', asserts'@asserts'' 
127 
else 
128 
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) 
129 
{ expr with expr_desc = Expr_appl(id, args', reset)}, 
130 
locals', 
131 
eqs', 
132 
asserts' 
133  
134 
(* For other cases, we just keep the structure, but convert subexpressions *) 
135 
 Expr_const _ 
136 
 Expr_ident _ > expr, locals, [], [] 
137 
 Expr_tuple el > 
138 
let el', l', eqs', asserts' = inline_tuple el in 
139 
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts' 
140 
 Expr_ite (g, t, e) > 
141 
let g', t', e', l', eqs', asserts' = inline_triple g t e in 
142 
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts' 
143 
 Expr_arrow (e1, e2) > 
144 
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in 
145 
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts' 
146 
 Expr_fby (e1, e2) > 
147 
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in 
148 
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts' 
149 
 Expr_array el > 
150 
let el', l', eqs', asserts' = inline_tuple el in 
151 
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts' 
152 
 Expr_access (e, dim) > 
153 
let e', l', eqs', asserts' = inline_expr e locals nodes in 
154 
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts' 
155 
 Expr_power (e, dim) > 
156 
let e', l', eqs', asserts' = inline_expr e locals nodes in 
157 
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts' 
158 
 Expr_pre e > 
159 
let e', l', eqs', asserts' = inline_expr e locals nodes in 
160 
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts' 
161 
 Expr_when (e, id, label) > 
162 
let e', l', eqs', asserts' = inline_expr e locals nodes in 
163 
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts' 
164 
 Expr_merge (id, branches) > 
165 
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in 
166 
let branches' = List.map2 (fun (label, _) v > label, v) branches el in 
167 
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts' 
168 
and inline_node nd nodes = 
169 
let new_locals, eqs, asserts = 
170 
List.fold_left (fun (locals, eqs, asserts) eq > 
171 
let eq_rhs', locals', new_eqs', asserts' = 
172 
inline_expr eq.eq_rhs locals nodes 
173 
in 
174 
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts 
175 
) (nd.node_locals, [], nd.node_asserts) nd.node_eqs 
176 
in 
177 
{ nd with 
178 
node_locals = new_locals; 
179 
node_eqs = eqs; 
180 
node_asserts = asserts; 
181 
} 
182  
183 
let inline_all_calls node nodes = 
184 
let nd = match node.top_decl_desc with Node nd > nd  _ > assert false in 
185 
{ node with top_decl_desc = Node (inline_node nd nodes) } 
186 

187  
188  
189  
190  
191 
let witness filename main_name orig inlined type_env clock_env = 
192 
let loc = Location.dummy_loc in 
193 
let rename_local_node nodes prefix id = 
194 
if List.exists (check_node_name id) nodes then 
195 
prefix ^ id 
196 
else 
197 
id 
198 
in 
199 
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with 
200 
Node nd > nd  _ > assert false in 
201 

202 
let orig_rename = rename_local_node orig "orig_" in 
203 
let inlined_rename = rename_local_node inlined "inlined_" in 
204 
let identity = (fun x > x) in 
205 
let is_node top = match top.top_decl_desc with Node _ > true  _ > false in 
206 
let orig = rename_prog orig_rename identity identity orig in 
207 
let inlined = rename_prog inlined_rename identity identity inlined in 
208 
let nodes_origs, others = List.partition is_node orig in 
209 
let nodes_inlined, _ = List.partition is_node inlined in 
210  
211 
(* One ok_i boolean variable per output var *) 
212 
let nb_outputs = List.length main_orig_node.node_outputs in 
213 
let ok_i = List.map (fun id > 
214 
mkvar_decl 
215 
loc 
216 
("OK" ^ string_of_int id, 
217 
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, 
218 
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, 
219 
false) 
220 
) (Utils.enumerate nb_outputs) 
221 
in 
222  
223 
(* OK = ok_1 and ok_2 and ... ok_n1 *) 
224 
let ok_ident = "OK" in 
225 
let ok_output = mkvar_decl 
226 
loc 
227 
(ok_ident, 
228 
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, 
229 
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, 
230 
false) 
231 
in 
232 
let main_ok_expr = 
233 
let mkv x = mkexpr loc (Expr_ident x) in 
234 
match ok_i with 
235 
 [] > assert false 
236 
 [x] > mkv x.var_id 
237 
 hd::tl > 
238 
List.fold_left (fun accu elem > 
239 
mkpredef_call loc "&&" [mkv elem.var_id; accu] 
240 
) (mkv hd.var_id) tl 
241 
in 
242  
243 
(* Building main node *) 
244  
245 
let main_node = { 
246 
node_id = "check"; 
247 
node_type = Types.new_var (); 
248 
node_clock = Clocks.new_var true; 
249 
node_inputs = main_orig_node.node_inputs; 
250 
node_outputs = [ok_output]; 
251 
node_locals = ok_i; 
252 
node_gencalls = []; 
253 
node_checks = []; 
254 
node_asserts = []; 
255 
node_eqs = [ 
256 
{ eq_loc = loc; 
257 
eq_lhs = List.map (fun v > v.var_id) ok_i; 
258 
eq_rhs = 
259 
let inputs = expr_of_expr_list loc (List.map (fun v > mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in 
260 
let call_orig = 
261 
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in 
262 
let call_inlined = 
263 
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in 
264 
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
265 
mkexpr loc (Expr_appl ("=", args, None)) 
266 
}; 
267 
{ eq_loc = loc; 
268 
eq_lhs = [ok_ident]; 
269 
eq_rhs = main_ok_expr; 
270 
} 
271 
]; 
272 
node_dec_stateless = false; 
273 
node_stateless = None; 
274 
node_spec = Some 
275 
{requires = []; 
276 
ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; 
277 
behaviors = []; 
278 
spec_loc = loc 
279 
}; 
280 
node_annot = []; 
281 
} 
282 
in 
283 
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in 
284 
let new_prog = others@nodes_origs@nodes_inlined@main in 
285 
let _ = Typing.type_prog type_env new_prog in 
286 
let _ = Clock_calculus.clock_prog clock_env new_prog in 
287  
288 

289 
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in 
290 
let witness_out = open_out witness_file in 
291 
let witness_fmt = Format.formatter_of_out_channel witness_out in 
292 
Format.fprintf witness_fmt 
293 
"(* Generated lustre file to check validity of inlining process *)@."; 
294 
Printers.pp_prog witness_fmt new_prog; 
295 
Format.fprintf witness_fmt "@."; 
296 
() (* xx *) 
297  
298 
let global_inline basename prog type_env clock_env = 
299 
(* We select the main node desc *) 
300 
let main_node, other_nodes, other_tops = 
301 
List.fold_left 
302 
(fun (main_opt, nodes, others) top > 
303 
match top.top_decl_desc with 
304 
 Node nd when nd.node_id = !Options.main_node > 
305 
Some top, nodes, others 
306 
 Node _ > main_opt, top::nodes, others 
307 
 _ > main_opt, nodes, top::others) 
308 
(None, [], []) prog 
309 
in 
310 
(* Recursively each call of a node in the top node is replaced *) 
311 
let main_node = Utils.desome main_node in 
312 
let main_node' = inline_all_calls main_node other_nodes in 
313 
let res = main_node'::other_tops in 
314 
if !Options.witnesses then ( 
315 
witness 
316 
basename 
317 
(match main_node.top_decl_desc with Node nd > nd.node_id  _ > assert false) 
318 
prog res type_env clock_env 
319 
); 
320 
res 
321  
322 
(* Local Variables: *) 
323 
(* compilecommand:"make C .." *) 
324 
(* End: *) 