36 using namespace SVFUtil;
47 if (expr.
getExpr().num_args() == 0)
51 res.insert(std::stoi(exprStr.substr(1, exprStr.size() - 1)));
55 const z3::expr &e = expr.
getExpr().arg(i);
56 extractSubVars(e, res);
69 extractSubVars(expr, r);
70 res.insert(r.begin(), r.end());
71 assert(!r.empty() &&
"symbol not init?");
72 if (r.size() == 1 && eq(expr, toZ3Expr(*r.begin())))
76 for (
const auto &
id: r)
78 extractCmpVars((*
this)[
id], res);
92 Z3Expr res = (getZ3Expr(cmp) == succ).simplify();
93 extractSubVars(res, initVars);
94 extractCmpVars(res, vars);
95 for (
const auto &
id: vars)
97 res = (res && toZ3Expr(
id) == getZ3Expr(
id)).simplify();
99 res = (res && (toZ3Expr(cmp) == getZ3Expr(cmp))).
simplify();
121 return eqVarToValMap(_varToVal, rhs.
getVarToVal()) &&
132 return lessThanVarToValMap(_varToVal, rhs.
getVarToVal()) ||
133 lessThanVarToValMap(_addrToVal, rhs.
getLocToVal());
138 if (lhs.size() != rhs.size())
return false;
139 for (
const auto &
item: lhs)
141 auto it = rhs.find(
item.first);
143 if (it == rhs.end() || !eq(
item.second, it->second))
151 if (lhs.size() != rhs.size())
return lhs.size() < rhs.size();
152 for (
const auto &
item: lhs)
154 auto it = rhs.find(
item.first);
159 if (!eq(
item.second, it->second))
160 return item.second.id() < it->second.id();
172 assert(loc.
is_numeral() &&
"location must be numeral");
173 s32_t virAddr = z3Expr2NumValue(loc);
174 assert(isVirtualMemAddress(virAddr) &&
"Pointer operand is not a physical address?");
175 store(getInternalID(virAddr), value);
185 assert(loc.
is_numeral() &&
"location must be numeral");
186 s32_t virAddr = z3Expr2NumValue(loc);
187 assert(isVirtualMemAddress(virAddr) &&
"Pointer operand is not a physical address?");
188 u32_t objId = getInternalID(virAddr);
189 assert(getInternalID(objId) == objId &&
"SVFVar idx overflow > 0x7f000000?");
198 std::cout.flags(std::ios::left);
199 std::cout <<
"-----------Var and Value-----------\n";
200 for (
const auto &
item: getVarToVal())
202 std::stringstream exprName;
203 exprName <<
"Var" <<
item.first;
204 std::cout << std::setw(25) << exprName.str();
206 if (sim.
is_numeral() && isVirtualMemAddress(z3Expr2NumValue(sim)))
208 std::cout <<
"\t Value: " << std::hex <<
"0x" << z3Expr2NumValue(sim) <<
"\n";
212 std::cout <<
"\t Value: " << std::dec << sim <<
"\n";
215 std::cout <<
"-----------------------------------------\n";
bool lessThanVarToValMap(const VarToValMap &lhs, const VarToValMap &rhs) const
void extractSubVars(const Z3Expr &expr, Set< u32_t > &res)
Extract sub SVFVar IDs of a Z3Expr.
void printExprValues()
Print values of all expressions.
void store(const Z3Expr &loc, const Z3Expr &value)
Store value to location.
RelExeState & operator=(const RelExeState &rhs)
const AddrToValMap & getLocToVal() const
const VarToValMap & getVarToVal() const
Z3Expr & load(const Z3Expr &loc)
Load value at location.
bool eqVarToValMap(const VarToValMap &lhs, const VarToValMap &rhs) const
Z3Expr buildRelZ3Expr(u32_t cmp, s32_t succ, Set< u32_t > &vars, Set< u32_t > &initVars)
Build relational Z3Expr.
bool operator==(const RelExeState &rhs) const
Overloading Operator==.
bool operator<(const RelExeState &rhs) const
Overloading Operator==.
void extractCmpVars(const Z3Expr &expr, Set< u32_t > &res)
Extract all related SVFVar IDs based on compare expr.
Map< u32_t, Z3Expr > VarToValMap
const std::string to_string() const
const z3::expr & getExpr() const
std::unordered_set< Key, Hash, KeyEqual, Allocator > Set