SVF::RelExeState Class Reference

#include <RelExeState.h>

Public Types
typedef Map< u32_t, Z3Expr >	VarToValMap
typedef VarToValMap	AddrToValMap

Public Member Functions
	RelExeState ()=default
	RelExeState (VarToValMap &varToVal, AddrToValMap &locToVal)
	RelExeState (const RelExeState &rhs)
virtual	~RelExeState ()=default
RelExeState &	operator= (const RelExeState &rhs)
	RelExeState (RelExeState &&rhs) noexcept
RelExeState &	operator= (RelExeState &&rhs) noexcept
bool	operator== (const RelExeState &rhs) const
	Overloading Operator==.
bool	operator!= (const RelExeState &rhs) const
	Overloading Operator!=.
bool	operator< (const RelExeState &rhs) const
	Overloading Operator==.
const VarToValMap &	getVarToVal () const
const AddrToValMap &	getLocToVal () const
Z3Expr &	operator[] (u32_t varId)
u32_t	hash () const
bool	existsVar (u32_t varId) const
	Return true if map has varId.
virtual Z3Expr &	getZ3Expr (u32_t varId)
	Return Z3 expression eagerly based on SVFVar ID.
virtual Z3Expr	toZ3Expr (u32_t varId) const
	Return Z3 expression lazily based on SVFVar ID.
void	extractSubVars (const Z3Expr &expr, Set< u32_t > &res)
	Extract sub SVFVar IDs of a Z3Expr.
void	extractCmpVars (const Z3Expr &expr, Set< u32_t > &res)
	Extract all related SVFVar IDs based on compare expr.
Z3Expr	buildRelZ3Expr (u32_t cmp, s32_t succ, Set< u32_t > &vars, Set< u32_t > &initVars)
	Build relational Z3Expr.
void	store (const Z3Expr &loc, const Z3Expr &value)
	Store value to location.
Z3Expr &	load (const Z3Expr &loc)
	Load value at location.
void	printExprValues ()
	Print values of all expressions.

Static Public Member Functions
static z3::context &	getContext ()
static u32_t	getVirtualMemAddress (u32_t idx)
	The physical address starts with 0x7f...... + idx.
static bool	isVirtualMemAddress (u32_t val)
	Check bit value of val start with 0x7F000000, filter by 0xFF000000.
static u32_t	getInternalID (u32_t idx)
	Return the internal index if idx is an address otherwise return the value of idx.
static s32_t	z3Expr2NumValue (const Z3Expr &e)
	Return int value from an expression if it is a numeral, otherwise return an approximate value.

Protected Member Functions
void	store (u32_t objId, const Z3Expr &z3Expr)
Z3Expr &	load (u32_t objId)

Protected Attributes
VarToValMap	_varToVal
AddrToValMap	_addrToVal

Private Member Functions
bool	eqVarToValMap (const VarToValMap &lhs, const VarToValMap &rhs) const
bool	lessThanVarToValMap (const VarToValMap &lhs, const VarToValMap &rhs) const

Friends
class	SVFIR2AbsState

Detailed Description

Definition at line 39 of file RelExeState.h.

Member Typedef Documentation

AddrToValMap

typedef VarToValMap SVF::RelExeState::AddrToValMap

Definition at line 45 of file RelExeState.h.

VarToValMap

typedef Map<u32_t, Z3Expr> SVF::RelExeState::VarToValMap

Definition at line 44 of file RelExeState.h.

Constructor & Destructor Documentation

RelExeState() [1/4]

SVF::RelExeState::RelExeState ( )

default

RelExeState() [2/4]

SVF::RelExeState::RelExeState ( VarToValMap &  varToVal, AddrToValMap &  locToVal  )

inline

Definition at line 54 of file RelExeState.h.

: _varToVal(varToVal), _addrToVal(locToVal) {}

RelExeState() [3/4]

SVF::RelExeState::RelExeState ( const RelExeState &  rhs )

inline

Definition at line 56 of file RelExeState.h.

                                        : _varToVal(rhs.getVarToVal()), _addrToVal(rhs.getLocToVal())
    {
 
    }

~RelExeState()

virtual SVF::RelExeState::~RelExeState ( )

