Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / inliner.ml @ 566dbf49

History | View | Annotate | Download (12.5 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
31 af5af1e8 ploc
let rename_expr rename expr = expr_replace_var rename expr
32
let rename_eq rename eq = 
33
  { eq with
34
    eq_lhs = List.map rename eq.eq_lhs; 
35
    eq_rhs = rename_expr rename eq.eq_rhs
36
  }
37
38 b09a175c ploc
(* 
39
    expr, locals', eqs = inline_call id args' reset locals nodes
40
41
We select the called node equations and variables.
42
   renamed_inputs = args
43
   renamed_eqs
44
45
the resulting expression is tuple_of_renamed_outputs
46
   
47
TODO: convert the specification/annotation/assert and inject them
48
TODO: deal with reset
49
*)
50
let inline_call orig_expr args reset locals node =
51
  let loc = orig_expr.expr_loc in
52
  let uid = orig_expr.expr_tag in
53 9603460e xthirioux
  let rename v =
54
    if v = tag_true || v = tag_false then v else
55
    (Format.fprintf Format.str_formatter "%s_%i_%s" 
56 b09a175c ploc
      node.node_id uid v;
57 9603460e xthirioux
    Format.flush_str_formatter ())
58 b09a175c ploc
  in
59 b08ffca7 xthirioux
  let eqs' = List.map (rename_eq rename) (get_node_eqs node)
60 b09a175c ploc
  in
61
  let rename_var v = { v with var_id = rename v.var_id } in
62
  let inputs' = List.map rename_var node.node_inputs in
63
  let outputs' = List.map rename_var node.node_outputs in
64
  let locals' = List.map rename_var node.node_locals in
65
66
  (* checking we are at the appropriate (early) step: node_checks and
67
     node_gencalls should be empty (not yet assigned) *)
68
  assert (node.node_checks = []);
69
  assert (node.node_gencalls = []);
70
71
  (* Bug included: todo deal with reset *)
72
  assert (reset = None);
73
74
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
75
  let expr = expr_of_expr_list 
76
    loc 
77
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
78
  in
79 af5af1e8 ploc
  let asserts' = (* We rename variables in assert expressions *)
80
    List.map 
81
      (fun a -> 
82
	{a with assert_expr = 
83
	    let expr = a.assert_expr in
84
	    rename_expr rename expr
85
      })
86
      node.node_asserts 
87
  in
88
  expr, 
89
  inputs'@outputs'@locals'@locals, 
90 04d15b97 xthirioux
  assign_inputs::eqs',
91 af5af1e8 ploc
  asserts'
92 b09a175c ploc
93
94
95
96
(* 
97
   new_expr, new_locals, new_eqs = inline_expr expr locals nodes
98
   
99
   Each occurence of a node in nodes in the expr should be replaced by fresh
100
   variables and the code of called node instance added to new_eqs
101
102
*)
103 566dbf49 ploc
let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
104
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
105
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
106 b09a175c ploc
  let inline_tuple el = 
107 af5af1e8 ploc
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
108
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
109
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
110
    ) el ([], locals, [], [])
111 b09a175c ploc
  in
112
  let inline_pair e1 e2 = 
113 af5af1e8 ploc
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
114 b09a175c ploc
    match el' with
115 af5af1e8 ploc
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
116 b09a175c ploc
    | _ -> assert false
117
  in
118
  let inline_triple e1 e2 e3 = 
119 af5af1e8 ploc
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
120 b09a175c ploc
    match el' with
121 af5af1e8 ploc
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
122 b09a175c ploc
    | _ -> assert false
123
  in
124 566dbf49 ploc
  
125 b09a175c ploc
  match expr.expr_desc with
126
  | Expr_appl (id, args, reset) ->
127 af5af1e8 ploc
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
128 566dbf49 ploc
    if List.exists (check_node_name id) nodes && (* the current node call is provided
129
						    as arguments nodes *)
130
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
131
							      it is explicitely inlined here *)
132
    then 
133 b09a175c ploc
      (* The node should be inlined *)
134 566dbf49 ploc
       let _ =     Format.eprintf "Inlining call to %s@." id in 
135 af5af1e8 ploc
      let node = try List.find (check_node_name id) nodes 
136 b09a175c ploc
	with Not_found -> (assert false) in
137 70df2f87 xthirioux
      let node = node_of_top node in
138 b09a175c ploc
      let node = inline_node node nodes in
