Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 949b2e1e

History | View | Annotate | Download (25.4 KB)

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 Lustre_types
14
open Corelang
15
open Format
16

    
17
(** Normalisation iters through the AST of expressions and bind fresh definition
18
    when some criteria are met. This creation of fresh definition is performed by
19
    the function mk_expr_alias_opt when the alias argument is on.
20

    
21
    Initial expressions, ie expressions attached a variable in an equation
22
    definition are not aliased. This non-alias feature is propagated in the
23
    expression AST for array access and power construct, tuple, and some special
24
    cases of arrows.
25

    
26
    Two global variables may impact the normalization process:
27
    - unfold_arrow_active
28
    - force_alias_ite: when set, bind a fresh alias for then and else
29
      definitions.
30
*)
31

    
32
(* Two global variables *)
33
let unfold_arrow_active = ref true
34
let force_alias_ite = ref false
35
let force_alias_internal_fun = ref false
36

    
37
  
38
let expr_true loc ck =
39
{ expr_tag = Utils.new_tag ();
40
  expr_desc = Expr_const (Const_tag tag_true);
41
  expr_type = Type_predef.type_bool;
42
  expr_clock = ck;
43
  expr_delay = Delay.new_var ();
44
  expr_annot = None;
45
  expr_loc = loc }
46

    
47
let expr_false loc ck =
48
{ expr_tag = Utils.new_tag ();
49
  expr_desc = Expr_const (Const_tag tag_false);
50
  expr_type = Type_predef.type_bool;
51
  expr_clock = ck;
52
  expr_delay = Delay.new_var ();
53
  expr_annot = None;
54
  expr_loc = loc }
55

    
56
let expr_once loc ck =
57
 { expr_tag = Utils.new_tag ();
58
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
59
  expr_type = Type_predef.type_bool;
60
  expr_clock = ck;
61
  expr_delay = Delay.new_var ();
62
  expr_annot = None;
63
  expr_loc = loc }
64

    
65
let is_expr_once =
66
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
67
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
68

    
69
let unfold_arrow expr =
70
 match expr.expr_desc with
71
 | Expr_arrow (e1, e2) ->
72
    let loc = expr.expr_loc in
73
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
74
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
75
 | _                   -> assert false
76

    
77

    
78

    
79
(* Get the equation in [defs] with [expr] as rhs, if any *)
80
let get_expr_alias defs expr =
81
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
82
 with
83
 | Not_found -> None
84
  
85
(* Replace [expr] with (tuple of) [locals] *)
86
let replace_expr locals expr =
87
 match locals with
88
 | []  -> assert false
89
 | [v] -> { expr with
90
   expr_tag = Utils.new_tag ();
91
   expr_desc = Expr_ident v.var_id }
92
 | _   -> { expr with
93
   expr_tag = Utils.new_tag ();
94
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
95

    
96
let unfold_offsets e offsets =
97
  let add_offset e d =
98
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
99
    let res = *)
100
    { e with
101
      expr_tag = Utils.new_tag ();
102
      expr_loc = d.Dimension.dim_loc;
103
      expr_type = Types.array_element_type e.expr_type;
104
      expr_desc = Expr_access (e, d) }
105
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
106
  in
107
 List.fold_left add_offset e offsets
108

    
109
(* Create an alias for [expr], if none exists yet *)
110
let mk_expr_alias node (defs, vars) expr =
111
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
112
  match get_expr_alias defs expr with
113
  | Some eq ->
114
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
115
    (defs, vars), replace_expr aliases expr
116
  | None    ->
117
    let new_aliases =
118
      List.map2
119
	(mk_fresh_var node expr.expr_loc)
120
	(Types.type_list_of_type expr.expr_type)
121
	(Clocks.clock_list_of_clock expr.expr_clock) in
122
    let new_def =
123
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
124
    in
125
    (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
126
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
127

    
128
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
129
   and [opt] is true *)
130
let mk_expr_alias_opt opt node (defs, vars) expr =
131
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132
  match expr.expr_desc with
