Project

General

Profile

Download (32.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 Lustre_types
14
open Corelang
15
open Format
16

    
17
(* To update thank to some command line options *)
18
let debug = ref false
19
          
20
(** Normalisation iters through the AST of expressions and bind fresh definition
21
    when some criteria are met. This creation of fresh definition is performed by
22
    the function mk_expr_alias_opt when the alias argument is on.
23

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

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

    
35
type param_t =
36
  {
37
    unfold_arrow_active: bool;
38
    force_alias_ite: bool;
39
    force_alias_internal_fun: bool;
40
  }
41

    
42
let params = ref
43
               {
44
                 unfold_arrow_active = false;
45
                 force_alias_ite = false;
46
                 force_alias_internal_fun =false;
47
               }
48

    
49
type norm_ctx_t =
50
  {
51
    parentid: ident;
52
    vars: var_decl list;
53
    is_output: ident -> bool; 
54
  }
55

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

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

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

    
84
let is_expr_once =
85
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
86
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
87

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

    
96

    
97

    
98
(* Get the equation in [defs] with [expr] as rhs, if any *)
99
let get_expr_alias defs expr =
100
 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)
101
 with
102
 | Not_found -> None
103
  
104
(* Replace [expr] with (tuple of) [locals] *)
105
let replace_expr locals expr =
106
 match locals with
107
 | []  -> assert false
108
 | [v] -> { expr with
109
   expr_tag = Utils.new_tag ();
110
   expr_desc = Expr_ident v.var_id }
111
 | _   -> { expr with
112
   expr_tag = Utils.new_tag ();
113
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
114

    
115
  
116
(* IS IT USED ? TODO 
117
(* Create an alias for [expr], if none exists yet *)
118
let mk_expr_alias (parentid, vars) (defs, vars) expr =
119
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
120
  match get_expr_alias defs expr with
121
  | Some eq ->
122
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
123
    (defs, vars), replace_expr aliases expr
124
  | None    ->
125
    let new_aliases =
126
      List.map2
127
	(mk_fresh_var (parentid, vars) expr.expr_loc)
128
	(Types.type_list_of_type expr.expr_type)
129
	(Clocks.clock_list_of_clock expr.expr_clock) in
130
    let new_def =
131
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
132
    in
133
    (* 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; *)
134
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
135
 *)
136
  
137
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
138
   and [opt] is true
139

    
140
  
141
 *)
142
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
143
  if !debug then
144
    Log.report ~plugin:"normalization" ~level:2
145
      (fun fmt -> Format.fprintf  fmt "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);
146
  match expr.expr_desc with
147
  | Expr_ident _ ->
148
    (defs, vars), expr
149
  | _                ->
150
    match get_expr_alias defs expr with
151
    | Some eq ->
152
       (* Format.eprintf "Found a preexisting definition@."; *)
153
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
154
      (defs, vars), replace_expr aliases expr
155
    | None    ->
156
       (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
157
        * Format.eprintf "existing defs are: @[[%a@]]@."
158
        *   (fprintf_list ~sep:"@ "(fun fmt eq ->
159
        *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
160
        *          Clocks.print_ck eq.eq_rhs.expr_clock
161
        *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
162
        *          (is_eq_expr eq.eq_rhs expr)
163
        *          Printers.pp_node_eq eq))
164
        *   defs; *)
165
      if opt
166
      then
167
	let new_aliases =
168
	  List.map2
169
	    (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)
170
	    (Types.type_list_of_type expr.expr_type)
171
	    (Clocks.clock_list_of_clock expr.expr_clock) in
172
	let new_def =
173
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
174
	in
175
	(* Typing and Registering machine type *) 
176
	let _ = if Machine_types.is_active then
177
                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
178
        in
179
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
180
      else
181
	(defs, vars), expr
182

    
183
(* Similar fonctions for dimensions *) 
184
let mk_dim_alias opt norm_ctx (defs, vars) dim =
185
  match dim.Dimension.dim_desc with
186
  | Dimension.Dbool _ | Dint _ 
187
    | Dident _ -> (defs, vars), dim (* Keep the same *)
188
  | _ when opt -> (* Cast to expression, normalizing *)
189
     let e = expr_of_dimension dim in
190
     let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in
191
     defvars, dimension_of_expr e
192

    
193
  | _ -> (defs, vars), dim (* Keep the same *)
194

    
195

    
196
let unfold_offsets norm_ctx defvars e offsets =
197
  let add_offset (defvars, e) d =
198
    (*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; *)
199
    let defvars, d = mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d in
200
    let new_e = 
201
      { e with
202
        expr_tag = Utils.new_tag ();
203
        expr_loc = d.Dimension.dim_loc;
204
        expr_type = Types.array_element_type e.expr_type;
205
        expr_desc = Expr_access (e, d) }
206
    in
207
    defvars, new_e
208
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
209
  in
210
  List.fold_left add_offset (defvars, e) offsets 
211

    
212
      
213
(* Create a (normalized) expression from [ref_e],
214
   replacing description with [norm_d],
215
   taking propagated [offsets] into account
216
   in order to change expression type *)
217
let mk_norm_expr offsets ref_e norm_d =
218
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
219
  let drop_array_type ty =
220
    Types.map_tuple_type Types.array_element_type ty in
221
  { ref_e with
222
    expr_desc = norm_d;
223
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
224
														
225
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
226
let normalize_list alias norm_ctx offsets norm_element defvars elist =
227
  List.fold_right
228
    (fun t (defvars, qlist) ->
229
      let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
230
      (defvars, norm_t :: qlist)
231
    ) elist (defvars, [])
232

    
233
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr =
234
  (* 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; *)
235
  match expr.expr_desc with
236
  | Expr_const _
237
    | Expr_ident _ ->
238
     unfold_offsets norm_ctx defvars expr offsets
239
  | Expr_array elist ->
240
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
241
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
242
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
243
  | Expr_power (e1, d) when offsets = [] ->
244
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
245
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
246
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
247
  | Expr_power (e1, _) ->
248
     normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
249
  | Expr_access (e1, d) ->
250
     normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 
251
    
252
  | Expr_tuple elist ->
253
     let defvars, norm_elist =
254
       normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
255
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
256
  | Expr_appl (id, args, None)
257
      when Basic_library.is_homomorphic_fun id 
258
	   && Types.is_array_type expr.expr_type ->
259
     let defvars, norm_args =
260
       normalize_list
261
	 alias
262
	 norm_ctx
263
	 offsets
264
	 (fun _ -> normalize_array_expr ~alias:true)
265
	 defvars
266
	 (expr_list_of_expr args)
267
     in
268
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
269
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
270
      && not (!params.force_alias_internal_fun || alias_basic) ->
271
     let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in
272
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
273
  | Expr_appl (id, args, r) ->
274
     let defvars, r =
275
       match r with
276
       | None -> defvars, None
277
       | Some r ->
278
	  let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in
279
	  defvars, Some norm_r
280
     in
281
     let defvars, norm_args = normalize_expr norm_ctx [] defvars args in
282
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
283
     if offsets <> []
284
     then
285
       let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in
286
       normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr
287
     else
288
       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
289
				    || not (Basic_library.is_expr_internal_fun expr)))
290
	 norm_ctx defvars norm_expr
291
  | Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) ->
