Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 81229f63

History | View | Annotate | Download (32.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 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 95944ba1 ploc
type norm_ctx_t =
47
  {
48
    parentid: ident;
49
    vars: var_decl list;
50
    is_output: ident -> bool; 
51
  }
52
53
           
54 2e6f9ba8 xthirioux
let expr_true loc ck =
55
{ expr_tag = Utils.new_tag ();
56
  expr_desc = Expr_const (Const_tag tag_true);
57
  expr_type = Type_predef.type_bool;
58
  expr_clock = ck;
59
  expr_delay = Delay.new_var ();
60
  expr_annot = None;
61
  expr_loc = loc }
62
63
let expr_false loc ck =
64
{ expr_tag = Utils.new_tag ();
65
  expr_desc = Expr_const (Const_tag tag_false);
66
  expr_type = Type_predef.type_bool;
67
  expr_clock = ck;
68
  expr_delay = Delay.new_var ();
69
  expr_annot = None;
70
  expr_loc = loc }
71
72
let expr_once loc ck =
73
 { expr_tag = Utils.new_tag ();
74
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
75
  expr_type = Type_predef.type_bool;
76
  expr_clock = ck;
77
  expr_delay = Delay.new_var ();
78
  expr_annot = None;
79
  expr_loc = loc }
80
81
let is_expr_once =
82
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
83
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
84
85
let unfold_arrow expr =
86
 match expr.expr_desc with
87
 | Expr_arrow (e1, e2) ->
88
    let loc = expr.expr_loc in
89 a38c681e xthirioux
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
90 2e6f9ba8 xthirioux
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
91
 | _                   -> assert false
92
93 22fe1c93 ploc
94
95
(* Get the equation in [defs] with [expr] as rhs, if any *)
96
let get_expr_alias defs expr =
97 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)
98 22fe1c93 ploc
 with
99 e49b6d55 xavier.thirioux
 | Not_found -> None
100
  
101 22fe1c93 ploc
(* Replace [expr] with (tuple of) [locals] *)
102
let replace_expr locals expr =
103
 match locals with
104
 | []  -> assert false
105
 | [v] -> { expr with
106
   expr_tag = Utils.new_tag ();
107
   expr_desc = Expr_ident v.var_id }
108
 | _   -> { expr with
109
   expr_tag = Utils.new_tag ();
110 fc886259 xthirioux
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
111 22fe1c93 ploc
112
let unfold_offsets e offsets =
113
  let add_offset e d =
114 fc886259 xthirioux
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
115
    let res = *)
116 22fe1c93 ploc
    { e with
117
      expr_tag = Utils.new_tag ();
118
      expr_loc = d.Dimension.dim_loc;
119
      expr_type = Types.array_element_type e.expr_type;
120 fc886259 xthirioux
      expr_desc = Expr_access (e, d) }
121
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
122
  in
123 22fe1c93 ploc
 List.fold_left add_offset e offsets
124
125 95944ba1 ploc
(* IS IT USED ? TODO 
126 22fe1c93 ploc
(* Create an alias for [expr], if none exists yet *)
127 95944ba1 ploc
let mk_expr_alias (parentid, vars) (defs, vars) expr =
128 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;*)
129 22fe1c93 ploc
  match get_expr_alias defs expr with
130
  | Some eq ->
131
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
132
    (defs, vars), replace_expr aliases expr
133
  | None    ->
134
    let new_aliases =
135
      List.map2
136 95944ba1 ploc
	(mk_fresh_var (parentid, vars) expr.expr_loc)
137 22fe1c93 ploc
	(Types.type_list_of_type expr.expr_type)
138
	(Clocks.clock_list_of_clock expr.expr_clock) in
139
    let new_def =
140
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
141 3ca6d126 ploc
    in
142 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; *)
143 3ca6d126 ploc
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
144 95944ba1 ploc
 *)
145
  
146 d4807c3d xthirioux
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
147
   and [opt] is true *)
148 95944ba1 ploc
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
149 04a63d25 xthirioux
(*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;*)
150 d4807c3d xthirioux
  match expr.expr_desc with
151
  | Expr_ident alias ->
152 04a63d25 xthirioux
    (defs, vars), expr
