Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / inliner.ml @ 7dedc5f0

History | View | Annotate | Download (11 KB)

1 b38ffff3 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 274c72ec ploc
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 36454535 ploc
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 274c72ec ploc
(* 
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
    Format.fprintf Format.str_formatter "%s_%i_%s" 
45
      node.node_id uid v;
46
    Format.flush_str_formatter ()
47
  in
48 36454535 ploc
  let eqs' = List.map (rename_eq rename) node.node_eqs
49 274c72ec ploc
  in
50
  let rename_var v = { v with var_id = rename v.var_id } in
51
  let inputs' = List.map rename_var node.node_inputs in
52
  let outputs' = List.map rename_var node.node_outputs in
53
  let locals' = List.map rename_var node.node_locals in
54
55
  (* checking we are at the appropriate (early) step: node_checks and
56
     node_gencalls should be empty (not yet assigned) *)
57
  assert (node.node_checks = []);
58
  assert (node.node_gencalls = []);
59
60
  (* Bug included: todo deal with reset *)
61
  assert (reset = None);
62
63
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
64
  let expr = expr_of_expr_list 
65
    loc 
66
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
67
  in
68 36454535 ploc
  let asserts' = (* We rename variables in assert expressions *)
69
    List.map 
70
      (fun a -> 
71
	{a with assert_expr = 
72
	    let expr = a.assert_expr in
73
	    rename_expr rename expr
74
      })
75
      node.node_asserts 
76
  in
77
  expr, 
78
  inputs'@outputs'@locals'@locals, 
79
  assign_inputs::eqs',
80
  asserts'
81 274c72ec ploc
82
83
84
85
(* 
86
   new_expr, new_locals, new_eqs = inline_expr expr locals nodes
87
   
88
   Each occurence of a node in nodes in the expr should be replaced by fresh
89
   variables and the code of called node instance added to new_eqs
90
91
*)
92
let rec inline_expr expr locals nodes =
93
  let inline_tuple el = 
94 36454535 ploc
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
95
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
96
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
97
    ) el ([], locals, [], [])
98 274c72ec ploc
  in
99
  let inline_pair e1 e2 = 
100 36454535 ploc
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
101 274c72ec ploc
    match el' with
102 36454535 ploc
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
103 274c72ec ploc
    | _ -> assert false
104
  in
105
  let inline_triple e1 e2 e3 = 
106 36454535 ploc
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
107 274c72ec ploc
    match el' with
108 36454535 ploc
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
109 274c72ec ploc
    | _ -> assert false
110
  in
111
    
112
  match expr.expr_desc with
113
  | Expr_appl (id, args, reset) ->
114 36454535 ploc
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
115 274c72ec ploc
    if List.exists (check_node_name id) nodes then 
116
      (* The node should be inlined *)
117 36454535 ploc
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
118
      let node = try List.find (check_node_name id) nodes 
119 274c72ec ploc
	with Not_found -> (assert false) in
120 36454535 ploc
      let node = 
121
	match node.top_decl_desc with Node nd -> nd | _ -> assert false in
122 274c72ec ploc
      let node = inline_node node nodes in
123 36454535 ploc
      let expr, locals', eqs'', asserts'' = 
124 274c72ec ploc
	inline_call expr args' reset locals' node in
125 36454535 ploc
      expr, locals', eqs'@eqs'', asserts'@asserts''
126 274c72ec ploc
    else 
127
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
128 36454535 ploc
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
129
      locals', 
130
      eqs', 
131
      asserts'
132 274c72ec ploc
133
  (* For other cases, we just keep the structure, but convert sub-expressions *)
134
  | Expr_const _ 
135 36454535 ploc
  | Expr_ident _ -> expr, locals, [], []
136 274c72ec ploc
  | Expr_tuple el -> 
137 36454535 ploc
    let el', l', eqs', asserts' = inline_tuple el in
138
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
139 274c72ec ploc
  | Expr_ite (g, t, e) ->
140 36454535 ploc
    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 274c72ec ploc
  | Expr_arrow (e1, e2) ->
143 36454535 ploc
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
144
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
145 274c72ec ploc
  | Expr_fby (e1, e2) ->
146 36454535 ploc
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
147
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
148 274c72ec ploc
  | Expr_array el ->
149 36454535 ploc
    let el', l', eqs', asserts' = inline_tuple el in
150
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
151 274c72ec ploc
  | Expr_access (e, dim) ->
152 36454535 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
153
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
154 274c72ec ploc
  | Expr_power (e, dim) ->