virtualdefault

RelExeState() [4/4]

SVF::RelExeState::RelExeState ( RelExeState &&  rhs )

inlinenoexcept

Definition at line 65 of file RelExeState.h.

                                           : _varToVal(std::move(rhs._varToVal)),
        _addrToVal(std::move(rhs._addrToVal))
    {
 
    }

Member Function Documentation

buildRelZ3Expr()

Z3Expr RelExeState::buildRelZ3Expr	(	u32_t	cmp,
		s32_t	succ,
		Set< u32_t > &	vars,
		Set< u32_t > &	initVars
	)

Build relational Z3Expr.

Build relational Z3Expr

Parameters

cmp
succ
vars	return all the relational vars of a given variable
initVars	the vars on the right hand side of cmp statement, e.g., {a} for "cmp = a > 1"

Returns

Definition at line 90 of file RelExeState.cpp.

{
    Z3Expr res = (getZ3Expr(cmp) == succ).simplify();
    extractSubVars(res, initVars);
    extractCmpVars(res, vars);
    for (const auto &id: vars)
    {
        res = (res && toZ3Expr(id) == getZ3Expr(id)).simplify();
    }
    res = (res && (toZ3Expr(cmp) == getZ3Expr(cmp))).simplify();
    vars.insert(cmp);
    return res;
}

eqVarToValMap()

bool RelExeState::eqVarToValMap ( const VarToValMap &  lhs, const VarToValMap &  rhs  ) const

private

Definition at line 136 of file RelExeState.cpp.

{
    if (lhs.size() != rhs.size()) return false;
    for (const auto &item: lhs)
    {
        auto it = rhs.find(item.first);
        // return false if SVFVar not exists in rhs or z3Expr not equal
        if (it == rhs.end() || !eq(item.second, it->second))
            return false;
    }
    return true;
}

existsVar()

bool SVF::RelExeState::existsVar ( u32_t  varId ) const

inline

Return true if map has varId.

Definition at line 137 of file RelExeState.h.

    {
        return _varToVal.count(varId);
    }

extractCmpVars()

void RelExeState::extractCmpVars	(	const Z3Expr &	expr,
		Set< u32_t > &	res
	)

Extract all related SVFVar IDs based on compare expr.

Extract all related SVFVar IDs based on compare expr

Parameters

expr
res

Definition at line 66 of file RelExeState.cpp.

{
    Set<u32_t> r;
    extractSubVars(expr, r);
    res.insert(r.begin(), r.end());
    assert(!r.empty() && "symbol not init?");
    if (r.size() == 1 && eq(expr, toZ3Expr(*r.begin())))
    {
        return;
    }
    for (const auto &id: r)
    {
        extractCmpVars((*this)[id], res);
    }
}

extractSubVars()

void RelExeState::extractSubVars	(	const Z3Expr &	expr,
		Set< u32_t > &	res
	)

Extract sub SVFVar IDs of a Z3Expr.

Extract sub SVFVar IDs of a Z3Expr

e.g., Given an expr "a+b", return {a.id, b.id}

Parameters

expr
res

Definition at line 45 of file RelExeState.cpp.

{
    if (expr.getExpr().num_args() == 0)
        if (!expr.getExpr().is_true() && !expr.getExpr().is_false() && !expr.is_numeral())
        {
            const std::string &exprStr = expr.to_string();
            res.insert(std::stoi(exprStr.substr(1, exprStr.size() - 1)));
        }
    for (u32_t i = 0; i < expr.getExpr().num_args(); ++i)
    {
        const z3::expr &e = expr.getExpr().arg(i);
        extractSubVars(e, res);
    }
}

getContext()

static z3::context & SVF::RelExeState::getContext ( )

inlinestatic

Definition at line 94 of file RelExeState.h.

    {
        return Z3Expr::getContext();
    }

getInternalID()

static u32_t SVF::RelExeState::getInternalID ( u32_t  idx )

inlinestatic

Return the internal index if idx is an address otherwise return the value of idx.

Definition at line 184 of file RelExeState.h.

    {
        return AddressValue::getInternalID(idx);
    }

getLocToVal()

const AddrToValMap & SVF::RelExeState::getLocToVal ( ) const

inline