139 af5af1e8 ploc
      let expr, locals', eqs'', asserts'' = 
140 b09a175c ploc
	inline_call expr args' reset locals' node in
141 af5af1e8 ploc
      expr, locals', eqs'@eqs'', asserts'@asserts''
142 b09a175c ploc
    else 
143
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
144 af5af1e8 ploc
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
145
      locals', 
146
      eqs', 
147
      asserts'
148 b09a175c ploc
149
  (* For other cases, we just keep the structure, but convert sub-expressions *)
150
  | Expr_const _ 
151 af5af1e8 ploc
  | Expr_ident _ -> expr, locals, [], []
152 b09a175c ploc
  | Expr_tuple el -> 
153 af5af1e8 ploc
    let el', l', eqs', asserts' = inline_tuple el in
154
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
155 b09a175c ploc
  | Expr_ite (g, t, e) ->
156 af5af1e8 ploc
    let g', t', e', l', eqs', asserts' = inline_triple g t e in
157
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
158 b09a175c ploc
  | Expr_arrow (e1, e2) ->
159 af5af1e8 ploc
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
160
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
161 b09a175c ploc
  | Expr_fby (e1, e2) ->
162 af5af1e8 ploc
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
163
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
164 b09a175c ploc
  | Expr_array el ->
165 af5af1e8 ploc
    let el', l', eqs', asserts' = inline_tuple el in
166
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
167 b09a175c ploc
  | Expr_access (e, dim) ->
168 af5af1e8 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
169
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
170 b09a175c ploc
  | Expr_power (e, dim) ->
171 af5af1e8 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
172
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
173 b09a175c ploc
  | Expr_pre e ->
174 af5af1e8 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
175
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
176 b09a175c ploc
  | Expr_when (e, id, label) ->
177 af5af1e8 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
178
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
179 b09a175c ploc
  | Expr_merge (id, branches) ->
180 af5af1e8 ploc
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
181 b09a175c ploc
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
182 af5af1e8 ploc
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
183 566dbf49 ploc
and inline_node ?(selection_on_annotation=false) nd nodes = 
184
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
185 af5af1e8 ploc
  let new_locals, eqs, asserts = 
186
    List.fold_left (fun (locals, eqs, asserts) eq ->
187
      let eq_rhs', locals', new_eqs', asserts' = 
188 b09a175c ploc
	inline_expr eq.eq_rhs locals nodes 
189
      in
190 af5af1e8 ploc
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
191 b08ffca7 xthirioux
    ) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
192 b09a175c ploc
  in
193
  { nd with
194
    node_locals = new_locals;
195 b08ffca7 xthirioux
    node_stmts = List.map (fun eq -> Eq eq) eqs;
196 af5af1e8 ploc
    node_asserts = asserts;
197 b09a175c ploc
  }
198
199
let inline_all_calls node nodes =
200
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
201
  { node with top_decl_desc = Node (inline_node nd nodes) }
202
    
203
204
205
206
207 592f508c ploc
let witness filename main_name orig inlined type_env clock_env =
208 b09a175c ploc
  let loc = Location.dummy_loc in
209
  let rename_local_node nodes prefix id =
210
    if List.exists (check_node_name id) nodes then
211
      prefix ^ id 
212
    else
213
      id
214
  in
215
  let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
216
  Node nd -> nd | _ -> assert false in
217
  
218
  let orig_rename = rename_local_node orig "orig_" in
219
  let inlined_rename = rename_local_node inlined "inlined_" in
220
  let identity = (fun x -> x) in
221
  let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
222
  let orig = rename_prog orig_rename identity identity orig in
223
  let inlined = rename_prog inlined_rename identity identity inlined in
224
  let nodes_origs, others = List.partition is_node orig in
225
  let nodes_inlined, _ = List.partition is_node inlined in
226
227 b50c665d ploc
  (* One ok_i boolean variable  per output var *)
228
  let nb_outputs = List.length main_orig_node.node_outputs in
229
  let ok_i = List.map (fun id ->
230
    mkvar_decl 
231
      loc 
232
      ("OK" ^ string_of_int id,
233
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
234
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
235
       false)
236
  ) (Utils.enumerate nb_outputs) 
237
  in
238
239
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
240 b09a175c ploc
  let ok_ident = "OK" in
241
  let ok_output = mkvar_decl 
242
    loc 
243
    (ok_ident,
244
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
245
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
246
     false)
247
  in
