Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 81229f63

History | View | Annotate | Download (32.1 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
type param_t =
33
  {
34
    unfold_arrow_active: bool;
35
    force_alias_ite: bool;
36
    force_alias_internal_fun: bool;
37
  }
38

    
39
let params = ref
40
               {
41
                 unfold_arrow_active = false;
42
                 force_alias_ite = false;
43
                 force_alias_internal_fun =false;
44
               }
45

    
46
type norm_ctx_t =
47
  {
48
    parentid: ident;
49
    vars: var_decl list;
50
    is_output: ident -> bool; 
51
  }
52

    
53
           
54
let expr_true loc ck =
55
{ expr_tag = Utils.new_tag ();
56
  expr_desc = Expr_const (Const_tag tag_true);
57
  expr_type = Type_predef.type_bool;
58
  expr_clock = ck;
59
  expr_delay = Delay.new_var ();
60
  expr_annot = None;
61
  expr_loc = loc }
62

    
63
let expr_false loc ck =
64
{ expr_tag = Utils.new_tag ();
65
  expr_desc = Expr_const (Const_tag tag_false);
66
  expr_type = Type_predef.type_bool;
67
  expr_clock = ck;
68
  expr_delay = Delay.new_var ();
69
  expr_annot = None;
70
  expr_loc = loc }
71

    
72
let expr_once loc ck =
73
 { expr_tag = Utils.new_tag ();
74
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
75
  expr_type = Type_predef.type_bool;
76
  expr_clock = ck;
77
  expr_delay = Delay.new_var ();
78
  expr_annot = None;
79
  expr_loc = loc }
80

    
81
let is_expr_once =
82
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
83
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
84

    
85
let unfold_arrow expr =
86
 match expr.expr_desc with
87
 | Expr_arrow (e1, e2) ->
88
    let loc = expr.expr_loc in
89
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
90
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
91
 | _                   -> assert false
92

    
93

    
94

    
95
(* Get the equation in [defs] with [expr] as rhs, if any *)
96
let get_expr_alias defs expr =
97
 try Some (List.find (fun eq -> Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock && is_eq_expr eq.eq_rhs expr) defs)
98
 with
99
 | Not_found -> None
100
  
101
(* Replace [expr] with (tuple of) [locals] *)
102
let replace_expr locals expr =
103
 match locals with
104
 | []  -> assert false
105
 | [v] -> { expr with
106
   expr_tag = Utils.new_tag ();
107
   expr_desc = Expr_ident v.var_id }
108
 | _   -> { expr with
109
   expr_tag = Utils.new_tag ();
110
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
111

    
112
let unfold_offsets e offsets =
113
  let add_offset e d =
114
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
115
    let res = *)
116
    { e with
117
      expr_tag = Utils.new_tag ();
118
      expr_loc = d.Dimension.dim_loc;
119
      expr_type = Types.array_element_type e.expr_type;
120
      expr_desc = Expr_access (e, d) }
121
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
122
  in
123
 List.fold_left add_offset e offsets
124

    
125
(* IS IT USED ? TODO 
126
(* Create an alias for [expr], if none exists yet *)
127
let mk_expr_alias (parentid, vars) (defs, vars) expr =
128
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
129
  match get_expr_alias defs expr with
130
  | Some eq ->
131
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
132
    (defs, vars), replace_expr aliases expr
133
  | None    ->
134
    let new_aliases =
135
      List.map2
136
	(mk_fresh_var (parentid, vars) expr.expr_loc)
137
	(Types.type_list_of_type expr.expr_type)
138
	(Clocks.clock_list_of_clock expr.expr_clock) in
139
    let new_def =
140
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
141
    in
142
    (* 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; *)
143
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
144
 *)
145
  
146
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
147
   and [opt] is true *)
148
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
149
(*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;*)
150
  match expr.expr_desc with
151
  | Expr_ident alias ->
152
    (defs, vars), expr
153
  | _                ->
