Revision 95944ba1 src/normalization.ml
src/normalization.ml  

43  43 
force_alias_internal_fun =false; 
44  44 
} 
45  45  
46 


46 
type norm_ctx_t = 

47 
{ 

48 
parentid: ident; 

49 
vars: var_decl list; 

50 
is_output: ident > bool; 

51 
} 

52  
53 


47  54 
let expr_true loc ck = 
48  55 
{ expr_tag = Utils.new_tag (); 
49  56 
expr_desc = Expr_const (Const_tag tag_true); 
...  ...  
115  122 
in 
116  123 
List.fold_left add_offset e offsets 
117  124  
125 
(* IS IT USED ? TODO 

118  126 
(* Create an alias for [expr], if none exists yet *) 
119 
let mk_expr_alias node (defs, vars) expr =


127 
let mk_expr_alias (parentid, vars) (defs, vars) expr =


120  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;*) 
121  129 
match get_expr_alias defs expr with 
122  130 
 Some eq > 
...  ...  
125  133 
 None > 
126  134 
let new_aliases = 
127  135 
List.map2 
128 
(mk_fresh_var node expr.expr_loc)


136 
(mk_fresh_var (parentid, vars) expr.expr_loc)


129  137 
(Types.type_list_of_type expr.expr_type) 
130  138 
(Clocks.clock_list_of_clock expr.expr_clock) in 
131  139 
let new_def = 
...  ...  
133  141 
in 
134  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; *) 
135  143 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
136  
144 
*) 

145 


137  146 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
138  147 
and [opt] is true *) 
139 
let mk_expr_alias_opt opt node (defs, vars) expr =


148 
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =


140  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;*) 
141  150 
match expr.expr_desc with 
142  151 
 Expr_ident alias > 
...  ...  
161  170 
then 
162  171 
let new_aliases = 
163  172 
List.map2 
164 
(mk_fresh_var node expr.expr_loc)


173 
(mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)


165  174 
(Types.type_list_of_type expr.expr_type) 
166  175 
(Clocks.clock_list_of_clock expr.expr_clock) in 
167  176 
let new_def = 
168  177 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
169  178 
in 
170  179 
(* Typing and Registering machine type *) 
171 
let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr in


180 
let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr in


172  181 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
173  182 
else 
174  183 
(defs, vars), expr 
...  ...  
186  195 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 
187  196 

188  197 
(* normalize_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *) 
189 
let rec normalize_list alias node offsets norm_element defvars elist =


198 
let rec normalize_list alias norm_ctx offsets norm_element defvars elist =


190  199 
List.fold_right 
191  200 
(fun t (defvars, qlist) > 
192 
let defvars, norm_t = norm_element alias node offsets defvars t in


201 
let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in


193  202 
(defvars, norm_t :: qlist) 
194  203 
) elist (defvars, []) 
195  204  
196 
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =


205 
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr =


197  206 
(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
198  207 
match expr.expr_desc with 
199  208 
 Expr_const _ 
200  209 
 Expr_ident _ > defvars, unfold_offsets expr offsets 
201  210 
 Expr_array elist > 
202 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in


211 
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in


203  212 
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in 
204 
mk_expr_alias_opt alias node defvars norm_expr


213 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


205  214 
 Expr_power (e1, d) when offsets = [] > 
206 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in


215 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


207  216 
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in 
208 
mk_expr_alias_opt alias node defvars norm_expr


217 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


209  218 
 Expr_power (e1, d) > 
210 
normalize_expr ~alias:alias node (List.tl offsets) defvars e1


219 
normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1


211  220 
 Expr_access (e1, d) > 
212 
normalize_expr ~alias:alias node (d::offsets) defvars e1


221 
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1


213  222 
 Expr_tuple elist > 
214  223 
let defvars, norm_elist = 
215 
normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias ~alias_basic:false) defvars elist in


224 
normalize_list alias norm_ctx offsets (fun alias > normalize_expr ~alias:alias ~alias_basic:false) defvars elist in


216  225 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
217  226 
 Expr_appl (id, args, None) 
218  227 
when Basic_library.is_homomorphic_fun id 
...  ...  
220  229 
let defvars, norm_args = 
221  230 
normalize_list 
222  231 
alias 
223 
node


232 
norm_ctx


224  233 
offsets 
225  234 
(fun _ > normalize_array_expr ~alias:true) 
226  235 
defvars 
...  ...  
229  238 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
230  239 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr 
231  240 
&& not (!params.force_alias_internal_fun  alias_basic) > 
232 
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in


241 
let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in


233  242 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 
234  243 
 Expr_appl (id, args, r) > 
235  244 
let defvars, r = 
236  245 
match r with 
237  246 
 None > defvars, None 