155 36454535 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
156
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
157 274c72ec ploc
  | Expr_pre e ->
158 36454535 ploc
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
159
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
160 274c72ec ploc
  | Expr_when (e, id, label) ->
161 36454535 ploc
    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 274c72ec ploc
  | Expr_merge (id, branches) ->
164 36454535 ploc
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
165 274c72ec ploc
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
166 36454535 ploc
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
167 274c72ec ploc
and inline_node nd nodes = 
168 36454535 ploc
  let new_locals, eqs, asserts = 
169
    List.fold_left (fun (locals, eqs, asserts) eq ->
170
      let eq_rhs', locals', new_eqs', asserts' = 
171 274c72ec ploc
	inline_expr eq.eq_rhs locals nodes 
172
      in
173 36454535 ploc
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
174
    ) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
175 274c72ec ploc
  in
176
  { nd with
177
    node_locals = new_locals;
178 36454535 ploc
    node_eqs = eqs;
179
    node_asserts = asserts;
180 274c72ec ploc
  }
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 2842f7ca ploc
let witness filename main_name orig inlined type_env clock_env =
191 274c72ec ploc
  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 9f8c4c1d ploc
  (* 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 274c72ec ploc
  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 9f8c4c1d ploc
  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 274c72ec ploc
  let main_node = {
245
    node_id = "check";
246
    node_type = Types.new_var ();
247
    node_clock = Clocks.new_var true;
248
    node_inputs = main_orig_node.node_inputs;
249
    node_outputs = [ok_output];
250
    node_locals = [];
251
    node_gencalls = [];
252
    node_checks = [];
253
    node_asserts = [];
254
    node_eqs = [
255
      { eq_loc = loc;
256 9f8c4c1d ploc
	eq_lhs = List.map (fun v -> v.var_id) ok_i;
257 274c72ec ploc
	eq_rhs = 
258
	  let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
259
	  let call_orig = 
260
	    mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
261
	  let call_inlined = 
262
	    mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
263
	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
264
	  mkexpr loc (Expr_appl ("=", args, None))
265 9f8c4c1d ploc
      };
266
      { eq_loc = loc;
267
	eq_lhs = [ok_ident];
268
	eq_rhs = main_ok_expr;
269
      }
270
    ];
271 316af809 ploc
    node_dec_stateless = false;
272 d3e4c22f xthirioux
    node_stateless = None;
273 274c72ec ploc
    node_spec = Some 
274
      {requires = []; 
275 0038002e ploc
       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
276
       behaviors = [];
277
       spec_loc = loc
278 274c72ec ploc
      };
279 0038002e ploc
    node_annot = [];
280 274c72ec ploc
  }
281
  in
282
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in
283
  let new_prog = others@nodes_origs@nodes_inlined@main in
284
  let _ = Typing.type_prog type_env new_prog in
285
  let _ = Clock_calculus.clock_prog clock_env new_prog in
286
287 2842f7ca ploc
   
288
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
289 274c72ec ploc
  let witness_out = open_out witness_file in
290
  let witness_fmt = Format.formatter_of_out_channel witness_out in
291
  Format.fprintf witness_fmt
292
    "(* Generated lustre file to check validity of inlining process *)@.";
293
  Printers.pp_prog witness_fmt new_prog;
294
  Format.fprintf witness_fmt "@.";
295
  () (* xx *)
296
297 2842f7ca ploc
let global_inline basename prog type_env clock_env =
298 274c72ec ploc
  (* We select the main node desc *)
299
  let main_node, other_nodes, other_tops = 
300
    List.fold_left 
301
      (fun (main_opt, nodes, others) top -> 
302
	match top.top_decl_desc with 
303
	| Node nd when nd.node_id = !Options.main_node -> 
304
	  Some top, nodes, others
305
	| Node _ -> main_opt, top::nodes, others
306
	| _ -> main_opt, nodes, top::others) 
307
      (None, [], []) prog 
308
  in
309
  (* Recursively each call of a node in the top node is replaced *)
310
  let main_node = Utils.desome main_node in
311
  let main_node' = inline_all_calls main_node other_nodes in
312
  let res = main_node'::other_tops in
313 2842f7ca ploc
  if !Options.witnesses then (
314
    witness 
315
      basename
316
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
317
      prog res type_env clock_env
318
  );
319 274c72ec ploc
  res
320 9f8c4c1d ploc
321
(* Local Variables: *)
322
(* compile-command:"make -C .." *)
323
(* End: *)