154
    match get_expr_alias defs expr with
155
    | Some eq ->
156
       (* Format.eprintf "Found a preexisting definition@."; *)
157
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
158
      (defs, vars), replace_expr aliases expr
159
    | None    ->
160
       (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
161
        * Format.eprintf "existing defs are: @[[%a@]]@."
162
        *   (fprintf_list ~sep:"@ "(fun fmt eq ->
163
        *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
164
        *          Clocks.print_ck eq.eq_rhs.expr_clock
165
        *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
166
        *          (is_eq_expr eq.eq_rhs expr)
167
        *          Printers.pp_node_eq eq))
168
        *   defs; *)
169
      if opt
170
      then
171
	let new_aliases =
172
	  List.map2
173
	    (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)
174
	    (Types.type_list_of_type expr.expr_type)
175
	    (Clocks.clock_list_of_clock expr.expr_clock) in
176
	let new_def =
177
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
178
	in
179
	(* Typing and Registering machine type *) 
180
	let _ = if Machine_types.is_active then
181
                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
182
        in
183
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
184
      else
185
	(defs, vars), expr
186

    
187
(* Create a (normalized) expression from [ref_e],
188
   replacing description with [norm_d],
189
   taking propagated [offsets] into account
190
   in order to change expression type *)
191
let mk_norm_expr offsets ref_e norm_d =
192
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
193
  let drop_array_type ty =
194
    Types.map_tuple_type Types.array_element_type ty in
195
  { ref_e with
196
    expr_desc = norm_d;
197
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
198
														
199
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
200
let rec normalize_list alias norm_ctx offsets norm_element defvars elist =
201
  List.fold_right
202
    (fun t (defvars, qlist) ->
203
      let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
204
      (defvars, norm_t :: qlist)
205
    ) elist (defvars, [])
206

    
207
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr =
208
  (*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;*)
209
  match expr.expr_desc with
210
  | Expr_const _
211
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
212
  | Expr_array elist ->
213
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
214
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
215
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
216
  | Expr_power (e1, d) when offsets = [] ->
217
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
218
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
219
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
220
  | Expr_power (e1, d) ->
221
     normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
222
  | Expr_access (e1, d) ->
223
     normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1
224
  | Expr_tuple elist ->
225
     let defvars, norm_elist =
226
       normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
227
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
228
  | Expr_appl (id, args, None)
229
      when Basic_library.is_homomorphic_fun id 
230
	&& Types.is_array_type expr.expr_type ->
231
     let defvars, norm_args =
232
       normalize_list
233
	 alias
234
	 norm_ctx
235
	 offsets
236
	 (fun _ -> normalize_array_expr ~alias:true)
237
	 defvars
238
	 (expr_list_of_expr args)
239
     in
240
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
241
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
242
      && not (!params.force_alias_internal_fun || alias_basic) ->
243
     let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in
244
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
245
  | Expr_appl (id, args, r) ->
246
     let defvars, r =
247
       match r with
248
       | None -> defvars, None
249
       | Some r ->
250
	  let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in
251
	  defvars, Some norm_r
252
     in
253
     let defvars, norm_args = normalize_expr norm_ctx [] defvars args in
254
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
255
     if offsets <> []
256
     then
257
       let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in
258
       normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr
259
     else
260
       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
261
				    || not (Basic_library.is_expr_internal_fun expr)))
262
	 norm_ctx defvars norm_expr
263
  | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
264
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
265
     normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr)
266
  | Expr_arrow (e1,e2) ->
267
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
268
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
269
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
270
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
271
  | Expr_pre e ->
272
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
273
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
274
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
275
  | Expr_fby (e1, e2) ->
276
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
277
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
278
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
279
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
280
  | Expr_when (e, c, l) ->
281
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
282
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
283
  | Expr_ite (c, t, e) ->
284
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
285
     let defvars, norm_t = normalize_cond_expr  norm_ctx offsets defvars t in
