Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / inliner.ml @ 36454535

History | View | Annotate | Download (10.3 KB)

1
open LustreSpec
2
open Corelang
3

    
4
let check_node_name id = (fun t -> 
5
  match t.top_decl_desc with 
6
  | Node nd -> nd.node_id = id 
7
  | _ -> false) 
8

    
9

    
10
let rename_expr rename expr = expr_replace_var rename expr
11
let rename_eq rename eq = 
12
  { eq with
13
    eq_lhs = List.map rename eq.eq_lhs; 
14
    eq_rhs = rename_expr rename eq.eq_rhs
15
  }
16

    
17
(* 
18
    expr, locals', eqs = inline_call id args' reset locals nodes
19

    
20
We select the called node equations and variables.
21
   renamed_inputs = args
22
   renamed_eqs
23

    
24
the resulting expression is tuple_of_renamed_outputs
25
   
26
TODO: convert the specification/annotation/assert and inject them
27
TODO: deal with reset
28
*)
29
let inline_call orig_expr args reset locals node =
30
  let loc = orig_expr.expr_loc in
31
  let uid = orig_expr.expr_tag in
32
  let rename v = 
33
    Format.fprintf Format.str_formatter "%s_%i_%s" 
34
      node.node_id uid v;
35
    Format.flush_str_formatter ()
36
  in
37
  let eqs' = List.map (rename_eq rename) node.node_eqs
38
  in
39
  let rename_var v = { v with var_id = rename v.var_id } in
40
  let inputs' = List.map rename_var node.node_inputs in
41
  let outputs' = List.map rename_var node.node_outputs in
42
  let locals' = List.map rename_var node.node_locals in
43

    
44
  (* checking we are at the appropriate (early) step: node_checks and
45
     node_gencalls should be empty (not yet assigned) *)
46
  assert (node.node_checks = []);
47
  assert (node.node_gencalls = []);
48

    
49
  (* Bug included: todo deal with reset *)
50
  assert (reset = None);
51

    
52
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
53
  let expr = expr_of_expr_list 
54
    loc 
55
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
56
  in
57
  let asserts' = (* We rename variables in assert expressions *)
58
    List.map 
59
      (fun a -> 
60
	{a with assert_expr = 
61
	    let expr = a.assert_expr in
62
	    rename_expr rename expr
63
      })
64
      node.node_asserts 
65
  in
66
  expr, 
67
  inputs'@outputs'@locals'@locals, 
68
  assign_inputs::eqs',
69
  asserts'
70

    
71

    
72

    
73

    
74
(* 
75
   new_expr, new_locals, new_eqs = inline_expr expr locals nodes
76
   
77
   Each occurence of a node in nodes in the expr should be replaced by fresh
78
   variables and the code of called node instance added to new_eqs
79

    
80
*)
81
let rec inline_expr expr locals nodes =
82
  let inline_tuple el = 
83
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
84
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
85
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
86
    ) el ([], locals, [], [])
87
  in
88
  let inline_pair e1 e2 = 
89
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
90
    match el' with
91
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
92
    | _ -> assert false
93
  in
94
  let inline_triple e1 e2 e3 = 
95
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
96
    match el' with
97
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
98
    | _ -> assert false
99
  in
100
    
101
  match expr.expr_desc with
102
  | Expr_appl (id, args, reset) ->
103
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
104
    if List.exists (check_node_name id) nodes then 
105
      (* The node should be inlined *)
106
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
107
      let node = try List.find (check_node_name id) nodes 
108
	with Not_found -> (assert false) in
109
      let node = 
110
	match node.top_decl_desc with Node nd -> nd | _ -> assert false in
111
      let node = inline_node node nodes in
112
      let expr, locals', eqs'', asserts'' = 
113
	inline_call expr args' reset locals' node in
114
      expr, locals', eqs'@eqs'', asserts'@asserts''
115
    else 
116
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
117
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
118
      locals', 
119
      eqs', 
120
      asserts'
121

    
122
  (* For other cases, we just keep the structure, but convert sub-expressions *)
123
  | Expr_const _ 
124
  | Expr_ident _ -> expr, locals, [], []
125
  | Expr_tuple el -> 
126
    let el', l', eqs', asserts' = inline_tuple el in
127
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
128
  | Expr_ite (g, t, e) ->
129
    let g', t', e', l', eqs', asserts' = inline_triple g t e in
130
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
131
  | Expr_arrow (e1, e2) ->
132
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
133
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
134
  | Expr_fby (e1, e2) ->
135
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
136
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
137
  | Expr_array el ->
138
    let el', l', eqs', asserts' = inline_tuple el in
139
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
140
  | Expr_access (e, dim) ->
141
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
142
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
143
  | Expr_power (e, dim) ->
144
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
145
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
146
  | Expr_pre e ->
147
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
148
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
149
  | Expr_when (e, id, label) ->
150
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
151
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
152
  | Expr_merge (id, branches) ->
153
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
154
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
155
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
156
and inline_node nd nodes = 
157
  let new_locals, eqs, asserts = 