133
  | Expr_ident alias ->
134
    (defs, vars), expr
135
  | _                ->
136
    match get_expr_alias defs expr with
137
    | Some eq ->
138
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
139
      (defs, vars), replace_expr aliases expr
140
    | None    ->
141
      if opt
142
      then
143
	let new_aliases =
144
	  List.map2
145
	    (mk_fresh_var node expr.expr_loc)
146
	    (Types.type_list_of_type expr.expr_type)
147
	    (Clocks.clock_list_of_clock expr.expr_clock) in
148
	let new_def =
149
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
150
	in
151
	(* Typing and Registering machine type *) 
152
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
153
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
154
      else
155
	(defs, vars), expr
156

    
157
(* Create a (normalized) expression from [ref_e],
158
   replacing description with [norm_d],
159
   taking propagated [offsets] into account
160
   in order to change expression type *)
161
let mk_norm_expr offsets ref_e norm_d =
162
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
163
  let drop_array_type ty =
164
    Types.map_tuple_type Types.array_element_type ty in
165
  { ref_e with
166
    expr_desc = norm_d;
167
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
168
														
169
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
170
let rec normalize_list alias node offsets norm_element defvars elist =
171
  List.fold_right
172
    (fun t (defvars, qlist) ->
173
      let defvars, norm_t = norm_element alias node offsets defvars t in
174
      (defvars, norm_t :: qlist)
175
    ) elist (defvars, [])
176

    
177
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =
178
  (*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;*)
179
  match expr.expr_desc with
180
  | Expr_const _
181
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
182
  | Expr_array elist ->
183
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
184
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
185
     mk_expr_alias_opt alias node defvars norm_expr
186
  | Expr_power (e1, d) when offsets = [] ->
187
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
188
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
189
     mk_expr_alias_opt alias node defvars norm_expr
190
  | Expr_power (e1, d) ->
191
     normalize_expr ~alias:alias node (List.tl offsets) defvars e1
192
  | Expr_access (e1, d) ->
193
     normalize_expr ~alias:alias node (d::offsets) defvars e1
194
  | Expr_tuple elist ->
195
     let defvars, norm_elist =
196
       normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
197
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
198
  | Expr_appl (id, args, None)
199
      when Basic_library.is_homomorphic_fun id 
200
	&& Types.is_array_type expr.expr_type ->
201
     let defvars, norm_args =
202
       normalize_list
203
	 alias
204
	 node
205
	 offsets
206
	 (fun _ -> normalize_array_expr ~alias:true)
207
	 defvars
208
	 (expr_list_of_expr args)
209
     in
210
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
211
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
212
      && not (!force_alias_internal_fun || alias_basic) ->
213
     let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
214
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
215
  | Expr_appl (id, args, r) ->
216
     let defvars, r =
217
       match r with
218
       | None -> defvars, None
219
       | Some r ->
220
	  let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in
221
	  defvars, Some norm_r
222
     in
223
     let defvars, norm_args = normalize_expr node [] defvars args in
224
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
225
     if offsets <> []
226
     then
227
       let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
228
       normalize_expr ~alias:alias node offsets defvars norm_expr
229
     else
230
       mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic
231
				    || not (Basic_library.is_expr_internal_fun expr)))
232
	 node defvars norm_expr
233
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
234
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
235
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
236
  | Expr_arrow (e1,e2) ->
237
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
238
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
239
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
240
     mk_expr_alias_opt alias node defvars norm_expr
241
  | Expr_pre e ->
242
     let defvars, norm_e = normalize_expr node offsets defvars e in
243
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
244
     mk_expr_alias_opt alias node defvars norm_expr
245
  | Expr_fby (e1, e2) ->
246
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
247
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
248
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
249
     mk_expr_alias_opt alias node defvars norm_expr
250
  | Expr_when (e, c, l) ->
251
     let defvars, norm_e = normalize_expr node offsets defvars e in
252
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
253
  | Expr_ite (c, t, e) ->
254
     let defvars, norm_c = normalize_guard node defvars c in
