Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 684d39e7

History | View | Annotate | Download (25.6 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
12
open Utils
13 8446bf03 ploc
open Lustre_types
14 22fe1c93 ploc
open Corelang
15
open Format
16
17 27dc3869 ploc
(** Normalisation iters through the AST of expressions and bind fresh definition
18
    when some criteria are met. This creation of fresh definition is performed by
19
    the function mk_expr_alias_opt when the alias argument is on.
20
21
    Initial expressions, ie expressions attached a variable in an equation
22
    definition are not aliased. This non-alias feature is propagated in the
23
    expression AST for array access and power construct, tuple, and some special
24
    cases of arrows.
25
26
    Two global variables may impact the normalization process:
27
    - unfold_arrow_active
28
    - force_alias_ite: when set, bind a fresh alias for then and else
29
      definitions.
30
*)
31
32 ad4774b0 ploc
type param_t =
33
  {
34
    unfold_arrow_active: bool;
35
    force_alias_ite: bool;
36
    force_alias_internal_fun: bool;
37
  }
38
39
let params = ref
40
               {
41
                 unfold_arrow_active = false;
42
                 force_alias_ite = false;
43
                 force_alias_internal_fun =false;
44
               }
45 27dc3869 ploc
46
  
47 2e6f9ba8 xthirioux
let expr_true loc ck =
48
{ expr_tag = Utils.new_tag ();
49
  expr_desc = Expr_const (Const_tag tag_true);
50
  expr_type = Type_predef.type_bool;
51
  expr_clock = ck;
52
  expr_delay = Delay.new_var ();
53
  expr_annot = None;
54
  expr_loc = loc }
55
56
let expr_false loc ck =
57
{ expr_tag = Utils.new_tag ();
58
  expr_desc = Expr_const (Const_tag tag_false);
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
let expr_once loc ck =
66
 { expr_tag = Utils.new_tag ();
67
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
68
  expr_type = Type_predef.type_bool;
69
  expr_clock = ck;
70
  expr_delay = Delay.new_var ();
71
  expr_annot = None;
72
  expr_loc = loc }
73
74
let is_expr_once =
75
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
76
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
77
78
let unfold_arrow expr =
79
 match expr.expr_desc with
80
 | Expr_arrow (e1, e2) ->
81
    let loc = expr.expr_loc in
82 a38c681e xthirioux
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
83 2e6f9ba8 xthirioux
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
84
 | _                   -> assert false
85
86 22fe1c93 ploc
87
88
(* Get the equation in [defs] with [expr] as rhs, if any *)
89
let get_expr_alias defs expr =
90 0bd19a92 THIRIOUX Xavier
 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)
91 22fe1c93 ploc
 with
92 e49b6d55 xavier.thirioux
 | Not_found -> None
93
  
94 22fe1c93 ploc
(* Replace [expr] with (tuple of) [locals] *)
95
let replace_expr locals expr =
96
 match locals with
97
 | []  -> assert false
98
 | [v] -> { expr with
99
   expr_tag = Utils.new_tag ();
100
   expr_desc = Expr_ident v.var_id }
101
 | _   -> { expr with
102
   expr_tag = Utils.new_tag ();
103 fc886259 xthirioux
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
104 22fe1c93 ploc
105
let unfold_offsets e offsets =
106
  let add_offset e d =
107 fc886259 xthirioux
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
108
    let res = *)
109 22fe1c93 ploc
    { e with
110
      expr_tag = Utils.new_tag ();
111
      expr_loc = d.Dimension.dim_loc;
112
      expr_type = Types.array_element_type e.expr_type;
113 fc886259 xthirioux
      expr_desc = Expr_access (e, d) }
114
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
115
  in
116 22fe1c93 ploc
 List.fold_left add_offset e offsets
117
118
(* Create an alias for [expr], if none exists yet *)
119
let mk_expr_alias node (defs, vars) expr =
120 a38c681e xthirioux
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
121 22fe1c93 ploc
  match get_expr_alias defs expr with
122
  | Some eq ->
123
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
124
    (defs, vars), replace_expr aliases expr
125
  | None    ->
126
    let new_aliases =
127
      List.map2
128
	(mk_fresh_var node expr.expr_loc)
129
	(Types.type_list_of_type expr.expr_type)
130
	(Clocks.clock_list_of_clock expr.expr_clock) in
131
    let new_def =
132
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
133 3ca6d126 ploc
    in
134 fc886259 xthirioux
    (* 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; *)
135 3ca6d126 ploc
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
136 22fe1c93 ploc
137 d4807c3d xthirioux
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
138
   and [opt] is true *)
