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 is_node_var node v =
|
31
|
try
|
32
|
ignore (Corelang.get_node_var v node); true
|
33
|
with Not_found -> false
|
34
|
|
35
|
let rename_expr rename expr = expr_replace_var rename expr
|
36
|
|
37
|
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
|
(*
|
43
|
let get_static_inputs input_arg_list =
|
44
|
List.fold_right (fun (vdecl, arg) res ->
|
45
|
if vdecl.var_dec_const
|
46
|
then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res
|
47
|
else res)
|
48
|
input_arg_list []
|
49
|
|
50
|
let get_carrier_inputs input_arg_list =
|
51
|
List.fold_right (fun (vdecl, arg) res ->
|
52
|
if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc
|
53
|
then (vdecl.var_id, ident_of_expr arg) :: res
|
54
|
else res)
|
55
|
input_arg_list []
|
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) in
|
77
|
let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
|
78
|
let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
|
79
|
let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
|
80
|
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
|
81
|
let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in
|
82
|
let rename_static v =
|
83
|
try
|
84
|
snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
|
85
|
with Not_found -> Dimension.mkdim_ident loc v in
|
86
|
let rename_carrier v =
|
87
|
try
|
88
|
snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
|
89
|
with Not_found -> v in
|
90
|
let rename_var v =
|
91
|
let vdecl =
|
92
|
Corelang.mkvar_decl v.var_loc
|
93
|
(rename v.var_id,
|
94
|
{ v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
|
95
|
{ v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
|
96
|
v.var_dec_const,
|
97
|
Utils.option_map (rename_expr rename) v.var_dec_value) in
|
98
|
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
|
*)
|
109
|
vdecl
|
110
|
end
|
111
|
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
|
112
|
in
|
113
|
let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
|
114
|
let outputs' = List.map rename_var node.node_outputs in
|
115
|
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)
|
117
|
@ (List.map rename_var node.node_locals)
|
118
|
in
|
119
|
(* checking we are at the appropriate (early) step: node_checks and
|
120
|
node_gencalls should be empty (not yet assigned) *)
|
121
|
assert (node.node_checks = []);
|
122
|
assert (node.node_gencalls = []);
|
123
|
|
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
|
128
|
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
|
129
|
in
|
130
|
let asserts' = (* We rename variables in assert expressions *)
|
131
|
List.map
|
132
|
(fun a ->
|
133
|
{a with assert_expr =
|
134
|
let expr = a.assert_expr in
|
135
|
rename_expr rename expr
|
136
|
})
|
137
|
node.node_asserts
|
138
|
in
|
139
|
expr,
|
140
|
inputs'@outputs'@locals'@locals,
|
141
|
assign_inputs::eqs',
|
142
|
asserts'
|
143
|
|
144
|
|
145
|
|
146
|
let inline_table = Hashtbl.create 23
|
147
|
|
148
|
(*
|
149
|
new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
|
150
|
|
151
|
Each occurence of a node in nodes in the expr should be replaced by fresh
|
152
|
variables and the code of called node instance added to new_eqs
|
153
|
|
154
|
*)
|
155
|
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
|
156
|
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
|
157
|
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
|
158
|
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, [], [])
|
163
|
in
|
164
|
let inline_pair e1 e2 =
|
165
|
let el', l', eqs', asserts' = inline_tuple [e1;e2] in
|
166
|
match el' with
|
167
|
| [e1'; e2'] -> e1', e2', l', eqs', asserts'
|
168
|
| _ -> assert false
|
169
|
in
|
170
|
let inline_triple e1 e2 e3 =
|
171
|
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
|
172
|
match el' with
|
173
|
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
|
174
|
| _ -> assert false
|
175
|
in
|
176
|
|
177
|
match expr.expr_desc with
|
178
|
| Expr_appl (id, args, reset) ->
|
179
|
let args', locals', eqs', asserts' = inline_expr args locals node nodes in
|
180
|
if List.exists (check_node_name id) nodes && (* the current node call is provided
|
181
|
as arguments nodes *)
|
182
|
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
|
183
|
it is explicitely inlined here *)
|
184
|
then
|
185
|
(* The node should be inlined *)
|
186
|
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
|
187
|
let called = try List.find (check_node_name id) nodes
|
188
|
with Not_found -> (assert false) in
|
189
|
let called = node_of_top called in
|
190
|
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''
|
194
|
else
|
195
|
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
|
196
|
{ expr with expr_desc = Expr_appl(id, args', reset)},
|
197
|
locals',
|
198
|
eqs',
|
199
|
asserts'
|
200
|
|
201
|
(* For other cases, we just keep the structure, but convert sub-expressions *)
|
202
|
| Expr_const _
|
203
|
| Expr_ident _ -> expr, locals, [], []
|
204
|
| Expr_tuple el ->
|
205
|
let el', l', eqs', asserts' = inline_tuple el in
|
206
|
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
|
207
|
| 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'
|
210
|
| 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'
|
213
|
| 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'
|
216
|
| Expr_array el ->
|
217
|
let el', l', eqs', asserts' = inline_tuple el in
|
218
|
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts'
|
219
|
| 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'
|
222
|
| 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'
|
225
|
| 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'
|
228
|
| 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'
|
231
|
| Expr_merge (id, branches) ->
|
232
|
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
|
233
|
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
|
234
|
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
|
235
|
|
236
|
and inline_node ?(selection_on_annotation=false) node nodes =
|
237
|
try copy_node (Hashtbl.find inline_table node.node_id)
|
238
|
with Not_found ->
|
239
|
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' =
|
243
|
inline_expr eq.eq_rhs locals node nodes
|
244
|
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)
|
247
|
in
|
248
|
let inlined =
|
249
|
{ node with
|
250
|
node_locals = new_locals;
|
251
|
node_stmts = List.map (fun eq -> Eq eq) eqs;
|
252
|
node_asserts = asserts;
|
253
|
}
|
254
|
in
|
255
|
begin
|
256
|
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
|
257
|
Hashtbl.add inline_table node.node_id inlined;
|
258
|
inlined
|
259
|
end
|
260
|
|
261
|
let inline_all_calls node nodes =
|
262
|
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
|
263
|
{ node with top_decl_desc = Node (inline_node nd nodes) }
|
264
|
|
265
|
|
266
|
|
267
|
|
268
|
|
269
|
let witness filename main_name orig inlined type_env clock_env =
|
270
|
let loc = Location.dummy_loc in
|
271
|
let rename_local_node nodes prefix id =
|
272
|
if List.exists (check_node_name id) nodes then
|
273
|
prefix ^ id
|
274
|
else
|
275
|
id
|
276
|
in
|
277
|
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
|
278
|
Node nd -> nd | _ -> assert false in
|
279
|
|
280
|
let orig_rename = rename_local_node orig "orig_" in
|
281
|
let inlined_rename = rename_local_node inlined "inlined_" in
|
282
|
let identity = (fun x -> x) in
|
283
|
let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
|
284
|
let orig = rename_prog orig_rename identity identity orig in
|
285
|
let inlined = rename_prog inlined_rename identity identity inlined in
|
286
|
let nodes_origs, others = List.partition is_node orig in
|
287
|
let nodes_inlined, _ = List.partition is_node inlined in
|
288
|
|
289
|
(* One ok_i boolean variable per output var *)
|
290
|
let nb_outputs = List.length main_orig_node.node_outputs in
|
291
|
let ok_ident = "OK" in
|
292
|
let ok_i = List.map (fun id ->
|
293
|
mkvar_decl
|
294
|
loc
|
295
|
(Format.sprintf "%s_%i" ok_ident id,
|
296
|
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
|
297
|
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
|
298
|
false,
|
299
|
None)
|
300
|
) (Utils.enumerate nb_outputs)
|
301
|
in
|
302
|
|
303
|
(* OK = ok_1 and ok_2 and ... ok_n-1 *)
|
304
|
let ok_output = mkvar_decl
|
305
|
loc
|
306
|
(ok_ident,
|
307
|
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
|
308
|
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
|
309
|
false,
|
310
|
None)
|
311
|
in
|
312
|
let main_ok_expr =
|
313
|
let mkv x = mkexpr loc (Expr_ident x) in
|
314
|
match ok_i with
|
315
|
| [] -> assert false
|
316
|
| [x] -> mkv x.var_id
|
317
|
| hd::tl ->
|
318
|
List.fold_left (fun accu elem ->
|
319
|
mkpredef_call loc "&&" [mkv elem.var_id; accu]
|
320
|
) (mkv hd.var_id) tl
|
321
|
in
|
322
|
|
323
|
(* Building main node *)
|
324
|
|
325
|
let ok_i_eq =
|
326
|
{ eq_loc = loc;
|
327
|
eq_lhs = List.map (fun v -> v.var_id) ok_i;
|
328
|
eq_rhs =
|
329
|
let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
|
330
|
let call_orig =
|
331
|
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
|
332
|
let call_inlined =
|
333
|
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
|
334
|
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in
|
335
|
mkexpr loc (Expr_appl ("=", args, None))
|
336
|
} in
|
337
|
let ok_eq =
|
338
|
{ eq_loc = loc;
|
339
|
eq_lhs = [ok_ident];
|
340
|
eq_rhs = main_ok_expr;
|
341
|
} in
|
342
|
let main_node = {
|
343
|
node_id = "check";
|
344
|
node_type = Types.new_var ();
|
345
|
node_clock = Clocks.new_var true;
|
346
|
node_inputs = main_orig_node.node_inputs;
|
347
|
node_outputs = [ok_output];
|
348
|
node_locals = ok_i;
|
349
|
node_gencalls = [];
|
350
|
node_checks = [];
|
351
|
node_asserts = [];
|
352
|
node_stmts = [Eq ok_i_eq; Eq ok_eq];
|
353
|
node_dec_stateless = false;
|
354
|
node_stateless = None;
|
355
|
node_spec = Some
|
356
|
{requires = [];
|
357
|
ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
|
358
|
behaviors = [];
|
359
|
spec_loc = loc
|
360
|
};
|
361
|
node_annot = [];
|
362
|
}
|
363
|
in
|
364
|
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
|
365
|
let new_prog = others@nodes_origs@nodes_inlined@main in
|
366
|
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
|
367
|
let witness_out = open_out witness_file in
|
368
|
let witness_fmt = Format.formatter_of_out_channel witness_out in
|
369
|
begin
|
370
|
List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i);
|
371
|
Format.fprintf witness_fmt
|
372
|
"(* Generated lustre file to check validity of inlining process *)@.";
|
373
|
Printers.pp_prog witness_fmt new_prog;
|
374
|
Format.fprintf witness_fmt "@.";
|
375
|
()
|
376
|
end (* xx *)
|
377
|
|
378
|
let global_inline basename prog type_env clock_env =
|
379
|
(* We select the main node desc *)
|
380
|
let main_node, other_nodes, other_tops =
|
381
|
List.fold_right
|
382
|
(fun top (main_opt, nodes, others) ->
|
383
|
match top.top_decl_desc with
|
384
|
| Node nd when nd.node_id = !Options.main_node ->
|
385
|
Some top, nodes, others
|
386
|
| Node _ -> main_opt, top::nodes, others
|
387
|
| _ -> main_opt, nodes, top::others)
|
388
|
prog (None, [], [])
|
389
|
in
|
390
|
|
391
|
(* Recursively each call of a node in the top node is replaced *)
|
392
|
let main_node = Utils.desome main_node in
|
393
|
let main_node' = inline_all_calls main_node other_nodes in
|
394
|
let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
|
395
|
res
|
396
|
|
397
|
let local_inline basename prog type_env clock_env =
|
398
|
let local_anns = Annotations.get_expr_annotations keyword in
|
399
|
if local_anns != [] then (
|
400
|
let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
|
401
|
ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
|
402
|
List.fold_right (fun top accu ->
|
403
|
( match top.top_decl_desc with
|
404
|
| Node nd when ISet.mem nd.node_id nodes_with_anns ->
|
405
|
{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
|
406
|
| _ -> top
|
407
|
)::accu) prog []
|
408
|
|
409
|
)
|
410
|
else
|
411
|
prog
|
412
|
|
413
|
|
414
|
(* Local Variables: *)
|
415
|
(* compile-command:"make -C .." *)
|
416
|
(* End: *)
|