lustrec / src / inliner.ml @ ef8a361a
History | View | Annotate | Download (17.9 KB)
1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|
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 | b09a175c | ploc | open LustreSpec |
13 | open Corelang |
||
14 | 566dbf49 | ploc | 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 | b09a175c | ploc | |
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 | fc886259 | xthirioux | let is_node_var node v = |
31 | try |
||
32 | ignore (Corelang.get_node_var v node); true |
||
33 | with Not_found -> false |
||
34 | b09a175c | ploc | |
35 | af5af1e8 | ploc | let rename_expr rename expr = expr_replace_var rename expr |
36 | fc886259 | xthirioux | |
37 | af5af1e8 | ploc | let rename_eq rename eq = |
38 | { eq with |
||
39 | eq_lhs = List.map rename eq.eq_lhs; |
||
40 | eq_rhs = rename_expr rename eq.eq_rhs |
||
41 | } |
||
42 | 45f0f48d | xthirioux | |
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 } |
||
82 | ec433d69 | xthirioux | (* |
83 | let get_static_inputs input_arg_list = |
||
84 | List.fold_right (fun (vdecl, arg) res -> |
||
85 | if vdecl.var_dec_const |
||
86 | then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res |
||
87 | else res) |
||
88 | input_arg_list [] |
||
89 | |||
90 | let get_carrier_inputs input_arg_list = |
||
91 | List.fold_right (fun (vdecl, arg) res -> |
||
92 | if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc |
||
93 | then (vdecl.var_id, ident_of_expr arg) :: res |
||
94 | else res) |
||
95 | input_arg_list [] |
||
96 | *) |
||
97 | b09a175c | ploc | (* |
98 | fc886259 | xthirioux | expr, locals', eqs = inline_call id args' reset locals node nodes |
99 | b09a175c | ploc | |
100 | We select the called node equations and variables. |
||
101 | renamed_inputs = args |
||
102 | renamed_eqs |
||
103 | |||
104 | the resulting expression is tuple_of_renamed_outputs |
||
105 | |||
106 | TODO: convert the specification/annotation/assert and inject them |
||
107 | *) |
||
108 | 45f0f48d | xthirioux | (** [inline_call node loc uid args reset locals caller] returns a tuple (expr, |
109 | locals, eqs, asserts) |
||
110 | *) |
||
111 | let inline_call node loc uid args reset locals caller = |
||
112 | 9603460e | xthirioux | let rename v = |
113 | fc886259 | xthirioux | if v = tag_true || v = tag_false || not (is_node_var node v) then v else |
114 | Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) |
||
115 | b09a175c | ploc | in |
116 | ec433d69 | xthirioux | let eqs' = List.map (rename_eq rename) (get_node_eqs node) in |
117 | let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in |
||
118 | let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in |
||
119 | let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in |
||
120 | let carrier_inputs, other_inputs = List.partition (fun (vdecl, arg) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in |
||
121 | let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in |
||
122 | fc886259 | xthirioux | let rename_static v = |
123 | try |
||
124 | ec433d69 | xthirioux | snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs) |
125 | with Not_found -> Dimension.mkdim_ident loc v in |
||
126 | fc886259 | xthirioux | let rename_carrier v = |
127 | try |
||
128 | ec433d69 | xthirioux | snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs) |
129 | fc886259 | xthirioux | with Not_found -> v in |
130 | let rename_var v = |
||
131 | ec433d69 | xthirioux | let vdecl = |
132 | Corelang.mkvar_decl v.var_loc |
||
133 | (rename v.var_id, |
||
134 | { v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc }, |
||
135 | { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc }, |
||
136 | v.var_dec_const, |
||
137 | Utils.option_map (rename_expr rename) v.var_dec_value) in |
||
138 | begin |
||
139 | 45f0f48d | xthirioux | (* |
140 | (try |
||
141 | Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs); |
||
142 | Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ())) |
||
143 | with Not_found -> ()); |
||
144 | (try |
||
145 | Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) |
||
146 | with Not_found -> ()); |
||
147 | (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*) |
||
148 | *) |
||
149 | ec433d69 | xthirioux | vdecl |
150 | end |
||
151 | 01d48bb0 | xthirioux | (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) |
152 | ec433d69 | xthirioux | in |
153 | let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in |
||
154 | b09a175c | ploc | let outputs' = List.map rename_var node.node_outputs in |
155 | ec433d69 | xthirioux | let locals' = |
156 | 01d48bb0 | xthirioux | (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) |
157 | ec433d69 | xthirioux | @ (List.map rename_var node.node_locals) |
158 | 01d48bb0 | xthirioux | in |
159 | b09a175c | ploc | (* checking we are at the appropriate (early) step: node_checks and |
160 | node_gencalls should be empty (not yet assigned) *) |
||
161 | assert (node.node_checks = []); |
||
162 | assert (node.node_gencalls = []); |
||
163 | |||
164 | 45f0f48d | xthirioux | (* Expressing reset locally in equations *) |
165 | let eqs_r' = |
||
166 | match reset with |
||
167 | None -> eqs' |
||
168 | | Some cond -> List.map (add_eq_reset_cond cond) eqs' |
||
169 | in |
||
170 | let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', |
||
171 | expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in |
||
172 | fc886259 | xthirioux | let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') |
173 | b09a175c | ploc | in |
174 | af5af1e8 | ploc | let asserts' = (* We rename variables in assert expressions *) |
175 | List.map |
||
176 | (fun a -> |
||
177 | {a with assert_expr = |
||
178 | let expr = a.assert_expr in |
||
179 | rename_expr rename expr |
||
180 | 45f0f48d | xthirioux | }) |
181 | af5af1e8 | ploc | node.node_asserts |
182 | in |
||
183 | 04a63d25 | xthirioux | let annots' = |
184 | Plugins.inline_annots rename node.node_annot |
||
185 | in |
||
186 | af5af1e8 | ploc | expr, |
187 | inputs'@outputs'@locals'@locals, |
||
188 | 45f0f48d | xthirioux | assign_inputs::eqs_r', |
189 | 04a63d25 | xthirioux | asserts', |
190 | annots' |
||
191 | b09a175c | ploc | |
192 | |||
193 | |||
194 | fc886259 | xthirioux | let inline_table = Hashtbl.create 23 |
195 | b09a175c | ploc | |
196 | (* |
||
197 | fc886259 | xthirioux | new_expr, new_locals, new_eqs = inline_expr expr locals node nodes |
198 | b09a175c | ploc | |
199 | Each occurence of a node in nodes in the expr should be replaced by fresh |
||
200 | variables and the code of called node instance added to new_eqs |
||
201 | |||
202 | *) |
||
203 | fc886259 | xthirioux | let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes = |
204 | 566dbf49 | ploc | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
205 | let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in |
||
206 | b09a175c | ploc | let inline_tuple el = |
207 | 04a63d25 | xthirioux | List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> |
208 | let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in |
||
209 | e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots' |
||
210 | ) el ([], locals, [], [], []) |
||
211 | b09a175c | ploc | in |
212 | let inline_pair e1 e2 = |
||
213 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in |
214 | b09a175c | ploc | match el' with |
215 | d2d9d4cb | ploc | | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots' |
216 | b09a175c | ploc | | _ -> assert false |
217 | in |
||
218 | let inline_triple e1 e2 e3 = |
||
219 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in |
220 | b09a175c | ploc | match el' with |
221 | 04a63d25 | xthirioux | | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots' |
222 | b09a175c | ploc | | _ -> assert false |
223 | in |
||
224 | 566dbf49 | ploc | |
225 | b09a175c | ploc | match expr.expr_desc with |
226 | | Expr_appl (id, args, reset) -> |
||
227 | 04a63d25 | xthirioux | let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in |
228 | 566dbf49 | ploc | if List.exists (check_node_name id) nodes && (* the current node call is provided |
229 | as arguments nodes *) |
||
230 | (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, |
||
231 | it is explicitely inlined here *) |
||
232 | then |
||
233 | b09a175c | ploc | (* The node should be inlined *) |
234 | fc886259 | xthirioux | (* let _ = Format.eprintf "Inlining call to %s@." id in *) |
235 | let called = try List.find (check_node_name id) nodes |
||
236 | b09a175c | ploc | with Not_found -> (assert false) in |
237 | fc886259 | xthirioux | let called = node_of_top called in |
238 | let called' = inline_node called nodes in |
||
239 | 04a63d25 | xthirioux | let expr, locals', eqs'', asserts'', annots'' = |
240 | 45f0f48d | xthirioux | inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in |
241 | 04a63d25 | xthirioux | expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots'' |
242 | b09a175c | ploc | else |
243 | (* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
||
244 | af5af1e8 | ploc | { expr with expr_desc = Expr_appl(id, args', reset)}, |
245 | locals', |
||
246 | eqs', |
||
247 | 04a63d25 | xthirioux | asserts', |
248 | annots' |
||
249 | b09a175c | ploc | |
250 | (* For other cases, we just keep the structure, but convert sub-expressions *) |
||
251 | | Expr_const _ |
||
252 | 04a63d25 | xthirioux | | Expr_ident _ -> expr, locals, [], [], [] |
253 | b09a175c | ploc | | Expr_tuple el -> |
254 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple el in |
255 | { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots' |
||
256 | b09a175c | ploc | | Expr_ite (g, t, e) -> |
257 | 04a63d25 | xthirioux | let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in |
258 | { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots' |
||
259 | b09a175c | ploc | | Expr_arrow (e1, e2) -> |
260 | 04a63d25 | xthirioux | let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |
261 | { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots' |
||
262 | b09a175c | ploc | | Expr_fby (e1, e2) -> |
263 | 04a63d25 | xthirioux | let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |
264 | { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots' |
||
265 | b09a175c | ploc | | Expr_array el -> |
266 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple el in |
267 | { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots' |
||
268 | b09a175c | ploc | | Expr_access (e, dim) -> |
269 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |
270 | { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots' |
||
271 | b09a175c | ploc | | Expr_power (e, dim) -> |
272 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |
273 | { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots' |
||
274 | b09a175c | ploc | | Expr_pre e -> |
275 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |
276 | { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots' |
||
277 | b09a175c | ploc | | Expr_when (e, id, label) -> |
278 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |
279 | { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots' |
||
280 | b09a175c | ploc | | Expr_merge (id, branches) -> |
281 | 04a63d25 | xthirioux | let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in |
282 | b09a175c | ploc | let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
283 | 04a63d25 | xthirioux | { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots' |
284 | fc886259 | xthirioux | |
285 | and inline_node ?(selection_on_annotation=false) node nodes = |
||
286 | ec433d69 | xthirioux | try copy_node (Hashtbl.find inline_table node.node_id) |
287 | fc886259 | xthirioux | with Not_found -> |
288 | 566dbf49 | ploc | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
289 | 04a63d25 | xthirioux | let new_locals, eqs, asserts, annots = |
290 | List.fold_left (fun (locals, eqs, asserts, annots) eq -> |
||
291 | let eq_rhs', locals', new_eqs', asserts', annots' = |
||
292 | fc886259 | xthirioux | inline_expr eq.eq_rhs locals node nodes |
293 | b09a175c | ploc | in |
294 | 04a63d25 | xthirioux | locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots |
295 | ) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node) |
||
296 | b09a175c | ploc | in |
297 | fc886259 | xthirioux | let inlined = |
298 | { node with |
||
299 | b09a175c | ploc | node_locals = new_locals; |
300 | b08ffca7 | xthirioux | node_stmts = List.map (fun eq -> Eq eq) eqs; |
301 | af5af1e8 | ploc | node_asserts = asserts; |
302 | 04a63d25 | xthirioux | node_annot = annots; |
303 | b09a175c | ploc | } |
304 | fc886259 | xthirioux | in |
305 | begin |
||
306 | (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) |
||
307 | Hashtbl.add inline_table node.node_id inlined; |
||
308 | inlined |
||
309 | end |
||
310 | b09a175c | ploc | |
311 | let inline_all_calls node nodes = |
||
312 | let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
||
313 | { node with top_decl_desc = Node (inline_node nd nodes) } |
||
314 | |||
315 | |||
316 | |||
317 | |||
318 | |||
319 | 592f508c | ploc | let witness filename main_name orig inlined type_env clock_env = |
320 | b09a175c | ploc | let loc = Location.dummy_loc in |
321 | let rename_local_node nodes prefix id = |
||
322 | if List.exists (check_node_name id) nodes then |
||
323 | prefix ^ id |
||
324 | else |
||
325 | id |
||
326 | in |
||
327 | let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with |
||
328 | Node nd -> nd | _ -> assert false in |
||
329 | |||
330 | let orig_rename = rename_local_node orig "orig_" in |
||
331 | let inlined_rename = rename_local_node inlined "inlined_" in |
||
332 | let identity = (fun x -> x) in |
||
333 | let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in |
||
334 | let orig = rename_prog orig_rename identity identity orig in |
||
335 | let inlined = rename_prog inlined_rename identity identity inlined in |
||
336 | let nodes_origs, others = List.partition is_node orig in |
||
337 | let nodes_inlined, _ = List.partition is_node inlined in |
||
338 | |||
339 | b50c665d | ploc | (* One ok_i boolean variable per output var *) |
340 | let nb_outputs = List.length main_orig_node.node_outputs in |
||
341 | ec433d69 | xthirioux | let ok_ident = "OK" in |
342 | b50c665d | ploc | let ok_i = List.map (fun id -> |
343 | mkvar_decl |
||
344 | loc |
||
345 | ec433d69 | xthirioux | (Format.sprintf "%s_%i" ok_ident id, |
346 | b50c665d | ploc | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
347 | {ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
||
348 | ec433d69 | xthirioux | false, |
349 | None) |
||
350 | b50c665d | ploc | ) (Utils.enumerate nb_outputs) |
351 | in |
||
352 | |||
353 | (* OK = ok_1 and ok_2 and ... ok_n-1 *) |
||
354 | b09a175c | ploc | let ok_output = mkvar_decl |
355 | loc |
||
356 | (ok_ident, |
||
357 | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
||
358 | {ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
||
359 | ec433d69 | xthirioux | false, |
360 | None) |
||
361 | b09a175c | ploc | in |
362 | b50c665d | ploc | let main_ok_expr = |
363 | let mkv x = mkexpr loc (Expr_ident x) in |
||
364 | match ok_i with |
||
365 | | [] -> assert false |
||
366 | | [x] -> mkv x.var_id |
||
367 | | hd::tl -> |
||
368 | List.fold_left (fun accu elem -> |
||
369 | mkpredef_call loc "&&" [mkv elem.var_id; accu] |
||
370 | ) (mkv hd.var_id) tl |
||
371 | in |
||
372 | |||
373 | (* Building main node *) |
||
374 | |||
375 | b08ffca7 | xthirioux | let ok_i_eq = |
376 | { eq_loc = loc; |
||
377 | eq_lhs = List.map (fun v -> v.var_id) ok_i; |
||
378 | eq_rhs = |
||
379 | let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
||
380 | let call_orig = |
||
381 | mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
||
382 | let call_inlined = |
||
383 | mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
||
384 | let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
||
385 | mkexpr loc (Expr_appl ("=", args, None)) |
||
386 | } in |
||
387 | let ok_eq = |
||
388 | { eq_loc = loc; |
||
389 | eq_lhs = [ok_ident]; |
||
390 | eq_rhs = main_ok_expr; |
||
391 | } in |
||
392 | b09a175c | ploc | let main_node = { |
393 | node_id = "check"; |
||
394 | node_type = Types.new_var (); |
||
395 | node_clock = Clocks.new_var true; |
||
396 | node_inputs = main_orig_node.node_inputs; |
||
397 | node_outputs = [ok_output]; |
||
398 | 9603460e | xthirioux | node_locals = ok_i; |
399 | b09a175c | ploc | node_gencalls = []; |
400 | node_checks = []; |
||
401 | node_asserts = []; |
||
402 | b08ffca7 | xthirioux | node_stmts = [Eq ok_i_eq; Eq ok_eq]; |
403 | 3ab5748b | ploc | node_dec_stateless = false; |
404 | 52cfee34 | xthirioux | node_stateless = None; |
405 | b09a175c | ploc | node_spec = Some |
406 | {requires = []; |
||
407 | 01c7d5e1 | ploc | ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; |
408 | behaviors = []; |
||
409 | spec_loc = loc |
||
410 | b09a175c | ploc | }; |
411 | 01c7d5e1 | ploc | node_annot = []; |
412 | b09a175c | ploc | } |
413 | in |
||
414 | ef34b4ae | xthirioux | let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in |
415 | b09a175c | ploc | let new_prog = others@nodes_origs@nodes_inlined@main in |
416 | 04a63d25 | xthirioux | (* |
417 | let _ = Typing.type_prog type_env new_prog in |
||
418 | let _ = Clock_calculus.clock_prog clock_env new_prog in |
||
419 | *) |
||
420 | |||
421 | 1bff14ac | ploc | let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |
422 | b09a175c | ploc | let witness_out = open_out witness_file in |
423 | let witness_fmt = Format.formatter_of_out_channel witness_out in |
||
424 | ec433d69 | xthirioux | begin |
425 | List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i); |
||
426 | Format.fprintf witness_fmt |
||
427 | "(* Generated lustre file to check validity of inlining process *)@."; |
||
428 | Printers.pp_prog witness_fmt new_prog; |
||
429 | Format.fprintf witness_fmt "@."; |
||
430 | () |
||
431 | end (* xx *) |
||
432 | b09a175c | ploc | |
433 | 592f508c | ploc | let global_inline basename prog type_env clock_env = |
434 | b09a175c | ploc | (* We select the main node desc *) |
435 | let main_node, other_nodes, other_tops = |
||
436 | ec433d69 | xthirioux | List.fold_right |
437 | (fun top (main_opt, nodes, others) -> |
||
438 | b09a175c | ploc | match top.top_decl_desc with |
439 | | Node nd when nd.node_id = !Options.main_node -> |
||
440 | Some top, nodes, others |
||
441 | | Node _ -> main_opt, top::nodes, others |
||
442 | | _ -> main_opt, nodes, top::others) |
||
443 | ec433d69 | xthirioux | prog (None, [], []) |
444 | b09a175c | ploc | in |
445 | 85da3a4b | ploc | |
446 | b09a175c | ploc | (* Recursively each call of a node in the top node is replaced *) |
447 | let main_node = Utils.desome main_node in |
||
448 | let main_node' = inline_all_calls main_node other_nodes in |
||
449 | ec433d69 | xthirioux | let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in |
450 | 85da3a4b | ploc | (* Code snippet from unstable branch. May be used when reactivating witnesses. |
451 | let res = main_node'::other_tops in |
||
452 | 53206908 | xthirioux | if !Options.witnesses then ( |
453 | witness |
||
454 | basename |
||
455 | (match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false) |
||
456 | prog res type_env clock_env |
||
457 | ); |
||
458 | 85da3a4b | ploc | *) |
459 | b09a175c | ploc | res |
460 | b50c665d | ploc | |
461 | 566dbf49 | ploc | let local_inline basename prog type_env clock_env = |
462 | let local_anns = Annotations.get_expr_annotations keyword in |
||
463 | if local_anns != [] then ( |
||
464 | let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |
||
465 | ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns; |
||
466 | List.fold_right (fun top accu -> |
||
467 | ( match top.top_decl_desc with |
||
468 | | Node nd when ISet.mem nd.node_id nodes_with_anns -> |
||
469 | { top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) } |
||
470 | | _ -> top |
||
471 | )::accu) prog [] |
||
472 | |||
473 | ) |
||
474 | else |
||
475 | prog |
||
476 | |||
477 | |||
478 | b50c665d | ploc | (* Local Variables: *) |
479 | (* compile-command:"make -C .." *) |
||
480 | (* End: *) |