SVF::RelationSolver Class Reference

#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 > &)

Detailed Description

Definition at line 38 of file RelationSolver.h.

Constructor & Destructor Documentation

RelationSolver()

SVF::RelationSolver::RelationSolver ( )

default

Member Function Documentation

abstract_consequence()

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.

{
    /*Returns the "abstract consequence" of lower and upper.
 
    The abstract consequence must be a superset of lower and *NOT* a
    superset of upper.
 
            Note that this is a fairly "simple" abstract consequence, in that it
    sets only one variable to a non-top interval. This improves performance
    of the SMT solver in many cases. In certain cases, other choices for
    the abstract consequence will lead to better algorithm performance.*/
 
    for (auto it = domain.getVarToVal().begin();
            it != domain.getVarToVal().end(); ++it)
    {
        AbstractState proposed = domain.top(); 
        proposed[it->first] = lower[it->first].getInterval();
        if (!(proposed >= upper)) 
        {
            return proposed; 
        }
    }
    return lower; 
}

beta()

AbstractState RelationSolver::beta	(	const Map< u32_t, s32_t > &	sigma,
		const AbstractState &	exeState
	)		const

Definition at line 245 of file RelationSolver.cpp.

{
    AbstractState res;
    for (const auto& item : exeState.getVarToVal())
    {
        res[item.first] = IntervalValue(
                              sigma.at(item.first), sigma.at(item.first));
    }
    return res;
}

bilateral()

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.

{
    AbstractState upper = domain.top();
    AbstractState lower = domain.bottom();
    u32_t meets_in_a_row = 0;
    z3::solver solver = Z3Expr::getSolver();
    z3::params p(Z3Expr::getContext());
    p.set(":timeout", static_cast<unsigned>(600)); // in milliseconds
    solver.set(p);
    AbstractState consequence;
 
    while (lower != upper)
    {
        if (meets_in_a_row == descend_check)
        {
            consequence = lower;
        }
        else
        {
            consequence = abstract_consequence(lower, upper, domain);
        }
        Z3Expr rhs = !(gamma_hat(consequence, domain));
        solver.push();
        solver.add(phi.getExpr() && rhs.getExpr());
        Map<u32_t, s32_t> solution;
        z3::check_result checkRes = solver.check();
        if (checkRes == z3::sat)
        {
            z3::model m = solver.get_model();
            for (u32_t i = 0; i < m.size(); i++)
            {
                z3::func_decl v = m[i];
                // assert(v.arity() == 0);
                if (v.arity() != 0)
                    continue;
                solution.emplace(std::stoi(v.name().str()),
                                 m.get_const_interp(v).get_numeral_int());
            }
            for (const auto& item : domain.getVarToVal())
            {
                if (solution.find(item.first) == solution.end())
                {
                    solution.emplace(item.first, 0);
                }
            }
            solver.pop();
            AbstractState newLower = domain.bottom();
            newLower.joinWith(lower);
            AbstractState rhs = beta(solution, domain);
            newLower.joinWith(rhs);
            lower = newLower;
            meets_in_a_row = 0;
        }
        else 
        {
            solver.pop();
            if (checkRes == z3::unknown)
            {
                if (solver.reason_unknown() == "timeout")
                    return upper;
            }
            AbstractState newUpper = domain.top();
            newUpper.meetWith(upper);
            newUpper.meetWith(consequence);
            upper = newUpper;
            meets_in_a_row += 1;
        }
    }
    return upper;
}

BoxedOptSolver()

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.

{
    Map<u32_t, Z3Expr> L_phi;
    Map<u32_t, s32_t> mid_values;
    while (1)
    {
        L_phi.clear();
        for (const auto& item : ret)
        {
            Z3Expr v = toIntZ3Expr(item.first);
            if (low_values.at(item.first) <= (high_values.at(item.first)))
            {
                s32_t mid = (low_values.at(item.first) + (high_values.at(item.first) - low_values.at(item.first)) / 2);
                updateMap(mid_values, item.first, mid);
                Z3Expr expr = (toIntVal(mid) <= v && v <= toIntVal(high_values.at(item.first)));
                L_phi[item.first] = expr;
            }
        }
        if (L_phi.empty())
            break;
        else
            decide_cpa_ext(phi, L_phi, mid_values, ret, low_values, high_values);
    }
    return ret;
}

BS()

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.

