Revision 9c4624e4
Added by Teme Kahsai about 9 years ago
src/normalization.ml  

53  53 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 
54  54 
 _ > assert false 
55  55  
56 
let unfold_arrow_active = ref true


56 
let unfold_arrow_active = ref true 

57  57 
let cpt_fresh = ref 0 
58  58  
59  59 
(* Generate a new local [node] variable *) 
...  ...  
131  131 
match expr.expr_desc with 
132  132 
 Expr_ident alias > 
133  133 
defvars, expr 
134 
 _ >


134 
 _ > 

135  135 
if opt 
136  136 
then 
137  137 
mk_expr_alias node defvars expr 
138  138 
else 
139  139 
defvars, expr 
140  140  
141 
(* Create a (normalized) expression from [ref_e],


141 
(* Create a (normalized) expression from [ref_e], 

142  142 
replacing description with [norm_d], 
143 
taking propagated [offsets] into account


143 
taking propagated [offsets] into account 

144  144 
in order to change expression type *) 
145  145 
let mk_norm_expr offsets ref_e norm_d = 
146  146 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
...  ...  
161  161 
let rec normalize_expr ?(alias=true) node offsets defvars expr = 
162  162 
(* Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
163  163 
match expr.expr_desc with 
164 
 Expr_const _


164 
 Expr_const _ 

165  165 
 Expr_ident _ > defvars, unfold_offsets expr offsets 
166  166 
 Expr_array elist > 
167  167 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
...  ...  
175  175 
normalize_expr ~alias:alias node (List.tl offsets) defvars e1 
176  176 
 Expr_access (e1, d) > 
177  177 
normalize_expr ~alias:alias node (d::offsets) defvars e1 
178 
 Expr_tuple elist >


178 
 Expr_tuple elist > 

179  179 
let defvars, norm_elist = 
180  180 
normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias) defvars elist in 
181  181 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
182 
 Expr_appl (id, args, None)


183 
when Basic_library.is_internal_fun id


182 
 Expr_appl (id, args, None) 

183 
when Basic_library.is_internal_fun id 

184  184 
&& Types.is_array_type expr.expr_type > 
185 
let defvars, norm_args =


186 
normalize_list


185 
let defvars, norm_args = 

186 
normalize_list 

187  187 
alias 
188  188 
node 
189 
offsets


190 
(fun _ > normalize_array_expr ~alias:true)


191 
defvars


192 
(expr_list_of_expr args)


189 
offsets 

190 
(fun _ > normalize_array_expr ~alias:true) 

191 
defvars 

192 
(expr_list_of_expr args) 

193  193 
in 
194  194 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
195  195 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id > 
...  ...  
233  233 
let defvars, norm_hl = normalize_branches node offsets defvars hl in 
234  234 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in 
235  235 
mk_expr_alias_opt alias node defvars norm_expr 
236 


236  
237  237 
(* Creates a conditional with a merge construct, which is more lazy *) 
238  238 
(* 
239  239 
let norm_conditional_as_merge alias node norm_expr offsets defvars expr = 
...  ...  
309  309 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in 
310  310 
defvars', {eq with eq_lhs = lhs' } 
311  311  
312 
let rec normalize_eq node defvars eq =


312 
let rec normalize_eq node defvars eq = 

313  313 
match eq.eq_rhs.expr_desc with 
314  314 
 Expr_pre _ 
315  315 
 Expr_fby _ > 
...  ...  
334  334 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
335  335 
norm_eq::defs', vars' 
336  336  
337 
(** normalize_node node returns a normalized node,


338 
ie.


337 
(** normalize_node node returns a normalized node, 

338 
ie. 

339  339 
 updated locals 
340  340 
 new equations 
341 



341 
 

342  342 
*) 
343 
let normalize_node node =


343 
let normalize_node node = 

344  344 
cpt_fresh := 0; 
345  345 
let inputs_outputs = node.node_inputs@node.node_outputs in 
346  346 
let is_local v = 
347  347 
List.for_all ((!=) v) inputs_outputs in 
348  348 
let orig_vars = inputs_outputs@node.node_locals in 
349 
let defs, vars =


349 
let defs, vars = 

350  350 
List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in 
351  351 
(* Normalize the asserts *) 
352 
let vars, assert_defs, asserts =


352 
let vars, assert_defs, asserts = 

353  353 
List.fold_left ( 
354  354 
fun (vars, def_accu, assert_accu) assert_ > 
355  355 
let assert_expr = assert_.assert_expr in 
356 
let (defs, vars'), expr =


357 
normalize_expr


358 
~alias:true


359 
node


356 
let (defs, vars'), expr = 

357 
normalize_expr 

358 
~alias:true 

359 
node 

360  360 
[] (* empty offset for arrays *) 
361  361 
([], vars) (* defvar only contains vars *) 
362  362 
assert_expr 
363  363 
in 
364 
(* Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars'; *)


364 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)


365  365 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
366  366 
) (vars, [], []) node.node_asserts in 
367  367 
let new_locals = List.filter is_local vars in 
368 
(* Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals; *)


368 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)


369  369  
370  370 
let new_annots = 
371  371 
if !Options.traces then 
372  372 
begin 
373 
(* Compute traceability info:


373 
(* Compute traceability info: 

374  374 
 gather newly bound variables 
375 
 compute the associated expression without aliases


375 
 compute the associated expression without aliases 

376  376 
*) 
377  377 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) new_locals in 
378  378 
let norm_traceability = { 
379  379 
annots = List.map (fun v > 
380  380 
let eq = 
381  381 
try 
382 
List.find (fun eq > eq.eq_lhs = [v.var_id]) defs


382 
List.find (fun eq > eq.eq_lhs = [v.var_id]) defs 

383  383 
with Not_found > (Format.eprintf "var not found %s@." v.var_id; assert false) in 
384  384 
let expr = substitute_expr diff_vars defs eq.eq_rhs in 
385  385 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
386  386 
(["traceability"], pair) 
387  387 
) diff_vars; 
388  388 
annot_loc = Location.dummy_loc 
389 
}


389 
} 

390  390 
in 
391  391 
norm_traceability::node.node_annot 
392  392 
end 
...  ...  
395  395 
in 
396  396  
397  397 
let node = 
398 
{ node with


399 
node_locals = new_locals;


398 
{ node with 

399 
node_locals = new_locals; 

400  400 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
401  401 
node_asserts = asserts; 
402  402 
node_annot = new_annots; 
403  403 
} 
404 
in ((*Printers.pp_node Format.err_formatter node;*)


404 
in ((*Printers.pp_node Format.err_formatter node;*) 

405  405 
node 
406  406 
) 
407  407  
...  ...  
413  413 
Hashtbl.replace Corelang.node_table nd.node_id decl'; 
414  414 
decl' 
415  415 
 Open _  ImportedNode _  Const _  TypeDef _ > decl 
416 


417 
let normalize_prog decls =


416  
417 
let normalize_prog decls = 

418  418 
List.map normalize_decl decls 
419  419  
420  420 
(* Local Variables: *) 
Also available in: Unified diff
do not use lusi for horn, and some logging for horn