Static Value-Flow Analysis
|
#include <RelationSolver.h>
Public Member Functions | |
RelationSolver ()=default | |
Z3Expr | gamma_hat (const AbstractState &exeState) const |
Return Z3Expr according to valToValMap. More... | |
Z3Expr | gamma_hat (const AbstractState &alpha, const AbstractState &exeState) const |
Return Z3Expr according to another valToValMap. More... | |
Z3Expr | gamma_hat (u32_t id, const AbstractState &exeState) const |
Return Z3Expr from a NodeID. More... | |
AbstractState | abstract_consequence (const AbstractState &lower, const AbstractState &upper, const AbstractState &domain) const |
AbstractState | beta (const Map< u32_t, s32_t > &sigma, const AbstractState &exeState) const |
virtual Z3Expr | toIntZ3Expr (u32_t varId) const |
Return Z3 expression lazily based on SVFVar ID. More... | |
Z3Expr | toIntVal (s32_t f) const |
Z3Expr | toRealVal (BoundedDouble f) const |
AbstractState | bilateral (const AbstractState &domain, const Z3Expr &phi, u32_t descend_check=0) |
AbstractState | RSY (const AbstractState &domain, const Z3Expr &phi) |
Map< u32_t, s32_t > | BoxedOptSolver (const Z3Expr &phi, Map< u32_t, s32_t > &ret, Map< u32_t, s32_t > &low_values, Map< u32_t, s32_t > &high_values) |
AbstractState | BS (const AbstractState &domain, const Z3Expr &phi) |
void | updateMap (Map< u32_t, s32_t > &map, u32_t key, const s32_t &value) |
void | decide_cpa_ext (const Z3Expr &phi, Map< u32_t, Z3Expr > &, Map< u32_t, s32_t > &, Map< u32_t, s32_t > &, Map< u32_t, s32_t > &, Map< u32_t, s32_t > &) |
Definition at line 38 of file RelationSolver.h.
|
default |
AbstractState RelationSolver::abstract_consequence | ( | const AbstractState & | lower, |
const AbstractState & | upper, | ||
const AbstractState & | domain | ||
) | const |
for variable in self.variables:
proposed = self.top.copy()
proposed.set_interval(variable, lower.interval_of(variable)) proposed._locToItvVal
if not proposed >= upper:
return proposed
return lower.copy()
Definition at line 170 of file RelationSolver.cpp.
AbstractState RelationSolver::beta | ( | const Map< u32_t, s32_t > & | sigma, |
const AbstractState & | exeState | ||
) | const |
Definition at line 245 of file RelationSolver.cpp.
AbstractState RelationSolver::bilateral | ( | const AbstractState & | domain, |
const Z3Expr & | phi, | ||
u32_t | descend_check = 0 |
||
) |
init variables
TODO: add option for timeout
start processing
compute domain.model_and(phi, domain.logic_not(domain.gamma_hat(consequence)))
find any solution, which is sat
unknown or unsat
for timeout reason return upper
Definition at line 36 of file RelationSolver.cpp.
Map< u32_t, s32_t > RelationSolver::BoxedOptSolver | ( | const Z3Expr & | phi, |
Map< u32_t, s32_t > & | ret, | ||
Map< u32_t, s32_t > & | low_values, | ||
Map< u32_t, s32_t > & | high_values | ||
) |
this is the S in the original paper
Definition at line 345 of file RelationSolver.cpp.
AbstractState RelationSolver::BS | ( | const AbstractState & | domain, |
const Z3Expr & | phi | ||
) |
because key of _varToItvVal is u32_t, -key may out of range for int so we do key + bias for -key
init low, ret, high
init objects -x
add a relation that x == -(x+bias)
optimize each object
fill in the return values
Definition at line 270 of file RelationSolver.cpp.
void RelationSolver::decide_cpa_ext | ( | const Z3Expr & | phi, |
Map< u32_t, Z3Expr > & | L_phi, | ||
Map< u32_t, s32_t > & | mid_values, | ||
Map< u32_t, s32_t > & | ret, | ||
Map< u32_t, s32_t > & | low_values, | ||
Map< u32_t, s32_t > & | high_values | ||
) |
find any solution, which is sat
id is the var id, value is the solution found for var_id add a relation to check if the solution meets phi_id
unknown or unsat, we consider unknown as unsat
Definition at line 373 of file RelationSolver.cpp.
Z3Expr RelationSolver::gamma_hat | ( | const AbstractState & | alpha, |
const AbstractState & | exeState | ||
) | const |
Return Z3Expr according to another valToValMap.
Definition at line 216 of file RelationSolver.cpp.
Z3Expr RelationSolver::gamma_hat | ( | const AbstractState & | exeState | ) | const |
Z3Expr RelationSolver::gamma_hat | ( | u32_t | id, |
const AbstractState & | exeState | ||
) | const |
AbstractState RelationSolver::RSY | ( | const AbstractState & | domain, |
const Z3Expr & | phi | ||
) |
TODO: add option for timeout
find any solution, which is sat
unknown or unsat
for timeout reason return upper
Definition at line 114 of file RelationSolver.cpp.
Definition at line 66 of file RelationSolver.h.
Return Z3 expression lazily based on SVFVar ID.
Definition at line 61 of file RelationSolver.h.
|
inline |
Definition at line 70 of file RelationSolver.h.
Definition at line 257 of file RelationSolver.cpp.