Definition at line 104 of file RelExeState.h.

    {
        return _addrToVal;
    }

getVarToVal()

const VarToValMap & SVF::RelExeState::getVarToVal ( ) const

inline

Definition at line 99 of file RelExeState.h.

    {
        return _varToVal;
    }

getVirtualMemAddress()

static u32_t SVF::RelExeState::getVirtualMemAddress ( u32_t  idx )

inlinestatic

The physical address starts with 0x7f...... + idx.

Definition at line 170 of file RelExeState.h.

    {
        return AddressValue::getVirtualMemAddress(idx);
    }

getZ3Expr()

virtual Z3Expr & SVF::RelExeState::getZ3Expr ( u32_t  varId )

inlinevirtual

Return Z3 expression eagerly based on SVFVar ID.

Definition at line 143 of file RelExeState.h.

    {
        return _varToVal[varId];
    }

hash()

u32_t SVF::RelExeState::hash ( ) const

inline

Definition at line 114 of file RelExeState.h.

    {
        size_t h = getVarToVal().size() * 2;
        SVF::Hash<SVF::u32_t> hf;
        for (const auto &t: getVarToVal())
        {
            h ^= hf(t.first) + 0x9e3779b9 + (h << 6) + (h >> 2);
            h ^= hf(t.second.id()) + 0x9e3779b9 + (h << 6) + (h >> 2);
        }
 
        size_t h2 = getVarToVal().size() * 2;
 
        for (const auto &t: getLocToVal())
        {
            h2 ^= hf(t.first) + 0x9e3779b9 + (h2 << 6) + (h2 >> 2);
            h2 ^= hf(t.second.id()) + 0x9e3779b9 + (h2 << 6) + (h2 >> 2);
        }
        SVF::Hash<std::pair<SVF::u32_t, SVF::u32_t>> pairH;
 
        return pairH(std::make_pair(h, h2));
    }

isVirtualMemAddress()

static bool SVF::RelExeState::isVirtualMemAddress ( u32_t  val )

inlinestatic

Check bit value of val start with 0x7F000000, filter by 0xFF000000.

Definition at line 176 of file RelExeState.h.

    {
        if (val == 0)
            assert(false && "val cannot be 0");
        return AddressValue::isVirtualMemAddress(val);
    }

lessThanVarToValMap()

bool RelExeState::lessThanVarToValMap ( const VarToValMap &  lhs, const VarToValMap &  rhs  ) const

private

Definition at line 149 of file RelExeState.cpp.

{
    if (lhs.size() != rhs.size()) return lhs.size() < rhs.size();
    for (const auto &item: lhs)
    {
        auto it = rhs.find(item.first);
        // lhs > rhs if SVFVar not exists in rhs
        if (it == rhs.end())
            return false;
        // judge from expr id
        if (!eq(item.second, it->second))
            return item.second.id() < it->second.id();
    }
    return false;
}

load() [1/2]

Z3Expr & RelExeState::load

(

const Z3Expr &

loc

)

Load value at location.

Load value at location

Parameters

loc	location, e.g., int_val(0x7f..01)

Returns

Definition at line 183 of file RelExeState.cpp.

{
    assert(loc.is_numeral() && "location must be numeral");
    s32_t virAddr = z3Expr2NumValue(loc);
    assert(isVirtualMemAddress(virAddr) && "Pointer operand is not a physical address?");
    u32_t objId = getInternalID(virAddr);
    assert(getInternalID(objId) == objId && "SVFVar idx overflow > 0x7f000000?");
    return load(objId);
}

load() [2/2]

Z3Expr & SVF::RelExeState::load ( u32_t  objId )

inlineprotected

Definition at line 210 of file RelExeState.h.

    {
        return _addrToVal[objId];
    }

operator!=()

bool SVF::RelExeState::operator!= ( const RelExeState &  rhs ) const

inline

Overloading Operator!=.

Definition at line 85 of file RelExeState.h.

    {
        return !(*this == rhs);
    }

operator<()

bool RelExeState::operator<

(

const RelExeState &

rhs

)

const

Overloading Operator==.

Overloading Operator<

Parameters

rhs

Returns

Definition at line 130 of file RelExeState.cpp.

