Project

General

Profile

Download (34.3 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
  unfold_arrow_active : bool;
37
  force_alias_ite : bool;
38
  force_alias_internal_fun : bool;
39
}
40

    
41
let params =
42
  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
  parentid : ident;
51
  vars : var_decl list;
52
  is_output : ident -> bool;
53
}
54

    
55
let expr_true loc ck =
56
  {
57
    expr_tag = Utils.new_tag ();
58
    expr_desc = Expr_const (Const_tag tag_true);
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

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

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

    
88
let is_expr_once =
89
  let dummy_expr_once = expr_once Location.dummy (Clocks.new_var true) in
90
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
91

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

    
100
(* Get the equation in [defs] with [expr] as rhs, if any *)
101
let get_expr_alias defs expr =
102
  try
103
    Some
104
      (List.find
105
         (fun eq ->
106
           Clocks.equal expr.expr_clock eq.eq_rhs.expr_clock
107
           && is_eq_expr eq.eq_rhs expr)
108
         defs)
109
  with Not_found -> None
110

    
111
(* Replace [expr] with (tuple of) [locals] *)
112
let replace_expr locals expr =
113
  match locals with
114
  | [] -> assert false
115
  | [ v ] ->
116
      { expr with expr_tag = Utils.new_tag (); expr_desc = Expr_ident v.var_id }
117
  | _ ->
118
      {
119
        expr with
120
        expr_tag = Utils.new_tag ();
121
        expr_desc = Expr_tuple (List.map expr_of_vdecl locals);
122
      }
123

    
124
(* IS IT USED ? TODO 
125
(* Create an alias for [expr], if none exists yet *)
126
let mk_expr_alias (parentid, vars) (defs, vars) expr =
127
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.pp expr.expr_type Clocks.pp_ck expr.expr_clock;*)
128
  match get_expr_alias defs expr with
129
  | Some eq ->
130
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
131
    (defs, vars), replace_expr aliases expr
132
  | None    ->
133
    let new_aliases =
134
      List.map2
135
	(mk_fresh_var (parentid, vars) expr.expr_loc)
136
	(Types.type_list_of_type expr.expr_type)
137
	(Clocks.clock_list_of_clock expr.expr_clock) in
138
    let new_def =
139
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
140
    in
141
    (* 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; *)
142
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
143
 *)
144

    
145
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
146
   and [opt] is true
147

    
148
  
149
 *)
150
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
151
  if !debug then
152
    Log.report ~plugin:"normalization" ~level:2 (fun fmt ->
153
        Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt
154
          Printers.pp_expr expr Types.pp expr.expr_type Clocks.pp
155
          expr.expr_clock);
156
  match expr.expr_desc with
157
  | Expr_ident _ -> (defs, vars), expr
158
  | _ -> (
159
      match get_expr_alias defs expr with
160
      | Some eq ->
161
          (* Format.eprintf "Found a preexisting definition@."; *)
162
          let aliases =
163
            List.map
164
              (fun id -> List.find (fun v -> v.var_id = id) vars)
165
              eq.eq_lhs
166
          in
167
          (defs, vars), replace_expr aliases expr
168
      | None ->
169
          (*
170
           Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
171
          * Format.eprintf "existing defs are: @[[%a@]]@."
172
          *   (fprintf_list ~sep:"@ "(fun fmt eq ->
173
          *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
174
          *          Clocks.pp_ck eq.eq_rhs.expr_clock
175
          *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
176
          *          (is_eq_expr eq.eq_rhs expr)
177
          *          Printers.pp_node_eq eq))
178
          *   defs; *)
179
          if opt then
180
            let new_aliases =
181
              List.map2
182
                (mk_fresh_var
183
                   (norm_ctx.parentid, norm_ctx.vars @ vars)
184
                   expr.expr_loc)
185
                (Types.type_list_of_type expr.expr_type)
186
                (Clocks.clock_list_of_clock expr.expr_clock)
187
            in
188
            let new_def =
189
              mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
190
            in
191
            (* Typing and Registering machine type *)
192
            let _ =
193
              if Machine_types.is_active then
194
                Machine_types.type_def
195
                  (norm_ctx.parentid, norm_ctx.vars)
196
                  new_aliases expr
197
            in
198
            (new_def :: defs, new_aliases @ vars), replace_expr new_aliases expr
199
          else (defs, vars), expr)
