Revision 36454535
Added by PierreLoïc Garoche over 8 years ago
src/normalization.ml  

196  196 
let defvars, norm_elist = 
197  197 
normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias) defvars elist in 
198  198 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
199 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id && Types.is_array_type expr.expr_type > 

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

199 
 Expr_appl (id, args, None) 

200 
when Basic_library.is_internal_fun id 

201 
&& Types.is_array_type expr.expr_type > 

202 
let defvars, norm_args = 

203 
normalize_list 

204 
alias 

205 
node 

206 
offsets 

207 
(fun _ > normalize_array_expr ~alias:true) 

208 
defvars 

209 
(expr_list_of_expr args) 

210 
in 

201  211 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
202  212 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id > 
203  213 
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in 
...  ...  
341  351 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
342  352 
norm_eq::defs', vars' 
343  353  
354 
(** normalize_node node returns a normalized node, 

355 
ie. 

356 
 updated locals 

357 
 new equations 

358 
 

359 
*) 

344  360 
let normalize_node node = 
345  361 
cpt_fresh := 0; 
346  362 
let inputs_outputs = node.node_inputs@node.node_outputs in 
347  363 
let is_local v = 
348  364 
List.for_all ((!=) v) inputs_outputs in 
365 
let orig_vars = inputs_outputs@node.node_locals in 

349  366 
let defs, vars = 
350 
List.fold_left (normalize_eq node) ([], inputs_outputs@node.node_locals) node.node_eqs in 

367 
List.fold_left (normalize_eq node) ([], orig_vars) node.node_eqs in 

368 
(* Normalize the asserts *) 

369 
let vars, assert_defs, asserts = 

370 
List.fold_left ( 

371 
fun (vars, def_accu, assert_accu) assert_ > 

372 
let assert_expr = assert_.assert_expr in 

373 
let (defs, vars'), expr = 

374 
normalize_expr 

375 
~alias:false 

376 
node 

377 
[] (* empty offset for arrays *) 

378 
([], vars) (* defvar only contains vars *) 

379 
assert_expr 

380 
in 

381 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 

382 
) (vars, [], []) node.node_asserts in 

351  383 
let new_locals = List.filter is_local vars in 
384 
(* Compute tracebaility info: 

385 
 gather newly bound variables 

386 
 compute the associated expression without aliases 

387 
*) 

388 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) new_locals in 

389 
let norm_traceability = { 

390 
annots = 

391 
List.map 

392 
(fun v > 

393 
let expr = substitute_expr diff_vars defs ( 

394 
let eq = List.find (fun eq > eq.eq_lhs = [v.var_id]) defs in 

395 
eq.eq_rhs) in 

396 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 

397 
["horn_backend";"trace"], pair 

398 
) 

399 
diff_vars ; 

400 
annot_loc = Location.dummy_loc 

401 
} 

402  
403 
in 

352  404 
let node = 
353 
{ node with node_locals = new_locals; node_eqs = defs } 

405 
{ node with 

406 
node_locals = new_locals; 

407 
node_eqs = defs @ assert_defs; 

408 
node_asserts = asserts; 

409 
node_annot = norm_traceability::node.node_annot; 

410 
} 

354  411 
in ((*Printers.pp_node Format.err_formatter node;*) node) 
355  412  
356  413 
let normalize_decl decl = 
Also available in: Unified diff
Merged horn_traces branch