Module Formula_optim

module Formula_optim: sig .. end
Formula optimizations


Constant propagation

Functions trying to propagate constants on the given expression.

val propagate_cst : Formula_type.formula ->
?recursive:int -> Smtlib2.smt_expr -> Smtlib2.smt_expr
val propagate_cst_bv : Formula_type.formula ->
?recursive:int -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr
val propagate_cst_abv : Formula_type.formula ->
?recursive:int -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr

Rebase

In the formula all the variables are in a SSA form. The rebase optimization will intent to redefine variables used in the expression by older variables declaration eg: esp1 := esp0 + 4 esp2 := esp1 + 4 esp3 := esp2 + 4 => esp2+4 will be replaced by esp1+8 thus obsolating the esp2 declaration. This reduce the number of variables defined and is crucial for some other optimizations

val rebase_expr : Formula_type.formula -> Smtlib2.smt_expr -> Smtlib2.smt_expr
val rebase_bvexpr : Formula_type.formula -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr
val rebase_abvexpr : Formula_type.formula -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr

Read-Over-Write

The Read-Over-Write as an array theory optimization based on the fact that read(store(M, addr, X),addr) = X. Thus the optimization will try for every read to replace it by its store value (if any). To do so the classic linear method look in the store chain if the read address has previously been written. The hybrid method does the same but in a more efficient manner.

val get_row_stats : unit -> int * int * int * int * int * int
Returns some stats about replacement that took place in the RoW optimization. Return values are:

Classic (linear)


val read_over_write : Formula_type.formula -> Smtlib2.smt_expr -> Smtlib2.smt_expr
val read_over_write_bv : Formula_type.formula -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr
val read_over_write_abv : Formula_type.formula -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr

Hybrid


val update_hybrid_memory : Formula_type.formula ->
string ->
Smtlib2.smt_abv_expr -> Formula_type.hybrid_mem_t * Smtlib2.smt_abv_expr
val read_over_write_hybrid : Formula_type.formula -> Smtlib2.smt_expr -> Smtlib2.smt_expr
val read_over_write_hybrid_bv : Formula_type.formula -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr
val read_over_write_hybrid_abv : Formula_type.formula -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr

Memory flattening

We call memory flattening the act of removing every array operations in the specific cases where all select/store are being made on constant addresses. This allows to generate formulas "solvable" by solvers not supporting the SMT array theory

class memory_flattener_visitor : object .. end
Class that remove all read in memory by constant bitvector values