200

    
201
(* Similar fonctions for dimensions *)
202
let mk_dim_alias opt norm_ctx (defs, vars) dim =
203
  match dim.Dimension.dim_desc with
204
  | Dimension.Dbool _ | Dint _ | Dident _ ->
205
      (defs, vars), dim (* Keep the same *)
206
  | _ when opt ->
207
      (* Cast to expression, normalizing *)
208
      let e = expr_of_dimension dim in
209
      let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in
210
      defvars, dimension_of_expr e
211
  | _ -> (defs, vars), dim
212
(* Keep the same *)
213

    
214
let unfold_offsets norm_ctx defvars e offsets =
215
  let add_offset (defvars, e) d =
216
    (*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.pp e.expr_type Dimension.pp_dimension d; *)
217
    let defvars, d =
218
      mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d
219
    in
220
    let new_e =
221
      {
222
        e with
223
        expr_tag = Utils.new_tag ();
224
        expr_loc = d.Dimension.dim_loc;
225
        expr_type = Types.array_element_type e.expr_type;
226
        expr_desc = Expr_access (e, d);
227
      }
228
    in
229
    defvars, new_e
230
    (*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
231
  in
232
  List.fold_left add_offset (defvars, e) offsets
233

    
234
(* Create a (normalized) expression from [ref_e],
235
   replacing description with [norm_d],
236
   taking propagated [offsets] into account
237
   in order to change expression type *)
238
let mk_norm_expr offsets ref_e norm_d =
239
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
240
  let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in
241
  {
242
    ref_e with
243
    expr_desc = norm_d;
244
    expr_type =
245
      Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type;
246
  }
247

    
248
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
249
let normalize_list alias norm_ctx offsets norm_element defvars elist =
250
  List.fold_right
251
    (fun t (defvars, qlist) ->
252
      let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
253
      defvars, norm_t :: qlist)
254
    elist (defvars, [])
255

    
256
let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets
257
    defvars expr =
258
  (* Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.pp expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
259
  match expr.expr_desc with
260
  | Expr_const _ | Expr_ident _ -> unfold_offsets norm_ctx defvars expr offsets
261
  | Expr_array elist ->
262
      let defvars, norm_elist =
263
        normalize_list alias norm_ctx offsets
264
          (fun _ -> normalize_array_expr ~alias:true)
265
          defvars elist
266
      in
267
      let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
268
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
269
  | Expr_power (e1, d) when offsets = [] ->
270
      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
271
      let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
272
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
273
  | Expr_power (e1, _) ->
274
      normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1
275
  | Expr_access (e1, d) ->
276
      normalize_expr ~alias norm_ctx (d :: offsets) defvars e1
277
  | Expr_tuple elist ->
278
      let defvars, norm_elist =
279
        normalize_list alias norm_ctx offsets
280
          (fun alias -> normalize_expr ~alias ~alias_basic:false)
281
          defvars elist
282
      in
283
      defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
284
  | Expr_appl (id, args, None)
285
    when Basic_library.is_homomorphic_fun id
286
         && Types.is_array_type expr.expr_type ->
287
      let defvars, norm_args =
288
        normalize_list alias norm_ctx offsets
289
          (fun _ -> normalize_array_expr ~alias:true)
290
          defvars (expr_list_of_expr args)
291
      in
292
      ( defvars,
293
        mk_norm_expr offsets expr
294
          (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )
295
  | Expr_appl (id, args, None)
296
    when Basic_library.is_expr_internal_fun expr
297
         && not (!params.force_alias_internal_fun || alias_basic) ->
298
      let defvars, norm_args =
299
        normalize_expr ~alias:true norm_ctx offsets defvars args
300
      in
301
      defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
302
  | Expr_appl (id, args, r) ->
303
      let defvars, r =
304
        match r with
305
        | None -> defvars, None
306
        | Some r ->
307
            let defvars, norm_r =
308
              normalize_expr ~alias_basic:true norm_ctx [] defvars r
309
            in
310
            defvars, Some norm_r
311
      in
312
      let defvars, norm_args = normalize_expr norm_ctx [] defvars args in
313
      let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
314
      if offsets <> [] then
315
        let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in
316
        normalize_expr ~alias norm_ctx offsets defvars norm_expr
317
      else
318
        mk_expr_alias_opt
319
          (alias
320
          && (!params.force_alias_internal_fun || alias_basic
321
             || not (Basic_library.is_expr_internal_fun expr)))
322
          norm_ctx defvars norm_expr
323
  | Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) ->
324
      (* Here we differ from Colaco paper: arrows are pushed to the top *)
325
      normalize_expr ~alias norm_ctx offsets defvars (unfold_arrow expr)
326
  | Expr_arrow (e1, e2) ->
327
      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
328
      let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
329
      let norm_expr =
330
        mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2))