286
     let defvars, norm_e = normalize_cond_expr  norm_ctx offsets defvars e in
287
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
288
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
289
  | Expr_merge (c, hl) ->
290
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
291
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
292
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
293

    
294
(* Creates a conditional with a merge construct, which is more lazy *)
295
(*
296
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
297
  match expr.expr_desc with
298
  | Expr_ite (c, t, e) ->
299
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
300
  | _ -> assert false
301
*)
302
and normalize_branches norm_ctx offsets defvars hl =
303
  List.fold_right
304
    (fun (t, h) (defvars, norm_q) ->
305
      let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in
306
      defvars, (t, norm_h) :: norm_q
307
    )
308
    hl (defvars, [])
309

    
310
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
311
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
312
  match expr.expr_desc with
313
  | Expr_power (e1, d) when offsets = [] ->
314
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
315
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
316
  | Expr_power (e1, d) ->
317
     normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
318
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1
319
  | Expr_array elist when offsets = [] ->
320
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
321
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
322
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
323
     let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
324
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
325
  |  _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr
326

    
327
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr =
328
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
329
  match expr.expr_desc with
330
  | Expr_access (e1, d) ->
331
     normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1
332
  | Expr_ite (c, t, e) ->
333
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
334
     let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
335
     let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
336
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
337
  | Expr_merge (c, hl) ->
338
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
339
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
340
  | _ when !params.force_alias_ite ->
341
     (* Forcing alias creation for then/else expressions *)
342
     let defvars, norm_expr =
343
       normalize_expr ~alias:alias norm_ctx offsets defvars expr
344
     in
345
     mk_expr_alias_opt true norm_ctx defvars norm_expr
346
  | _ -> (* default case without the force_alias_ite option *)
347
     normalize_expr ~alias:alias norm_ctx offsets defvars expr
348
       
349
and normalize_guard norm_ctx defvars expr =
350
  let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in
351
  mk_expr_alias_opt true norm_ctx defvars norm_expr
352

    
353
(* outputs cannot be memories as well. If so, introduce new local variable.
354
*)
355
let decouple_outputs norm_ctx defvars eq =
356
  let rec fold_lhs defvars lhs tys cks =
357
    match lhs, tys, cks with
358
    | [], [], []          -> defvars, []
359
    | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
360
			     if norm_ctx.is_output v
361
			     then
362
			       let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in
363
			       let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
364
			       (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
365
			     else
366
			       (defs_q, vars_q), v::lhs_q
367
    | _                   -> assert false in
368
  let defvars', lhs' =
369
    fold_lhs
370
      defvars
371
      eq.eq_lhs
372
      (Types.type_list_of_type eq.eq_rhs.expr_type)
373
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
374
  defvars', {eq with eq_lhs = lhs' }
375

    
376
let rec normalize_eq norm_ctx defvars eq =
377
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
378
  match eq.eq_rhs.expr_desc with
379
  | Expr_pre _
380
  | Expr_fby _  ->
381
    let (defvars', eq') = decouple_outputs norm_ctx defvars eq in
382
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in
383
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
384
    (norm_eq::defs', vars')
385
  | Expr_array _ ->
386
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
387
    let norm_eq = { eq with eq_rhs = norm_rhs } in
388
    (norm_eq::defs', vars')
389
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
390
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
391
    let norm_eq = { eq with eq_rhs = norm_rhs } in
392
    (norm_eq::defs', vars')
393
  | Expr_appl _ ->
394
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
395
    let norm_eq = { eq with eq_rhs = norm_rhs } in
396
    (norm_eq::defs', vars')
397
  | _ ->
398
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
399
    let norm_eq = { eq with eq_rhs = norm_rhs } in
400
    norm_eq::defs', vars'
401

    
402
let normalize_eq_split norm_ctx defvars eq =
403
  try
404
    let defs, vars = normalize_eq norm_ctx defvars eq in
