lustrec / src / normalization.ml @ 59020713
History  View  Annotate  Download (31.1 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(********************************************************************) 
11  
12 
open Utils 
13 
open Lustre_types 
14 
open Corelang 
15 
open Format 
16  
17 
(** 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 nonalias 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 
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  
46 
type norm_ctx_t = 
47 
{ 
48 
parentid: ident; 
49 
vars: var_decl list; 
50 
is_output: ident > bool; 
51 
} 
52  
53 

54 
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 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in 
90 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 
91 
 _ > assert false 
92  
93  
94  
95 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
96 
let get_expr_alias defs expr = 
97 
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 
with 
99 
 Not_found > None 
100 

101 
(* 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 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } 
111  
112 
let unfold_offsets e offsets = 
113 
let add_offset e d = 
114 
(*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 
{ 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 
expr_desc = Expr_access (e, d) } 
121 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 
122 
in 
123 
List.fold_left add_offset e offsets 
124  
125 
(* IS IT USED ? TODO 
126 
(* Create an alias for [expr], if none exists yet *) 
127 
let mk_expr_alias (parentid, vars) (defs, vars) expr = 
128 
(*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 
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 
(mk_fresh_var (parentid, vars) expr.expr_loc) 
137 
(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 
in 
142 
(* 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 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
144 
*) 
145 

146 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
147 
and [opt] is true *) 
148 
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr = 
149 
(*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 
match expr.expr_desc with 
151 
 Expr_ident alias > 
152 
(defs, vars), expr 
153 
 _ > 
154 
match get_expr_alias defs expr with 
155 
 Some eq > 
156 
(* Format.eprintf "Found a preexisting definition@."; *) 
157 
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 
(* 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 
if opt 
170 
then 
171 
let new_aliases = 
172 
List.map2 
173 
(mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc) 
174 
(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 
in 
179 
(* Typing and Registering machine type *) 
180 
let _ = if Machine_types.is_active then 
181 
Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr 
182 
in 
183 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
184 
else 
185 
(defs, vars), expr 
186  
187 
(* Create a (normalized) expression from [ref_e], 
188 
replacing description with [norm_d], 
189 
taking propagated [offsets] into account 
190 
in order to change expression type *) 
191 
let mk_norm_expr offsets ref_e norm_d = 
192 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
193 
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 

199 
(* normalize_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *) 
200 
let rec normalize_list alias norm_ctx offsets norm_element defvars elist = 
201 
List.fold_right 
202 
(fun t (defvars, qlist) > 
203 
let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in 
204 
(defvars, norm_t :: qlist) 
205 
) elist (defvars, []) 
206  
207 
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr = 
208 
(*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 
match expr.expr_desc with 
210 
 Expr_const _ 
211 
 Expr_ident _ > defvars, unfold_offsets expr offsets 
212 
 Expr_array elist > 
213 
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
214 
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in 
215 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
216 
 Expr_power (e1, d) when offsets = [] > 
217 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 
218 
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in 
219 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
220 
 Expr_power (e1, d) > 
221 
normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1 
222 
 Expr_access (e1, d) > 
223 
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 
224 
 Expr_tuple elist > 
225 
let defvars, norm_elist = 
226 
normalize_list alias norm_ctx offsets (fun alias > normalize_expr ~alias:alias ~alias_basic:false) defvars elist in 
227 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
228 
 Expr_appl (id, args, None) 
229 
when Basic_library.is_homomorphic_fun id 
230 
&& Types.is_array_type expr.expr_type > 
231 
let defvars, norm_args = 
232 
normalize_list 
233 
alias 
234 
norm_ctx 
235 
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 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr 
242 
&& not (!params.force_alias_internal_fun  alias_basic) > 
243 
let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in 
244 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 
245 
 Expr_appl (id, args, r) > 
246 
let defvars, r = 
247 
match r with 
248 
 None > defvars, None 
249 
 Some r > 
250 
let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in 
251 
defvars, Some norm_r 
252 
in 
253 
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in 
254 
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in 
255 
if offsets <> [] 
256 
then 
257 
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in 
258 
normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr 
259 
else 
260 
mk_expr_alias_opt (alias && (!params.force_alias_internal_fun  alias_basic 
261 
 not (Basic_library.is_expr_internal_fun expr))) 
262 
norm_ctx defvars norm_expr 
263 
 Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) > 
264 
(* Here we differ from Colaco paper: arrows are pushed to the top *) 
265 
normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr) 
266 
 Expr_arrow (e1,e2) > 
267 
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 
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in 
270 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
271 
 Expr_pre e > 
272 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in 
273 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in 
274 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
275 
 Expr_fby (e1, e2) > 
276 
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 
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in 
279 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
280 
 Expr_when (e, c, l) > 
281 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in 
282 
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) 
283 
 Expr_ite (c, t, e) > 
284 
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 
let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in 
288 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
289 
 Expr_merge (c, hl) > 
290 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in 
291 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in 
292 
mk_expr_alias_opt alias norm_ctx defvars norm_expr 
293  
294 
(* Creates a conditional with a merge construct, which is more lazy *) 
295 
(* 
296 
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 
*) 
302 
and normalize_branches norm_ctx offsets defvars hl = 
303 
List.fold_right 
304 
(fun (t, h) (defvars, norm_q) > 
305 
let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in 
306 
defvars, (t, norm_h) :: norm_q 
307 
) 
308 
hl (defvars, []) 
309  
310 
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr = 
311 
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
312 
match expr.expr_desc with 
313 
 Expr_power (e1, d) when offsets = [] > 
314 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in 
315 
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) 
316 
 Expr_power (e1, d) > 
317 
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 
 Expr_array elist when offsets = [] > 
320 
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
321 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 
322 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr > 
323 
let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in 
324 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
325 
 _ > normalize_expr ~alias:alias norm_ctx offsets defvars expr 
326  
327 
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr = 
328 
(*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 
normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1 
332 
 Expr_ite (c, t, e) > 
333 
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 
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) 
337 
 Expr_merge (c, hl) > 
338 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in 
339 
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) 
340 
 _ when !params.force_alias_ite > 
341 
(* Forcing alias creation for then/else expressions *) 
342 
let defvars, norm_expr = 
343 
normalize_expr ~alias:alias norm_ctx offsets defvars expr 
344 
in 
345 
mk_expr_alias_opt true norm_ctx defvars norm_expr 
346 
 _ > (* default case without the force_alias_ite option *) 
347 
normalize_expr ~alias:alias norm_ctx offsets defvars expr 
348 

349 
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  
353 
(* outputs cannot be memories as well. If so, introduce new local variable. 
354 
*) 
355 
let decouple_outputs norm_ctx defvars eq = 
356 
let rec fold_lhs defvars lhs tys cks = 
357 
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 
if norm_ctx.is_output v 
361 
then 
362 
let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in 
363 
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 
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 
let rec normalize_eq norm_ctx defvars eq = 
377 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) 
378 
match eq.eq_rhs.expr_desc with 
379 
 Expr_pre _ 
380 
 Expr_fby _ > 
381 
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 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 
384 
(norm_eq::defs', vars') 
385 
 Expr_array _ > 
386 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 
387 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
388 
(norm_eq::defs', vars') 
389 
 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type > 
390 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 
391 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
392 
(norm_eq::defs', vars') 
393 
 Expr_appl _ > 
394 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 
395 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
396 
(norm_eq::defs', vars') 
397 
 _ > 
398 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in 
399 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
400 
norm_eq::defs', vars' 
401  
402 
let normalize_eq_split norm_ctx defvars eq = 
403 
try 
404 
let defs, vars = normalize_eq norm_ctx defvars eq in 
405 
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 
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq; 
415 
raise ex 
416 
) 
417  
418 
(* 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 
in 
429 
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 
(* Inlining any calls *) 
454 
let nodes = get_nodes decls in 
455 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in 
456 
let vars, eqs = 
457 
if calls = [] && not (eq_has_arrows eq) then 
458 
vars, [eq] 
459 
else 
460 
assert false (* TODO *) 
461 
in 
462 

463 
(* Normalizing expr and eqs *) 
464 
let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in 
465 
(* let todefine = 
466 
List.fold_left 
467 
(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) 
468 
(ISet.add output_id ISet.empty) vars in 
469 
*) 
470  
471 
(* Typing / Clocking *) 
472 
try 
473 
ignore (Typing.type_var_decl_list vars !Global.type_env vars); 
474 
(* 
475 
let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *) 
476 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) 
477 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in 
478 
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) 
479 
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in 
480 
(* check that table is empty *) 
481 
if (not (ISet.is_empty undefined_vars)) then 
482 
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); 
483 

