Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / inliner.ml @ b3f91fdb

History | View | Annotate | Download (14.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
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 get_static_inputs node args =
31
  List.fold_right2 (fun vdecl arg static ->
32
    if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static)
33
    node.node_inputs
34
    (Corelang.expr_list_of_expr args)
35
    []
36

    
37
let get_carrier_inputs node args =
38
  List.fold_right2 (fun vdecl arg carrier ->
39
    if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier)
40
    node.node_inputs
41
    (Corelang.expr_list_of_expr args)
42
    []
43

    
44
let is_node_var node v =
45
 try
46
   ignore (Corelang.get_node_var v node); true
47
 with Not_found -> false
48

    
49
let rename_expr rename expr = expr_replace_var rename expr
50

    
51
let rename_eq rename eq = 
52
  { eq with
53
    eq_lhs = List.map rename eq.eq_lhs; 
54
    eq_rhs = rename_expr rename eq.eq_rhs
55
  }
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)
77
  in
78
  let static_inputs = get_static_inputs node args in
79
  let carrier_inputs = get_carrier_inputs node args in
80
  let rename_static v =
81
    try
82
      List.assoc v static_inputs
83
    with Not_found -> Dimension.mkdim_ident loc v
84
    (*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*)
85
  in
86
  let rename_carrier v =
87
    try
88
      List.assoc v carrier_inputs
89
    with Not_found -> v in
90
  let rename_var v =
91
  (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
92
    { v with
93
      var_id = rename v.var_id;
94
      var_type = Types.rename_static rename_static v.var_type;
95
      var_clock = Clocks.rename_static rename_carrier v.var_clock;
96
    } in
97
  let inputs' = List.map rename_var node.node_inputs in
98
  let outputs' = List.map rename_var node.node_outputs in
99
  let locals' = List.map rename_var node.node_locals in
100
  (* checking we are at the appropriate (early) step: node_checks and
101
     node_gencalls should be empty (not yet assigned) *)
102
  assert (node.node_checks = []);
103
  assert (node.node_gencalls = []);
104

    
105
  (* Bug included: todo deal with reset *)
106
  assert (reset = None);
107

    
108
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
109
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
110
  in
111
  let asserts' = (* We rename variables in assert expressions *)
112
    List.map 
113
      (fun a -> 
114
	{a with assert_expr = 
115
	    let expr = a.assert_expr in
116
	    rename_expr rename expr
117
      })
118
      node.node_asserts 
119
  in
120
  expr, 
121
  inputs'@outputs'@locals'@locals, 
122
  assign_inputs::eqs',
123
  asserts'
124

    
125

    
126

    
127
let inline_table = Hashtbl.create 23
128

    
129
(* 
130
   new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
131
   
132
   Each occurence of a node in nodes in the expr should be replaced by fresh
133
   variables and the code of called node instance added to new_eqs
134

    
135
*)
136
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
137
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
138
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
139
  let inline_tuple el = 
140
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
141
      let e', locals', eqs', asserts' = inline_expr e locals node nodes in
142
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
143
    ) el ([], locals, [], [])
144
  in
145
  let inline_pair e1 e2 = 
146
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
147
    match el' with
148
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
149
    | _ -> assert false
150
  in
151
  let inline_triple e1 e2 e3 = 
152
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
153
    match el' with
154
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
155
    | _ -> assert false
156
  in
157
  
158
  match expr.expr_desc with
159
  | Expr_appl (id, args, reset) ->
160
    let args', locals', eqs', asserts' = inline_expr args locals node nodes in 
161
    if List.exists (check_node_name id) nodes && (* the current node call is provided
162
						    as arguments nodes *)
163
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
164
							      it is explicitely inlined here *)
165
    then 
166
      (* The node should be inlined *)
167
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
168
      let called = try List.find (check_node_name id) nodes 
169
	with Not_found -> (assert false) in
170
      let called = node_of_top called in
171
      let called' = inline_node called nodes in
172
      let expr, locals', eqs'', asserts'' = 
173
	inline_call called' expr args' reset locals' node in
174
      expr, locals', eqs'@eqs'', asserts'@asserts''
175
    else 
176
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
177
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
178
      locals', 
179
      eqs', 
180
      asserts'
181

    
182
  (* For other cases, we just keep the structure, but convert sub-expressions *)
183
  | Expr_const _ 
184
  | Expr_ident _ -> expr, locals, [], []
185
  | Expr_tuple el -> 
186
    let el', l', eqs', asserts' = inline_tuple el in
187
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
188
  | Expr_ite (g, t, e) ->
189
    let g', t', e', l', eqs', asserts' = inline_triple g t e in
190
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
191
  | Expr_arrow (e1, e2) ->
192
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
193
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
194
  | Expr_fby (e1, e2) ->
195
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
196
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
197
  | Expr_array el ->
198
    let el', l', eqs', asserts' = inline_tuple el in
199
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
200
  | Expr_access (e, dim) ->
201
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
202
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
203
  | Expr_power (e, dim) ->
204
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
205
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
206
  | Expr_pre e ->
207
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
208
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
209
  | Expr_when (e, id, label) ->
210
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
211
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
212
  | Expr_merge (id, branches) ->
213
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
214
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
215
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
216

    
217
and inline_node ?(selection_on_annotation=false) node nodes =
218
  try Hashtbl.find inline_table node.node_id
219
  with Not_found ->
220
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
221
  let new_locals, eqs, asserts = 
222
    List.fold_left (fun (locals, eqs, asserts) eq ->
223
      let eq_rhs', locals', new_eqs', asserts' = 
224
	inline_expr eq.eq_rhs locals node nodes 
225
      in
226
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
227
    ) (node.node_locals, [], node.node_asserts) (get_node_eqs node)
228
  in