255
     let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
256
     let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
257
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
258
     mk_expr_alias_opt alias node defvars norm_expr
259
  | Expr_merge (c, hl) ->
260
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
261
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
262
     mk_expr_alias_opt alias node defvars norm_expr
263

    
264
(* Creates a conditional with a merge construct, which is more lazy *)
265
(*
266
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
267
  match expr.expr_desc with
268
  | Expr_ite (c, t, e) ->
269
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
270
  | _ -> assert false
271
*)
272
and normalize_branches node offsets defvars hl =
273
  List.fold_right
274
    (fun (t, h) (defvars, norm_q) ->
275
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
276
      defvars, (t, norm_h) :: norm_q
277
    )
278
    hl (defvars, [])
279

    
280
and normalize_array_expr ?(alias=true) node offsets defvars expr =
281
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
282
  match expr.expr_desc with
283
  | Expr_power (e1, d) when offsets = [] ->
284
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
285
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
286
  | Expr_power (e1, d) ->
287
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
288
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
289
  | Expr_array elist when offsets = [] ->
290
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
291
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
292
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
293
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
294
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
295
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
296

    
297
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
298
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
299
  match expr.expr_desc with
300
  | Expr_access (e1, d) ->
301
     normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
302
  | Expr_ite (c, t, e) ->
303
     let defvars, norm_c = normalize_guard node defvars c in
304
     let defvars, norm_t = normalize_cond_expr node offsets defvars t in
305
     let defvars, norm_e = normalize_cond_expr node offsets defvars e in
306
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
307
  | Expr_merge (c, hl) ->
308
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
309
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
310
  | _ when !force_alias_ite ->
311
     (* Forcing alias creation for then/else expressions *)
312
     let defvars, norm_expr =
313
       normalize_expr ~alias:alias node offsets defvars expr
314
     in
315
     mk_expr_alias_opt true node defvars norm_expr
316
  | _ -> (* default case without the force_alias_ite option *)
317
     normalize_expr ~alias:alias node offsets defvars expr
318
       
319
and normalize_guard node defvars expr =
320
  let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in
321
  mk_expr_alias_opt true node defvars norm_expr
322

    
323
(* outputs cannot be memories as well. If so, introduce new local variable.
324
*)
325
let decouple_outputs node defvars eq =
326
  let rec fold_lhs defvars lhs tys cks =
327
   match lhs, tys, cks with
328
   | [], [], []          -> defvars, []
329
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
330
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
331
			    then
332
			      let newvar = mk_fresh_var node eq.eq_loc t c in
333
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
334
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
335
			    else
336
			      (defs_q, vars_q), v::lhs_q
337
   | _                   -> assert false in
338
  let defvars', lhs' =
339
    fold_lhs
340
      defvars
341
      eq.eq_lhs
342
      (Types.type_list_of_type eq.eq_rhs.expr_type)
343
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
344
  defvars', {eq with eq_lhs = lhs' }
345

    
346
let rec normalize_eq node defvars eq =
347
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
348
  match eq.eq_rhs.expr_desc with
349
  | Expr_pre _
350
  | Expr_fby _  ->
351
    let (defvars', eq') = decouple_outputs node defvars eq in
352
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
353
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
354
    (norm_eq::defs', vars')
355
  | Expr_array _ ->
356
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
357
    let norm_eq = { eq with eq_rhs = norm_rhs } in
358
    (norm_eq::defs', vars')
359
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
360
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
361
    let norm_eq = { eq with eq_rhs = norm_rhs } in
362
    (norm_eq::defs', vars')
363
  | Expr_appl _ ->
364
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
365
    let norm_eq = { eq with eq_rhs = norm_rhs } in
366
    (norm_eq::defs', vars')
367
  | _ ->
368
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
369
    let norm_eq = { eq with eq_rhs = norm_rhs } in
370
    norm_eq::defs', vars'
371

    
372
let normalize_eq_split node defvars eq =
373
  
374
  let defs, vars = normalize_eq node defvars eq in