139 04a63d25 xthirioux
let mk_expr_alias_opt opt node (defs, vars) expr =
140
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
141 d4807c3d xthirioux
  match expr.expr_desc with
142
  | Expr_ident alias ->
143 04a63d25 xthirioux
    (defs, vars), expr
144 8deaa2dd tkahsai
  | _                ->
145 04a63d25 xthirioux
    match get_expr_alias defs expr with
146
    | Some eq ->
147 c35de73b ploc
       (* Format.eprintf "Found a preexisting definition@."; *)
148 04a63d25 xthirioux
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
149
      (defs, vars), replace_expr aliases expr
150
    | None    ->
151 c35de73b ploc
       (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
152
        * Format.eprintf "existing defs are: @[[%a@]]@."
153
        *   (fprintf_list ~sep:"@ "(fun fmt eq ->
154
        *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
155
        *          Clocks.print_ck eq.eq_rhs.expr_clock
156
        *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
157
        *          (is_eq_expr eq.eq_rhs expr)
158
        *          Printers.pp_node_eq eq))
159
        *   defs; *)
160 04a63d25 xthirioux
      if opt
161
      then
162
	let new_aliases =
163
	  List.map2
164
	    (mk_fresh_var node expr.expr_loc)
165
	    (Types.type_list_of_type expr.expr_type)
166
	    (Clocks.clock_list_of_clock expr.expr_clock) in
167
	let new_def =
168
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
169 66359a5e ploc
	in
170
	(* Typing and Registering machine type *) 
171 f4050bef ploc
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
172 66359a5e ploc
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
173 04a63d25 xthirioux
      else
174
	(defs, vars), expr
175 22fe1c93 ploc
176 8deaa2dd tkahsai
(* Create a (normalized) expression from [ref_e],
177 22fe1c93 ploc
   replacing description with [norm_d],
178 8deaa2dd tkahsai
   taking propagated [offsets] into account
179 22fe1c93 ploc
   in order to change expression type *)
180
let mk_norm_expr offsets ref_e norm_d =
181 e49b6d55 xavier.thirioux
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
182 22fe1c93 ploc
  let drop_array_type ty =
183
    Types.map_tuple_type Types.array_element_type ty in
184
  { ref_e with
185
    expr_desc = norm_d;
186
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
187 e49b6d55 xavier.thirioux
														
188 22fe1c93 ploc
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
189
let rec normalize_list alias node offsets norm_element defvars elist =
190
  List.fold_right
191
    (fun t (defvars, qlist) ->
192
      let defvars, norm_t = norm_element alias node offsets defvars t in
193
      (defvars, norm_t :: qlist)
194
    ) elist (defvars, [])
195
196 0a10042e ploc
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =
197 e49b6d55 xavier.thirioux
  (*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;*)
198 22fe1c93 ploc
  match expr.expr_desc with
199 8deaa2dd tkahsai
  | Expr_const _
200 22fe1c93 ploc
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
201
  | Expr_array elist ->
202 0a10042e ploc
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
203
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
204
     mk_expr_alias_opt alias node defvars norm_expr
205 22fe1c93 ploc
  | Expr_power (e1, d) when offsets = [] ->
206 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
207
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
208
     mk_expr_alias_opt alias node defvars norm_expr
209 22fe1c93 ploc
  | Expr_power (e1, d) ->
210 0a10042e ploc
     normalize_expr ~alias:alias node (List.tl offsets) defvars e1
211 22fe1c93 ploc
  | Expr_access (e1, d) ->
212 0a10042e ploc
     normalize_expr ~alias:alias node (d::offsets) defvars e1
213 8deaa2dd tkahsai
  | Expr_tuple elist ->
214 0a10042e ploc
     let defvars, norm_elist =
215
       normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
216
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
217 8deaa2dd tkahsai
  | Expr_appl (id, args, None)
218 04a63d25 xthirioux
      when Basic_library.is_homomorphic_fun id 
219 af5af1e8 ploc
	&& Types.is_array_type expr.expr_type ->
220 0a10042e ploc
     let defvars, norm_args =
221
       normalize_list
222
	 alias
223
	 node
224
	 offsets
225
	 (fun _ -> normalize_array_expr ~alias:true)
226
	 defvars
227
	 (expr_list_of_expr args)
228
     in
229
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
230 3436d1a6 ploc
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
231 ad4774b0 ploc
      && not (!params.force_alias_internal_fun || alias_basic) ->
232 0a10042e ploc
     let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
233
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
234 22fe1c93 ploc
  | Expr_appl (id, args, r) ->
235 0a10042e ploc
     let defvars, r =
236
       match r with
237
       | None -> defvars, None
238
       | Some r ->
239
	  let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in
240
	  defvars, Some norm_r
241
     in
242
     let defvars, norm_args = normalize_expr node [] defvars args in
243
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
244
     if offsets <> []
245
     then
246
       let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
247
       normalize_expr ~alias:alias node offsets defvars norm_expr
248
     else
249 ad4774b0 ploc
       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
250 0a10042e ploc
				    || not (Basic_library.is_expr_internal_fun expr)))