{
    u32_t bias = 0;
    s32_t infinity = INT32_MAX/2 - 1;
 
    // int infinity = (INT32_MAX) - 1;
    // int infinity = 20;
    Map<u32_t, s32_t> ret;
    Map<u32_t, s32_t> low_values, high_values;
    Z3Expr new_phi = phi;
    for (const auto& item: domain.getVarToVal())
    {
        IntervalValue interval = item.second.getInterval();
        updateMap(ret, item.first, interval.ub().getIntNumeral());
        if (interval.lb().is_minus_infinity())
            updateMap(low_values, item.first, -infinity);
        else
            updateMap(low_values, item.first, interval.lb().getIntNumeral());
        if (interval.ub().is_plus_infinity())
            updateMap(high_values, item.first, infinity);
        else
            updateMap(high_values, item.first, interval.ub().getIntNumeral());
        if (item.first > bias)
            bias = item.first + 1;
    }
    for (const auto& item: domain.getVarToVal())
    {
        IntervalValue interval = item.second.getInterval();
        u32_t reverse_key = item.first + bias;
        updateMap(ret, reverse_key, -interval.lb().getIntNumeral());
        if (interval.ub().is_plus_infinity())
            updateMap(low_values, reverse_key, -infinity);
        else
            updateMap(low_values, reverse_key, -interval.ub().getIntNumeral());
        if (interval.lb().is_minus_infinity())
            updateMap(high_values, reverse_key, infinity);
        else
            updateMap(high_values, reverse_key, -interval.lb().getIntNumeral());
        new_phi = (new_phi && (toIntZ3Expr(reverse_key) == -1 * toIntZ3Expr(item.first)));
    }
    BoxedOptSolver(new_phi.simplify(), ret, low_values, high_values);
    AbstractState retInv;
    for (const auto& item: ret)
    {
        if (item.first >= bias)
        {
            if (!retInv.inVarToValTable(item.first-bias))
                retInv[item.first-bias] = IntervalValue::top();
 
            if (item.second == (infinity))
                retInv[item.first - bias] = IntervalValue(BoundedInt::minus_infinity(),
                                            retInv[item.first - bias].getInterval().ub());
            else
                retInv[item.first - bias] = IntervalValue(float(-item.second), retInv[item.first - bias].getInterval().ub());
 
        }
        else
        {
            if (item.second == (infinity))
                retInv[item.first] = IntervalValue(retInv[item.first].getInterval().lb(),
                                                   BoundedInt::plus_infinity());
            else
                retInv[item.first] = IntervalValue(retInv[item.first].getInterval().lb(), float(item.second));
        }
    }
    return retInv;
}

decide_cpa_ext()

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.

{
    while (1)
    {
        Z3Expr join_expr(Z3Expr::getContext().bool_val(false));
        for (const auto& item : L_phi)
            join_expr = (join_expr || item.second);
        join_expr = (join_expr && phi).simplify();
        z3::solver& solver = Z3Expr::getSolver();
        solver.push();
        solver.add(join_expr.getExpr());
        Map<u32_t, double> solution;
        z3::check_result checkRes = solver.check();
        if (checkRes == z3::sat)
        {
            z3::model m = solver.get_model();
            solver.pop();
            for(const auto & item : L_phi)
            {
                u32_t id = item.first;
                int value = m.eval(toIntZ3Expr(id).getExpr()).get_numeral_int();
                // int value = m.eval(Z3Expr::getContext().int_const(std::to_string(id).c_str())).get_numeral_int();
                Z3Expr expr = (item.second && toIntZ3Expr(id) == value);
                solver.push();
                solver.add(expr.getExpr());
                // solution meets phi_id
                if (solver.check() == z3::sat)
                {
                    updateMap(ret, id, (value));
                    updateMap(low_values, id, ret.at(id) + 1);
 
                    s32_t mid = (low_values.at(id) + high_values.at(id) + 1) / 2;
                    updateMap(mid_values, id, mid);
                    Z3Expr v = toIntZ3Expr(id);
                    // Z3Expr v = Z3Expr::getContext().int_const(std::to_string(id).c_str());
                    Z3Expr expr = (toIntVal(mid_values.at(id)) <= v && v <= toIntVal(high_values.at(id)));
                    L_phi[id] = expr;
                }
                solver.pop();
            }
        }
        else 
        {
            solver.pop();
            for (const auto& item : L_phi)
                high_values.at(item.first) = mid_values.at(item.first) - 1;
            return;
        }
    }
 
}

gamma_hat() [1/3]

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 res(Z3Expr::getContext().bool_val(true));
    for (auto& item : exeState.getVarToVal())
    {
        IntervalValue interval = alpha[item.first].getInterval();
        if (interval.isBottom())
            return Z3Expr::getContext().bool_val(false);
        if (interval.isTop())
            continue;
        Z3Expr v = toIntZ3Expr(item.first);
        res = (res && v >= (int)interval.lb().getNumeral() &&
               v <= (int)interval.ub().getNumeral()).simplify();
    }
    return res;
}

