lustrec / src / normalization.ml @ ad4774b0
History  View  Annotate  Download (20.9 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 LustreSpec 
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 

47 
let expr_true loc ck = 
48 
{ expr_tag = Utils.new_tag (); 
49 
expr_desc = Expr_const (Const_tag tag_true); 
50 
expr_type = Type_predef.type_bool; 
51 
expr_clock = ck; 
52 
expr_delay = Delay.new_var (); 
53 
expr_annot = None; 
54 
expr_loc = loc } 
55  
56 
let expr_false loc ck = 
57 
{ expr_tag = Utils.new_tag (); 
58 
expr_desc = Expr_const (Const_tag tag_false); 
59 
expr_type = Type_predef.type_bool; 
60 
expr_clock = ck; 
61 
expr_delay = Delay.new_var (); 
62 
expr_annot = None; 
63 
expr_loc = loc } 
64  
65 
let expr_once loc ck = 
66 
{ expr_tag = Utils.new_tag (); 
67 
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); 
68 
expr_type = Type_predef.type_bool; 
69 
expr_clock = ck; 
70 
expr_delay = Delay.new_var (); 
71 
expr_annot = None; 
72 
expr_loc = loc } 
73  
74 
let is_expr_once = 
75 
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in 
76 
fun expr > Corelang.is_eq_expr expr dummy_expr_once 
77  
78 
let unfold_arrow expr = 
79 
match expr.expr_desc with 
80 
 Expr_arrow (e1, e2) > 
81 
let loc = expr.expr_loc in 
82 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in 
83 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 
84 
 _ > assert false 
85  
86 
let cpt_fresh = ref 0 
87  
88 
(* Generate a new local [node] variable *) 
89 
let mk_fresh_var node loc ty ck = 
90 
let vars = get_node_vars node in 
91 
let rec aux () = 
92 
incr cpt_fresh; 
93 
let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in 
94 
if List.exists (fun v > v.var_id = s) vars then aux () else 
95 
{ 
96 
var_id = s; 
97 
var_orig = false; 
98 
var_dec_type = dummy_type_dec; 
99 
var_dec_clock = dummy_clock_dec; 
100 
var_dec_const = false; 
101 
var_dec_value = None; 
102 
var_parent_nodeid = Some node.node_id; 
103 
var_type = ty; 
104 
var_clock = ck; 
105 
var_loc = loc 
106 
} 
107 
in aux () 
108  
109 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
110 
let get_expr_alias defs expr = 
111 
try Some (List.find (fun eq > is_eq_expr eq.eq_rhs expr) defs) 
112 
with 
113 
 Not_found > None 
114 

115 
(* Replace [expr] with (tuple of) [locals] *) 
116 
let replace_expr locals expr = 
117 
match locals with 
118 
 [] > assert false 
119 
 [v] > { expr with 
120 
expr_tag = Utils.new_tag (); 
121 
expr_desc = Expr_ident v.var_id } 
122 
 _ > { expr with 
123 
expr_tag = Utils.new_tag (); 
124 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } 
125  
126 
let unfold_offsets e offsets = 
127 
let add_offset e d = 
128 
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; 
129 
let res = *) 
130 
{ e with 
131 
expr_tag = Utils.new_tag (); 
132 
expr_loc = d.Dimension.dim_loc; 
133 
expr_type = Types.array_element_type e.expr_type; 
134 
expr_desc = Expr_access (e, d) } 
135 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 
136 
in 
137 
List.fold_left add_offset e offsets 
138  
139 
(* Create an alias for [expr], if none exists yet *) 
140 
let mk_expr_alias node (defs, vars) expr = 
141 
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) 
142 
match get_expr_alias defs expr with 
143 
 Some eq > 
144 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
145 
(defs, vars), replace_expr aliases expr 
146 
 None > 
147 
let new_aliases = 
148 
List.map2 
149 
(mk_fresh_var node expr.expr_loc) 
150 
(Types.type_list_of_type expr.expr_type) 
151 
(Clocks.clock_list_of_clock expr.expr_clock) in 
152 
let new_def = 
153 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
154 
in 
155 
(* 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; *) 
156 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
157  
158 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
159 
and [opt] is true *) 
160 
let mk_expr_alias_opt opt node (defs, vars) expr = 
161 
(*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;*) 
162 
match expr.expr_desc with 
163 
 Expr_ident alias > 