292
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
293
     normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr)
294
  | Expr_arrow (e1,e2) ->
295
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
296
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
297
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
298
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
299
  | Expr_pre e ->
300
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
301
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
302
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
303
  | Expr_fby (e1, e2) ->
304
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
305
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
306
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
307
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
308
  | Expr_when (e, c, l) ->
309
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
310
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
311
  | Expr_ite (c, t, e) ->
312
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
313
     let defvars, norm_t = normalize_cond_expr  norm_ctx offsets defvars t in
314
     let defvars, norm_e = normalize_cond_expr  norm_ctx offsets defvars e in
315
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
316
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
317
  | Expr_merge (c, hl) ->
318
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
319
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
320
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
321

    
322
(* Creates a conditional with a merge construct, which is more lazy *)
323
(*
324
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
325
  match expr.expr_desc with
326
  | Expr_ite (c, t, e) ->
327
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
328
  | _ -> assert false
329
*)
330
and normalize_branches norm_ctx offsets defvars hl =
331
  List.fold_right
332
    (fun (t, h) (defvars, norm_q) ->
333
      let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in
334
      defvars, (t, norm_h) :: norm_q
335
    )
336
    hl (defvars, [])
337

    
338
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
339
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
340
  match expr.expr_desc with
341
  | Expr_power (e1, d) when offsets = [] ->
