Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/normalization.ml
16 16

  
17 17
(* To update thank to some command line options *)
18 18
let debug = ref false
19
          
19

  
20 20
(** Normalisation iters through the AST of expressions and bind fresh definition
21 21
    when some criteria are met. This creation of fresh definition is performed by
22 22
    the function mk_expr_alias_opt when the alias argument is on.
......
32 32
      definitions.
33 33
*)
34 34

  
35
type param_t =
36
  {
37
    unfold_arrow_active: bool;
38
    force_alias_ite: bool;
39
    force_alias_internal_fun: bool;
40
  }
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
    }
41 48

  
42
let params = ref
43
               {
44
                 unfold_arrow_active = false;
45
                 force_alias_ite = false;
46
                 force_alias_internal_fun =false;
47
               }
49
type norm_ctx_t = {
50
  parentid : ident;
51
  vars : var_decl list;
52
  is_output : ident -> bool;
53
}
48 54

  
49
type norm_ctx_t =
55
let expr_true loc ck =
50 56
  {
51
    parentid: ident;
52
    vars: var_decl list;
53
    is_output: ident -> bool; 
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;
54 64
  }
55 65

  
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 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 }
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
  }
74 76

  
75 77
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 }
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
  }
83 87

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

  
88 92
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

  
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
97 99

  
98 100
(* Get the equation in [defs] with [expr] as rhs, if any *)
99 101
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
  
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

  
104 111
(* Replace [expr] with (tuple of) [locals] *)
105 112
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) }
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
      }
114 123

  
115
  
116 124
(* IS IT USED ? TODO 
117 125
(* Create an alias for [expr], if none exists yet *)
118 126
let mk_expr_alias (parentid, vars) (defs, vars) expr =
......
133 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; *)
134 142
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
135 143
 *)
136
  
144

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

  
......
141 149
 *)
142 150
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
143 151
  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);
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);
146 156
  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 *) 
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 *)
184 202
let mk_dim_alias opt norm_ctx (defs, vars) dim =
185 203
  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

  
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 *)
195 213

  
196 214
let unfold_offsets norm_ctx defvars e offsets =
197 215
  let add_offset (defvars, e) d =
198 216
    (*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
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
202 223
        expr_tag = Utils.new_tag ();
203 224
        expr_loc = d.Dimension.dim_loc;
204 225
        expr_type = Types.array_element_type e.expr_type;
205
        expr_desc = Expr_access (e, d) }
226
        expr_desc = Expr_access (e, d);
227
      }
206 228
    in
207 229
    defvars, new_e
208
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
230
    (*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
209 231
  in
210
  List.fold_left add_offset (defvars, e) offsets 
232
  List.fold_left add_offset (defvars, e) offsets
211 233

  
212
      
213 234
(* Create a (normalized) expression from [ref_e],
214 235
   replacing description with [norm_d],
215 236
   taking propagated [offsets] into account
216 237
   in order to change expression type *)
217 238
let mk_norm_expr offsets ref_e norm_d =
218 239
  (*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
240
  let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in
241
  {
242
    ref_e with
222 243
    expr_desc = norm_d;
223
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
224
														
244
    expr_type =
245
      Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type;
246
  }
247

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

  
233
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr =
256
let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets
257
    defvars expr =
234 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; *)
235 259
  match expr.expr_desc with
236
  | Expr_const _
237
    | Expr_ident _ ->
238
     unfold_offsets norm_ctx defvars expr offsets
260
  | Expr_const _ | Expr_ident _ -> unfold_offsets norm_ctx defvars expr offsets
239 261
  | 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
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
243 269
  | 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
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
247 273
  | Expr_power (e1, _) ->
248
     normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
274
      normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1
249 275
  | Expr_access (e1, d) ->
250
     normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 
251
    
276
      normalize_expr ~alias norm_ctx (d :: offsets) defvars e1
252 277
  | 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)
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)
256 284
  | 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))
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))
273 302
  | 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
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
291 323
  | 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
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
299 333
  | 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
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
303 337
  | 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
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
308 342
  | 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))
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))
311 345
  | 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
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
317 353
  | 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
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
321 357

  
322 358
(* Creates a conditional with a merge construct, which is more lazy *)
323 359
(*
......
330 366
and normalize_branches norm_ctx offsets defvars hl =
331 367
  List.fold_right
332 368
    (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
    )
369
      let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in
370
      defvars, (t, norm_h) :: norm_q)