164 
(defs, vars), expr 
165 
 _ > 
166 
match get_expr_alias defs expr with 
167 
 Some eq > 
168 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
169 
(defs, vars), replace_expr aliases expr 
170 
 None > 
171 
if opt 
172 
then 
173 
let new_aliases = 
174 
List.map2 
175 
(mk_fresh_var node expr.expr_loc) 
176 
(Types.type_list_of_type expr.expr_type) 
177 
(Clocks.clock_list_of_clock expr.expr_clock) in 
178 
let new_def = 
179 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
180 
in 
181 
(* Typing and Registering machine type *) 
182 
let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr 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 node offsets norm_element defvars elist = 
201 
List.fold_right 
202 
(fun t (defvars, qlist) > 
203 
let defvars, norm_t = norm_element alias node offsets defvars t in 
204 
(defvars, norm_t :: qlist) 
205 
) elist (defvars, []) 
206  
207 
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node 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 node 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 node defvars norm_expr 
216 
 Expr_power (e1, d) when offsets = [] > 
217 
let defvars, norm_e1 = normalize_expr node 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 node defvars norm_expr 
220 
 Expr_power (e1, d) > 
221 
normalize_expr ~alias:alias node (List.tl offsets) defvars e1 
222 
 Expr_access (e1, d) > 
223 
normalize_expr ~alias:alias node (d::offsets) defvars e1 
224 
 Expr_tuple elist > 
225 
let defvars, norm_elist = 
226 
normalize_list alias node 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 
node 
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 node 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 node [] defvars r in 
251 
defvars, Some norm_r 
252 
in 
253 
let defvars, norm_args = normalize_expr node [] 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 node [] defvars norm_expr in 
258 
normalize_expr ~alias:alias node 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 
node 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 node offsets defvars (unfold_arrow expr) 
266 
 Expr_arrow (e1,e2) > 
267 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
268 
let defvars, norm_e2 = normalize_expr node 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 node defvars norm_expr 
271 
 Expr_pre e > 
272 
let defvars, norm_e = normalize_expr node offsets defvars e in 
273 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in 
274 
mk_expr_alias_opt alias node defvars norm_expr 
275 
 Expr_fby (e1, e2) > 
276 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
277 
let defvars, norm_e2 = normalize_expr node 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 node defvars norm_expr 
280 
 Expr_when (e, c, l) > 
281 
let defvars, norm_e = normalize_expr node 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 node defvars c in 
285 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in 
286 
let defvars, norm_e = normalize_cond_expr node 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 node defvars norm_expr 
289 
 Expr_merge (c, hl) > 
290 
let defvars, norm_hl = normalize_branches node 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 node 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 node offsets defvars hl = 
303 
List.fold_right 
304 
(fun (t, h) (defvars, norm_q) > 
305 
let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in 
306 
defvars, (t, norm_h) :: norm_q 
307 
) 
308 
hl (defvars, []) 
309  
310 
and normalize_array_expr ?(alias=true) node 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 node 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 node (List.tl offsets) defvars e1 
318 
 Expr_access (e1, d) > normalize_array_expr ~alias:alias node (d::offsets) defvars e1 
319 
 Expr_array elist when offsets = [] > 
320 
let defvars, norm_elist = normalize_list alias node 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 node 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 node offsets defvars expr 
326  
327 
and normalize_cond_expr ?(alias=true) node 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 node (d::offsets) defvars e1 
332 
 Expr_ite (c, t, e) > 
333 
let defvars, norm_c = normalize_guard node defvars c in 
334 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in 
335 
let defvars, norm_e = normalize_cond_expr node 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 node 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 node offsets defvars expr 
344 
in 
345 
mk_expr_alias_opt true node defvars norm_expr 
346 
 _ > (* default case without the force_alias_ite option *) 
347 
normalize_expr ~alias:alias node offsets defvars expr 
348 