238  247 
 Some r > 
239 
let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in


248 
let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in


240  249 
defvars, Some norm_r 
241  250 
in 
242 
let defvars, norm_args = normalize_expr node [] defvars args in


251 
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in


243  252 
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in 
244  253 
if offsets <> [] 
245  254 
then 
246 
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in


247 
normalize_expr ~alias:alias node offsets defvars norm_expr


255 
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in


256 
normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr


248  257 
else 
249  258 
mk_expr_alias_opt (alias && (!params.force_alias_internal_fun  alias_basic 
250  259 
 not (Basic_library.is_expr_internal_fun expr))) 
251 
node defvars norm_expr


260 
norm_ctx defvars norm_expr


252  261 
 Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) > 
253  262 
(* Here we differ from Colaco paper: arrows are pushed to the top *) 
254 
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)


263 
normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr)


255  264 
 Expr_arrow (e1,e2) > 
256 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in


257 
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in


265 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


266 
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in


258  267 
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in 
259 
mk_expr_alias_opt alias node defvars norm_expr


268 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


260  269 
 Expr_pre e > 
261 
let defvars, norm_e = normalize_expr node offsets defvars e in


270 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in


262  271 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in 
263 
mk_expr_alias_opt alias node defvars norm_expr


272 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


264  273 
 Expr_fby (e1, e2) > 
265 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in


266 
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in


274 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


275 
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in


267  276 
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in 
268 
mk_expr_alias_opt alias node defvars norm_expr


277 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


269  278 
 Expr_when (e, c, l) > 
270 
let defvars, norm_e = normalize_expr node offsets defvars e in


279 
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in


271  280 
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) 
272  281 
 Expr_ite (c, t, e) > 
273 
let defvars, norm_c = normalize_guard node defvars c in


274 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in


275 
let defvars, norm_e = normalize_cond_expr node offsets defvars e in


282 
let defvars, norm_c = normalize_guard norm_ctx defvars c in


283 
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in


284 
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in


276  285 
let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in 
277 
mk_expr_alias_opt alias node defvars norm_expr


286 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


278  287 
 Expr_merge (c, hl) > 
279 
let defvars, norm_hl = normalize_branches node offsets defvars hl in


288 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in


280  289 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in 
281 
mk_expr_alias_opt alias node defvars norm_expr


290 
mk_expr_alias_opt alias norm_ctx defvars norm_expr


282  291  
283  292 
(* Creates a conditional with a merge construct, which is more lazy *) 
284  293 
(* 
...  ...  
288  297 
let defvars, norm_t = norm_expr (alias node offsets defvars t in 
289  298 
 _ > assert false 
290  299 
*) 
291 
and normalize_branches node offsets defvars hl =


300 
and normalize_branches norm_ctx offsets defvars hl =


292  301 
List.fold_right 
293  302 
(fun (t, h) (defvars, norm_q) > 
294 
let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in


303 
let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in


295  304 
defvars, (t, norm_h) :: norm_q 
296  305 
) 
297  306 
hl (defvars, []) 
298  307  
299 
and normalize_array_expr ?(alias=true) node offsets defvars expr =


308 
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =


300  309 
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
301  310 
match expr.expr_desc with 
302  311 
 Expr_power (e1, d) when offsets = [] > 
303 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in


312 
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in


304  313 
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) 
305  314 
 Expr_power (e1, d) > 
306 
normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1


307 
 Expr_access (e1, d) > normalize_array_expr ~alias:alias node (d::offsets) defvars e1


315 
normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1


316 
 Expr_access (e1, d) > normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1


308  317 
 Expr_array elist when offsets = [] > 
309 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in


318 
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in


310  319 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 
311  320 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr > 
312 
let defvars, norm_args = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in


321 
let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in


313  322 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
314 
 _ > normalize_expr ~alias:alias node offsets defvars expr


323 
 _ > normalize_expr ~alias:alias norm_ctx offsets defvars expr


315  324  
316 
and normalize_cond_expr ?(alias=true) node offsets defvars expr =


325 
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr =


317  326 
(*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
318  327 
match expr.expr_desc with 
319  328 
 Expr_access (e1, d) > 
320 
normalize_cond_expr ~alias:alias node (d::offsets) defvars e1


329 
normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1


321  330 
 Expr_ite (c, t, e) > 
322 
let defvars, norm_c = normalize_guard node defvars c in


323 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in


324 
let defvars, norm_e = normalize_cond_expr node offsets defvars e in


331 
let defvars, norm_c = normalize_guard norm_ctx defvars c in


332 
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in


333 
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in


325  334 
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) 
326  335 
 Expr_merge (c, hl) > 
327 
let defvars, norm_hl = normalize_branches node offsets defvars hl in