248 b50c665d ploc
  let main_ok_expr =
249
    let mkv x = mkexpr loc (Expr_ident x) in
250
    match ok_i with
251
    | [] -> assert false
252
    | [x] -> mkv x.var_id 
253
    | hd::tl -> 
254
      List.fold_left (fun accu elem -> 
255
	mkpredef_call loc "&&" [mkv elem.var_id; accu]
256
      ) (mkv hd.var_id) tl
257
  in
258
259
  (* Building main node *)
260
261 b08ffca7 xthirioux
  let ok_i_eq =
262
    { eq_loc = loc;
263
      eq_lhs = List.map (fun v -> v.var_id) ok_i;
264
      eq_rhs = 
265
	let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
266
	let call_orig = 
267
	  mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
268
	let call_inlined = 
269
	  mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
270
	let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
271
	mkexpr loc (Expr_appl ("=", args, None))
272
    } in
273
  let ok_eq =
274
    { eq_loc = loc;
275
      eq_lhs = [ok_ident];
276
      eq_rhs = main_ok_expr;
277
    } in
278 b09a175c ploc
  let main_node = {
279
    node_id = "check";
280
    node_type = Types.new_var ();
281
    node_clock = Clocks.new_var true;
282
    node_inputs = main_orig_node.node_inputs;
283
    node_outputs = [ok_output];
284 9603460e xthirioux
    node_locals = ok_i;
285 b09a175c ploc
    node_gencalls = [];
286
    node_checks = [];
287
    node_asserts = [];
288 b08ffca7 xthirioux
    node_stmts = [Eq ok_i_eq; Eq ok_eq];
289 3ab5748b ploc
    node_dec_stateless = false;
290 52cfee34 xthirioux
    node_stateless = None;
291 b09a175c ploc
    node_spec = Some 
292
      {requires = []; 
293 01c7d5e1 ploc
       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
294
       behaviors = [];
295
       spec_loc = loc
296 b09a175c ploc
      };
297 01c7d5e1 ploc
    node_annot = [];
298 b09a175c ploc
  }
299
  in
300 ef34b4ae xthirioux
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
301 b09a175c ploc
  let new_prog = others@nodes_origs@nodes_inlined@main in
302
  let _ = Typing.type_prog type_env new_prog in
303
  let _ = Clock_calculus.clock_prog clock_env new_prog in
304
305 592f508c ploc
   
306
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
307 b09a175c ploc
  let witness_out = open_out witness_file in
308
  let witness_fmt = Format.formatter_of_out_channel witness_out in
309
  Format.fprintf witness_fmt
310
    "(* Generated lustre file to check validity of inlining process *)@.";
311
  Printers.pp_prog witness_fmt new_prog;
312
  Format.fprintf witness_fmt "@.";
313
  () (* xx *)
314
315 592f508c ploc
let global_inline basename prog type_env clock_env =
316 b09a175c ploc
  (* We select the main node desc *)
317
  let main_node, other_nodes, other_tops = 
318
    List.fold_left 
319
      (fun (main_opt, nodes, others) top -> 
320
	match top.top_decl_desc with 
321
	| Node nd when nd.node_id = !Options.main_node -> 
322
	  Some top, nodes, others
323
	| Node _ -> main_opt, top::nodes, others
324
	| _ -> main_opt, nodes, top::others) 
325
      (None, [], []) prog 
326
  in
327
  (* Recursively each call of a node in the top node is replaced *)
328
  let main_node = Utils.desome main_node in
329
  let main_node' = inline_all_calls main_node other_nodes in
330
  let res = main_node'::other_tops in
331 592f508c ploc
  if !Options.witnesses then (
332
    witness 
333
      basename
334
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
335
      prog res type_env clock_env
336
  );
337 b09a175c ploc
  res
338 b50c665d ploc
339 566dbf49 ploc
let local_inline basename prog type_env clock_env =
340
  let local_anns = Annotations.get_expr_annotations keyword in
341
  if local_anns != [] then (
342
    let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
343
    ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
344
    List.fold_right (fun top accu -> 
345
      ( match top.top_decl_desc with
346
      | Node nd when ISet.mem nd.node_id nodes_with_anns ->
347
	{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
348
      | _ -> top
349
      )::accu) prog []
350
    
351
)
352
 else
353
  prog
354
355
356 b50c665d ploc
(* Local Variables: *)
357
(* compile-command:"make -C .." *)
358
(* End: *)