229
  let inlined = 
230
  { node with
231
    node_locals = new_locals;
232
    node_stmts = List.map (fun eq -> Eq eq) eqs;
233
    node_asserts = asserts;
234
  }
235
  in
236
  begin
237
    (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
238
    Hashtbl.add inline_table node.node_id inlined;
239
    inlined
240
  end
241

    
242
let inline_all_calls node nodes =
243
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
244
  { node with top_decl_desc = Node (inline_node nd nodes) }
245
    
246

    
247

    
248

    
249

    
250
let witness filename main_name orig inlined type_env clock_env =
251
  let loc = Location.dummy_loc in
252
  let rename_local_node nodes prefix id =
253
    if List.exists (check_node_name id) nodes then
254
      prefix ^ id 
255
    else
256
      id
257
  in
258
  let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
259
  Node nd -> nd | _ -> assert false in
260
  
261
  let orig_rename = rename_local_node orig "orig_" in
262
  let inlined_rename = rename_local_node inlined "inlined_" in
263
  let identity = (fun x -> x) in
264
  let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
265
  let orig = rename_prog orig_rename identity identity orig in
266
  let inlined = rename_prog inlined_rename identity identity inlined in
267
  let nodes_origs, others = List.partition is_node orig in
268
  let nodes_inlined, _ = List.partition is_node inlined in
269

    
270
  (* One ok_i boolean variable  per output var *)
271
  let nb_outputs = List.length main_orig_node.node_outputs in
272
  let ok_i = List.map (fun id ->
273
    mkvar_decl 
274
      loc 
275
      ("OK" ^ string_of_int id,
276
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
277
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
278
       false)
279
  ) (Utils.enumerate nb_outputs) 
280
  in
281

    
282
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
283
  let ok_ident = "OK" in
284
  let ok_output = mkvar_decl 
285
    loc 
286
    (ok_ident,
287
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
288
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
289
     false)
290
  in
291
  let main_ok_expr =
292
    let mkv x = mkexpr loc (Expr_ident x) in
293
    match ok_i with
294
    | [] -> assert false
295
    | [x] -> mkv x.var_id 
296
    | hd::tl -> 
297
      List.fold_left (fun accu elem -> 
298
	mkpredef_call loc "&&" [mkv elem.var_id; accu]
299
      ) (mkv hd.var_id) tl
300
  in
301

    
302
  (* Building main node *)
303

    
304
  let ok_i_eq =
305
    { eq_loc = loc;
306
      eq_lhs = List.map (fun v -> v.var_id) ok_i;
307
      eq_rhs = 
308
	let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
309
	let call_orig = 
310
	  mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
311
	let call_inlined = 
312
	  mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
313
	let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
314
	mkexpr loc (Expr_appl ("=", args, None))
315
    } in
316
  let ok_eq =
317
    { eq_loc = loc;
318
      eq_lhs = [ok_ident];
319
      eq_rhs = main_ok_expr;
320
    } in
321
  let main_node = {
322
    node_id = "check";
323
    node_type = Types.new_var ();
324
    node_clock = Clocks.new_var true;
325
    node_inputs = main_orig_node.node_inputs;
326
    node_outputs = [ok_output];
327
    node_locals = ok_i;
328
    node_gencalls = [];
329
    node_checks = [];
330
    node_asserts = [];
331
    node_stmts = [Eq ok_i_eq; Eq ok_eq];
332
    node_dec_stateless = false;
333
    node_stateless = None;
334
    node_spec = Some 
335
      {requires = []; 
336
       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
337
       behaviors = [];
338
       spec_loc = loc
339
      };
340
    node_annot = [];
341
  }
342
  in
343
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
344
  let new_prog = others@nodes_origs@nodes_inlined@main in
345

    
346
  let _ = Typing.type_prog type_env new_prog in
347
  let _ = Clock_calculus.clock_prog clock_env new_prog in
348

    
349
   
350
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
351
  let witness_out = open_out witness_file in
352
  let witness_fmt = Format.formatter_of_out_channel witness_out in
353
  Format.fprintf witness_fmt
354
    "(* Generated lustre file to check validity of inlining process *)@.";
355
  Printers.pp_prog witness_fmt new_prog;
356
  Format.fprintf witness_fmt "@.";
357
  () (* xx *)
358

    
359
let global_inline basename prog type_env clock_env =
360
  (* We select the main node desc *)
361
  let main_node, other_nodes, other_tops = 
362
    List.fold_left 
363
      (fun (main_opt, nodes, others) top -> 
364
	match top.top_decl_desc with 
365
	| Node nd when nd.node_id = !Options.main_node -> 
366
	  Some top, nodes, others
367
	| Node _ -> main_opt, top::nodes, others
368
	| _ -> main_opt, nodes, top::others) 
369
      (None, [], []) prog 
370
  in
371
  (* Recursively each call of a node in the top node is replaced *)
372
  let main_node = Utils.desome main_node in
373
  let main_node' = inline_all_calls main_node other_nodes in
374
  let res = main_node'::other_tops in
375
  if !Options.witnesses then (
376
    witness 
377
      basename
378
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
379
      prog res type_env clock_env
380
  );
381
  res
382

    
383
let local_inline basename prog type_env clock_env =
384
  let local_anns = Annotations.get_expr_annotations keyword in
385
  if local_anns != [] then (
386
    let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
387
    ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
388
    List.fold_right (fun top accu -> 
389
      ( match top.top_decl_desc with
390
      | Node nd when ISet.mem nd.node_id nodes_with_anns ->
391
	{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
392
      | _ -> top
393
      )::accu) prog []
394
    
395
)
396
 else
397
  prog
398

    
399

    
400
(* Local Variables: *)
401
(* compile-command:"make -C .." *)
402
(* End: *)