336 
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in


328  337 
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) 
329  338 
 _ when !params.force_alias_ite > 
330  339 
(* Forcing alias creation for then/else expressions *) 
331  340 
let defvars, norm_expr = 
332 
normalize_expr ~alias:alias node offsets defvars expr


341 
normalize_expr ~alias:alias norm_ctx offsets defvars expr


333  342 
in 
334 
mk_expr_alias_opt true node defvars norm_expr


343 
mk_expr_alias_opt true norm_ctx defvars norm_expr


335  344 
 _ > (* default case without the force_alias_ite option *) 
336 
normalize_expr ~alias:alias node offsets defvars expr


345 
normalize_expr ~alias:alias norm_ctx offsets defvars expr


337  346 

338 
and normalize_guard node defvars expr =


339 
let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in


340 
mk_expr_alias_opt true node defvars norm_expr


347 
and normalize_guard norm_ctx defvars expr =


348 
let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in


349 
mk_expr_alias_opt true norm_ctx defvars norm_expr


341  350  
342  351 
(* outputs cannot be memories as well. If so, introduce new local variable. 
343  352 
*) 
344 
let decouple_outputs node defvars eq =


353 
let decouple_outputs norm_ctx defvars eq =


345  354 
let rec fold_lhs defvars lhs tys cks = 
346  355 
match lhs, tys, cks with 
347  356 
 [], [], [] > defvars, [] 
348  357 
 v::qv, t::qt, c::qc > let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in 
349 
if List.exists (fun o > o.var_id = v) node.node_outputs


358 
if norm_ctx.is_output v


350  359 
then 
351 
let newvar = mk_fresh_var node eq.eq_loc t c in


360 
let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in


352  361 
let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in 
353  362 
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q 
354  363 
else 
...  ...  
362  371 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in 
363  372 
defvars', {eq with eq_lhs = lhs' } 
364  373  
365 
let rec normalize_eq node defvars eq =


374 
let rec normalize_eq norm_ctx defvars eq =


366  375 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) 
367  376 
match eq.eq_rhs.expr_desc with 
368  377 
 Expr_pre _ 
369  378 
 Expr_fby _ > 
370 
let (defvars', eq') = decouple_outputs node defvars eq in


371 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in


379 
let (defvars', eq') = decouple_outputs norm_ctx defvars eq in


380 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in


372  381 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 
373  382 
(norm_eq::defs', vars') 
374  383 
 Expr_array _ > 
375 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in


384 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in


376  385 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
377  386 
(norm_eq::defs', vars') 
378  387 
 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type > 
379 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in


388 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in


380  389 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
381  390 
(norm_eq::defs', vars') 
382  391 
 Expr_appl _ > 
383 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in


392 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in


384  393 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
385  394 
(norm_eq::defs', vars') 
386  395 
 _ > 
387 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in


396 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in


388  397 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
389  398 
norm_eq::defs', vars' 
390  399  
391 
let normalize_eq_split node defvars eq =


400 
let normalize_eq_split norm_ctx defvars eq =


392  401 
try 
393 
let defs, vars = normalize_eq node defvars eq in


402 
let defs, vars = normalize_eq norm_ctx defvars eq in


394  403 
List.fold_right (fun eq (def, vars) > 
395  404 
let eq_defs = Splitting.tuple_split_eq eq in 
396  405 
if eq_defs = [eq] then 
397  406 
eq::def, vars 
398  407 
else 
399 
List.fold_left (normalize_eq node) (def, vars) eq_defs


408 
List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs


400  409 
) defs ([], vars) 
401  410  
402  411 
with _ > ( 
...  ...  
404  413 
assert false 
405  414 
) 
406  415  
407 
let normalize_eexpr decls node vars ee =


416 
let normalize_eexpr decls norm_ctx vars ee = ee (*


408  417 
(* New output variable *) 
409  418 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in 
410  419 
let output_var = 
...  ...  
474  483 

475  484 
; 
476  485 
raise exc 
477 


486 
*) 

478  487 

479  488 

480 
let normalize_spec decls node vars s = 

481 
let nee = normalize_eexpr decls node vars in 

489 
let normalize_spec decls iovars s = s (* 

490 
(* Each stmt is normalized *) 

491 
let orig_vars = iovars @ s.locals in 

492 
let not_is_orig_var v = 

493 
List.for_all ((!=) v) orig_vars in 

494 
let defs, vars = 

495 
let eqs, auts = List.fold_right (fun (el,al) s > match s with Eq e > e::el, al  Aut a > el, a::al) s.stmts ([], []) in 

496 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

497 
List.fold_left (normalize_eq node) ([], orig_vars) eqs 

498 
in 

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

500  
501 
(* 

502 


503 
{s with 

504 
locals = s.locals @ new_locals; 

505 
stmts = List.map (fun eq > Eq eq) defs; 

506 
let nee _ = () in 

507 
(*normalize_eexpr decls iovars in *) 

482  508 
List.iter nee s.assume; 
483  509 
List.iter nee s.guarantees; 
484  510 
List.iter (fun m > 
485  511 
List.iter nee m.require; 
486  512 
List.iter nee m.ensure 
487 
) s.modes 

488 


513 
) s.modes; 

514 
*) 

515 
s 

516 
*) 