153 8deaa2dd tkahsai
  | _                ->
154 04a63d25 xthirioux
    match get_expr_alias defs expr with
155
    | Some eq ->
156 c35de73b ploc
       (* Format.eprintf "Found a preexisting definition@."; *)
157 04a63d25 xthirioux
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
158
      (defs, vars), replace_expr aliases expr
159
    | None    ->
160 c35de73b ploc
       (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
161
        * Format.eprintf "existing defs are: @[[%a@]]@."
162
        *   (fprintf_list ~sep:"@ "(fun fmt eq ->
163
        *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
164
        *          Clocks.print_ck eq.eq_rhs.expr_clock
165
        *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
166
        *          (is_eq_expr eq.eq_rhs expr)
167
        *          Printers.pp_node_eq eq))
168
        *   defs; *)
169 04a63d25 xthirioux
      if opt
170
      then
171
	let new_aliases =
172
	  List.map2
173 59020713 ploc
	    (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)
174 04a63d25 xthirioux
	    (Types.type_list_of_type expr.expr_type)
175
	    (Clocks.clock_list_of_clock expr.expr_clock) in
176
	let new_def =
177
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
178 66359a5e ploc
	in
179
	(* Typing and Registering machine type *) 
180 59020713 ploc
	let _ = if Machine_types.is_active then
181
                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
182
        in
183 66359a5e ploc
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
184 04a63d25 xthirioux
      else
185
	(defs, vars), expr
186 22fe1c93 ploc
187 8deaa2dd tkahsai
(* Create a (normalized) expression from [ref_e],
188 22fe1c93 ploc
   replacing description with [norm_d],
189 8deaa2dd tkahsai
   taking propagated [offsets] into account
190 22fe1c93 ploc
   in order to change expression type *)
191
let mk_norm_expr offsets ref_e norm_d =
192 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};*)
193 22fe1c93 ploc
  let drop_array_type ty =
194
    Types.map_tuple_type Types.array_element_type ty in
195
  { ref_e with
196
    expr_desc = norm_d;
197
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
198 e49b6d55 xavier.thirioux
														
199 22fe1c93 ploc
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
200 95944ba1 ploc
let rec normalize_list alias norm_ctx offsets norm_element defvars elist =
201 22fe1c93 ploc
  List.fold_right
202
    (fun t (defvars, qlist) ->
203 95944ba1 ploc
      let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
204 22fe1c93 ploc
      (defvars, norm_t :: qlist)
205
    ) elist (defvars, [])
206
207 95944ba1 ploc
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr =
208 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;*)
209 22fe1c93 ploc
  match expr.expr_desc with
210 8deaa2dd tkahsai
  | Expr_const _
211 22fe1c93 ploc
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
212
  | Expr_array elist ->
213 95944ba1 ploc
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
214 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
215 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
216 22fe1c93 ploc
  | Expr_power (e1, d) when offsets = [] ->
217 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
218 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
219 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
220 22fe1c93 ploc
  | Expr_power (e1, d) ->
221 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
222 22fe1c93 ploc
  | Expr_access (e1, d) ->
223 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1
224 8deaa2dd tkahsai
  | Expr_tuple elist ->
225 0a10042e ploc
     let defvars, norm_elist =
226 95944ba1 ploc
       normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
227 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
228 8deaa2dd tkahsai
  | Expr_appl (id, args, None)
229 04a63d25 xthirioux
      when Basic_library.is_homomorphic_fun id 
230 af5af1e8 ploc
	&& Types.is_array_type expr.expr_type ->
231 0a10042e ploc
     let defvars, norm_args =
232
       normalize_list
233
	 alias
234 95944ba1 ploc
	 norm_ctx
235 0a10042e ploc
	 offsets
236
	 (fun _ -> normalize_array_expr ~alias:true)
237
	 defvars
238
	 (expr_list_of_expr args)
239
     in
240
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
241 3436d1a6 ploc
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
242 ad4774b0 ploc
      && not (!params.force_alias_internal_fun || alias_basic) ->
243 95944ba1 ploc
     let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in
244 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
245 22fe1c93 ploc
  | Expr_appl (id, args, r) ->