158
    List.fold_left (fun (locals, eqs, asserts) eq ->
159
      let eq_rhs', locals', new_eqs', asserts' = 
160
	inline_expr eq.eq_rhs locals nodes 
161
      in
162
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
163
    ) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
164
  in
165
  { nd with
166
    node_locals = new_locals;
167
    node_eqs = eqs;
168
    node_asserts = asserts;
169
  }
170

    
171
let inline_all_calls node nodes =
172
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
173
  { node with top_decl_desc = Node (inline_node nd nodes) }
174
    
175

    
176

    
177

    
178

    
179
let witness filename main_name orig inlined type_env clock_env =
180
  let loc = Location.dummy_loc in
181
  let rename_local_node nodes prefix id =
182
    if List.exists (check_node_name id) nodes then
183
      prefix ^ id 
184
    else
185
      id
186
  in
187
  let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
188
  Node nd -> nd | _ -> assert false in
189
  
190
  let orig_rename = rename_local_node orig "orig_" in
191
  let inlined_rename = rename_local_node inlined "inlined_" in
192
  let identity = (fun x -> x) in
193
  let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
194
  let orig = rename_prog orig_rename identity identity orig in
195
  let inlined = rename_prog inlined_rename identity identity inlined in
196
  let nodes_origs, others = List.partition is_node orig in
197
  let nodes_inlined, _ = List.partition is_node inlined in
198

    
199
  (* One ok_i boolean variable  per output var *)
200
  let nb_outputs = List.length main_orig_node.node_outputs in
201
  let ok_i = List.map (fun id ->
202
    mkvar_decl 
203
      loc 
204
      ("OK" ^ string_of_int id,
205
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
206
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
207
       false)
208
  ) (Utils.enumerate nb_outputs) 
209
  in
210

    
211
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
212
  let ok_ident = "OK" in
213
  let ok_output = mkvar_decl 
214
    loc 
215
    (ok_ident,
216
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
217
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
218
     false)
219
  in
220
  let main_ok_expr =
221
    let mkv x = mkexpr loc (Expr_ident x) in
222
    match ok_i with
223
    | [] -> assert false
224
    | [x] -> mkv x.var_id 
225
    | hd::tl -> 
226
      List.fold_left (fun accu elem -> 
227
	mkpredef_call loc "&&" [mkv elem.var_id; accu]
228
      ) (mkv hd.var_id) tl
229
  in
230

    
231
  (* Building main node *)
232

    
233
  let main_node = {
234
    node_id = "check";
235
    node_type = Types.new_var ();
236
    node_clock = Clocks.new_var true;
237
    node_inputs = main_orig_node.node_inputs;
238
    node_outputs = [ok_output];
239
    node_locals = [];
240
    node_gencalls = [];
241
    node_checks = [];
242
    node_asserts = [];
243
    node_eqs = [
244
      { eq_loc = loc;
245
	eq_lhs = List.map (fun v -> v.var_id) ok_i;
246
	eq_rhs = 
247
	  let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
248
	  let call_orig = 
249
	    mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
250
	  let call_inlined = 
251
	    mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
252
	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
253
	  mkexpr loc (Expr_appl ("=", args, None))
254
      };
255
      { eq_loc = loc;
256
	eq_lhs = [ok_ident];
257
	eq_rhs = main_ok_expr;
258
      }
259
    ];
260
    node_dec_stateless = false;
261
    node_stateless = None;
262
    node_spec = Some 
263
      {requires = []; 
264
       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
265
       behaviors = [];
266
       spec_loc = loc
267
      };
268
    node_annot = [];
269
  }
270
  in
271
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in
272
  let new_prog = others@nodes_origs@nodes_inlined@main in
273
  let _ = Typing.type_prog type_env new_prog in
274
  let _ = Clock_calculus.clock_prog clock_env new_prog in
275

    
276
   
277
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
278
  let witness_out = open_out witness_file in
279
  let witness_fmt = Format.formatter_of_out_channel witness_out in
280
  Format.fprintf witness_fmt
281
    "(* Generated lustre file to check validity of inlining process *)@.";
282
  Printers.pp_prog witness_fmt new_prog;
283
  Format.fprintf witness_fmt "@.";
284
  () (* xx *)
285

    
286
let global_inline basename prog type_env clock_env =
287
  (* We select the main node desc *)
288
  let main_node, other_nodes, other_tops = 
289
    List.fold_left 
290
      (fun (main_opt, nodes, others) top -> 
291
	match top.top_decl_desc with 
292
	| Node nd when nd.node_id = !Options.main_node -> 
293
	  Some top, nodes, others
294
	| Node _ -> main_opt, top::nodes, others
295
	| _ -> main_opt, nodes, top::others) 
296
      (None, [], []) prog 
297
  in
298
  (* Recursively each call of a node in the top node is replaced *)
299
  let main_node = Utils.desome main_node in
300
  let main_node' = inline_all_calls main_node other_nodes in
301
  let res = main_node'::other_tops in
302
  if !Options.witnesses then (
303
    witness 
304
      basename
305
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
306
      prog res type_env clock_env
307
  );
308
  res
309

    
310
(* Local Variables: *)
311
(* compile-command:"make -C .." *)
312
(* End: *)