405
    List.fold_right (fun eq (def, vars) -> 
406
        let eq_defs = Splitting.tuple_split_eq eq in
407
        if eq_defs = [eq] then
408
          eq::def, vars 
409
        else
410
          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
411
      ) defs ([], vars)  
412
    
413
  with ex -> (
414
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
415
    raise ex
416
  )
417

    
418
(* Projecting an eexpr to an eexpr associated to a single
419
   variable. Returns the updated ee, the bounded variable and the
420
   associated statement *)
421
let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
422
  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
423
  (* don't do anything is eexpr is just a variable *)
424
  let skip =
425
    match ee.eexpr_qfexpr.expr_desc with
426
    | Expr_ident _ | Expr_const _ -> true
427
    | _ -> false
428
  in
429
  if skip then
430
    ee, (def, vars)
431
  else (
432
    (* New output variable *)
433
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
434
    let output_var = 
435
      mkvar_decl 
436
        ee.eexpr_loc 
437
        (output_id, 
438
         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
439
         mkclock ee.eexpr_loc Ckdec_any, 
440
         false (* not a constant *),
441
         None,
442
         None
443
        ) 
444
    in
445
    let output_expr = expr_of_vdecl output_var in
446
    (* Rebuilding an eexpr with a silly expression, just a variable *)
447
    let ee' = { ee with eexpr_qfexpr = output_expr } in
448

    
449
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
450
       inline possible calls within, normalize it and type/clock the
451
       result.  *)
452
    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
453

    
454

    
455
    (* (\* Inlining any calls *\)
456
     * let nodes = get_nodes decls in
457
     * let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
458
     * let vars, eqs =
459
     *   if calls = [] && not (eq_has_arrows eq) then
460
     *     vars, [eq]    
461
     *   else
462
     *     assert false (\* TODO *\)
463
     * in *)
464
    
465
    (* Normalizing expr and eqs *)
466
    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in
467
    let vars = output_var :: vars in 
468
(*    let todefine =
469
      List.fold_left
470
        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
471
        (ISet.add output_id ISet.empty) vars in
472
 *)      
473

    
474
    (* Typing / Clocking *)
475
    try
476
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
477
        (*
478
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
479
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
480
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
481
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
482
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
483
  (* check that table is empty *)
484
    if (not (ISet.is_empty undefined_vars)) then
485
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
486
    
487
    (*Format.eprintf "normalized eqs %a@.@?" 
488
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
489
         *)
490

    
491
    ee', (defs, vars)
492
    
493
  with (Types.Error (loc,err)) as exc ->
494
    eprintf "Typing error for eexpr %a: %a%a%a@."
495
      Printers.pp_eexpr ee
496
      Types.pp_error err
497
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
498
      Location.pp_loc loc
499
  
500
      
501
    ;
502
    raise exc
503
                                     
504
  )
505
    
506
   (*
507
  
508
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
509
  (* Calls are first inlined *)
510
  
511
  (*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;  *)
512
  let (new_locals, eqs) =
513
    if calls = [] && not (eq_has_arrows eq) then
514
      (locals, [eq])     
515
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
516
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
517
      (*Format.eprintf "eqs %a@.@?" 
518
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
519
      (new_locals, eqs)
520
*)
521
           (locals, [eq])     
522
 
523
    ) in
524
  (* Normalizing expr and eqs *)
525
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
526
    let todefine = List.fold_left
527
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
528
    (ISet.add output_id ISet.empty) vars in
529
  
530
  try
531
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
532
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
533
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
534
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
535
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
536
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
537
  (* check that table is empty *)
538
    if (not (ISet.is_empty undefined_vars)) then
539
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
540
    
541
    (*Format.eprintf "normalized eqs %a@.@?" 
542
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
543
    ee.eexpr_normalized <- Some (output_var, defs, vars)
544
    
545
  with (Types.Error (loc,err)) as exc ->
546
    eprintf "Typing error for eexpr %a: %a%a%a@."
547
      Printers.pp_eexpr ee
548
      Types.pp_error err
549
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
550
      Location.pp_loc loc
551
  
552
      
553
    ;
554
    raise exc
555
                                                 *)    
556
 
557

    
558
(* We use node local vars to make sure we are creating fresh variables *) 
559
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  
560
  (* Original set of variables actually visible from here: in/out and
561
     spec locals (no node locals) *)
562
  let orig_vars = in_vars @ out_vars @ s.locals in
563
  (* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)
564
  let not_is_orig_var v =
565
    List.for_all ((!=) v) orig_vars in
566
  let norm_ctx = {
567
      parentid = parentid;
568
      vars = in_vars @ out_vars @ l_vars;
569
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
570
    }
571
  in
572
  (* Normalizing existing stmts *)
573
  let eqs, auts = List.fold_right (fun s (el,al)  -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
574
  if auts != [] then assert false; (* Automata should be expanded by now. *)
575
  let defsvars = 
576
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
577
  in
578
  (* Iterate through predicates and normalize them on the go, creating
579
     fresh variables for any guarantees/assumes/require/ensure *)
580
  let process_predicates l defvars =
581
    (* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
582
    let res = List.fold_right (fun ee (accu, defvars) ->
583
        let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
584
        ee'::accu, defvars
585
      ) l ([], defvars)
586
    in
587
    (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
588
     * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
589
    res
590
  in
591

    
592
  
593
  let assume', defsvars = process_predicates s.assume defsvars in
594
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
595
  let modes', (defs, vars) =
596
    List.fold_right (
597
        fun m (accu_m, defsvars) ->
598
        let require', defsvars = process_predicates m.require defsvars in
599
        let ensure', defsvars = process_predicates m.ensure defsvars in
600
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
601
      ) s.modes ([], defsvars)
602
  in
603
  
604
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
605
  new_locals, defs,      
606
  {s with
607
    (* locals = s.locals @ new_locals; *)
608
    stmts = [];
609
    assume = assume';
610
    guarantees = guarantees';
611
    modes = modes'
612
  }
613
(* let nee _ = () in
614
 *   (\*normalize_eexpr decls iovars in *\)
615
 *   List.iter nee s.assume;
616
 *   List.iter nee s.guarantees;
617
 *   List.iter (fun m -> 
618
 *       List.iter nee m.require;
619
 *     List.iter nee m.ensure
620
 *     ) s.modes; *)
621
   
622

    
623
                                                                     
624
  
625
  
626
    
627
(* The normalization phase introduces new local variables
628
   - output cannot be memories. If this happen, new local variables acting as
629
   memories are introduced. 
630
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
631
   access
632
   Thoses values are shared, ie. no duplicate expressions are introduced.
633

    
634
   Concerning specification, a similar process is applied, replacing an
635
   expression by a list of local variables and definitions
636
*)
637

    
638
(** normalize_node node returns a normalized node, 
639
    ie. 
640
    - updated locals
641
    - new equations
642
    -
643
*)
644
let normalize_node decls node =
645
  reset_cpt_fresh ();
646
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
647
  let not_is_orig_var v =
648
    List.for_all ((!=) v) orig_vars in
649
  let norm_ctx = {
650
      parentid = node.node_id;
651
      vars = get_node_vars node;
652
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
653
    }
654
  in
655

    
656
  let eqs, auts = get_node_eqs node in
657
  if auts != [] then assert false; (* Automata should be expanded by now. *)
658
  let spec, new_vars, eqs =
659
    begin
660
      (* Update mutable fields of eexpr to perform normalization of
661
	 specification.
662

    
663
	 Careful: we do not normalize annotations, since they can have the form
664
	 x = (a, b, c) *)
665
      match node.node_spec with
666
      | None 
667
        | Some (NodeSpec _) -> node.node_spec, [], eqs
668
      | Some (Contract s) ->
669
         let new_locals, new_stmts, s' = normalize_spec
670
                    decls
671
                    node.node_id
672
                    (node.node_inputs, node.node_outputs, node.node_locals)
673
                    s
674
         in
675
         (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
676
          * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
677
         Some (Contract s'), new_locals, new_stmts@eqs
678
    end
679
  in
680
  let defs, vars =
681
    List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
682
  (* Normalize the asserts *)
683
  let vars, assert_defs, asserts =
684
    List.fold_left (
685
        fun (vars, def_accu, assert_accu) assert_ ->
686
	let assert_expr = assert_.assert_expr in
687
	let (defs, vars'), expr = 
688
	  normalize_expr 
689
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
690
	    norm_ctx 
691
	    [] (* empty offset for arrays *)
692
	    ([], vars) (* defvar only contains vars *)
693
	    assert_expr
694
	in
695
        (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
696
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
697
      ) (vars, [], []) node.node_asserts in
698
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
699
							  vars and initial locals ones *)
700
  
701
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
702
						       beginning of the list the
703
						       local declared ones *)
704
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
705

    
706

    
707
  (* Updating annotations: traceability and machine types for fresh variables *)
708
  
709
  (* Compute traceability info:
710
     - gather newly bound variables
711
     - compute the associated expression without aliases
712
   *)
713
  let new_annots =
714
    if !Options.traces then
715
      begin
716
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
717
	let norm_traceability = {
718
	    annots = List.map (fun v ->
719
	                 let eq =
720
	                   try
721
		             List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
722
	                   with Not_found -> 
723
		             (
724
		               Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
725
		               assert false
726
		             ) 
727
	                 in
728
	                 let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
729
	                 let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
730
	                 Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
731
	                 (["traceability"], pair)
732
	               ) diff_vars;
733
	    annot_loc = Location.dummy_loc
734
	  }
735
	in
736
	norm_traceability::node.node_annot
737
      end
738
    else
739
      node.node_annot
740
  in
741

    
742
  let new_annots =
743
    List.fold_left (fun annots v ->
744
        if Machine_types.is_active && Machine_types.is_exportable v then
745
	  let typ = Machine_types.get_specified_type v in
746
  	  let typ_name = Machine_types.type_name typ in
747

    
748
	  let loc = v.var_loc in
749
	  let typ_as_string =
750
	    mkexpr
751
	      loc
752
	      (Expr_const
753
	         (Const_string typ_name))
754
	  in
755
	  let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
756
	  Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
757
	  {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
758
        else
759
	  annots
760
      ) new_annots new_locals
761
  in
762
  
763
  
764
  let node =
765
    { node with
766
      node_locals = all_locals;
767
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
768
      node_asserts = asserts;
769
      node_annot = new_annots;
770
      node_spec = spec;
771
    }
772
  in ((*Printers.pp_node Format.err_formatter node;*)
773
      node
774
    )
775

    
776
let normalize_inode decls nd =
777
  reset_cpt_fresh ();
778
  match nd.nodei_spec with
779
    None | Some (NodeSpec _) -> nd
780
    | Some (Contract _) -> assert false
781
                         
782
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
783
  match decl.top_decl_desc with
784
  | Node nd ->
785
     let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
786
     update_node nd.node_id decl';
787
     decl'
788
  | ImportedNode nd ->
789
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
790
     update_node nd.nodei_id decl';
791
     decl'
792
     
793
    | Include _| Open _ | Const _ | TypeDef _ -> decl
794

    
795
let normalize_prog p decls =
796
  (* Backend specific configurations for normalization *)
797
  params := p;
798

    
799
  (* Main algorithm: iterates over nodes *)
800
  List.map (normalize_decl decls) decls
801

    
802

    
803
(* Fake interface for outside uses *)
804
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
805
  mk_expr_alias_opt
806
    opt
807
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
808
    (defs, vars)
809
    expr
810

    
811
    
812
           (* Local Variables: *)
813
           (* compile-command:"make -C .." *)
814
           (* End: *)
815