lustrec / src / inliner.ml @ 01c7d5e1
History | View | Annotate | Download (9.54 KB)
1 |
open LustreSpec |
---|---|
2 |
open Corelang |
3 |
|
4 |
let check_node_name id = (fun t -> |
5 |
match t.top_decl_desc with |
6 |
| Node nd -> nd.node_id = id |
7 |
| _ -> false) |
8 |
|
9 |
|
10 |
(* |
11 |
expr, locals', eqs = inline_call id args' reset locals nodes |
12 |
|
13 |
We select the called node equations and variables. |
14 |
renamed_inputs = args |
15 |
renamed_eqs |
16 |
|
17 |
the resulting expression is tuple_of_renamed_outputs |
18 |
|
19 |
TODO: convert the specification/annotation/assert and inject them |
20 |
TODO: deal with reset |
21 |
*) |
22 |
let inline_call orig_expr args reset locals node = |
23 |
let loc = orig_expr.expr_loc in |
24 |
let uid = orig_expr.expr_tag in |
25 |
let rename v = |
26 |
Format.fprintf Format.str_formatter "%s_%i_%s" |
27 |
node.node_id uid v; |
28 |
Format.flush_str_formatter () |
29 |
in |
30 |
let eqs' = List.map |
31 |
(fun eq -> { eq with |
32 |
eq_lhs = List.map rename eq.eq_lhs; |
33 |
eq_rhs = expr_replace_var rename eq.eq_rhs |
34 |
} ) node.node_eqs |
35 |
in |
36 |
let rename_var v = { v with var_id = rename v.var_id } in |
37 |
let inputs' = List.map rename_var node.node_inputs in |
38 |
let outputs' = List.map rename_var node.node_outputs in |
39 |
let locals' = List.map rename_var node.node_locals in |
40 |
|
41 |
(* checking we are at the appropriate (early) step: node_checks and |
42 |
node_gencalls should be empty (not yet assigned) *) |
43 |
assert (node.node_checks = []); |
44 |
assert (node.node_gencalls = []); |
45 |
|
46 |
(* Bug included: todo deal with reset *) |
47 |
assert (reset = None); |
48 |
|
49 |
let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in |
50 |
let expr = expr_of_expr_list |
51 |
loc |
52 |
(List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs') |
53 |
in |
54 |
expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs' |
55 |
|
56 |
|
57 |
|
58 |
|
59 |
(* |
60 |
new_expr, new_locals, new_eqs = inline_expr expr locals nodes |
61 |
|
62 |
Each occurence of a node in nodes in the expr should be replaced by fresh |
63 |
variables and the code of called node instance added to new_eqs |
64 |
|
65 |
*) |
66 |
let rec inline_expr expr locals nodes = |
67 |
let inline_tuple el = |
68 |
List.fold_right (fun e (el_tail, locals, eqs) -> |
69 |
let e', locals', eqs' = inline_expr e locals nodes in |
70 |
e'::el_tail, locals', eqs'@eqs |
71 |
) el ([], locals, []) |
72 |
in |
73 |
let inline_pair e1 e2 = |
74 |
let el', l', eqs' = inline_tuple [e1;e2] in |
75 |
match el' with |
76 |
| [e1'; e2'] -> e1', e2', l', eqs' |
77 |
| _ -> assert false |
78 |
in |
79 |
let inline_triple e1 e2 e3 = |
80 |
let el', l', eqs' = inline_tuple [e1;e2;e3] in |
81 |
match el' with |
82 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs' |
83 |
| _ -> assert false |
84 |
in |
85 |
|
86 |
match expr.expr_desc with |
87 |
| Expr_appl (id, args, reset) -> |
88 |
let args', locals', eqs' = inline_expr args locals nodes in |
89 |
if List.exists (check_node_name id) nodes then |
90 |
(* The node should be inlined *) |
91 |
(* let _ = Format.eprintf "Inlining call to %s@." id in |
92 |
*) let node = try List.find (check_node_name id) nodes |
93 |
with Not_found -> (assert false) in |
94 |
let node = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
95 |
let node = inline_node node nodes in |
96 |
let expr, locals', eqs'' = |
97 |
inline_call expr args' reset locals' node in |
98 |
expr, locals', eqs'@eqs'' |
99 |
else |
100 |
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
101 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs' |
102 |
|
103 |
(* For other cases, we just keep the structure, but convert sub-expressions *) |
104 |
| Expr_const _ |
105 |
| Expr_ident _ -> expr, locals, [] |
106 |
| Expr_tuple el -> |
107 |
let el', l', eqs' = inline_tuple el in |
108 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs' |
109 |
| Expr_ite (g, t, e) -> |
110 |
let g', t', e', l', eqs' = inline_triple g t e in |
111 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs' |
112 |
| Expr_arrow (e1, e2) -> |
113 |
let e1', e2', l', eqs' = inline_pair e1 e2 in |
114 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs' |
115 |
| Expr_fby (e1, e2) -> |
116 |
let e1', e2', l', eqs' = inline_pair e1 e2 in |
117 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs' |
118 |
| Expr_array el -> |
119 |
let el', l', eqs' = inline_tuple el in |
120 |
{ expr with expr_desc = Expr_array el' }, l', eqs' |
121 |
| Expr_access (e, dim) -> |
122 |
let e', l', eqs' = inline_expr e locals nodes in |
123 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs' |
124 |
| Expr_power (e, dim) -> |
125 |
let e', l', eqs' = inline_expr e locals nodes in |
126 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs' |
127 |
| Expr_pre e -> |
128 |
let e', l', eqs' = inline_expr e locals nodes in |
129 |
{ expr with expr_desc = Expr_pre e' }, l', eqs' |
130 |
| Expr_when (e, id, label) -> |
131 |
let e', l', eqs' = inline_expr e locals nodes in |
132 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs' |
133 |
| Expr_merge (id, branches) -> |
134 |
let el, l', eqs' = inline_tuple (List.map snd branches) in |
135 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
136 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs' |
137 |
and inline_node nd nodes = |
138 |
let new_locals, eqs = |
139 |
List.fold_left (fun (locals, eqs) eq -> |
140 |
let eq_rhs', locals', new_eqs' = |
141 |
inline_expr eq.eq_rhs locals nodes |
142 |
in |
143 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs |
144 |
) (nd.node_locals, []) nd.node_eqs |
145 |
in |
146 |
{ nd with |
147 |
node_locals = new_locals; |
148 |
node_eqs = eqs |
149 |
} |
150 |
|
151 |
let inline_all_calls node nodes = |
152 |
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
153 |
{ node with top_decl_desc = Node (inline_node nd nodes) } |
154 |
|
155 |
|
156 |
|
157 |
|
158 |
|
159 |
let witness filename main_name orig inlined type_env clock_env = |
160 |
let loc = Location.dummy_loc in |
161 |
let rename_local_node nodes prefix id = |
162 |
if List.exists (check_node_name id) nodes then |
163 |
prefix ^ id |
164 |
else |
165 |
id |
166 |
in |
167 |
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with |
168 |
Node nd -> nd | _ -> assert false in |
169 |
|
170 |
let orig_rename = rename_local_node orig "orig_" in |
171 |
let inlined_rename = rename_local_node inlined "inlined_" in |
172 |
let identity = (fun x -> x) in |
173 |
let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in |
174 |
let orig = rename_prog orig_rename identity identity orig in |
175 |
let inlined = rename_prog inlined_rename identity identity inlined in |
176 |
let nodes_origs, others = List.partition is_node orig in |
177 |
let nodes_inlined, _ = List.partition is_node inlined in |
178 |
|
179 |
(* One ok_i boolean variable per output var *) |
180 |
let nb_outputs = List.length main_orig_node.node_outputs in |
181 |
let ok_i = List.map (fun id -> |
182 |
mkvar_decl |
183 |
loc |
184 |
("OK" ^ string_of_int id, |
185 |
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
186 |
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
187 |
false) |
188 |
) (Utils.enumerate nb_outputs) |
189 |
in |
190 |
|
191 |
(* OK = ok_1 and ok_2 and ... ok_n-1 *) |
192 |
let ok_ident = "OK" in |
193 |
let ok_output = mkvar_decl |
194 |
loc |
195 |
(ok_ident, |
196 |
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
197 |
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
198 |
false) |
199 |
in |
200 |
let main_ok_expr = |
201 |
let mkv x = mkexpr loc (Expr_ident x) in |
202 |
match ok_i with |
203 |
| [] -> assert false |
204 |
| [x] -> mkv x.var_id |
205 |
| hd::tl -> |
206 |
List.fold_left (fun accu elem -> |
207 |
mkpredef_call loc "&&" [mkv elem.var_id; accu] |
208 |
) (mkv hd.var_id) tl |
209 |
in |
210 |
|
211 |
(* Building main node *) |
212 |
|
213 |
let main_node = { |
214 |
node_id = "check"; |
215 |
node_type = Types.new_var (); |
216 |
node_clock = Clocks.new_var true; |
217 |
node_inputs = main_orig_node.node_inputs; |
218 |
node_outputs = [ok_output]; |
219 |
node_locals = []; |
220 |
node_gencalls = []; |
221 |
node_checks = []; |
222 |
node_asserts = []; |
223 |
node_eqs = [ |
224 |
{ eq_loc = loc; |
225 |
eq_lhs = List.map (fun v -> v.var_id) ok_i; |
226 |
eq_rhs = |
227 |
let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
228 |
let call_orig = |
229 |
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
230 |
let call_inlined = |
231 |
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
232 |
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
233 |
mkexpr loc (Expr_appl ("=", args, None)) |
234 |
}; |
235 |
{ eq_loc = loc; |
236 |
eq_lhs = [ok_ident]; |
237 |
eq_rhs = main_ok_expr; |
238 |
} |
239 |
]; |
240 |
node_dec_stateless = false; |
241 |
node_stateless = None; |
242 |
node_spec = Some |
243 |
{requires = []; |
244 |
ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; |
245 |
behaviors = []; |
246 |
spec_loc = loc |
247 |
}; |
248 |
node_annot = []; |
249 |
} |
250 |
in |
251 |
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in |
252 |
let new_prog = others@nodes_origs@nodes_inlined@main in |
253 |
let _ = Typing.type_prog type_env new_prog in |
254 |
let _ = Clock_calculus.clock_prog clock_env new_prog in |
255 |
|
256 |
|
257 |
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |
258 |
let witness_out = open_out witness_file in |
259 |
let witness_fmt = Format.formatter_of_out_channel witness_out in |
260 |
Format.fprintf witness_fmt |
261 |
"(* Generated lustre file to check validity of inlining process *)@."; |
262 |
Printers.pp_prog witness_fmt new_prog; |
263 |
Format.fprintf witness_fmt "@."; |
264 |
() (* xx *) |
265 |
|
266 |
let global_inline basename prog type_env clock_env = |
267 |
(* We select the main node desc *) |
268 |
let main_node, other_nodes, other_tops = |
269 |
List.fold_left |
270 |
(fun (main_opt, nodes, others) top -> |
271 |
match top.top_decl_desc with |
272 |
| Node nd when nd.node_id = !Options.main_node -> |
273 |
Some top, nodes, others |
274 |
| Node _ -> main_opt, top::nodes, others |
275 |
| _ -> main_opt, nodes, top::others) |
276 |
(None, [], []) prog |
277 |
in |
278 |
(* Recursively each call of a node in the top node is replaced *) |
279 |
let main_node = Utils.desome main_node in |
280 |
let main_node' = inline_all_calls main_node other_nodes in |
281 |
let res = main_node'::other_tops in |
282 |
if !Options.witnesses then ( |
283 |
witness |
284 |
basename |
285 |
(match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false) |
286 |
prog res type_env clock_env |
287 |
); |
288 |
res |
289 |
|
290 |
(* Local Variables: *) |
291 |
(* compile-command:"make -C .." *) |
292 |
(* End: *) |