246 0a10042e ploc
     let defvars, r =
247
       match r with
248
       | None -> defvars, None
249
       | Some r ->
250 95944ba1 ploc
	  let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in
251 0a10042e ploc
	  defvars, Some norm_r
252
     in
253 95944ba1 ploc
     let defvars, norm_args = normalize_expr norm_ctx [] defvars args in
254 0a10042e ploc
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
255
     if offsets <> []
256
     then
257 95944ba1 ploc
       let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in
258
       normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr
259 0a10042e ploc
     else
260 ad4774b0 ploc
       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
261 0a10042e ploc
				    || not (Basic_library.is_expr_internal_fun expr)))
262 95944ba1 ploc
	 norm_ctx defvars norm_expr
263 ad4774b0 ploc
  | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
264 0a10042e ploc
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
265 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr)
266 2e6f9ba8 xthirioux
  | Expr_arrow (e1,e2) ->
267 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
268
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
269 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
270 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
271 22fe1c93 ploc
  | Expr_pre e ->
272 95944ba1 ploc
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
273 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
274 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
275 22fe1c93 ploc
  | Expr_fby (e1, e2) ->
276 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
277
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
278 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
279 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
280 22fe1c93 ploc
  | Expr_when (e, c, l) ->
281 95944ba1 ploc
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
282 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
283 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
284 95944ba1 ploc
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
285
     let defvars, norm_t = normalize_cond_expr  norm_ctx offsets defvars t in
286
     let defvars, norm_e = normalize_cond_expr  norm_ctx offsets defvars e in
287 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
288 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
289 22fe1c93 ploc
  | Expr_merge (c, hl) ->
290 95944ba1 ploc
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
291 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
292 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
293 8deaa2dd tkahsai
294 52cfee34 xthirioux
(* Creates a conditional with a merge construct, which is more lazy *)
295
(*
296 0a10042e ploc
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
297
  match expr.expr_desc with
298
  | Expr_ite (c, t, e) ->
299
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
300
  | _ -> assert false
301 52cfee34 xthirioux
*)
302 95944ba1 ploc
and normalize_branches norm_ctx offsets defvars hl =
303 0a10042e ploc
  List.fold_right
304
    (fun (t, h) (defvars, norm_q) ->
305 95944ba1 ploc
      let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in
306 0a10042e ploc
      defvars, (t, norm_h) :: norm_q
307
    )
308
    hl (defvars, [])
309 22fe1c93 ploc
310 95944ba1 ploc
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
311 04a63d25 xthirioux
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
312 22fe1c93 ploc
  match expr.expr_desc with
313
  | Expr_power (e1, d) when offsets = [] ->
314 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
315 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
316 22fe1c93 ploc
  | Expr_power (e1, d) ->
317 95944ba1 ploc
     normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
318
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1
319 22fe1c93 ploc
  | Expr_array elist when offsets = [] ->
320 95944ba1 ploc
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
321 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
322 04a63d25 xthirioux
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
323 95944ba1 ploc
     let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
324 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
325 95944ba1 ploc
  |  _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr
326 22fe1c93 ploc
327 95944ba1 ploc
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr =
328 22fe1c93 ploc
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
329
  match expr.expr_desc with
330
  | Expr_access (e1, d) ->
331 95944ba1 ploc
     normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1
332 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
333 95944ba1 ploc
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
334
     let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
335
     let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
336 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
337 22fe1c93 ploc
  | Expr_merge (c, hl) ->
338 95944ba1 ploc
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
339 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
340 ad4774b0 ploc
  | _ when !params.force_alias_ite ->
341 27dc3869 ploc
     (* Forcing alias creation for then/else expressions *)
342
     let defvars, norm_expr =
343 95944ba1 ploc
       normalize_expr ~alias:alias norm_ctx offsets defvars expr
344 27dc3869 ploc
     in
345 95944ba1 ploc
     mk_expr_alias_opt true norm_ctx defvars norm_expr
346 27dc3869 ploc
  | _ -> (* default case without the force_alias_ite option *)
347 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx offsets defvars expr
348 0a10042e ploc
       
349 95944ba1 ploc
and normalize_guard norm_ctx defvars expr =
350
  let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in