484 
(*Format.eprintf "normalized eqs %a@.@?" 
485 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) 
486 
*) 
487  
488 
ee', (defs, vars) 
489 

490 
with (Types.Error (loc,err)) as exc > 
491 
eprintf "Typing error for eexpr %a: %a%a%a@." 
492 
Printers.pp_eexpr ee 
493 
Types.pp_error err 
494 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs 
495 
Location.pp_loc loc 
496 

497 

498 
; 
499 
raise exc 
500 

501 
) 
502 

503 
(* 
504 

505 
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in 
506 
(* Calls are first inlined *) 
507 

508 
(*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; *) 
509 
let (new_locals, eqs) = 
510 
if calls = [] && not (eq_has_arrows eq) then 
511 
(locals, [eq]) 
512 
else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *) 
513 
(* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in 
514 
(*Format.eprintf "eqs %a@.@?" 
515 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *) 
516 
(new_locals, eqs) 
517 
*) 
518 
(locals, [eq]) 
519 

520 
) in 
521 
(* Normalizing expr and eqs *) 
522 
let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in 
523 
let todefine = List.fold_left 
524 
(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) 
525 
(ISet.add output_id ISet.empty) vars in 
526 

527 
try 
528 
let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in 
529 
let env = Typing.type_var_decl [] env output_var in (* typing the variable *) 
530 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) 
531 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in 
532 
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) 
533 
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in 
534 
(* check that table is empty *) 
535 
if (not (ISet.is_empty undefined_vars)) then 
536 
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); 
537 