336 371
    hl (defvars, [])
337 372

  
338
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
373
and normalize_array_expr ?(alias = true) norm_ctx offsets defvars expr =
339 374
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
340 375
  match expr.expr_desc with
341 376
  | 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))
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))
344 379
  | 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
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
347 383
  | 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)
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)
350 390
  | 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 =
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 =
356 402
  (* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
357 403
  match expr.expr_desc with
358 404
  | Expr_access (e1, d) ->
359
     normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1
405
      normalize_cond_expr ~alias norm_ctx (d :: offsets) defvars e1
360 406
  | 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))
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))
365 411
  | 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))
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))
368 414
  | _ 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
       
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

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

  
381 430
(* outputs cannot be memories as well. If so, introduce new local variable.
......
383 432
let decouple_outputs norm_ctx defvars eq =
384 433
  let rec fold_lhs defvars lhs tys cks =
385 434
    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
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
396 447
  let defvars', lhs' =
397
    fold_lhs
398
      defvars
399
      eq.eq_lhs
448
    fold_lhs defvars eq.eq_lhs
400 449
      (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' }
450
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock)
451
  in
452
  defvars', { eq with eq_lhs = lhs' }
403 453

  
404 454
let normalize_eq norm_ctx defvars eq =
405
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
455
  (*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
406 456
  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')
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'
413 464
  | 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')
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'
421 478
  | 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')
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'
425 484
  | _ ->
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'
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'
429 490

  
430 491
let normalize_eq_split norm_ctx defvars eq =
431 492
  try
432 493
    let defs, vars = normalize_eq norm_ctx defvars eq in
433
    List.fold_right (fun eq (def, vars) -> 
494
    List.fold_right
495
      (fun eq (def, vars) ->
434 496
        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 -> (
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 ->
442 501
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
443 502
    raise ex
444
  )
445 503

  
446 504
(* Projecting an eexpr to an eexpr associated to a single
447 505
   variable. Returns the updated ee, the bounded variable and the
448 506
   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. *)
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. *)
451 510
  (* don't do anything is eexpr is just a variable *)
452 511
  let skip =
453 512
    match ee.eexpr_qfexpr.expr_desc with
454 513
    | Expr_ident _ | Expr_const _ -> true
455 514
    | _ -> false
456 515
  in
457
  if skip then
458
    ee, (def, vars)
459
  else (
516
  if skip then ee, (def, vars)
517
  else
460 518
    (* New output variable *)
461 519
    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
        ) 
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 )
472 529
    in
473 530
    let output_expr = expr_of_vdecl output_var in
474 531
    (* Rebuilding an eexpr with a silly expression, just a variable *)
......
476 533

  
477 534
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
478 535
       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

  
536
       result. *)
537
    let eq = mkeq ee.eexpr_loc ([ output_id ], ee.eexpr_qfexpr) in
482 538

  
483 539
    (* (\* Inlining any calls *\)
484 540
     * let nodes = get_nodes decls in
......
489 545
     *   else
490 546
     *     assert false (\* TODO *\)
491 547
     * in *)
492
    
548

  
493 549
    (* 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
 *)      
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
    *)