349 
and normalize_guard node defvars expr = 
350 
let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in 
351 
mk_expr_alias_opt true node defvars norm_expr 
352  
353 
(* outputs cannot be memories as well. If so, introduce new local variable. 
354 
*) 
355 
let decouple_outputs node 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 List.exists (fun o > o.var_id = v) node.node_outputs 
361 
then 
362 
let newvar = mk_fresh_var node 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 node 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 node defvars eq in 
382 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] 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 node [] 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 node [] 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 node [] 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 node [] defvars eq.eq_rhs in 
399 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
400 
norm_eq::defs', vars' 
401  
402 
(** normalize_node node returns a normalized node, 
403 
ie. 
404 
 updated locals 
405 
 new equations 
406 
 
407 
*) 
408 
let normalize_node node = 
409 
cpt_fresh := 0; 
410 
let inputs_outputs = node.node_inputs@node.node_outputs in 
411 
let orig_vars = inputs_outputs@node.node_locals in 
412 
let not_is_orig_var v = 
413 
List.for_all ((!=) v) orig_vars in 
414 
let defs, vars = 
415 
let eqs, auts = get_node_eqs node in 
416 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
417 
List.fold_left (normalize_eq node) ([], orig_vars) eqs in 
418 
(* Normalize the asserts *) 
419 
let vars, assert_defs, asserts = 
420 
List.fold_left ( 
421 
fun (vars, def_accu, assert_accu) assert_ > 
422 
let assert_expr = assert_.assert_expr in 
423 
let (defs, vars'), expr = 
424 
normalize_expr 
425 
~alias:true (* forcing introduction of new equations for fcn calls *) 
426 
node 
427 
[] (* empty offset for arrays *) 
428 
([], vars) (* defvar only contains vars *) 
429 
assert_expr 
430 
in 
431 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
432 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
433 
) (vars, [], []) node.node_asserts in 
434 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
435 
vars and initial locals ones *) 
436 

437 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
438 
beginning of the list the 
439 
local declared ones *) 
440 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
441  
442  
443 
(* Updating annotations: traceability and machine types for fresh variables *) 
444 

445 
(* Compute traceability info: 
446 
 gather newly bound variables 
447 
 compute the associated expression without aliases 
448 
*) 
449 
let new_annots = 
450 
if !Options.traces then 
451 
begin 
452 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
453 
let norm_traceability = { 
454 
annots = List.map (fun v > 
455 
let eq = 
456 
try 
457 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
458 
with Not_found > 
459 
( 
460 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
461 
assert false 
462 
) 
463 
in 
464 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
465 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
466 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 
467 
(["traceability"], pair) 
468 
) diff_vars; 
469 
annot_loc = Location.dummy_loc 
470 
} 
471 
in 
472 
norm_traceability::node.node_annot 
473 
end 
474 
else 
475 
node.node_annot 
476 
in 
477  
478 
let new_annots = 
479 
List.fold_left (fun annots v > 
480 
if Machine_types.is_active && Machine_types.is_exportable v then 
481 
let typ = Machine_types.get_specified_type v in 
482 
let typ_name = Machine_types.type_name typ in 
483  
484 
let loc = v.var_loc in 
485 
let typ_as_string = 
486 
mkexpr 
487 
loc 
488 
(Expr_const 
489 
(Const_string typ_name)) 
490 
in 
491 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 
492 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 
493 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 
494 
else 
495 
annots 
496 
) new_annots new_locals 
497 
in 
498 
let node = 
499 
{ node with 
500 
node_locals = all_locals; 
501 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
502 
node_asserts = asserts; 
503 
node_annot = new_annots; 
504 
} 
505 
in ((*Printers.pp_node Format.err_formatter node;*) 
506 
node 
507 
) 
508  
509  
510 
let normalize_decl decl = 
511 
match decl.top_decl_desc with 
512 
 Node nd > 
513 
let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in 
514 
Hashtbl.replace Corelang.node_table nd.node_id decl'; 
515 
decl' 
516 
 Open _  ImportedNode _  Const _  TypeDef _ > decl 
517  
518 
let normalize_prog p decls = 
519 
(* Backend specific configurations for normalization *) 
520 
params := p; 
521  
522 
(* Main algorithm: iterates over nodes *) 
523 
List.map normalize_decl decls 
524  
525 

526 
(* Local Variables: *) 
527 
(* compilecommand:"make C .." *) 
528 
(* End: *) 
529 
