Revision 36454535
Added by Pierre-Loïc Garoche over 10 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