501 560

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

  
565
      (*
506 566
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
507 567
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
508 568
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
......
515 575
    (*Format.eprintf "normalized eqs %a@.@?" 
516 576
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
517 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;
518 584

  
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
   (*
585
      raise exc
586

  
587
(*
535 588
  
536 589
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
537 590
  (* Calls are first inlined *)
......
580 633
      
581 634
    ;
582 635
    raise exc
583
                                                 *)    
584
 
636
                                                 *)
585 637

  
586
(* We use node local vars to make sure we are creating fresh variables *) 
638
(* We use node local vars to make sure we are creating fresh variables *)
587 639
let normalize_spec parentid (in_vars, out_vars, l_vars) s =
588 640
  (* Original set of variables actually visible from here: in/out and
589 641
     spec locals (no node locals) *)
590 642
  let orig_vars = in_vars @ out_vars @ s.locals in
591 643
  (* 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;
644
  let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
645
  let norm_ctx =
646
    {
647
      parentid;
596 648
      vars = in_vars @ out_vars @ l_vars;
597
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
649
      is_output =
650
        (fun _ -> false) (* no need to introduce fresh variables for outputs *);
598 651
    }
599 652
  in
600 653
  (* 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
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 ([], [])
605 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
606 663
  (* Iterate through predicates and normalize them on the go, creating
607 664
     fresh variables for any guarantees/assumes/require/ensure *)
608 665
  let process_predicates l defvars =
609 666
    (* 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)
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)
614 673
    in
615 674
    (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
616 675
     * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
617 676
    res
618 677
  in
619 678

  
620
  
621 679
  let assume', defsvars = process_predicates s.assume defsvars in
622 680
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
623 681
  let modes', (defs, vars) =
624
    List.fold_right (
625
        fun m (accu_m, defsvars) ->
682
    List.fold_right
683
      (fun m (accu_m, defsvars) ->
626 684
        let require', defsvars = process_predicates m.require defsvars in
627 685
        let ensure', defsvars = process_predicates m.ensure defsvars in
628
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
629
      ) s.modes ([], defsvars)
686
        { m with require = require'; ensure = ensure' } :: accu_m, defsvars)
687
      s.modes ([], defsvars)
630 688
  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
  }
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
    } )
641 702
(* let nee _ = () in
642 703
 *   (\*normalize_eexpr decls iovars in *\)
643 704
 *   List.iter nee s.assume;
......
646 707
 *       List.iter nee m.require;
647 708
 *     List.iter nee m.ensure
648 709
 *     ) s.modes; *)
649
   
650 710

  
651
                                                                     
652
  
653
  
654
    
655 711
(* The normalization phase introduces new local variables
656 712
   - output cannot be memories. If this happen, new local variables acting as
657 713
   memories are introduced. 
......
671 727
*)
672 728
let normalize_node node =
673 729
  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 = {
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
    {
678 734
      parentid = node.node_id;
679 735
      vars = get_node_vars node;
680
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
736
      is_output =
737
        (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
681 738
    }
682 739
  in
683 740

  
684 741
  let eqs, auts = get_node_eqs node in
685
  if auts != [] then assert false; (* Automata should be expanded by now. *)
742
  if auts != [] then assert false;
743
  (* Automata should be expanded by now. *)
686 744
  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
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
706 761
  in
707 762
  let defs, vars =
708
    List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
763
    List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs
764
  in
709 765
  (* Normalize the asserts *)
710 766
  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
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
722 779
        (*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;*)
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
732 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;*)
733 795

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

  
736 798
  (* Compute traceability info:
737 799
     - gather newly bound variables
738 800
     - compute the associated expression without aliases
739
   *)
801
  *)
740 802
  let new_annots =
741 803
    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
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
767 842
  in
768 843

  
769 844
  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
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
788 863
  in
789
  
790
  
864

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

  
803 878
let normalize_inode nd =
804 879
  reset_cpt_fresh ();
805 880
  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 =
881
  | None | Some (NodeSpec _) -> nd
882
  | Some (Contract _) -> assert false
883

  
884
let normalize_decl (decl : top_decl) : top_decl =
810 885
  match decl.top_decl_desc with
811 886
  | Node nd ->
812
     let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
813
     update_node nd.node_id decl';
814
     decl'
887
      let decl' = { decl with top_decl_desc = Node (normalize_node nd) } in
888
      update_node nd.node_id decl';
889
      decl'
815 890
  | 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
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
821 897

  
822 898
let normalize_prog p decls =
823 899
  (* Backend specific configurations for normalization *)
......
826 902
  (* Main algorithm: iterates over nodes *)
827 903
  List.map normalize_decl decls
828 904

  
829

  
830 905
(* Fake interface for outside uses *)
831 906
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
907
  mk_expr_alias_opt opt
908
    { parentid; vars = ctx_vars; is_output = (fun _ -> false) }
909
    (defs, vars) expr
837 910

  
838
    
839
           (* Local Variables: *)
840
           (* compile-command:"make -C .." *)
841
           (* End: *)
842
    
911
(* Local Variables: *)
912
(* compile-command:"make -C .." *)
913
(* End: *)

Also available in: Unified diff