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) (get_node_eqs node)
|
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 expr = expr_of_expr_list
|
66
|
loc
|
67
|
(List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
|
68
|
in
|
69
|
let asserts' = (* We rename variables in assert expressions *)
|
70
|
List.map
|
71
|
(fun a ->
|
72
|
{a with assert_expr =
|
73
|
let expr = a.assert_expr in
|
74
|
rename_expr rename expr
|
75
|
})
|
76
|
node.node_asserts
|
77
|
in
|
78
|
expr,
|
79
|
inputs'@outputs'@locals'@locals,
|
80
|
assign_inputs::eqs',
|
81
|
asserts'
|
82
|
|
83
|
|
84
|
|
85
|
|
86
|
(*
|
87
|
new_expr, new_locals, new_eqs = inline_expr expr locals nodes
|
88
|
|
89
|
Each occurence of a node in nodes in the expr should be replaced by fresh
|
90
|
variables and the code of called node instance added to new_eqs
|
91
|
|
92
|
*)
|
93
|
let rec inline_expr expr locals nodes =
|
94
|
let inline_tuple el =
|
95
|
List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
|
96
|
let e', locals', eqs', asserts' = inline_expr e locals nodes in
|
97
|
e'::el_tail, locals', eqs'@eqs, asserts@asserts'
|
98
|
) el ([], locals, [], [])
|
99
|
in
|
100
|
let inline_pair e1 e2 =
|
101
|
let el', l', eqs', asserts' = inline_tuple [e1;e2] in
|
102
|
match el' with
|
103
|
| [e1'; e2'] -> e1', e2', l', eqs', asserts'
|
104
|
| _ -> assert false
|
105
|
in
|
106
|
let inline_triple e1 e2 e3 =
|
107
|
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
|
108
|
match el' with
|
109
|
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
|
110
|
| _ -> assert false
|
111
|
in
|
112
|
|
113
|
match expr.expr_desc with
|
114
|
| Expr_appl (id, args, reset) ->
|
115
|
let args', locals', eqs', asserts' = inline_expr args locals nodes in
|
116
|
if List.exists (check_node_name id) nodes then
|
117
|
(* The node should be inlined *)
|
118
|
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
|
119
|
let node = try List.find (check_node_name id) nodes
|
120
|
with Not_found -> (assert false) in
|
121
|
let node = node_of_top node in
|
122
|
let node = inline_node node nodes in
|
123
|
let expr, locals', eqs'', asserts'' =
|
124
|
inline_call expr args' reset locals' node in
|
125
|
expr, locals', eqs'@eqs'', asserts'@asserts''
|
126
|
else
|
127
|
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
|
128
|
{ expr with expr_desc = Expr_appl(id, args', reset)},
|
129
|
locals',
|
130
|
eqs',
|
131
|
asserts'
|
132
|
|
133
|
(* For other cases, we just keep the structure, but convert sub-expressions *)
|
134
|
| Expr_const _
|
135
|
| Expr_ident _ -> expr, locals, [], []
|
136
|
| Expr_tuple el ->
|
137
|
let el', l', eqs', asserts' = inline_tuple el in
|
138
|
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
|
139
|
| Expr_ite (g, t, e) ->
|
140
|
let g', t', e', l', eqs', asserts' = inline_triple g t e in
|
141
|
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
|
142
|
| Expr_arrow (e1, e2) ->
|
143
|
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
|
144
|
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
|
145
|
| Expr_fby (e1, e2) ->
|
146
|
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
|
147
|
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
|
148
|
| Expr_array el ->
|
149
|
let el', l', eqs', asserts' = inline_tuple el in
|
150
|
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts'
|
151
|
| Expr_access (e, dim) ->
|
152
|
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
153
|
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
|
154
|
| Expr_power (e, dim) ->
|
155
|
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
156
|
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
|
157
|
| Expr_pre e ->
|
158
|
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
159
|
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
|
160
|
| Expr_when (e, id, label) ->
|
161
|
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
162
|
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
|
163
|
| Expr_merge (id, branches) ->
|
164
|
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
|
165
|
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
|
166
|
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
|
167
|
and inline_node nd nodes =
|
168
|
let new_locals, eqs, asserts =
|
169
|
List.fold_left (fun (locals, eqs, asserts) eq ->
|
170
|
let eq_rhs', locals', new_eqs', asserts' =
|
171
|
inline_expr eq.eq_rhs locals nodes
|
172
|
in
|
173
|
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
|
174
|
) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
|
175
|
in
|
176
|
{ nd with
|
177
|
node_locals = new_locals;
|
178
|
node_stmts = List.map (fun eq -> Eq eq) eqs;
|
179
|
node_asserts = asserts;
|
180
|
}
|
181
|
|
182
|
let inline_all_calls node nodes =
|
183
|
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
|
184
|
{ node with top_decl_desc = Node (inline_node nd nodes) }
|
185
|
|
186
|
|
187
|
|
188
|
|
189
|
|
190
|
let witness filename main_name orig inlined type_env clock_env =
|
191
|
let loc = Location.dummy_loc in
|
192
|
let rename_local_node nodes prefix id =
|
193
|
if List.exists (check_node_name id) nodes then
|
194
|
prefix ^ id
|
195
|
else
|
196
|
id
|
197
|
in
|
198
|
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
|
199
|
Node nd -> nd | _ -> assert false in
|
200
|
|
201
|
let orig_rename = rename_local_node orig "orig_" in
|
202
|
let inlined_rename = rename_local_node inlined "inlined_" in
|
203
|
let identity = (fun x -> x) in
|
204
|
let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
|
205
|
let orig = rename_prog orig_rename identity identity orig in
|
206
|
let inlined = rename_prog inlined_rename identity identity inlined in
|
207
|
let nodes_origs, others = List.partition is_node orig in
|
208
|
let nodes_inlined, _ = List.partition is_node inlined in
|
209
|
|
210
|
(* One ok_i boolean variable per output var *)
|
211
|
let nb_outputs = List.length main_orig_node.node_outputs in
|
212
|
let ok_i = List.map (fun id ->
|
213
|
mkvar_decl
|
214
|
loc
|
215
|
("OK" ^ string_of_int id,
|
216
|
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
|
217
|
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
|
218
|
false)
|
219
|
) (Utils.enumerate nb_outputs)
|
220
|
in
|
221
|
|
222
|
(* OK = ok_1 and ok_2 and ... ok_n-1 *)
|
223
|
let ok_ident = "OK" in
|
224
|
let ok_output = mkvar_decl
|
225
|
loc
|
226
|
(ok_ident,
|
227
|
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
|
228
|
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
|
229
|
false)
|
230
|
in
|
231
|
let main_ok_expr =
|
232
|
let mkv x = mkexpr loc (Expr_ident x) in
|
233
|
match ok_i with
|
234
|
| [] -> assert false
|
235
|
| [x] -> mkv x.var_id
|
236
|
| hd::tl ->
|
237
|
List.fold_left (fun accu elem ->
|
238
|
mkpredef_call loc "&&" [mkv elem.var_id; accu]
|
239
|
) (mkv hd.var_id) tl
|
240
|
in
|
241
|
|
242
|
(* Building main node *)
|
243
|
|
244
|
let ok_i_eq =
|
245
|
{ eq_loc = loc;
|
246
|
eq_lhs = List.map (fun v -> v.var_id) ok_i;
|
247
|
eq_rhs =
|
248
|
let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
|
249
|
let call_orig =
|
250
|
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
|
251
|
let call_inlined =
|
252
|
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
|
253
|
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in
|
254
|
mkexpr loc (Expr_appl ("=", args, None))
|
255
|
} in
|
256
|
let ok_eq =
|
257
|
{ eq_loc = loc;
|
258
|
eq_lhs = [ok_ident];
|
259
|
eq_rhs = main_ok_expr;
|
260
|
} in
|
261
|
let main_node = {
|
262
|
node_id = "check";
|
263
|
node_type = Types.new_var ();
|
264
|
node_clock = Clocks.new_var true;
|
265
|
node_inputs = main_orig_node.node_inputs;
|
266
|
node_outputs = [ok_output];
|
267
|
node_locals = ok_i;
|
268
|
node_gencalls = [];
|
269
|
node_checks = [];
|
270
|
node_asserts = [];
|
271
|
node_stmts = [Eq ok_i_eq; Eq ok_eq];
|
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
|
(* compile-command:"make -C .." *)
|
324
|
(* End: *)
|