538 
(*Format.eprintf "normalized eqs %a@.@?" 
539 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) 
540 
ee.eexpr_normalized < Some (output_var, defs, vars) 
541 

542 
with (Types.Error (loc,err)) as exc > 
543 
eprintf "Typing error for eexpr %a: %a%a%a@." 
544 
Printers.pp_eexpr ee 
545 
Types.pp_error err 
546 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs 
547 
Location.pp_loc loc 
548 

549 

550 
; 
551 
raise exc 
552 
*) 
553 

554  
555 
(* We use node local vars to make sure we are creating fresh variables *) 
556 
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s = 
557 
(* Original set of variables actually visible from here: iun/out and 
558 
spec locals (no node locals) *) 
559 
let orig_vars = in_vars @ out_vars @ s.locals in 
560 
let not_is_orig_var v = 
561 
List.for_all ((!=) v) orig_vars in 
562 
let norm_ctx = { 
563 
parentid = parentid; 
564 
vars = in_vars @ out_vars @ l_vars; 
565 
is_output = (fun _ > false) (* no need to introduce fresh variables for outputs *); 
566 
} 
567 
in 
568 
(* Normalizing existing stmts *) 
569 
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 
570 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
571 
let defsvars = 
572 
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs 
573 
in 
574 
(* Iterate through predicates and normalize them on the go, creating 
575 
fresh variables for any guarantees/assumes/require/ensure *) 
576 
let process_predicates l defvars = 
577 
List.fold_right (fun ee (accu, defvars) > 
578 
let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in 
579 
ee'::accu, defvars 
580 
) l ([], defvars) 
581 
in 
582  
583 

584 
let assume', defsvars = process_predicates s.assume defsvars in 
585 
let guarantees', defsvars = process_predicates s.guarantees defsvars in 
586 
let modes', (defs, vars) = 
587 
List.fold_right ( 
588 
fun m (accu_m, defsvars) > 
589 
let require', defsvars = process_predicates m.require defsvars in 
590 
let ensure', defsvars = process_predicates m.ensure defsvars in 
591 
{ m with require = require'; ensure = ensure' }:: accu_m, defsvars 
592 
) s.modes ([], defsvars) 
593 
in 
594 

595 
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) 
596 

597 

598 
{s with 
599 
locals = s.locals @ new_locals; 
600 
stmts = List.map (fun eq > Eq eq) defs; 
601 
assume = assume'; 
602 
guarantees = guarantees'; 
603 
modes = modes' 
604 
} 
605 
(* let nee _ = () in 
606 
* (\*normalize_eexpr decls iovars in *\) 
607 
* List.iter nee s.assume; 
608 
* List.iter nee s.guarantees; 
609 
* List.iter (fun m > 
610 
* List.iter nee m.require; 
611 
* List.iter nee m.ensure 
612 
* ) s.modes; *) 
613 

614  
615 

616 

617 

618 

619 
(* The normalization phase introduces new local variables 
620 
 output cannot be memories. If this happen, new local variables acting as 
621 
memories are introduced. 
622 
 array constants, pre, arrow, fby, ite, merge, calls to node with index 
623 
access 
624 
Thoses values are shared, ie. no duplicate expressions are introduced. 
625  
626 
Concerning specification, a similar process is applied, replacing an 
627 
expression by a list of local variables and definitions 
628 
*) 
629  
630 
(** normalize_node node returns a normalized node, 
631 
ie. 
632 
 updated locals 
633 
 new equations 
634 
 
635 
*) 
636 
let normalize_node decls node = 
637 
reset_cpt_fresh (); 
638 
let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in 
639 
let not_is_orig_var v = 
640 
List.for_all ((!=) v) orig_vars in 
641 
let norm_ctx = { 
642 
parentid = node.node_id; 
643 
vars = get_node_vars node; 
644 
is_output = (fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs); 
645 
} 
646 
in 
647 