351
  mk_expr_alias_opt true norm_ctx defvars norm_expr
352 22fe1c93 ploc
353
(* outputs cannot be memories as well. If so, introduce new local variable.
354
*)
355 95944ba1 ploc
let decouple_outputs norm_ctx defvars eq =
356 22fe1c93 ploc
  let rec fold_lhs defvars lhs tys cks =
357 a742719e ploc
    match lhs, tys, cks with
358
    | [], [], []          -> defvars, []
359
    | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
360 95944ba1 ploc
			     if norm_ctx.is_output v
361 a742719e ploc
			     then
362 95944ba1 ploc
			       let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in
363 a742719e ploc
			       let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
364
			       (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
365
			     else
366
			       (defs_q, vars_q), v::lhs_q
367
    | _                   -> assert false in
368 22fe1c93 ploc
  let defvars', lhs' =
369
    fold_lhs
370
      defvars
371
      eq.eq_lhs
372
      (Types.type_list_of_type eq.eq_rhs.expr_type)
373
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
374
  defvars', {eq with eq_lhs = lhs' }
375
376 95944ba1 ploc
let rec normalize_eq norm_ctx defvars eq =
377 04a63d25 xthirioux
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
378 22fe1c93 ploc
  match eq.eq_rhs.expr_desc with
379
  | Expr_pre _
380
  | Expr_fby _  ->
381 95944ba1 ploc
    let (defvars', eq') = decouple_outputs norm_ctx defvars eq in
382
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in
383 22fe1c93 ploc
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
384
    (norm_eq::defs', vars')
385
  | Expr_array _ ->
386 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
387 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
388
    (norm_eq::defs', vars')
389 04a63d25 xthirioux
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
390 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
391 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
392
    (norm_eq::defs', vars')
393
  | Expr_appl _ ->
394 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
395 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
396
    (norm_eq::defs', vars')
397
  | _ ->
398 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
399 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
400
    norm_eq::defs', vars'
401
402 95944ba1 ploc
let normalize_eq_split norm_ctx defvars eq =
403 8fa4e28e ploc
  try
404 95944ba1 ploc
    let defs, vars = normalize_eq norm_ctx defvars eq in
405 59020713 ploc
    List.fold_right (fun eq (def, vars) -> 
406
        let eq_defs = Splitting.tuple_split_eq eq in
407
        if eq_defs = [eq] then
408
          eq::def, vars 
409
        else
410
          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
411
      ) defs ([], vars)  
412
    
413
  with ex -> (
414 8fa4e28e ploc
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
415 59020713 ploc
    raise ex
416 8fa4e28e ploc
  )
417
418 59020713 ploc
(* Projecting an eexpr to an eexpr associated to a single
419
   variable. Returns the updated ee, the bounded variable and the
420
   associated statement *)
421
let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
422
  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