gamma_hat() [2/3]

Z3Expr RelationSolver::gamma_hat

(

const AbstractState &

exeState

)

const

Return Z3Expr according to valToValMap.

Definition at line 199 of file RelationSolver.cpp.

{
    Z3Expr res(Z3Expr::getContext().bool_val(true));
    for (auto& item : exeState.getVarToVal())
    {
        IntervalValue interval = item.second.getInterval();
        if (interval.isBottom())
            return Z3Expr::getContext().bool_val(false);
        if (interval.isTop())
            continue;
        Z3Expr v = toIntZ3Expr(item.first);
        res = (res && v >= (int)interval.lb().getNumeral() &&
               v <= (int)interval.ub().getNumeral()).simplify();
    }
    return res;
}

gamma_hat() [3/3]

Z3Expr RelationSolver::gamma_hat	(	u32_t	id,
		const AbstractState &	exeState
	)		const

Return Z3Expr from a NodeID.

Definition at line 234 of file RelationSolver.cpp.

{
    auto it = exeState.getVarToVal().find(id);
    assert(it != exeState.getVarToVal().end() && "id not in varToVal?");
    Z3Expr v = toIntZ3Expr(id);
    // Z3Expr v = Z3Expr::getContext().int_const(std::to_string(id).c_str());
    Z3Expr res = (v >= (int)it->second.getInterval().lb().getNumeral() &&
                  v <= (int)it->second.getInterval().ub().getNumeral());
    return res;
}

RSY()

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.

{
    AbstractState lower = domain.bottom();
    z3::solver& solver = Z3Expr::getSolver();
    z3::params p(Z3Expr::getContext());
    p.set(":timeout", static_cast<unsigned>(600)); // in milliseconds
    solver.set(p);
    while (1)
    {
        Z3Expr rhs = !(gamma_hat(lower, domain));
        solver.push();
        solver.add(phi.getExpr() && rhs.getExpr());
        Map<u32_t, s32_t> solution;
        z3::check_result checkRes = solver.check();
        if (checkRes == z3::sat)
        {
            z3::model m = solver.get_model();
            for (u32_t i = 0; i < m.size(); i++)
            {
                z3::func_decl v = m[i];
                if (v.arity() != 0)
                    continue;
 
                solution.emplace(std::stoi(v.name().str()),
                                 m.get_const_interp(v).get_numeral_int());
            }
            for (const auto& item : domain.getVarToVal())
            {
                if (solution.find(item.first) == solution.end())
                {
                    solution.emplace(item.first, 0);
                }
            }
            solver.pop();
            AbstractState newLower = domain.bottom();
            newLower.joinWith(lower);
            newLower.joinWith(beta(solution, domain));
            lower = newLower;
        }
        else 
        {
            solver.pop();
            if (checkRes == z3::unknown)
            {
                if (solver.reason_unknown() == "timeout")
                    return domain.top();
            }
            break;
        }
    }
    return lower;
}

toIntVal()

Z3Expr SVF::RelationSolver::toIntVal ( s32_t  f ) const

inline

Definition at line 66 of file RelationSolver.h.

    {
        return Z3Expr::getContext().int_val(f);
    }

toIntZ3Expr()

virtual Z3Expr SVF::RelationSolver::toIntZ3Expr ( u32_t  varId ) const

inlinevirtual

Return Z3 expression lazily based on SVFVar ID.

Definition at line 61 of file RelationSolver.h.

    {
        return Z3Expr::getContext().int_const(std::to_string(varId).c_str());
    }

toRealVal()

Z3Expr SVF::RelationSolver::toRealVal ( BoundedDouble  f ) const

inline

Definition at line 70 of file RelationSolver.h.

    {
        return Z3Expr::getContext().real_val(std::to_string(f.getFVal()).c_str());
    }

updateMap()

void RelationSolver::updateMap	(	Map< u32_t, s32_t > &	map,
		u32_t	key,
		const s32_t &	value
	)

Definition at line 257 of file RelationSolver.cpp.

{
    auto it = map.find(key);
    if (it == map.end())
    {
        map.emplace(key, value);
    }
    else
    {
        it->second = value;
    }
}

---

The documentation for this class was generated from the following files:

• /home/runner/work/SVF/SVF/svf/include/AE/Core/RelationSolver.h
• /home/runner/work/SVF/SVF/svf/lib/AE/Core/RelationSolver.cpp