251
	 node defvars norm_expr
252 ad4774b0 ploc
  | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
253 0a10042e ploc
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
254
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
255 2e6f9ba8 xthirioux
  | Expr_arrow (e1,e2) ->
256 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
257
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
258
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
259
     mk_expr_alias_opt alias node defvars norm_expr
260 22fe1c93 ploc
  | Expr_pre e ->
261 0a10042e ploc
     let defvars, norm_e = normalize_expr node offsets defvars e in
262
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
263
     mk_expr_alias_opt alias node defvars norm_expr
264 22fe1c93 ploc
  | Expr_fby (e1, e2) ->
265 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
266
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
267
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
268
     mk_expr_alias_opt alias node defvars norm_expr
269 22fe1c93 ploc
  | Expr_when (e, c, l) ->
270 0a10042e ploc
     let defvars, norm_e = normalize_expr node offsets defvars e in
271
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
272 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
273 0a10042e ploc
     let defvars, norm_c = normalize_guard node defvars c in
274
     let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
275
     let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
276
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
277
     mk_expr_alias_opt alias node defvars norm_expr
278 22fe1c93 ploc
  | Expr_merge (c, hl) ->
279 0a10042e ploc
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
280
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
281
     mk_expr_alias_opt alias node defvars norm_expr
282 8deaa2dd tkahsai
283 52cfee34 xthirioux
(* Creates a conditional with a merge construct, which is more lazy *)
284
(*
285 0a10042e ploc
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
286
  match expr.expr_desc with
287
  | Expr_ite (c, t, e) ->
288
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
289
  | _ -> assert false
290 52cfee34 xthirioux
*)
291 22fe1c93 ploc
and normalize_branches node offsets defvars hl =
292 0a10042e ploc
  List.fold_right
293
    (fun (t, h) (defvars, norm_q) ->
294
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
295
      defvars, (t, norm_h) :: norm_q
296
    )
297
    hl (defvars, [])
298 22fe1c93 ploc
299
and normalize_array_expr ?(alias=true) node offsets defvars expr =
300 04a63d25 xthirioux
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
301 22fe1c93 ploc
  match expr.expr_desc with
302
  | Expr_power (e1, d) when offsets = [] ->
303 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
304
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
305 22fe1c93 ploc
  | Expr_power (e1, d) ->
306 0a10042e ploc
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
307 22fe1c93 ploc
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
308
  | Expr_array elist when offsets = [] ->
309 0a10042e ploc
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
310
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
311 04a63d25 xthirioux
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
312 0a10042e ploc
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
313
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
314 22fe1c93 ploc
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
315
316
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
317
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
318
  match expr.expr_desc with
319
  | Expr_access (e1, d) ->
320 0a10042e ploc
     normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
321 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
322 0a10042e ploc
     let defvars, norm_c = normalize_guard node defvars c in