342
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
343
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
344
  | Expr_power (e1, _) ->
345
     normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
346
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1
347
  | Expr_array elist when offsets = [] ->
348
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
349
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
350
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
351
     let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
352
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
353
  |  _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr
354

    
355
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr =
356
  (* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
357
  match expr.expr_desc with
358
  | Expr_access (e1, d) ->
359
     normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1
360
  | Expr_ite (c, t, e) ->
361
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
362
     let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
363
     let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
364
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
365
  | Expr_merge (c, hl) ->
366
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
367
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
368
  | _ when !params.force_alias_ite ->
369
     (* Forcing alias creation for then/else expressions *)
370
     let defvars, norm_expr =
371
       normalize_expr ~alias:alias norm_ctx offsets defvars expr
372
     in
373
     mk_expr_alias_opt true norm_ctx defvars norm_expr
374
  | _ -> (* default case without the force_alias_ite option *)
375
     normalize_expr ~alias:alias norm_ctx offsets defvars expr
376
       
377
and normalize_guard norm_ctx defvars expr =
378
  let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in
379
  mk_expr_alias_opt true norm_ctx defvars norm_expr
380

    
381
(* outputs cannot be memories as well. If so, introduce new local variable.
382
*)
383
let decouple_outputs norm_ctx defvars eq =
384
  let rec fold_lhs defvars lhs tys cks =
385
    match lhs, tys, cks with
386
    | [], [], []          -> defvars, []
387
    | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
388
			     if norm_ctx.is_output v
389
			     then
390
			       let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in
391
			       let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
392
			       (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
393
			     else
394
			       (defs_q, vars_q), v::lhs_q
395
    | _                   -> assert false in
396
  let defvars', lhs' =
397
    fold_lhs
398
      defvars
399
      eq.eq_lhs
400
      (Types.type_list_of_type eq.eq_rhs.expr_type)
401
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
402
  defvars', {eq with eq_lhs = lhs' }
403

    
404
let normalize_eq norm_ctx defvars eq =
405
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
406
  match eq.eq_rhs.expr_desc with
407
  | Expr_pre _
408
  | Expr_fby _  ->
409
    let (defvars', eq') = decouple_outputs norm_ctx defvars eq in
410
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in
411
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
412
    (norm_eq::defs', vars')
413
  | Expr_array _ ->
414
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
415
    let norm_eq = { eq with eq_rhs = norm_rhs } in
416
    (norm_eq::defs', vars')
417
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
418
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
419
    let norm_eq = { eq with eq_rhs = norm_rhs } in
420
    (norm_eq::defs', vars')
421
  | Expr_appl _ ->
422
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
423
    let norm_eq = { eq with eq_rhs = norm_rhs } in
424
    (norm_eq::defs', vars')
425
  | _ ->
426
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
427
    let norm_eq = { eq with eq_rhs = norm_rhs } in
428
    norm_eq::defs', vars'
429

    
430
let normalize_eq_split norm_ctx defvars eq =
431
  try
432
    let defs, vars = normalize_eq norm_ctx defvars eq in
433
    List.fold_right (fun eq (def, vars) -> 
434
        let eq_defs = Splitting.tuple_split_eq eq in
435
        if eq_defs = [eq] then
436
          eq::def, vars 
437
        else
438
          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
439
      ) defs ([], vars)  
440
    
441
  with ex -> (
442
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
443
    raise ex
444
  )
445

    
446
(* Projecting an eexpr to an eexpr associated to a single
447
   variable. Returns the updated ee, the bounded variable and the
448
   associated statement *)
449
let normalize_pred_eexpr norm_ctx (def,vars) ee =
450
  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
451
  (* don't do anything is eexpr is just a variable *)
452
  let skip =
453
    match ee.eexpr_qfexpr.expr_desc with
454
    | Expr_ident _ | Expr_const _ -> true
455
    | _ -> false
456
  in
457
  if skip then
458
    ee, (def, vars)
459
  else (
460
    (* New output variable *)
461
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
462
    let output_var = 
463
      mkvar_decl 
464
        ee.eexpr_loc 
465
        (output_id, 
466
         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
467
         mkclock ee.eexpr_loc Ckdec_any, 
468
         false (* not a constant *),
469
         None,
470
         None
471
        ) 
472
    in
473
    let output_expr = expr_of_vdecl output_var in
474
    (* Rebuilding an eexpr with a silly expression, just a variable *)
475
    let ee' = { ee with eexpr_qfexpr = output_expr } in
476

    
477
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
478
       inline possible calls within, normalize it and type/clock the
479
       result.  *)
480
    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
481

    
482

    
483
    (* (\* Inlining any calls *\)
484
     * let nodes = get_nodes decls in
485
     * let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
486
     * let vars, eqs =
487
     *   if calls = [] && not (eq_has_arrows eq) then
488
     *     vars, [eq]    
489
     *   else
490
     *     assert false (\* TODO *\)
491
     * in *)
492
    
493
    (* Normalizing expr and eqs *)
494
    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in
495
    let vars = output_var :: vars in 
496
(*    let todefine =
497
      List.fold_left
498
        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
499
        (ISet.add output_id ISet.empty) vars in
500
 *)      
501

    
502
    (* Typing / Clocking *)
503
    try
504
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
505
        (*
506
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
507
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
508
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
509
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
510
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
511
  (* check that table is empty *)
512
    if (not (ISet.is_empty undefined_vars)) then
513
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
514
    
515
    (*Format.eprintf "normalized eqs %a@.@?" 
516
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
517
         *)
518

    
519
    ee', (defs, vars)
520
    
521
  with (Types.Error (loc,err)) as exc ->
522
    eprintf "Typing error for eexpr %a: %a%a%a@."
523
      Printers.pp_eexpr ee
524
      Types.pp_error err
525
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
526
      Location.pp_loc loc
527
  
528
      
529
    ;
530
    raise exc
531
                                     
532
  )
533
    
534
   (*
535
  
536
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
537
  (* Calls are first inlined *)
538
  
539
  (*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;  *)
540
  let (new_locals, eqs) =
541
    if calls = [] && not (eq_has_arrows eq) then
542
      (locals, [eq])     
543
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
544
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
545
      (*Format.eprintf "eqs %a@.@?" 
546
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
547
      (new_locals, eqs)
548
*)
549
           (locals, [eq])     
550
 
551
    ) in
552
  (* Normalizing expr and eqs *)
553
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
554
    let todefine = List.fold_left
555
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
556
    (ISet.add output_id ISet.empty) vars in
557
  
558
  try
559
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
560
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
561
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
562
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
563
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
564
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
565
  (* check that table is empty *)
566
    if (not (ISet.is_empty undefined_vars)) then
567
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
568
    
569
    (*Format.eprintf "normalized eqs %a@.@?" 
570
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
571
    ee.eexpr_normalized <- Some (output_var, defs, vars)
572
    
573
  with (Types.Error (loc,err)) as exc ->
574
    eprintf "Typing error for eexpr %a: %a%a%a@."
575
      Printers.pp_eexpr ee
576
      Types.pp_error err
577
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
578
      Location.pp_loc loc
579
  
580
      
581
    ;
582
    raise exc
583
                                                 *)    
584
 
585

    
586
(* We use node local vars to make sure we are creating fresh variables *) 
587
let normalize_spec parentid (in_vars, out_vars, l_vars) s =
588
  (* Original set of variables actually visible from here: in/out and
589
     spec locals (no node locals) *)
590
  let orig_vars = in_vars @ out_vars @ s.locals in
591
  (* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)
592
  let not_is_orig_var v =
593
    List.for_all ((!=) v) orig_vars in
594
  let norm_ctx = {
595
      parentid = parentid;
596
      vars = in_vars @ out_vars @ l_vars;
597
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
598
    }
599
  in
600
  (* Normalizing existing stmts *)
601
  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
602
  if auts != [] then assert false; (* Automata should be expanded by now. *)
603
  let defsvars = 
604
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
605
  in
606
  (* Iterate through predicates and normalize them on the go, creating
607
     fresh variables for any guarantees/assumes/require/ensure *)
608
  let process_predicates l defvars =
609
    (* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
610
    let res = List.fold_right (fun ee (accu, defvars) ->
611
        let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in
612
        ee'::accu, defvars
613
      ) l ([], defvars)
614
    in
615
    (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
616
     * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
617
    res
618
  in
619

    
620
  
621
  let assume', defsvars = process_predicates s.assume defsvars in
622
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
623
  let modes', (defs, vars) =
624
    List.fold_right (
625
        fun m (accu_m, defsvars) ->
626
        let require', defsvars = process_predicates m.require defsvars in
627
        let ensure', defsvars = process_predicates m.ensure defsvars in
628
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
629
      ) s.modes ([], defsvars)
630
  in
631
  
632
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
633
  new_locals, defs,      
634
  {s with
635
    (* locals = s.locals @ new_locals; *)
636
    stmts = [];
637
    assume = assume';
638
    guarantees = guarantees';
639
    modes = modes'
640
  }
641
(* let nee _ = () in
642
 *   (\*normalize_eexpr decls iovars in *\)
643
 *   List.iter nee s.assume;
644
 *   List.iter nee s.guarantees;
645
 *   List.iter (fun m -> 
646
 *       List.iter nee m.require;
647
 *     List.iter nee m.ensure
648
 *     ) s.modes; *)
649
   
650

    
651
                                                                     
652
  
653
  
654
    
655
(* The normalization phase introduces new local variables
656
   - output cannot be memories. If this happen, new local variables acting as
657
   memories are introduced. 
658
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
659
   access
660
   Thoses values are shared, ie. no duplicate expressions are introduced.
661

    
662
   Concerning specification, a similar process is applied, replacing an
663
   expression by a list of local variables and definitions
664
*)
665

    
666
(** normalize_node node returns a normalized node, 
667
    ie. 
668
    - updated locals
669
    - new equations
670
    -
671
*)
672
let normalize_node node =
673
  reset_cpt_fresh ();
674
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
675
  let not_is_orig_var v =
676
    List.for_all ((!=) v) orig_vars in
677
  let norm_ctx = {
678
      parentid = node.node_id;
679
      vars = get_node_vars node;
680
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
681
    }
682
  in
683

    
684
  let eqs, auts = get_node_eqs node in
685
  if auts != [] then assert false; (* Automata should be expanded by now. *)
686
  let spec, new_vars, eqs =
687
    begin
688
      (* Update mutable fields of eexpr to perform normalization of
689
	 specification.
690

    
691
	 Careful: we do not normalize annotations, since they can have the form
692
	 x = (a, b, c) *)
693
      match node.node_spec with
694
      | None 
695
        | Some (NodeSpec _) -> node.node_spec, [], eqs
696
      | Some (Contract s) ->
697
         let new_locals, new_stmts, s' = normalize_spec
698
                    node.node_id
699
                    (node.node_inputs, node.node_outputs, node.node_locals)
700
                    s
701
         in
702
         (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
703
          * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
704
         Some (Contract s'), new_locals, new_stmts@eqs
705
    end
706
  in
707
  let defs, vars =
708
    List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
709
  (* Normalize the asserts *)
710
  let vars, assert_defs, asserts =
711
    List.fold_left (
712
        fun (vars, def_accu, assert_accu) assert_ ->
713
	let assert_expr = assert_.assert_expr in
714
	let (defs, vars'), expr = 
715
	  normalize_expr 
716
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
717
	    norm_ctx 
718
	    [] (* empty offset for arrays *)
719
	    ([], vars) (* defvar only contains vars *)
720
	    assert_expr
721
	in
722
        (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
723
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
724
      ) (vars, [], []) node.node_asserts in
725
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
726
							  vars and initial locals ones *)
727
  
728
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
729
						       beginning of the list the
730
						       local declared ones *)
731
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
732

    
733

    
734
  (* Updating annotations: traceability and machine types for fresh variables *)
735
  
736
  (* Compute traceability info:
737
     - gather newly bound variables
738
     - compute the associated expression without aliases
739
   *)
740
  let new_annots =
741
    if !Options.traces then
742
      begin
743
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
744
	let norm_traceability = {
745
	    annots = List.map (fun v ->
746
	                 let eq =
747
	                   try
748
		             List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
749
	                   with Not_found -> 
750
		             (
751
		               Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
752
		               assert false
753
		             ) 
754
	                 in
755
	                 let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
756
	                 let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
757
	                 Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
758
	                 (["traceability"], pair)
759
	               ) diff_vars;
760
	    annot_loc = Location.dummy_loc
761
	  }
762
	in
763
	norm_traceability::node.node_annot
764
      end
765
    else
766
      node.node_annot
767
  in
768

    
769
  let new_annots =
770
    List.fold_left (fun annots v ->
771
        if Machine_types.is_active && Machine_types.is_exportable v then
772
	  let typ = Machine_types.get_specified_type v in
773
  	  let typ_name = Machine_types.type_name typ in
774

    
775
	  let loc = v.var_loc in
776
	  let typ_as_string =
777
	    mkexpr
778
	      loc
779
	      (Expr_const
780
	         (Const_string typ_name))
781
	  in
782
	  let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
783
	  Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
784
	  {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
785
        else
786
	  annots
787
      ) new_annots new_locals
788
  in
789
  
790
  
791
  let node =
792
    { node with
793
      node_locals = all_locals;
794
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
795
      node_asserts = asserts;
796
      node_annot = new_annots;
797
      node_spec = spec;
798
    }
799
  in ((*Printers.pp_node Format.err_formatter node;*)
800
      node
801
    )
802

    
803
let normalize_inode nd =
804
  reset_cpt_fresh ();
805
  match nd.nodei_spec with
806
    None | Some (NodeSpec _) -> nd
807
    | Some (Contract _) -> assert false
808
                         
809
let normalize_decl (decl: top_decl) : top_decl =
810
  match decl.top_decl_desc with
811
  | Node nd ->
812
     let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
813
     update_node nd.node_id decl';
814
     decl'
815
  | ImportedNode nd ->
816
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode nd)} in
817
     update_node nd.nodei_id decl';
818
     decl'
819
     
820
    | Include _| Open _ | Const _ | TypeDef _ -> decl
821

    
822
let normalize_prog p decls =
823
  (* Backend specific configurations for normalization *)
824
  params := p;
825

    
826
  (* Main algorithm: iterates over nodes *)
827
  List.map normalize_decl decls
828

    
829

    
830
(* Fake interface for outside uses *)
831
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
832
  mk_expr_alias_opt
833
    opt
834
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
835
    (defs, vars)
836
    expr
837

    
838
    
839
           (* Local Variables: *)
840
           (* compile-command:"make -C .." *)
841
           (* End: *)
842
    
(42-42/63)