489  517 

490  518 
(* The normalization phase introduces new local variables 
491  519 
 output cannot be memories. If this happen, new local variables acting as 
...  ...  
510  538 
let orig_vars = inputs_outputs@node.node_locals in 
511  539 
let not_is_orig_var v = 
512  540 
List.for_all ((!=) v) orig_vars in 
541 
let norm_ctx = { 

542 
parentid = node.node_id; 

543 
vars = get_node_vars node; 

544 
is_output = (fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs); 

545 
} 

546 
in 

547 


513  548 
let defs, vars = 
514  549 
let eqs, auts = get_node_eqs node in 
515  550 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
516 
List.fold_left (normalize_eq node) ([], orig_vars) eqs in


551 
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in


517  552 
(* Normalize the asserts *) 
518  553 
let vars, assert_defs, asserts = 
519  554 
List.fold_left ( 
...  ...  
522  557 
let (defs, vars'), expr = 
523  558 
normalize_expr 
524  559 
~alias:true (* forcing introduction of new equations for fcn calls *) 
525 
node


560 
norm_ctx


526  561 
[] (* empty offset for arrays *) 
527  562 
([], vars) (* defvar only contains vars *) 
528  563 
assert_expr 
...  ...  
594  629 
annots 
595  630 
) new_annots new_locals 
596  631 
in 
597 
if !Options.spec <> "no" then


632 
let spec =


598  633 
begin 
599  634 
(* Update mutable fields of eexpr to perform normalization of 
600  635 
specification. 
601  636  
602  637 
Careful: we do not normalize annotations, since they can have the form 
603  638 
x = (a, b, c) *) 
604 
(* List.iter *) 

605 
(* (fun a > *) 

606 
(* List.iter *) 

607 
(* (fun (_, ann) > normalize_eexpr decls node inputs_outputs ann) *) 

608 
(* a.annots *) 

609 
(* ) *) 

610 
(* node.node_annot; *) 

611 
match node.node_spec with None > ()  Some s > normalize_spec decls node [] s 

612 
end; 

639 
match node.node_spec with None > None  Some s > Some (normalize_spec decls inputs_outputs s) 

640 
end 

641 
in 

642 


613  643 

614 


615  644 
let node = 
616  645 
{ node with 
617  646 
node_locals = all_locals; 
618  647 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
619  648 
node_asserts = asserts; 
620  649 
node_annot = new_annots; 
650 
node_spec = spec; 

621  651 
} 
622  652 
in ((*Printers.pp_node Format.err_formatter node;*) 
623  653 
node 
624  654 
) 
625  655  
626  
656 
let normalize_inode decls nd = 

657 
reset_cpt_fresh (); 

658 
match nd.nodei_spec with 

659 
None > nd 

660 
 Some s > 

661 
let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in 

662 
let s = normalize_spec decls inputs_outputs s in 

663 
{ nd with nodei_spec = Some s } 

664 


627  665 
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl = 
628  666 
match decl.top_decl_desc with 
629  667 
 Node nd > 
630 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in 

631 
Hashtbl.replace Corelang.node_table nd.node_id decl'; 

632 
decl' 

633 
 Include _ Open _  ImportedNode _  Const _  TypeDef _ > decl 

668 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in 

669 
update_node nd.node_id decl'; 

670 
decl' 

671 
 ImportedNode nd > 

672 
let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in 

673 
update_node nd.nodei_id decl'; 

674 
decl' 

675 


676 
 Include _ Open _  Const _  TypeDef _ > decl 

634  677  
635  678 
let normalize_prog p decls = 
636  679 
(* Backend specific configurations for normalization *) 
...  ...  
639  682 
(* Main algorithm: iterates over nodes *) 
640  683 
List.map (normalize_decl decls) decls 
641  684  
685  
686 
(* Fake interface for outside uses *) 

687 
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr = 

688 
mk_expr_alias_opt 

689 
opt 

690 
{parentid = parentid; vars = ctx_vars; is_output = (fun _ > false) } 

691 
(defs, vars) 

692 
expr 

693  
642  694 

643  695 
(* Local Variables: *) 
644  696 
(* compilecommand:"make C .." *) 
Also available in: Unified diff