648 
let defs, vars = 
649 
let eqs, auts = get_node_eqs node in 
650 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
651 
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in 
652 
(* Normalize the asserts *) 
653 
let vars, assert_defs, asserts = 
654 
List.fold_left ( 
655 
fun (vars, def_accu, assert_accu) assert_ > 
656 
let assert_expr = assert_.assert_expr in 
657 
let (defs, vars'), expr = 
658 
normalize_expr 
659 
~alias:true (* forcing introduction of new equations for fcn calls *) 
660 
norm_ctx 
661 
[] (* empty offset for arrays *) 
662 
([], vars) (* defvar only contains vars *) 
663 
assert_expr 
664 
in 
665 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
666 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
667 
) (vars, [], []) node.node_asserts in 
668 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
669 
vars and initial locals ones *) 
670 

671 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
672 
beginning of the list the 
673 
local declared ones *) 
674 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
675  
676  
677 
(* Updating annotations: traceability and machine types for fresh variables *) 
678 

679 
(* Compute traceability info: 
680 
 gather newly bound variables 
681 
 compute the associated expression without aliases 
682 
*) 
683 
let new_annots = 
684 
if !Options.traces then 
685 
begin 
686 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
687 
let norm_traceability = { 
688 
annots = List.map (fun v > 
689 
let eq = 
690 
try 
691 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
692 
with Not_found > 
693 
( 
694 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
695 
assert false 
696 
) 
697 
in 
698 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
699 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
700 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 
701 
(["traceability"], pair) 
702 
) diff_vars; 
703 
annot_loc = Location.dummy_loc 
704 
} 
705 
in 
706 
norm_traceability::node.node_annot 
707 
end 
708 
else 
709 
node.node_annot 
710 
in 
711  
712 
let new_annots = 
713 
List.fold_left (fun annots v > 
714 
if Machine_types.is_active && Machine_types.is_exportable v then 
715 
let typ = Machine_types.get_specified_type v in 
716 
let typ_name = Machine_types.type_name typ in 
717  
718 
let loc = v.var_loc in 
719 
let typ_as_string = 
720 
mkexpr 
721 
loc 
722 
(Expr_const 
723 
(Const_string typ_name)) 
724 
in 
725 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 
726 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 
727 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 
728 
else 
729 
annots 
730 
) new_annots new_locals 
731 
in 
732 
let spec = 
733 
begin 
734 
(* Update mutable fields of eexpr to perform normalization of 
735 
specification. 
736  
737 
Careful: we do not normalize annotations, since they can have the form 
738 
x = (a, b, c) *) 
739 
match node.node_spec with None > None  Some s > Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 
740 
end 
741 
in 
742 

743 

744 
let node = 
745 
{ node with 
746 
node_locals = all_locals; 
747 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
748 
node_asserts = asserts; 
749 
node_annot = new_annots; 
750 
node_spec = spec; 
751 
} 
752 
in ((*Printers.pp_node Format.err_formatter node;*) 
753 
node 
754 
) 
755  
756 
let normalize_inode decls nd = 
757 
reset_cpt_fresh (); 
758 
match nd.nodei_spec with 
759 
None > nd 
760 
 Some s > 
761 
let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in 
762 
{ nd with nodei_spec = Some s } 
763 

764 
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl = 
765 
match decl.top_decl_desc with 
766 
 Node nd > 
767 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in 
768 
update_node nd.node_id decl'; 
769 
decl' 
770 
 ImportedNode nd > 
771 
let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in 
772 
update_node nd.nodei_id decl'; 
773 
decl' 
774 

775 
 Include _ Open _  Const _  TypeDef _ > decl 
776  
777 
let normalize_prog p decls = 
778 
(* Backend specific configurations for normalization *) 
779 
params := p; 
780  
781 
(* Main algorithm: iterates over nodes *) 
782 
List.map (normalize_decl decls) decls 
783  
784  
785 
(* Fake interface for outside uses *) 
786 
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr = 
787 
mk_expr_alias_opt 
788 
opt 
789 
{parentid = parentid; vars = ctx_vars; is_output = (fun _ > false) } 
790 
(defs, vars) 
791 
expr 
792  
793 

794 
(* Local Variables: *) 
795 
(* compilecommand:"make C .." *) 
796 
(* End: *) 
797 
