Project

General

Profile

Download (17.8 KB) Statistics
| Branch: | Tag: | Revision:
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 Utils
13
open LustreSpec
14
open Corelang
15
open Format
16
open Normalization_common
17

    
18
(* Create a (normalized) expression from [ref_e],
19
   replacing description with [norm_d],
20
   taking propagated [offsets] into account
21
   in order to change expression type *)
22
let mk_norm_expr offsets ref_e norm_d =
23
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
24
  let drop_array_type ty =
25
    Types.map_tuple_type Types.array_element_type ty in
26
  { ref_e with
27
    expr_desc = norm_d;
28
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
29
														
30
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
31
let rec normalize_list alias node offsets norm_element defvars elist =
32
  List.fold_right
33
    (fun t (defvars, qlist) ->
34
      let defvars, norm_t = norm_element alias node offsets defvars t in
35
      (defvars, norm_t :: qlist)
36
    ) elist (defvars, [])
37

    
38
let rec normalize_expr ?(alias=true) node offsets defvars expr =
39
  (*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
40
  match expr.expr_desc with
41
  | Expr_const _
42
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
43
  | Expr_array elist ->
44
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
45
    let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
46
    mk_expr_alias_opt alias node defvars norm_expr
47
  | Expr_power (e1, d) when offsets = [] ->
48
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
49
    let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
50
    mk_expr_alias_opt alias node defvars norm_expr
51
  | Expr_power (e1, d) ->
52
    normalize_expr ~alias:alias node (List.tl offsets) defvars e1
53
  | Expr_access (e1, d) ->
54
    normalize_expr ~alias:alias node (d::offsets) defvars e1
55
  | Expr_tuple elist ->
56
    let defvars, norm_elist =
57
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
58
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
59
  | Expr_appl (id, args, None)
60
      when Basic_library.is_homomorphic_fun id 
61
	&& Types.is_array_type expr.expr_type ->
62
    let defvars, norm_args =
63
      normalize_list
64
	alias
65
	node
66
	offsets
67
	(fun _ -> normalize_array_expr ~alias:true)
68
	defvars
69
	(expr_list_of_expr args)
70
    in
71
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
72
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
73
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
74
    defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
75
  | Expr_appl (id, args, r) ->
76
    let defvars, norm_args = normalize_expr node [] defvars args in
77
    let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
78
    if offsets <> []
79
    then
80
      let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
81
      normalize_expr ~alias:alias node offsets defvars norm_expr
82
    else
83
      mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr
84
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
85
    (* Here we differ from Colaco paper: arrows are pushed to the top *)
86
    normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
87
  | Expr_arrow (e1,e2) ->
88
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
89
    let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
90
    let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
91
    mk_expr_alias_opt alias node defvars norm_expr
92
  | Expr_pre e ->
93
    let defvars, norm_e = normalize_expr node offsets defvars e in
94
    let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
95
    mk_expr_alias_opt alias node defvars norm_expr
96
  | Expr_fby (e1, e2) ->
97
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
98
    let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
99
    let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
100
    mk_expr_alias_opt alias node defvars norm_expr
101
  | Expr_when (e, c, l) ->
102
    let defvars, norm_e = normalize_expr node offsets defvars e in
103
    defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
104
  | Expr_ite (c, t, e) ->
105
    let defvars, norm_c = normalize_guard node defvars c in
106
    let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
107
    let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
108
    let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
109
    mk_expr_alias_opt alias node defvars norm_expr
110
  | Expr_merge (c, hl) ->
111
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
112
    let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
113
    mk_expr_alias_opt alias node defvars norm_expr
114

    
115
(* Creates a conditional with a merge construct, which is more lazy *)
116
(*
117
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
118
 match expr.expr_desc with
119
 | Expr_ite (c, t, e) ->
120
   let defvars, norm_t = norm_expr (alias node offsets defvars t in
121
 | _ -> assert false
122
*)
123
and normalize_branches node offsets defvars hl =
124
 List.fold_right
125
   (fun (t, h) (defvars, norm_q) ->
126
     let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
127
     defvars, (t, norm_h) :: norm_q
128
   )
129
   hl (defvars, [])
130

    
131
and normalize_array_expr ?(alias=true) node offsets defvars expr =
132
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
133
  match expr.expr_desc with
134
  | Expr_power (e1, d) when offsets = [] ->
135
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
136
    defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
137
  | Expr_power (e1, d) ->
138
    normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
139
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
140
  | Expr_array elist when offsets = [] ->
141
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
142
    defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
143
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
144
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
145
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
146
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
147

    
148
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
149
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
150
  match expr.expr_desc with
151
  | Expr_access (e1, d) ->
152
    normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
153
  | Expr_ite (c, t, e) ->
154
    let defvars, norm_c = normalize_guard node defvars c in
155
    let defvars, norm_t = normalize_cond_expr node offsets defvars t in
156
    let defvars, norm_e = normalize_cond_expr node offsets defvars e in
157
    defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
158
  | Expr_merge (c, hl) ->
159
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
160
    defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
161
  | _ -> normalize_expr ~alias:alias node offsets defvars expr
162

    
163
and normalize_guard node defvars expr =
164
  let defvars, norm_expr = normalize_expr node [] defvars expr in
165
  mk_expr_alias_opt true node defvars norm_expr
166

    
167
(* outputs cannot be memories as well. If so, introduce new local variable.
168
*)
169
let decouple_outputs node defvars eq =
170
  let rec fold_lhs defvars lhs tys cks =
171
   match lhs, tys, cks with
172
   | [], [], []          -> defvars, []
173
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
174
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
175
			    then
176
			      let newvar = mk_fresh_var node eq.eq_loc t c in
177
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
178
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
179
			    else
180
			      (defs_q, vars_q), v::lhs_q
181
   | _                   -> assert false in
182
  let defvars', lhs' =
183
    fold_lhs
184
      defvars
185
      eq.eq_lhs
186
      (Types.type_list_of_type eq.eq_rhs.expr_type)
187
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
188
  defvars', {eq with eq_lhs = lhs' }
189

    
190
let rec normalize_eq node defvars eq =
191
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
192
  match eq.eq_rhs.expr_desc with
193
  | Expr_pre _
194
  | Expr_fby _  ->
195
    let (defvars', eq') = decouple_outputs node defvars eq in
196
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
197
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
198
    (norm_eq::defs', vars')
199
  | Expr_array _ ->
200
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
201
    let norm_eq = { eq with eq_rhs = norm_rhs } in
202
    (norm_eq::defs', vars')
203
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
204
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
205
    let norm_eq = { eq with eq_rhs = norm_rhs } in
206
    (norm_eq::defs', vars')
207
  | Expr_appl _ ->
208
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
209
    let norm_eq = { eq with eq_rhs = norm_rhs } in
210
    (norm_eq::defs', vars')
211
  | _ ->
212
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
213
    let norm_eq = { eq with eq_rhs = norm_rhs } in
214
    norm_eq::defs', vars'
215

    
216
let normalize_eq_split node defvars eq =
217
  
218
  let defs, vars = normalize_eq node defvars eq in
219
  List.fold_right (fun eq (def, vars) -> 
220
    let eq_defs = Splitting.tuple_split_eq eq in
221
    if eq_defs = [eq] then
222
      eq::def, vars 
223
    else
224
      List.fold_left (normalize_eq node) (def, vars) eq_defs
225
  ) defs ([], vars)  
226

    
227
let normalize_eexpr decls node vars ee =
228
  (* New output variable *)
229
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
230
  let output_var = 
231
    mkvar_decl 
232
      ee.eexpr_loc 
233
      (output_id, 
234
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
235
       mkclock ee.eexpr_loc Ckdec_any, 
236
       false (* not a constant *),
237
       None) 
238
  in
239
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
240
  (* Calls are first inlined *)
241
  (* let nodes = get_registered_nodes () in *)
242
  Format.eprintf "Reg nodes #####@.";
243
  List.iter (fun nd -> Format.eprintf "node %s@." (node_name nd)) decls;
244
  Format.eprintf "Reg nodes #####@.";
245
  let calls = ISet.elements (get_expr_calls decls ee.eexpr_qfexpr) in
246
  let calls = List.map 
247
    (fun called_nd -> try
248
			(List.find (fun nd -> node_name nd = called_nd) decls)
249
			  		  with _ -> Format.eprintf "looking for node %s@." called_nd; assert false
250
    ) calls
251

    
252
  in
253
  (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls;  *)
254
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
255
  let (new_locals, eqs) =
256
    if calls = [] && not (expr_has_arrows ee.eexpr_qfexpr) then
257
      let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
258
      (locals, [eq])
259
    else (
260
      Format.eprintf "Ici@.";
261
      let e, new_locals, eqs, _ (* asserts *), _ (* annots *) =
262
	Inliner.inline_expr ee.eexpr_qfexpr locals node calls
263
      in
264
      let eq = mkeq ee.eexpr_loc ([output_id], e) in
265
      (*Format.eprintf "eqs %a@.@?" 
266
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
267
      (new_locals, eq::eqs)
268
    ) in
269
  (* Normalizing expr and eqs *)
270
  let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
271
  let todefine = List.fold_left
272
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
273
    (ISet.add output_id ISet.empty) vars in
274
  try
275
    let env = Typing.type_var_decl_list quant_vars Basic_library.type_env quant_vars in
276
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
277
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
278
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
279
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
280
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
281
  (* check that table is empty *)
282
    if (not (ISet.is_empty undefined_vars)) then
283
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
284
    
285
    (*Format.eprintf "normalized eqs %a@.@?" 
286
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
287
    ee.eexpr_normalized <- Some (output_var, defs, vars)
288
  with (Types.Error (loc,err)) as exc ->
289
    eprintf "Typing error for eexpr %a: %a%a%a@."
290
      Printers.pp_eexpr ee
291
      Types.pp_error err
292
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
293
      Location.pp_loc loc
294
      
295
;
296
    raise exc
297

    
298
let normalize_spec decls node vars s =
299
  let nee = normalize_eexpr decls node vars in
300
  List.iter nee s.requires;
301
  List.iter nee s.ensures;
302
  List.iter (fun (_, assumes, ensures, _) -> 
303
      List.iter nee assumes;
304
    List.iter nee ensures
305
  ) s.behaviors
306
  
307
    
308
(* The normalization phase introduces new local variables
309
   - output cannot be memories. If this happen, new local variables acting as
310
   memories are introduced. 
311
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
312
   access
313
   Thoses values are shared, ie. no duplicate expressions are introduced.
314

    
315
   Concerning specification, a similar process is applied, replacing an
316
   expression by a list of local variables and definitions
317
*)
318

    
319
(** normalize_node prog node returns a normalized node, 
320
    ie. 
321
    - updated locals
322
    - new equations
323
    -
324
*)
325
let normalize_node decls node = 
326
  cpt_fresh := 0;
327
  let inputs_outputs = node.node_inputs@node.node_outputs in
328
  let is_local v =
329
    List.for_all ((!=) v) inputs_outputs in
330
  let orig_vars = inputs_outputs@node.node_locals in
331
  let defs, vars =
332
    List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
333
  (* Normalize the asserts *)
334
  let vars, assert_defs, asserts =
335
    List.fold_left (
336
    fun (vars, def_accu, assert_accu) assert_ ->
337
      let assert_expr = assert_.assert_expr in
338
      let (defs, vars'), expr = 
339
	normalize_expr 
340
	  ~alias:false 
341
	  node 
342
	  [] (* empty offset for arrays *)
343
	  ([], vars) (* defvar only contains vars *)
344
	  assert_expr
345
      in
346
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
347
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
348
    ) (vars, [], []) node.node_asserts in
349
  let new_locals = List.filter is_local vars in
350
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
351

    
352
  let new_annots =
353
    if !Options.traces then
354
      begin
355
	(* Compute traceability info:
356
	   - gather newly bound variables
357
	   - compute the associated expression without aliases
358
	*)
359
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
360
	let norm_traceability = {
361
	  annots = List.map (fun v ->
362
	    let eq =
363
	      try
364
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
365
	      with Not_found -> 
366
		(
367
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
368
		  assert false
369
		) 
370
	    in
371
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
372
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
373
	    (["traceability"], pair)
374
	  ) diff_vars;
375
	  annot_loc = Location.dummy_loc
376
	}
377
	in
378
	norm_traceability::node.node_annot
379
      end
380
    else
381
      node.node_annot
382
  in
383
  if !Options.spec <> "no" then 
384
    begin
385
      (* Update mutable fields of eexpr to perform normalization of specification/annotations *)
386
      List.iter 
387
	(fun a -> 
388
	  List.iter 
389
	    (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann) 
390
	    a.annots
391
	)
392
	node.node_annot;
393
	match node.node_spec with None -> () | Some s -> normalize_spec decls node [] s 
394
    end;
395
  
396
 
397
 let new_locals = List.filter is_local vars in
398
  let node =
399
  { node with
400
    node_locals = new_locals;
401
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
402
    node_asserts = asserts;
403
    node_annot = new_annots;
404
  }
405
  in ((*Printers.pp_node Format.err_formatter node;*)
406
    node
407
)
408

    
409
let normalize_decl decls decl =
410
  match decl.top_decl_desc with
411
  | Node nd ->
412
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
413
    Hashtbl.replace Corelang.node_table nd.node_id decl';
414
    decl'
415
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
416

    
417
let normalize_prog decls =
418
  List.map (normalize_decl decls) decls
419

    
420
(* Local Variables: *)
421
(* compile-command:"make -C .." *)
422
(* End: *)
(39-39/62)