Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ master

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