375
  List.fold_right (fun eq (def, vars) -> 
376
    let eq_defs = Splitting.tuple_split_eq eq in
377
    if eq_defs = [eq] then
378
      eq::def, vars 
379
    else
380
      List.fold_left (normalize_eq node) (def, vars) eq_defs
381
  ) defs ([], vars)  
382

    
383
let normalize_eexpr decls node vars ee =
384
  (* New output variable *)
385
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
386
  let output_var = 
387
    mkvar_decl 
388
      ee.eexpr_loc 
389
      (output_id, 
390
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
391
       mkclock ee.eexpr_loc Ckdec_any, 
392
       false (* not a constant *),
393
       None,
394
       None
395
      ) 
396
  in
397
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
398
  (* Calls are first inlined *)
399
  let nodes = get_nodes decls in
400
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
401
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
402
   let calls = List.map 
403
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
404
  in
405
*)
406
  (*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;  *)
407
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
408
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
409
  let (new_locals, eqs) =
410
    if calls = [] && not (eq_has_arrows eq) then
411
      (locals, [eq])     
412
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
413
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
414
      (*Format.eprintf "eqs %a@.@?" 
415
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
416
      (new_locals, eqs)
417
*)
418
           (locals, [eq])     
419
 
420
    ) in
421
  (* Normalizing expr and eqs *)
422
  let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
423
  let todefine = List.fold_left
424
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
425
    (ISet.add output_id ISet.empty) vars in
426
  try
427
    let env = Typing.type_var_decl_list quant_vars Basic_library.type_env quant_vars in
428
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
429
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
430
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
431
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
432
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
433
  (* check that table is empty *)
434
    if (not (ISet.is_empty undefined_vars)) then
435
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
436
    
437
    (*Format.eprintf "normalized eqs %a@.@?" 
438
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
439
    ee.eexpr_normalized <- Some (output_var, defs, vars)
440
  with (Types.Error (loc,err)) as exc ->
441
    eprintf "Typing error for eexpr %a: %a%a%a@."
442
      Printers.pp_eexpr ee
443
      Types.pp_error err
444
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
445
      Location.pp_loc loc
446
      
447
;
448
    raise exc
449

    
450
let normalize_spec decls node vars s =
451
  let nee = normalize_eexpr decls node vars in
452
  List.iter nee s.requires;
453
  List.iter nee s.ensures;
454
  List.iter (fun (_, assumes, ensures, _) -> 
455
      List.iter nee assumes;
456
    List.iter nee ensures
457
  ) s.behaviors
458
  
459
    
460
(* The normalization phase introduces new local variables
461
   - output cannot be memories. If this happen, new local variables acting as
462
   memories are introduced. 
463
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
464
   access
465
   Thoses values are shared, ie. no duplicate expressions are introduced.
466

    
467
   Concerning specification, a similar process is applied, replacing an
468
   expression by a list of local variables and definitions
469
*)
470

    
471
(** normalize_node node returns a normalized node, 
472
    ie. 
473
    - updated locals
474
    - new equations
475
    -
476
*)
477
let normalize_node decls node =
478
  reset_cpt_fresh ();
479
  let inputs_outputs = node.node_inputs@node.node_outputs in
480
  let is_local v =
481
    List.for_all ((<>) v) inputs_outputs in
482
  let orig_vars = inputs_outputs@node.node_locals in
483
  let not_is_orig_var v =
484
    List.for_all ((!=) v) orig_vars in
485
  let defs, vars =
486
    let eqs, auts = get_node_eqs node in
487
    if auts != [] then assert false; (* Automata should be expanded by now. *)
488
    List.fold_left (normalize_eq node) ([], orig_vars) eqs in
489
  (* Normalize the asserts *)
490
  let vars, assert_defs, asserts =
491
    List.fold_left (
492
      fun (vars, def_accu, assert_accu) assert_ ->
493
	let assert_expr = assert_.assert_expr in
494
	let (defs, vars'), expr = 
495
	  normalize_expr 
496
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
497
	    node 
498
	    [] (* empty offset for arrays *)
499
	    ([], vars) (* defvar only contains vars *)
500
	    assert_expr
501
	in
502
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
503
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
504
    ) (vars, [], []) node.node_asserts in
505
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
506
							  vars and initial locals ones *)
507
  
508
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
509
						       beginning of the list the
510
						       local declared ones *)