331
      in
332
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
333
  | Expr_pre e ->
334
      let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
335
      let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
336
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
337
  | Expr_fby (e1, e2) ->
338
      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
339
      let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
340
      let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
341
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
342
  | Expr_when (e, c, l) ->
343
      let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
344
      defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
345
  | Expr_ite (c, t, e) ->
346
      let defvars, norm_c = normalize_guard norm_ctx defvars c in
347
      let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
348
      let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
349
      let norm_expr =
350
        mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
351
      in
352
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
353
  | Expr_merge (c, hl) ->
354
      let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
355
      let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
356
      mk_expr_alias_opt alias norm_ctx defvars norm_expr
357

    
358
(* Creates a conditional with a merge construct, which is more lazy *)
359
(*
360
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
361
  match expr.expr_desc with
362
  | Expr_ite (c, t, e) ->
363
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
364
  | _ -> assert false
365
*)
366
and normalize_branches norm_ctx offsets defvars hl =
367
  List.fold_right
368
    (fun (t, h) (defvars, norm_q) ->
369
      let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in
370
      defvars, (t, norm_h) :: norm_q)
371
    hl (defvars, [])
372

    
373
and normalize_array_expr ?(alias = true) norm_ctx offsets defvars expr =
374
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
375
  match expr.expr_desc with
376
  | Expr_power (e1, d) when offsets = [] ->
377
      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
378
      defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
379
  | Expr_power (e1, _) ->
380
      normalize_array_expr ~alias norm_ctx (List.tl offsets) defvars e1
381
  | Expr_access (e1, d) ->
382
      normalize_array_expr ~alias norm_ctx (d :: offsets) defvars e1
383
  | Expr_array elist when offsets = [] ->
384
      let defvars, norm_elist =
385
        normalize_list alias norm_ctx offsets
386
          (fun _ -> normalize_array_expr ~alias:true)
387
          defvars elist
388
      in
389
      defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
390
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
391
      let defvars, norm_args =
392
        normalize_list alias norm_ctx offsets
393
          (fun _ -> normalize_array_expr ~alias:true)
394
          defvars (expr_list_of_expr args)
395
      in
