Project

General

Profile

Download (33.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
  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_loc (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.eq_clock 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.print_ty expr.expr_type Clocks.print_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.print_ty expr.expr_type Clocks.print_ck
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.print_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.print_ty 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.print_ty 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.print_ty 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 is 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 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 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
    let output_expr = expr_of_vdecl output_var in
531
    (* Rebuilding an eexpr with a silly expression, just a variable *)
532
    let ee' = { ee with eexpr_qfexpr = output_expr } in
533

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

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

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

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

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

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

    
585
      raise exc
586

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

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

    
679
  let assume', defsvars = process_predicates s.assume defsvars in
680
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
681
  let modes', (defs, vars) =
682
    List.fold_right
683
      (fun m (accu_m, defsvars) ->
684
        let require', defsvars = process_predicates m.require defsvars in
685
        let ensure', defsvars = process_predicates m.ensure defsvars in
686
        { m with require = require'; ensure = ensure' } :: accu_m, defsvars)
687
      s.modes ([], defsvars)
688
  in
689

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

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

    
718
   Concerning specification, a similar process is applied, replacing an
719
   expression by a list of local variables and definitions
720
*)
721

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

    
741
  let eqs, auts = get_node_eqs node in
742
  if auts != [] then assert false;
743
  (* Automata should be expanded by now. *)
744
  let spec, new_vars, eqs =
745
    (* Update mutable fields of eexpr to perform normalization of
746
       specification.
747

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

    
787
  (* we filter out inout
788
     vars and initial locals ones *)
789
  let all_locals = node.node_locals @ new_locals in
790

    
791
  (* we add again, at the
792
     beginning of the list the
793
     local declared ones *)
794
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
795

    
796
  (* Updating annotations: traceability and machine types for fresh variables *)
797

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

    
844
  let new_annots =
845
    List.fold_left
846
      (fun annots v ->
847
        if Machine_types.is_active && Machine_types.is_exportable v then (
848
          let typ = Machine_types.get_specified_type v in
849
          let typ_name = Machine_types.type_name typ in
850

    
851
          let loc = v.var_loc in
852
          let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in
853
          let pair =
854
            expr_to_eexpr
855
              (expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])
856
          in
857
          Annotations.add_expr_ann node.node_id pair.eexpr_tag
858
            Machine_types.keyword;
859
          { annots = [ Machine_types.keyword, pair ]; annot_loc = loc }
860
          :: annots)
861
        else annots)
862
      new_annots new_locals
863
  in
864

    
865
  let node =
866
    {
867
      node with
868
      node_locals = all_locals;
869
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
870
      node_asserts = asserts;
871
      node_annot = new_annots;
872
      node_spec = spec;
873
    }
874
  in
875
  (*Printers.pp_node Format.err_formatter node;*)
876
  node
877

    
878
let normalize_inode nd =
879
  reset_cpt_fresh ();
880
  match nd.nodei_spec with
881
  | None | Some (NodeSpec _) -> nd
882
  | Some (Contract _) -> assert false
883

    
884
let normalize_decl (decl : top_decl) : top_decl =
885
  match decl.top_decl_desc with
886
  | Node nd ->
887
      let decl' = { decl with top_decl_desc = Node (normalize_node nd) } in
888
      update_node nd.node_id decl';
889
      decl'
890
  | ImportedNode nd ->
891
      let decl' =
892
        { decl with top_decl_desc = ImportedNode (normalize_inode nd) }
893
      in
894
      update_node nd.nodei_id decl';
895
      decl'
896
  | Include _ | Open _ | Const _ | TypeDef _ -> decl
897

    
898
let normalize_prog p decls =
899
  (* Backend specific configurations for normalization *)
900
  params := p;
901

    
902
  (* Main algorithm: iterates over nodes *)
903
  List.map normalize_decl decls
904

    
905
(* Fake interface for outside uses *)
906
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
907
  mk_expr_alias_opt opt
908
    { parentid; vars = ctx_vars; is_output = (fun _ -> false) }
909
    (defs, vars) expr
910

    
911
(* Local Variables: *)
912
(* compile-command:"make -C .." *)
913
(* End: *)
(43-43/66)