423
  (* don't do anything is eexpr is just a variable *)
424
  let skip =
425
    match ee.eexpr_qfexpr.expr_desc with
426
    | Expr_ident _ | Expr_const _ -> true
427
    | _ -> false
428 949b2e1e ploc
  in
429 59020713 ploc
  if skip then
430
    ee, (def, vars)
431
  else (
432
    (* New output variable *)
433
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
434
    let output_var = 
435
      mkvar_decl 
436
        ee.eexpr_loc 
437
        (output_id, 
438
         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
439
         mkclock ee.eexpr_loc Ckdec_any, 
440
         false (* not a constant *),
441
         None,
442
         None
443
        ) 
444
    in
445
    let output_expr = expr_of_vdecl output_var in
446
    (* Rebuilding an eexpr with a silly expression, just a variable *)
447
    let ee' = { ee with eexpr_qfexpr = output_expr } in
448
449
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
450
       inline possible calls within, normalize it and type/clock the
451
       result.  *)
452
    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
453 1fd3d002 ploc
454
455
    (* (\* Inlining any calls *\)
456
     * let nodes = get_nodes decls in
457
     * let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
458
     * let vars, eqs =
459
     *   if calls = [] && not (eq_has_arrows eq) then
460
     *     vars, [eq]    
461
     *   else
462
     *     assert false (\* TODO *\)
463
     * in *)
464 59020713 ploc
    
465
    (* Normalizing expr and eqs *)
466 1fd3d002 ploc
    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in
467
    let vars = output_var :: vars in 
468 59020713 ploc
(*    let todefine =
469
      List.fold_left
470
        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
471
        (ISet.add output_id ISet.empty) vars in
472
 *)      
473
474
    (* Typing / Clocking *)
475
    try
476
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
477
        (*
478
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
479
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
480
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
481
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
482
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
483
  (* check that table is empty *)
484
    if (not (ISet.is_empty undefined_vars)) then
485
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
486
    
487
    (*Format.eprintf "normalized eqs %a@.@?" 
488
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
489
         *)
490
491
    ee', (defs, vars)
492
    
493
  with (Types.Error (loc,err)) as exc ->
494
    eprintf "Typing error for eexpr %a: %a%a%a@."
495
      Printers.pp_eexpr ee
496
      Types.pp_error err
497
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
498
      Location.pp_loc loc
499
  
500
      
501
    ;
502
    raise exc
503
                                     
504
  )
505
    
506
   (*
507 8fa4e28e ploc
  
508 949b2e1e ploc
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
509
  (* Calls are first inlined *)
510 59020713 ploc
  
511 949b2e1e ploc
  (*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;  *)
512
  let (new_locals, eqs) =
513
    if calls = [] && not (eq_has_arrows eq) then
514
      (locals, [eq])     
515
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
516
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
517
      (*Format.eprintf "eqs %a@.@?" 
518
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
519
      (new_locals, eqs)
520
*)
521
           (locals, [eq])     
522
 
523
    ) in
524
  (* Normalizing expr and eqs *)
525 8fa4e28e ploc
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
526
    let todefine = List.fold_left
527 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)
528
    (ISet.add output_id ISet.empty) vars in
529 8fa4e28e ploc
  
530 949b2e1e ploc
  try
531 2d27eedd ploc
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
532 949b2e1e ploc
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
533
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
534
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
535
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
536
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
537
  (* check that table is empty *)
538
    if (not (ISet.is_empty undefined_vars)) then
539
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
540
    
541
    (*Format.eprintf "normalized eqs %a@.@?" 
542
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
543
    ee.eexpr_normalized <- Some (output_var, defs, vars)
544 8fa4e28e ploc
    
545 949b2e1e ploc
  with (Types.Error (loc,err)) as exc ->
546
    eprintf "Typing error for eexpr %a: %a%a%a@."
547
      Printers.pp_eexpr ee
548
      Types.pp_error err
549
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
550
      Location.pp_loc loc
551 8fa4e28e ploc
  
552 949b2e1e ploc
      
553 8fa4e28e ploc
    ;
554 949b2e1e ploc
    raise exc
555 95944ba1 ploc
                                                 *)    
556 8fa4e28e ploc
 
557 59020713 ploc
558
(* We use node local vars to make sure we are creating fresh variables *) 
559
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  
560 f4cba4b8 ploc
  (* Original set of variables actually visible from here: in/out and
561 59020713 ploc
     spec locals (no node locals) *)
562
  let orig_vars = in_vars @ out_vars @ s.locals in
563 1fd3d002 ploc
  (* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)
564 95944ba1 ploc
  let not_is_orig_var v =
565
    List.for_all ((!=) v) orig_vars in
566 59020713 ploc
  let norm_ctx = {
567
      parentid = parentid;
568
      vars = in_vars @ out_vars @ l_vars;
569
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
570
    }
571
  in
572
  (* Normalizing existing stmts *)
573
  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
574
  if auts != [] then assert false; (* Automata should be expanded by now. *)
575
  let defsvars = 
576
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
577
  in
578
  (* Iterate through predicates and normalize them on the go, creating
579
     fresh variables for any guarantees/assumes/require/ensure *)
580
  let process_predicates l defvars =