396
      ( defvars,
397
        mk_norm_expr offsets expr
398
          (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )
399
  | _ -> normalize_expr ~alias norm_ctx offsets defvars expr
400

    
401
and normalize_cond_expr ?(alias = true) norm_ctx offsets defvars expr =
402
  (* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
403
  match expr.expr_desc with
404
  | Expr_access (e1, d) ->
405
      normalize_cond_expr ~alias norm_ctx (d :: offsets) defvars e1
406
  | Expr_ite (c, t, e) ->
407
      let defvars, norm_c = normalize_guard norm_ctx defvars c in
408
      let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
409
      let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
410
      defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
411
  | Expr_merge (c, hl) ->
412
      let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
413
      defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
414
  | _ when !params.force_alias_ite ->
415
      (* Forcing alias creation for then/else expressions *)
416
      let defvars, norm_expr =
417
        normalize_expr ~alias norm_ctx offsets defvars expr
418
      in
419
      mk_expr_alias_opt true norm_ctx defvars norm_expr
420
  | _ ->
421
      (* default case without the force_alias_ite option *)
422
      normalize_expr ~alias norm_ctx offsets defvars expr
423

    
424
and normalize_guard norm_ctx defvars expr =
425
  let defvars, norm_expr =
426
    normalize_expr ~alias_basic:true norm_ctx [] defvars expr
427
  in
428
  mk_expr_alias_opt true norm_ctx defvars norm_expr
429

    
430
(* outputs cannot be memories as well. If so, introduce new local variable.
431
*)
432
let decouple_outputs norm_ctx defvars eq =
433
  let rec fold_lhs defvars lhs tys cks =
434
    match lhs, tys, cks with
435
    | [], [], [] -> defvars, []
436
    | v :: qv, t :: qt, c :: qc ->
437
        let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
438
        if norm_ctx.is_output v then
439
          let newvar =
440
            mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c
441
          in
442
          let neweq = mkeq eq.eq_loc ([ v ], expr_of_vdecl newvar) in
443
          (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
444
        else (defs_q, vars_q), v :: lhs_q
445
    | _ -> assert false
446
  in
447
  let defvars', lhs' =
448
    fold_lhs defvars eq.eq_lhs
449
      (Types.type_list_of_type eq.eq_rhs.expr_type)
450
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock)
451
  in
452
  defvars', { eq with eq_lhs = lhs' }
453

    
454
let normalize_eq norm_ctx defvars eq =
455
  (*Format.eprintf "normalize_eq %a@." Types.pp eq.eq_rhs.expr_type;*)
456
  match eq.eq_rhs.expr_desc with
457
  | Expr_pre _ | Expr_fby _ ->
458
      let defvars', eq' = decouple_outputs norm_ctx defvars eq in
459
      let (defs', vars'), norm_rhs =
460
        normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs
461
      in
462
      let norm_eq = { eq' with eq_rhs = norm_rhs } in
463
      norm_eq :: defs', vars'
464
  | Expr_array _ ->
465
      let (defs', vars'), norm_rhs =
466
        normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
467
      in
468
      let norm_eq = { eq with eq_rhs = norm_rhs } in
469
      norm_eq :: defs', vars'
470
  | Expr_appl (id, _, None)
471
    when Basic_library.is_homomorphic_fun id
472
         && Types.is_array_type eq.eq_rhs.expr_type ->
473
      let (defs', vars'), norm_rhs =
474
        normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
475
      in
476
      let norm_eq = { eq with eq_rhs = norm_rhs } in
477
      norm_eq :: defs', vars'
478
  | Expr_appl _ ->
479
      let (defs', vars'), norm_rhs =
480
        normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
481
      in
482
      let norm_eq = { eq with eq_rhs = norm_rhs } in
483
      norm_eq :: defs', vars'
484
  | _ ->
485
      let (defs', vars'), norm_rhs =
486
        normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
487
      in
488
      let norm_eq = { eq with eq_rhs = norm_rhs } in
489
      norm_eq :: defs', vars'
490

    
491
let normalize_eq_split norm_ctx defvars eq =
492
  try
493
    let defs, vars = normalize_eq norm_ctx defvars eq in
494
    List.fold_right
495
      (fun eq (def, vars) ->
496
        let eq_defs = Splitting.tuple_split_eq eq in
497
        if eq_defs = [ eq ] then eq :: def, vars
498
        else List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs)
499
      defs ([], vars)
500
  with ex ->
501
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
502
    raise ex
503

    
504
(* Projecting an eexpr to an eexpr associated to a single
505
   variable. Returns the updated ee, the bounded variable and the
506
   associated statement *)
507
let normalize_pred_eexpr norm_ctx (def, vars) ee =
508
  assert (ee.eexpr_quantifiers = []);
509
  (* We do not normalize quantifiers yet. This is for very far future. *)
510
  (* (\* don't do anything if eexpr is just a variable *\)
511
   * let skip =
512
   *   match ee.eexpr_qfexpr.expr_desc with
513
   *   | Expr_ident _ | Expr_const _ -> true
514
   *   | _ -> false
515
   * in
516
   * if skip then None, ee, (def, vars)
517
   * else *)
518
    (* New output variable *)
519
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
520
    let output_var =
521
      mkvar_decl ~var_is_contract:true ee.eexpr_loc
522
        ( output_id,
523
          mktyp ee.eexpr_loc Tydec_bool,
524
          (* It is a predicate, hence a bool *)
525
          mkclock ee.eexpr_loc Ckdec_any,
526
          false (* not a constant *),
527
          None,
528
          None )
529
    in
530
    (* It is a predicate, hence a bool *)
531
    output_var.var_type <- Type_predef.type_bool;
532
    let output_expr = expr_of_vdecl output_var in
533
    (* Rebuilding an eexpr with a silly expression, just a variable *)
534
    let ee' = { ee with eexpr_qfexpr = output_expr } in
535

    
536
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
537
       inline possible calls within, normalize it and type/clock the
538
       result. *)
539
    let eq = mkeq ee.eexpr_loc ([ output_id ], ee.eexpr_qfexpr) in
540

    
541
    (* (\* Inlining any calls *\)
542
     * let nodes = get_nodes decls in
543
     * let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
544
     * let vars, eqs =
545
     *   if calls = [] && not (eq_has_arrows eq) then
546
     *     vars, [eq]    
547
     *   else
548
     *     assert false (\* TODO *\)
549
     * in *)
550

    
551
    (* Normalizing expr and eqs *)
552
    let defs, vars =
553
      List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ]
554
    in
555
    (* let vars = output_var :: vars in *)
556

    
557
    (* let todefine =
558
       List.fold_left
559
         (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
560
         (ISet.add output_id ISet.empty) vars in
561
    *)
562

    
563
    (* Typing / Clocking *)
564
    try
565
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
566

    
567
      (*
568
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
569
    (* Format.eprintf "typing var %s: %a@." output_id Types.pp output_var.var_type; *)
570
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
571
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.pp) env;*)
572
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
573
  (* check that table is empty *)
574
    if (not (ISet.is_empty undefined_vars)) then
575
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
576
    
577
    (*Format.eprintf "normalized eqs %a@.@?" 
578
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
579
         *)
580
      output_var, ee', (defs, vars)
581
    with Types.Error (loc, err) as exc ->
582
      eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee
583
        Types.pp_error err
584
        (pp_comma_list Printers.pp_node_eq)
585
        defs Location.pp loc;
586

    
587
      raise exc
588

    
589
(*
590
  
591
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
592
  (* Calls are first inlined *)
593
  
594
  (*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;  *)
595
  let (new_locals, eqs) =
596
    if calls = [] && not (eq_has_arrows eq) then
597
      (locals, [eq])     
598
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
599
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
600
      (*Format.eprintf "eqs %a@.@?" 
601
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
602
      (new_locals, eqs)
603
*)
604
           (locals, [eq])     
605
 
606
    ) in
607
  (* Normalizing expr and eqs *)
608
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
609
    let todefine = List.fold_left
610
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
611
    (ISet.add output_id ISet.empty) vars in
612
  
613
  try
614
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
615
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
616
    (* Format.eprintf "typing var %s: %a@." output_id Types.pp output_var.var_type; *)
617
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
618
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.pp) env;*)
619
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
620
  (* check that table is empty *)