323
     let defvars, norm_t = normalize_cond_expr node offsets defvars t in
324
     let defvars, norm_e = normalize_cond_expr node offsets defvars e in
325
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
326 22fe1c93 ploc
  | Expr_merge (c, hl) ->
327 0a10042e ploc
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
328
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
329 ad4774b0 ploc
  | _ when !params.force_alias_ite ->
330 27dc3869 ploc
     (* Forcing alias creation for then/else expressions *)
331
     let defvars, norm_expr =
332
       normalize_expr ~alias:alias node offsets defvars expr
333
     in
334
     mk_expr_alias_opt true node defvars norm_expr
335
  | _ -> (* default case without the force_alias_ite option *)
336
     normalize_expr ~alias:alias node offsets defvars expr
337 0a10042e ploc
       
338 22fe1c93 ploc
and normalize_guard node defvars expr =
339 0a10042e ploc
  let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in
340 d4807c3d xthirioux
  mk_expr_alias_opt true node defvars norm_expr
341 22fe1c93 ploc
342
(* outputs cannot be memories as well. If so, introduce new local variable.
343
*)
344
let decouple_outputs node defvars eq =
345
  let rec fold_lhs defvars lhs tys cks =
346 a742719e ploc
    match lhs, tys, cks with
347
    | [], [], []          -> defvars, []
348
    | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
349
			     if List.exists (fun o -> o.var_id = v) node.node_outputs
350
			     then
351
			       let newvar = mk_fresh_var node eq.eq_loc t c in
352
			       let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
353
			       (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
354
			     else
355
			       (defs_q, vars_q), v::lhs_q
356
    | _                   -> assert false in
357 22fe1c93 ploc
  let defvars', lhs' =
358
    fold_lhs
359
      defvars
360
      eq.eq_lhs
361
      (Types.type_list_of_type eq.eq_rhs.expr_type)
362
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
363
  defvars', {eq with eq_lhs = lhs' }
364
365 8deaa2dd tkahsai
let rec normalize_eq node defvars eq =
366 04a63d25 xthirioux
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
367 22fe1c93 ploc
  match eq.eq_rhs.expr_desc with
368
  | Expr_pre _
369
  | Expr_fby _  ->
370
    let (defvars', eq') = decouple_outputs node defvars eq in
371
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
372
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
373
    (norm_eq::defs', vars')
374
  | Expr_array _ ->
375
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
376
    let norm_eq = { eq with eq_rhs = norm_rhs } in
377
    (norm_eq::defs', vars')
378 04a63d25 xthirioux
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
379 22fe1c93 ploc
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
380
    let norm_eq = { eq with eq_rhs = norm_rhs } in
381
    (norm_eq::defs', vars')
382
  | Expr_appl _ ->
383
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
384
    let norm_eq = { eq with eq_rhs = norm_rhs } in
385
    (norm_eq::defs', vars')
386
  | _ ->
387
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
388
    let norm_eq = { eq with eq_rhs = norm_rhs } in
389
    norm_eq::defs', vars'
390
391 949b2e1e ploc
let normalize_eq_split node defvars eq =
392 8fa4e28e ploc
  try
393
    let defs, vars = normalize_eq node defvars eq in
394 949b2e1e ploc
  List.fold_right (fun eq (def, vars) -> 
395
    let eq_defs = Splitting.tuple_split_eq eq in
396
    if eq_defs = [eq] then
397
      eq::def, vars 
398
    else
399
      List.fold_left (normalize_eq node) (def, vars) eq_defs
400
  ) defs ([], vars)  
401
402 8fa4e28e ploc
  with _ -> (
403
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
404
    assert false
405
  )
406
407 949b2e1e ploc
let normalize_eexpr decls node vars ee =
408
  (* New output variable *)
409
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
410
  let output_var = 
411
    mkvar_decl 
412
      ee.eexpr_loc 
413
      (output_id, 
414
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
415
       mkclock ee.eexpr_loc Ckdec_any, 
416
       false (* not a constant *),
417
       None,
418
       None
419
      ) 
420
  in
421 8fa4e28e ploc
  
422 949b2e1e ploc
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
423
  (* Calls are first inlined *)