581 1fd3d002 ploc
    (* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
582
    let res = List.fold_right (fun ee (accu, defvars) ->
583 59020713 ploc
        let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
584
        ee'::accu, defvars
585
      ) l ([], defvars)
586 1fd3d002 ploc
    in
587
    (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
588
     * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
589
    res
590 95944ba1 ploc
  in
591
592 59020713 ploc
  
593
  let assume', defsvars = process_predicates s.assume defsvars in
594
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
595
  let modes', (defs, vars) =
596
    List.fold_right (
597
        fun m (accu_m, defsvars) ->
598
        let require', defsvars = process_predicates m.require defsvars in
599
        let ensure', defsvars = process_predicates m.ensure defsvars in
600
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
601
      ) s.modes ([], defsvars)
602
  in
603
  
604
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
605 f4cba4b8 ploc
  new_locals, defs,      
606 95944ba1 ploc
  {s with
607 1fd3d002 ploc
    (* locals = s.locals @ new_locals; *)
608 f4cba4b8 ploc
    stmts = [];
609 59020713 ploc
    assume = assume';
610
    guarantees = guarantees';
611
    modes = modes'
612
  }
613
(* let nee _ = () in
614
 *   (\*normalize_eexpr decls iovars in *\)
615
 *   List.iter nee s.assume;
616
 *   List.iter nee s.guarantees;
617
 *   List.iter (fun m -> 
618
 *       List.iter nee m.require;
619
 *     List.iter nee m.ensure
620
 *     ) s.modes; *)
621
   
622
623
                                                                     
624
  
625
  
626 949b2e1e ploc
    
627
(* The normalization phase introduces new local variables
628
   - output cannot be memories. If this happen, new local variables acting as
629
   memories are introduced. 
630
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
631
   access
632
   Thoses values are shared, ie. no duplicate expressions are introduced.
633
634
   Concerning specification, a similar process is applied, replacing an
635
   expression by a list of local variables and definitions
636
*)
637
638
(** normalize_node node returns a normalized node, 
639
    ie. 
640 af5af1e8 ploc
    - updated locals
641
    - new equations
642 8deaa2dd tkahsai
    -
643 af5af1e8 ploc
*)
644 949b2e1e ploc
let normalize_node decls node =
645 7065d912 ploc
  reset_cpt_fresh ();
646 59020713 ploc
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
647 50dadc21 ploc
  let not_is_orig_var v =
648
    List.for_all ((!=) v) orig_vars in
649 95944ba1 ploc
  let norm_ctx = {
650
      parentid = node.node_id;
651
      vars = get_node_vars node;
652
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
653
    }
654
  in
655 f4cba4b8 ploc
656
  let eqs, auts = get_node_eqs node in
657
  if auts != [] then assert false; (* Automata should be expanded by now. *)
658
  let spec, new_vars, eqs =
659
    begin
660
      (* Update mutable fields of eexpr to perform normalization of
661
	 specification.
662
663
	 Careful: we do not normalize annotations, since they can have the form
664
	 x = (a, b, c) *)
665
      match node.node_spec with
666
      | None 
667
        | Some (NodeSpec _) -> node.node_spec, [], eqs
668
      | Some (Contract s) ->
669
         let new_locals, new_stmts, s' = normalize_spec
670
                    decls
671
                    node.node_id
672
                    (node.node_inputs, node.node_outputs, node.node_locals)
673
                    s
674
         in
675 1fd3d002 ploc
         (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
676
          * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
677 f4cba4b8 ploc
         Some (Contract s'), new_locals, new_stmts@eqs
678
    end
679
  in
680 8deaa2dd tkahsai
  let defs, vars =
681 f4cba4b8 ploc
    List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
682 af5af1e8 ploc
  (* Normalize the asserts *)
683 8deaa2dd tkahsai
  let vars, assert_defs, asserts =
684 af5af1e8 ploc
    List.fold_left (
685 f4cba4b8 ploc
        fun (vars, def_accu, assert_accu) assert_ ->
686 50dadc21 ploc
	let assert_expr = assert_.assert_expr in
687
	let (defs, vars'), expr = 
688
	  normalize_expr 
689
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
690 95944ba1 ploc
	    norm_ctx 
691 50dadc21 ploc
	    [] (* empty offset for arrays *)
692
	    ([], vars) (* defvar only contains vars *)
693
	    assert_expr
694
	in
695 f4cba4b8 ploc
        (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
696 50dadc21 ploc
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
697 f4cba4b8 ploc
      ) (vars, [], []) node.node_asserts in
698 50dadc21 ploc
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
699
							  vars and initial locals ones *)
700 66359a5e ploc
  
701
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
702 50dadc21 ploc
						       beginning of the list the
703
						       local declared ones *)
704 8deaa2dd tkahsai
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
705 f2b1c245 ploc
706 66359a5e ploc
707
  (* Updating annotations: traceability and machine types for fresh variables *)
708
  
709
  (* Compute traceability info:
710
     - gather newly bound variables
711
     - compute the associated expression without aliases
712 f4cba4b8 ploc
   *)
713 ea1c2906 ploc
  let new_annots =
714
    if !Options.traces then
715
      begin
716 66359a5e ploc
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
717 ea1c2906 ploc
	let norm_traceability = {
718 f4cba4b8 ploc
	    annots = List.map (fun v ->
719
	                 let eq =
720
	                   try
721
		             List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
722
	                   with Not_found -> 
723
		             (
724
		               Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
725
		               assert false
726
		             ) 
727
	                 in
728
	                 let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
729
	                 let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
730
	                 Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
731
	                 (["traceability"], pair)
732
	               ) diff_vars;
733
	    annot_loc = Location.dummy_loc
734
	  }
735 ea1c2906 ploc
	in
736
	norm_traceability::node.node_annot
737
      end
738
    else
739
      node.node_annot
740 af5af1e8 ploc
  in
741 ea1c2906 ploc
742 66359a5e ploc
  let new_annots =
743
    List.fold_left (fun annots v ->
744 f4cba4b8 ploc
        if Machine_types.is_active && Machine_types.is_exportable v then
745
	  let typ = Machine_types.get_specified_type v in
746
  	  let typ_name = Machine_types.type_name typ in
747
748
	  let loc = v.var_loc in
749
	  let typ_as_string =
750
	    mkexpr
751
	      loc
752
	      (Expr_const
753
	         (Const_string typ_name))
754
	  in
755
	  let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
756
	  Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
757
	  {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
758
        else
759
	  annots
760
      ) new_annots new_locals
761 95944ba1 ploc
  in
762
  
763 949b2e1e ploc
  
764 22fe1c93 ploc
  let node =
765 50dadc21 ploc
    { node with
766 66359a5e ploc
      node_locals = all_locals;
767 50dadc21 ploc
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
768
      node_asserts = asserts;
769
      node_annot = new_annots;
770 95944ba1 ploc
      node_spec = spec;
771 50dadc21 ploc
    }
772 8deaa2dd tkahsai
  in ((*Printers.pp_node Format.err_formatter node;*)
773 f4cba4b8 ploc
      node
774
    )
775 f2b1c245 ploc
776 95944ba1 ploc
let normalize_inode decls nd =
777
  reset_cpt_fresh ();
778
  match nd.nodei_spec with
779 f4cba4b8 ploc
    None | Some (NodeSpec _) -> nd
780
    | Some (Contract _) -> assert false
781
                         
782 82906771 ploc
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
783 22fe1c93 ploc
  match decl.top_decl_desc with
784
  | Node nd ->
785 95944ba1 ploc
     let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
786
     update_node nd.node_id decl';
787
     decl'
788
  | ImportedNode nd ->
789
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
790
     update_node nd.nodei_id decl';
791
     decl'
792
     
793
    | Include _| Open _ | Const _ | TypeDef _ -> decl
794 8deaa2dd tkahsai
795 ad4774b0 ploc
let normalize_prog p decls =
796 27dc3869 ploc
  (* Backend specific configurations for normalization *)
797 ad4774b0 ploc
  params := p;
798 22fe1c93 ploc
799 27dc3869 ploc
  (* Main algorithm: iterates over nodes *)
800 82906771 ploc
  List.map (normalize_decl decls) decls
801 ad4774b0 ploc
802 95944ba1 ploc
803
(* Fake interface for outside uses *)
804
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
805
  mk_expr_alias_opt
806
    opt
807
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
808
    (defs, vars)
809
    expr
810
811 ad4774b0 ploc
    
812
           (* Local Variables: *)
813
           (* compile-command:"make -C .." *)
814
           (* End: *)
815