{
    return lessThanVarToValMap(_varToVal, rhs.getVarToVal()) ||
           lessThanVarToValMap(_addrToVal, rhs.getLocToVal());
}

operator=() [1/2]

RelExeState & RelExeState::operator=

(

const RelExeState &

rhs

)

Definition at line 104 of file RelExeState.cpp.

{
    if (*this != rhs)
    {
        _varToVal = rhs.getVarToVal();
        _addrToVal = rhs.getLocToVal();
    }
    return *this;
}

operator=() [2/2]

RelExeState & SVF::RelExeState::operator= ( RelExeState &&  rhs )

inlinenoexcept

Definition at line 71 of file RelExeState.h.

    {
        if (&rhs != this)
        {
            _varToVal = std::move(rhs._varToVal);
            _addrToVal = std::move(rhs._addrToVal);
        }
        return *this;
    }

operator==()

bool RelExeState::operator==

(

const RelExeState &

rhs

)

const

Overloading Operator==.

Overloading Operator==

Parameters

rhs

Returns

Definition at line 119 of file RelExeState.cpp.

{
    return eqVarToValMap(_varToVal, rhs.getVarToVal()) &&
           eqVarToValMap(_addrToVal, rhs.getLocToVal());
}

operator[]()

Z3Expr & SVF::RelExeState::operator[] ( u32_t  varId )

inline

Definition at line 109 of file RelExeState.h.

    {
        return getZ3Expr(varId);
    }

printExprValues()

void RelExeState::printExprValues

(

)

Print values of all expressions.

Print values of all expressions

Definition at line 196 of file RelExeState.cpp.

{
    std::cout.flags(std::ios::left);
    std::cout << "-----------Var and Value-----------\n";
    for (const auto &item: getVarToVal())
    {
        std::stringstream exprName;
        exprName << "Var" << item.first;
        std::cout << std::setw(25) << exprName.str();
        const Z3Expr &sim = item.second.simplify();
        if (sim.is_numeral() && isVirtualMemAddress(z3Expr2NumValue(sim)))
        {
            std::cout << "\t Value: " << std::hex << "0x" << z3Expr2NumValue(sim) << "\n";
        }
        else
        {
            std::cout << "\t Value: " << std::dec << sim << "\n";
        }
    }
    std::cout << "-----------------------------------------\n";
}

store() [1/2]

void RelExeState::store	(	const Z3Expr &	loc,
		const Z3Expr &	value
	)

Store value to location.

Store value to location

Parameters

loc	location, e.g., int_val(0x7f..01)
value

Definition at line 170 of file RelExeState.cpp.

{
    assert(loc.is_numeral() && "location must be numeral");
    s32_t virAddr = z3Expr2NumValue(loc);
    assert(isVirtualMemAddress(virAddr) && "Pointer operand is not a physical address?");
    store(getInternalID(virAddr), value);
}

store() [2/2]

void SVF::RelExeState::store ( u32_t  objId, const Z3Expr &  z3Expr  )

inlineprotected

Definition at line 205 of file RelExeState.h.

    {
        _addrToVal[objId] = z3Expr.simplify();
    }

toZ3Expr()

virtual Z3Expr SVF::RelExeState::toZ3Expr ( u32_t  varId ) const

inlinevirtual

Return Z3 expression lazily based on SVFVar ID.

Definition at line 149 of file RelExeState.h.

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

z3Expr2NumValue()

static s32_t SVF::RelExeState::z3Expr2NumValue ( const Z3Expr &  e )

inlinestatic

Return int value from an expression if it is a numeral, otherwise return an approximate value.

Definition at line 190 of file RelExeState.h.

    {
        assert(e.is_numeral() && "not numeral?");
        return e.get_numeral_int64();
    }

Friends And Related Symbol Documentation

SVFIR2AbsState

friend class SVFIR2AbsState

friend

Definition at line 41 of file RelExeState.h.

Member Data Documentation

_addrToVal

AddrToValMap SVF::RelExeState::_addrToVal

protected

Definition at line 49 of file RelExeState.h.

_varToVal

VarToValMap SVF::RelExeState::_varToVal

protected

Definition at line 48 of file RelExeState.h.

---

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

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