Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / inliner.ml @ d3e4c22f

History | View | Annotate | Download (8.74 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
(* 
11
    expr, locals', eqs = inline_call id args' reset locals nodes
12

    
13
We select the called node equations and variables.
14
   renamed_inputs = args
15
   renamed_eqs
16

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

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

    
46
  (* Bug included: todo deal with reset *)
47
  assert (reset = None);
48

    
49
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
50
  let expr = expr_of_expr_list 
51
    loc 
52
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
53
  in
54
  expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs'
55

    
56

    
57

    
58

    
59
(* 
60
   new_expr, new_locals, new_eqs = inline_expr expr locals nodes
61
   
62
   Each occurence of a node in nodes in the expr should be replaced by fresh
63
   variables and the code of called node instance added to new_eqs
64

    
65
*)
66
let rec inline_expr expr locals nodes =
67
  let inline_tuple el = 
68
    List.fold_right (fun e (el_tail, locals, eqs) -> 
69
      let e', locals', eqs' = inline_expr e locals nodes in
70
      e'::el_tail, locals', eqs'@eqs
71
    ) el ([], locals, [])
72
  in
73
  let inline_pair e1 e2 = 
74
    let el', l', eqs' = inline_tuple [e1;e2] in
75
    match el' with
76
    | [e1'; e2'] -> e1', e2', l', eqs'
77
    | _ -> assert false
78
  in
79
  let inline_triple e1 e2 e3 = 
80
    let el', l', eqs' = inline_tuple [e1;e2;e3] in
81
    match el' with
82
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs'
83
    | _ -> assert false
84
  in
85
    
86
  match expr.expr_desc with
87
  | Expr_appl (id, args, reset) ->
88
    let args', locals', eqs' = inline_expr args locals nodes in 
89
    if List.exists (check_node_name id) nodes then 
90
      (* The node should be inlined *)
91
(*      let _ =     Format.eprintf "Inlining call to %s@." id in
92
  *)    let node = try List.find (check_node_name id) nodes 
93
	with Not_found -> (assert false) in
94
      let node = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
95
      let node = inline_node node nodes in
96
      let expr, locals', eqs'' = 
97
	inline_call expr args' reset locals' node in
98
      expr, locals', eqs'@eqs''
99
    else 
100
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
101
      { expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs'
102

    
103
  (* For other cases, we just keep the structure, but convert sub-expressions *)
104
  | Expr_const _ 
105
  | Expr_ident _ -> expr, locals, []
106
  | Expr_tuple el -> 
107
    let el', l', eqs' = inline_tuple el in
108
    { expr with expr_desc = Expr_tuple el' }, l', eqs'
109
  | Expr_ite (g, t, e) ->
110
    let g', t', e', l', eqs' = inline_triple g t e in
111
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs'
112
  | Expr_arrow (e1, e2) ->
113
    let e1', e2', l', eqs' = inline_pair e1 e2 in
114
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs'
115
  | Expr_fby (e1, e2) ->
116
    let e1', e2', l', eqs' = inline_pair e1 e2 in
117
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs'
118
  | Expr_array el ->
119
    let el', l', eqs' = inline_tuple el in
120
    { expr with expr_desc = Expr_array el' }, l', eqs'
121
  | Expr_access (e, dim) ->
122
    let e', l', eqs' = inline_expr e locals nodes in 
123
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs'
124
  | Expr_power (e, dim) ->
125
    let e', l', eqs' = inline_expr e locals nodes in 
126
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs'
127
  | Expr_pre e ->
128
    let e', l', eqs' = inline_expr e locals nodes in 
129
    { expr with expr_desc = Expr_pre e' }, l', eqs'
130
  | Expr_when (e, id, label) ->
131
    let e', l', eqs' = inline_expr e locals nodes in 
132
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs'
133
  | Expr_merge (id, branches) ->
134
    let el, l', eqs' = inline_tuple (List.map snd branches) in
135
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
136
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs'
137
  | Expr_uclock _
138
  | Expr_dclock _
139
  | Expr_phclock _ -> assert false 
140
and inline_node nd nodes = 
141
  let new_locals, eqs = 
142
    List.fold_left (fun (locals, eqs) eq ->
143
      let eq_rhs', locals', new_eqs' = 
144
	inline_expr eq.eq_rhs locals nodes 
145
      in
146
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs 
147
    ) (nd.node_locals, []) nd.node_eqs
148
  in
149
  { nd with
150
    node_locals = new_locals;
151
    node_eqs = eqs
152
  }
153

    
154
let inline_all_calls node nodes =
155
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
156
  { node with top_decl_desc = Node (inline_node nd nodes) }
157
    
158

    
159

    
160

    
161

    
162
let witness filename main_name orig inlined type_env clock_env =
163
  let loc = Location.dummy_loc in
164
  let rename_local_node nodes prefix id =
165
    if List.exists (check_node_name id) nodes then
166
      prefix ^ id 
167
    else
168
      id
169
  in
170
  let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
171
  Node nd -> nd | _ -> assert false in
172
  
173
  let orig_rename = rename_local_node orig "orig_" in
174
  let inlined_rename = rename_local_node inlined "inlined_" in
175
  let identity = (fun x -> x) in
176
  let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
177
  let orig = rename_prog orig_rename identity identity orig in
178
  let inlined = rename_prog inlined_rename identity identity inlined in
179
  let nodes_origs, others = List.partition is_node orig in
180
  let nodes_inlined, _ = List.partition is_node inlined in
181

    
182
  let ok_ident = "OK" in
183
  let ok_output = mkvar_decl 
184
    loc 
185
    (ok_ident,
186
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
187
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
188
     false)
189
  in
190
  let main_node = {
191
    node_id = "check";
192
    node_type = Types.new_var ();
193
    node_clock = Clocks.new_var true;
194
    node_inputs = main_orig_node.node_inputs;
195
    node_outputs = [ok_output];
196
    node_locals = [];
197
    node_gencalls = [];
198
    node_checks = [];
199
    node_asserts = [];
200
    node_eqs = [
201
      { eq_loc = loc;
202
	eq_lhs = [ok_ident];
203
	eq_rhs = 
204
	  let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
205
	  let call_orig = 
206
	    mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
207
	  let call_inlined = 
208
	    mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
209
	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
210
	  mkexpr loc (Expr_appl ("=", args, None))
211
      }];
212
    node_dec_stateless = true;
213
    node_stateless = None;
214
    node_spec = Some 
215
      {requires = []; 
216
       ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];
217
       behaviors = []
218
      };
219
    node_annot = None;
220
  }
221
  in
222
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in
223
  let new_prog = others@nodes_origs@nodes_inlined@main in
224
  let _ = Typing.type_prog type_env new_prog in
225
  let _ = Clock_calculus.clock_prog clock_env new_prog in
226

    
227
   
228
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
229
  let witness_out = open_out witness_file in
230
  let witness_fmt = Format.formatter_of_out_channel witness_out in
231
  Format.fprintf witness_fmt
232
    "(* Generated lustre file to check validity of inlining process *)@.";
233
  Printers.pp_prog witness_fmt new_prog;
234
  Format.fprintf witness_fmt "@.";
235
  () (* xx *)
236

    
237
let global_inline basename prog type_env clock_env =
238
  (* We select the main node desc *)
239
  let main_node, other_nodes, other_tops = 
240
    List.fold_left 
241
      (fun (main_opt, nodes, others) top -> 
242
	match top.top_decl_desc with 
243
	| Node nd when nd.node_id = !Options.main_node -> 
244
	  Some top, nodes, others
245
	| Node _ -> main_opt, top::nodes, others
246
	| _ -> main_opt, nodes, top::others) 
247
      (None, [], []) prog 
248
  in
249
  (* Recursively each call of a node in the top node is replaced *)
250
  let main_node = Utils.desome main_node in
251
  let main_node' = inline_all_calls main_node other_nodes in
252
  let res = main_node'::other_tops in
253
  if !Options.witnesses then (
254
    witness 
255
      basename
256
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
257
      prog res type_env clock_env
258
  );
259
  res