621
    if (not (ISet.is_empty undefined_vars)) then
622
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
623
    
624
    (*Format.eprintf "normalized eqs %a@.@?" 
625
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
626
    ee.eexpr_normalized <- Some (output_var, defs, vars)
627
    
628
  with (Types.Error (loc,err)) as exc ->
629
    eprintf "Typing error for eexpr %a: %a%a%a@."
630
      Printers.pp_eexpr ee
631
      Types.pp_error err
632
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
633
      Location.pp_loc loc
634
  
635
      
636
    ;
637
    raise exc
638
                                                 *)
639

    
640
(* We use node local vars to make sure we are creating fresh variables *)
641
let normalize_spec parentid (in_vars, out_vars, l_vars) s =
642
  (* Original set of variables actually visible from here: in/out and
643
     spec locals (no node locals) *)
644
  let orig_vars = in_vars @ out_vars @ s.locals in
645
  (* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)
646
  let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
647
  let norm_ctx =
648
    {
649
      parentid;
650
      vars = in_vars @ out_vars @ l_vars;
651
      is_output =
652
        (fun _ -> false) (* no need to introduce fresh variables for outputs *);
653
    }
654
  in
655
  (* Normalizing existing stmts *)
656
  let eqs, auts =
657
    List.fold_right
658
      (fun s (el, al) ->
659
        match s with Eq e -> e :: el, al | Aut a -> el, a :: al)
660
      s.stmts ([], [])
661
  in
662
  if auts != [] then assert false;
663
  (* Automata should be expanded by now. *)
664
  let defsvars = List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
665
  (* Iterate through predicates and normalize them on the go, creating
666
     fresh variables for any guarantees/assumes/require/ensure *)
667
  let process_predicates l defvars =