424
  let nodes = get_nodes decls in
425
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
426
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
427
   let calls = List.map 
428
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
429
  in
430
*)
431
  (*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;  *)
432
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
433
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
434
  let (new_locals, eqs) =
435
    if calls = [] && not (eq_has_arrows eq) then
436
      (locals, [eq])     
437
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
438
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
439
      (*Format.eprintf "eqs %a@.@?" 
440
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
441
      (new_locals, eqs)
442
*)
443
           (locals, [eq])     
444
 
445
    ) in
446
  (* Normalizing expr and eqs *)
447 8fa4e28e ploc
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
448
    let todefine = List.fold_left
449 949b2e1e ploc
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
450
    (ISet.add output_id ISet.empty) vars in
451 8fa4e28e ploc
  
452 949b2e1e ploc
  try
453 2d27eedd ploc
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
454 949b2e1e ploc
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
455
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
456
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
457
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
458
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
459
  (* check that table is empty *)
460
    if (not (ISet.is_empty undefined_vars)) then
461
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
462
    
463
    (*Format.eprintf "normalized eqs %a@.@?" 
464
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
465
    ee.eexpr_normalized <- Some (output_var, defs, vars)
466 8fa4e28e ploc
    
467 949b2e1e ploc
  with (Types.Error (loc,err)) as exc ->
468
    eprintf "Typing error for eexpr %a: %a%a%a@."
469
      Printers.pp_eexpr ee
470
      Types.pp_error err
471
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
472
      Location.pp_loc loc
473 8fa4e28e ploc
  
474 949b2e1e ploc
      
475 8fa4e28e ploc
    ;
476 949b2e1e ploc
    raise exc
477 8fa4e28e ploc
    
478
 
479
    
480 949b2e1e ploc
let normalize_spec decls node vars s =
481
  let nee = normalize_eexpr decls node vars in
482 778c80fd ploc
  List.iter nee s.assume;
483
  List.iter nee s.guarantees;
484
  List.iter (fun m -> 
485
      List.iter nee m.require;
486
    List.iter nee m.ensure
487
  ) s.modes
488 949b2e1e ploc
  
489
    
490
(* The normalization phase introduces new local variables
491
   - output cannot be memories. If this happen, new local variables acting as
492
   memories are introduced. 
493
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
494
   access
495
   Thoses values are shared, ie. no duplicate expressions are introduced.
496
497
   Concerning specification, a similar process is applied, replacing an
498
   expression by a list of local variables and definitions
499
*)
500
501
(** normalize_node node returns a normalized node, 
502
    ie. 
503 af5af1e8 ploc
    - updated locals
504
    - new equations
505 8deaa2dd tkahsai
    -
506 af5af1e8 ploc
*)
507 949b2e1e ploc
let normalize_node decls node =
508 7065d912 ploc
  reset_cpt_fresh ();
509 22fe1c93 ploc
  let inputs_outputs = node.node_inputs@node.node_outputs in
510 af5af1e8 ploc
  let orig_vars = inputs_outputs@node.node_locals in
511 50dadc21 ploc
  let not_is_orig_var v =
512
    List.for_all ((!=) v) orig_vars in
513 8deaa2dd tkahsai
  let defs, vars =
514 333e3a25 ploc
    let eqs, auts = get_node_eqs node in
515
    if auts != [] then assert false; (* Automata should be expanded by now. *)
516
    List.fold_left (normalize_eq node) ([], orig_vars) eqs in
517 af5af1e8 ploc
  (* Normalize the asserts *)
518 8deaa2dd tkahsai
  let vars, assert_defs, asserts =
519 af5af1e8 ploc
    List.fold_left (
520 50dadc21 ploc
      fun (vars, def_accu, assert_accu) assert_ ->
521
	let assert_expr = assert_.assert_expr in
522
	let (defs, vars'), expr = 
523
	  normalize_expr 
524
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
525
	    node 
526
	    [] (* empty offset for arrays *)
527
	    ([], vars) (* defvar only contains vars *)
528
	    assert_expr
529
	in
530 8deaa2dd tkahsai
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
531 50dadc21 ploc
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
532 af5af1e8 ploc
    ) (vars, [], []) node.node_asserts in
533 50dadc21 ploc
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
534
							  vars and initial locals ones *)
535 66359a5e ploc
  
536
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
537 50dadc21 ploc
						       beginning of the list the
538
						       local declared ones *)