511
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
512

    
513

    
514
  (* Updating annotations: traceability and machine types for fresh variables *)
515
  
516
  (* Compute traceability info:
517
     - gather newly bound variables
518
     - compute the associated expression without aliases
519
  *)
520
  let new_annots =
521
    if !Options.traces then
522
      begin
523
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
524
	let norm_traceability = {
525
	  annots = List.map (fun v ->
526
	    let eq =
527
	      try
528
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
529
	      with Not_found -> 
530
		(
531
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
532
		  assert false
533
		) 
534
	    in
535
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
536
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
537
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
538
	    (["traceability"], pair)
539
	  ) diff_vars;
540
	  annot_loc = Location.dummy_loc
541
	}
542
	in
543
	norm_traceability::node.node_annot
544
      end
545
    else
546
      node.node_annot
547
  in
548

    
549
  let new_annots =
550
    List.fold_left (fun annots v ->
551
      if Machine_types.is_active && Machine_types.is_exportable v then
552
	let typ = Machine_types.get_specified_type v in
553
  	let typ_name = Machine_types.type_name typ in
554

    
555
	let loc = v.var_loc in
556
	let typ_as_string =
557
	  mkexpr
558
	    loc
559
	    (Expr_const
560
	       (Const_string typ_name))
561
	in
562
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
563
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
564
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
565
      else
566
	annots
567
    ) new_annots new_locals
568
  in
569
  if !Options.spec <> "no" then 
570
    begin
571
      (* Update mutable fields of eexpr to perform normalization of specification/annotations *)
572
      List.iter 
573
	(fun a -> 
574
	  List.iter 
575
	    (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann) 
576
	    a.annots
577
	)
578
	node.node_annot;
579
      match node.node_spec with None -> () | Some s -> normalize_spec decls node [] s 
580
    end;
581
  
582
 
583
 let new_locals = List.filter is_local vars in (* TODO a quoi ca sert ? *)
584
  let node =
585
    { node with
586
      node_locals = all_locals;
587
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
588
      node_asserts = asserts;
589
      node_annot = new_annots;
590
    }
591
  in ((*Printers.pp_node Format.err_formatter node;*)
592
    node
593
  )
594

    
595

    
596
let normalize_decl (decls: program) (decl: top_decl) : top_decl =
597
  match decl.top_decl_desc with
598
  | Node nd ->
599
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
600
    Hashtbl.replace Corelang.node_table nd.node_id decl';
601
    decl'
602
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
603

    
604
let normalize_prog ?(backend="C") decls : program =
605
  let old_unfold_arrow_active = !unfold_arrow_active in
606
  let old_force_alias_ite = !force_alias_ite in
607
  let old_force_alias_internal_fun = !force_alias_internal_fun in
608
  
609
  (* Backend specific configurations for normalization *)
610
  let _ =
611
    match backend with
612
    | "lustre" ->
613
    (* Special treatment of arrows in lustre backend. We want to keep them *)
614
       unfold_arrow_active := false;
615
    | "emf" -> (
616
       (* Forcing ite normalization *)
617
      force_alias_ite := true;
618
      force_alias_internal_fun := true;
619
    )
620
    | _ -> () (* No fancy options for other backends *)
621
  in
622

    
623
  (* Main algorithm: iterates over nodes *)
624
  let res = List.map (normalize_decl decls) decls in
625
  
626
  (* Restoring previous settings *)
627
  unfold_arrow_active := old_unfold_arrow_active;
628
  force_alias_ite := old_force_alias_ite;
629
  force_alias_internal_fun := old_force_alias_internal_fun;
630
  res
631
  
632
  (* Local Variables: *)
633
(* compile-command:"make -C .." *)
634
(* End: *)