668
    (* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
669
    let res =
670
      List.fold_right
671
        (fun ee (outputs, accu, defvars) ->
672
          let x, ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in
673
          x :: outputs, ee' :: accu, defvars)
674
        l ([], [], defvars)
675
    in
676
    (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
677
     * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
678
    res
679
  in
680

    
681
  let outs_asm, assume', defsvars = process_predicates s.assume defsvars in
682
  let outs_grt, guarantees', defsvars = process_predicates s.guarantees defsvars in
683
  let outs, modes', (defs, vars) =
684
    List.fold_right
685
      (fun m (outs, accu_m, defsvars) ->
686
        let outs_req, require', defsvars = process_predicates m.require defsvars in
687
        let outs_ens, ensure', defsvars = process_predicates m.ensure defsvars in
688
        outs_req @ outs_ens @ outs,
689
        { m with require = require'; ensure = ensure' } :: accu_m,
690
        defsvars)
691
      s.modes (outs_asm @ outs_grt, [], defsvars)
692
  in
693

    
694
  let new_locals = List.filter not_is_orig_var vars in
695
  (* removing inouts and initial locals ones *)
696
  ( new_locals,
697
    outs,
698
    defs,
699
    {
700
      s with
701
      (* locals = s.locals @ new_locals; *)
702
      stmts = [];
703
      assume = assume';
704
      guarantees = guarantees';
705
      modes = modes';
706
    } )
707
(* let nee _ = () in
708
 *   (\*normalize_eexpr decls iovars in *\)
709
 *   List.iter nee s.assume;
710
 *   List.iter nee s.guarantees;
711
 *   List.iter (fun m -> 
712
 *       List.iter nee m.require;
713
 *     List.iter nee m.ensure
714
 *     ) s.modes; *)
715

    
716
(* The normalization phase introduces new local variables
717
   - output cannot be memories. If this happen, new local variables acting as
718
   memories are introduced. 
719
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
720
   access
721
   Thoses values are shared, ie. no duplicate expressions are introduced.
722

    
723
   Concerning specification, a similar process is applied, replacing an
724
   expression by a list of local variables and definitions
725
*)
726

    
727
(** normalize_node node returns a normalized node, 
728
    ie. 
729
    - updated locals
730
    - new equations
731
    -
732
*)
733
let normalize_node ?(first=true) node =
734
  reset_cpt_fresh ();
735
  let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in
736
  let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
737
  let norm_ctx =
738
    {
739
      parentid = node.node_id;
740
      vars = get_node_vars node;
741
      is_output =
742
        (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
743
    }
744
  in
745

    
746
  let eqs, auts = get_node_eqs node in
747
  if auts != [] then assert false;
748
  (* Automata should be expanded by now. *)
749
  let node_spec, new_vars, new_outs, eqs =
750
    (* Update mutable fields of eexpr to perform normalization of
751
       specification.
752

    
753
       Careful: we do not normalize annotations, since they can have the form
754
       x = (a, b, c) *)
755
    match node.node_spec with
756
    | None | Some (NodeSpec _) ->
757
      node.node_spec, [], [], eqs
758
    | Some (Contract s) ->
759
      let new_locals, new_outs, new_stmts, s' =
760
        normalize_spec node.node_id
761
          (node.node_inputs, node.node_outputs, node.node_locals)
762
          s
763
      in
764
      (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
765
       * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
766
      Some (Contract s'), new_locals, new_outs, new_stmts @ eqs
767
  in
768
  let defs, vars =
769
    List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs
770
  in
771
  (* Normalize the asserts *)
772
  let vars, assert_defs, node_asserts =
773
    List.fold_left
774
      (fun (vars, def_accu, assert_accu) assert_ ->
775
        let assert_expr = assert_.assert_expr in
776
        let (defs, vars'), expr =
777
          normalize_expr ~alias:true
778
            (* forcing introduction of new equations for fcn calls *)
779
            norm_ctx []
780
            (* empty offset for arrays *)
781
            ([], vars)
782
            (* defvar only contains vars *)
783
            assert_expr
784
        in
785
        (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
786
        ( vars',
787
          defs @ def_accu,
788
          { assert_ with assert_expr = expr } :: assert_accu ))
789
      (vars, [], []) node.node_asserts
790
  in
791
  let new_locals = List.filter not_is_orig_var vars in
792

    
793
  (* we filter out inout
794
     vars and initial locals ones *)
795
  let node_locals = node.node_locals @ new_locals in
796

    
797
  (* we add again, at the
798
     beginning of the list the
799
     local declared ones *)
800
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
801

    
802
  (* Updating annotations: traceability and machine types for fresh variables *)
803

    
804
  (* Compute traceability info:
805
     - gather newly bound variables
806
     - compute the associated expression without aliases
807
  *)
808
  let new_annots =
809
    if !Options.traces then
810
      let diff_vars =
811
        List.filter (fun v -> not (List.mem v node.node_locals)) node_locals
812
      in
813
      let norm_traceability =
814
        {
815
          annots =
816
            List.map
817
              (fun v ->
818
                let eq =
819
                  try
820
                    List.find
821
                      (fun eq ->
822
                        List.exists (fun v' -> v' = v.var_id) eq.eq_lhs)
823
                      (defs @ assert_defs)
824
                  with Not_found ->
825
                    Format.eprintf
826
                      "Traceability annotation generation: var %s not found@."
827
                      v.var_id;
828
                    assert false
829
                in
830
                let expr =
831
                  substitute_expr diff_vars (defs @ assert_defs) eq.eq_rhs
832
                in
833
                let pair =
834
                  mkeexpr expr.expr_loc
835
                    (mkexpr expr.expr_loc
836
                       (Expr_tuple
837
                          [ expr_of_ident v.var_id expr.expr_loc; expr ]))
838
                in
839
                Annotations.add_expr_ann node.node_id pair.eexpr_tag
840
                  [ "traceability" ];
841
                [ "traceability" ], pair)
842
              diff_vars;
843
          annot_loc = Location.dummy;
844
        }
845
      in
846
      norm_traceability :: node.node_annot
847
    else node.node_annot
848
  in
849

    
850
  let node_annot =
851
    List.fold_left
852
      (fun annots v ->
853
        if Machine_types.is_active && Machine_types.is_exportable v then (
854
          let typ = Machine_types.get_specified_type v in
855
          let typ_name = Machine_types.type_name typ in
856

    
857
          let loc = v.var_loc in
858
          let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in
859
          let pair =
860
            expr_to_eexpr
861
              (expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])
862
          in
863
          Annotations.add_expr_ann node.node_id pair.eexpr_tag
864
            Machine_types.keywords;
865
          { annots = [ Machine_types.keywords, pair ]; annot_loc = loc }
866
          :: annots)
867
        else annots)
868
      new_annots new_locals
869
  in
870

    
871
  let node_inputs, node_outputs =
872
    if node.node_iscontract && first then
873
      node.node_inputs @ node.node_outputs, new_outs
874
    else
875
      node.node_inputs, node.node_outputs
876
  in
877

    
878
  let node =
879
    {
880
      node with
881
      node_inputs;
882
      node_outputs;
883
      node_locals;
884
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
885
      node_asserts;
886
      node_annot;
887
      node_spec
888
    }
889
  in
890
  (*Printers.pp_node Format.err_formatter node;*)
891
  node
892

    
893
let normalize_inode nd =
894
  reset_cpt_fresh ();
895
  match nd.nodei_spec with
896
  | None | Some (NodeSpec _) -> nd
897
  | Some (Contract _) -> assert false
898

    
899
let normalize_decl ?first (decl : top_decl) : top_decl =
900
  match decl.top_decl_desc with
901
  | Node nd ->
902
      let decl' = { decl with top_decl_desc = Node (normalize_node ?first nd) } in
903
      update_node nd.node_id decl';
904
      decl'
905
  | ImportedNode nd ->
906
      let decl' =
907
        { decl with top_decl_desc = ImportedNode (normalize_inode nd) }
908
      in
909
      update_node nd.nodei_id decl';
910
      decl'
911
  | Include _ | Open _ | Const _ | TypeDef _ -> decl
912

    
913
let normalize_prog ?first p decls =
914
  (* Backend specific configurations for normalization *)
915
  params := p;
916

    
917
  (* Main algorithm: iterates over nodes *)
918
  List.map (normalize_decl ?first) decls
919

    
920
(* Fake interface for outside uses *)
921
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
922
  mk_expr_alias_opt opt
923
    { parentid; vars = ctx_vars; is_output = (fun _ -> false) }
924
    (defs, vars) expr
925

    
926
(* Local Variables: *)
927
(* compile-command:"make -C .." *)
928
(* End: *)
(58-58/99)