539 8deaa2dd tkahsai
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
540 f2b1c245 ploc
541 66359a5e ploc
542
  (* Updating annotations: traceability and machine types for fresh variables *)
543
  
544
  (* Compute traceability info:
545
     - gather newly bound variables
546
     - compute the associated expression without aliases
547
  *)
548 ea1c2906 ploc
  let new_annots =
549
    if !Options.traces then
550
      begin
551 66359a5e ploc
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
552 ea1c2906 ploc
	let norm_traceability = {
553
	  annots = List.map (fun v ->
554
	    let eq =
555
	      try
556 45f0f48d xthirioux
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
557
	      with Not_found -> 
558
		(
559
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
560
		  assert false
561
		) 
562
	    in
563 b98a4a58 ploc
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
564 ea1c2906 ploc
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
565 66359a5e ploc
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
566 ea1c2906 ploc
	    (["traceability"], pair)
567
	  ) diff_vars;
568
	  annot_loc = Location.dummy_loc
569 8deaa2dd tkahsai
	}
570 ea1c2906 ploc
	in
571
	norm_traceability::node.node_annot
572
      end
573
    else
574
      node.node_annot
575 af5af1e8 ploc
  in
576 ea1c2906 ploc
577 66359a5e ploc
  let new_annots =
578
    List.fold_left (fun annots v ->
579 f4050bef ploc
      if Machine_types.is_active && Machine_types.is_exportable v then
580 66359a5e ploc
	let typ = Machine_types.get_specified_type v in
581
  	let typ_name = Machine_types.type_name typ in
582
583
	let loc = v.var_loc in
584
	let typ_as_string =
585
	  mkexpr
586
	    loc
587
	    (Expr_const
588
	       (Const_string typ_name))
589
	in
590
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
591
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
592
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
593
      else
594
	annots
595
    ) new_annots new_locals
596
  in
597 949b2e1e ploc
  if !Options.spec <> "no" then 
598
    begin
599 8fa4e28e ploc
      (* Update mutable fields of eexpr to perform normalization of
600
	 specification.
601
602
	 Careful: we do not normalize annotations, since they can have the form
603
	 x = (a, b, c) *)
604
      (* List.iter  *)
605
      (* 	(fun a ->  *)
606
      (* 	  List.iter  *)
607
      (* 	    (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann)  *)
608
      (* 	    a.annots *)
609
      (* 	) *)
610
      (* 	node.node_annot; *)
611 949b2e1e ploc
      match node.node_spec with None -> () | Some s -> normalize_spec decls node [] s 
612
    end;
613
  
614
 
615 22fe1c93 ploc
  let node =
616 50dadc21 ploc
    { node with
617 66359a5e ploc
      node_locals = all_locals;
618 50dadc21 ploc
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
619
      node_asserts = asserts;
620
      node_annot = new_annots;
621
    }
622 8deaa2dd tkahsai
  in ((*Printers.pp_node Format.err_formatter node;*)
623 f2b1c245 ploc
    node
624 50dadc21 ploc
  )
625 f2b1c245 ploc
626 22fe1c93 ploc
627 82906771 ploc
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
628 22fe1c93 ploc
  match decl.top_decl_desc with
629
  | Node nd ->
630 949b2e1e ploc
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
631 f2b1c245 ploc
    Hashtbl.replace Corelang.node_table nd.node_id decl';
632
    decl'
633 19a1e66b ploc
    | Include _| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
634 8deaa2dd tkahsai
635 ad4774b0 ploc
let normalize_prog p decls =
636 27dc3869 ploc
  (* Backend specific configurations for normalization *)
637 ad4774b0 ploc
  params := p;
638 22fe1c93 ploc
639 27dc3869 ploc
  (* Main algorithm: iterates over nodes *)
640 82906771 ploc
  List.map (normalize_decl decls) decls
641 ad4774b0 ploc
642
    
643
           (* Local Variables: *)
644
           (* compile-command:"make -C .." *)
645
           (* End: *)
646