Skip to content

Commit

Permalink
Merge pull request #1267 from jumormt/master
Browse files Browse the repository at this point in the history 
rename API names in AE
  • Loading branch information
@yuleisui
yuleisui authored Dec 2, 2023
2 parents b3cb909 + 885f8cd commit 7a3e537
Show file tree
Hide file tree
Showing 10 changed files with 411 additions and 396 deletions.
195 changes: 99 additions & 96 deletions svf/include/AbstractExecution/ConsExeState.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,6 @@ class ConsExeState final : public ExeState

static ConsExeState globalConsES;

protected:
VarToValMap _varToVal;
LocToValMap _locToVal;

public:
ConsExeState(): ExeState(ExeState::SingleValueK) {}

Expand Down Expand Up @@ -101,8 +97,7 @@ class ConsExeState final : public ExeState

using ExeState::operator==;
using ExeState::operator!=;
/// Exposed APIs
//{%

bool operator==(const ConsExeState &rhs) const;

bool operator!=(const ConsExeState &other) const
Expand All @@ -114,129 +109,157 @@ class ConsExeState final : public ExeState

u32_t hash() const override;

/// Merge rhs into this
bool joinWith(const ConsExeState &rhs);
protected:

/// Build global execution state
void buildGlobES(ConsExeState &globES, Set<u32_t> &vars);
VarToValMap _varToVal; ///< Map a variable (symbol) to its constant value
LocToValMap _locToVal; ///< Map a memory address to its stored constant value

/// Update symbolic states based on the summary/side-effect of callee
void applySummary(const ConsExeState &summary);
public:

/// Whether state is null state (uninitialized state)
inline bool isNullState() const
/// get memory addresses of variable
virtual Addrs &getAddrs(u32_t id) override
{
return _varToVal.size() == 1 && eq((*_varToVal.begin()).second, -1) && _locToVal.empty();
auto it = globalConsES._varToAddrs.find(id);
if (it != globalConsES._varToAddrs.end()) return it->second;
return _varToAddrs[id];
}

/// Print values of all expressions
void printExprValues() const;

/// Print values of all expressions
void printExprValues(std::ostream &oss) const override;

std::string toString() const override;

std::string pcToString() const;

std::string varToString(u32_t varId) const;

std::string locToString(u32_t objId) const;

bool applySelect(u32_t res, u32_t cond, u32_t top, u32_t fop);
/// get constant value of variable
inline SingleAbsValue &operator[](u32_t varId)
{
auto it = globalConsES._varToVal.find(varId);
if (it != globalConsES._varToVal.end())
return it->second;
else
return _varToVal[varId];
}

bool applyPhi(u32_t res, std::vector<u32_t> &ops);
/// whether the variable is in varToAddrs table
virtual inline bool inVarToAddrsTable(u32_t id) const override
{
return _varToAddrs.find(id) != _varToAddrs.end() ||
globalConsES._varToAddrs.find(id) != globalConsES._varToAddrs.end();
}

inline bool inVarToVal(u32_t varId) const
/// whether the variable is in varToVal table
inline bool inVarToValTable(u32_t varId) const
{
return _varToVal.count(varId) || globalConsES._varToVal.count(varId);
}

inline bool inLocalLocToVal(const SingleAbsValue &loc) const
/// whether the memory address stores memory addresses
virtual inline bool inLocToAddrsTable(u32_t id) const override
{
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 inLocalLocToVal(objId);
return globalConsES._locToAddrs.find(id) != globalConsES._locToAddrs.end() || inLocalLocToAddrsTable(id);
}

inline bool inLocalLocToVal(u32_t varId) const
/// whether the memory address stores constant value
inline bool inLocToValTable(u32_t varId) const
{
return _locToVal.count(varId);
return inLocalLocToValTable(varId) || globalConsES._locToVal.count(varId);
}

inline bool inLocToVal(u32_t varId) const
inline const VarToValMap &getVarToVal() const
{
return inLocalLocToVal(varId) || globalConsES._locToVal.count(varId);
return _varToVal;
}

inline bool equalVar(u32_t lhs, u32_t rhs)
inline const LocToValMap &getLocToVal() const
{
if (!inVarToVal(lhs) || !inVarToVal(rhs)) return false;
return eq((*this)[lhs], (*this)[rhs]);
return _locToVal;
}
//%}

virtual inline bool inVarToAddrsTable(u32_t id) const override
virtual inline bool inLocalLocToAddrsTable(u32_t id) const
{
return _varToVAddrs.find(id) != _varToVAddrs.end() ||
globalConsES._varToVAddrs.find(id) != globalConsES._varToVAddrs.end();
return _locToAddrs.find(id) != _locToAddrs.end();
}

virtual inline bool inLocToAddrsTable(u32_t id) const override
inline bool inLocalLocToValTable(u32_t varId) const
{
return globalConsES._locToVAddrs.find(id) != globalConsES._locToVAddrs.end() || inLocalLocToAddrsTable(id);
return _locToVal.count(varId);
}

virtual inline bool inLocalLocToAddrsTable(u32_t id) const
inline bool inLocalLocToValTable(const SingleAbsValue& addr) const
{
return _locToVAddrs.find(id) != _locToVAddrs.end();
return _locToVal.count(getInternalID(addr.getNumeral()));
}

virtual VAddrs &getVAddrs(u32_t id) override
public:

/// Merge rhs into this
bool joinWith(const ConsExeState &rhs);

/// Build global execution state
void buildGlobES(ConsExeState &globES, Set<u32_t> &vars);

/// Update symbolic states based on the summary/side-effect of callee
void applySummary(const ConsExeState &summary);

inline bool equalVar(u32_t lhs, u32_t rhs)
{
auto it = globalConsES._varToVAddrs.find(id);
if (it != globalConsES._varToVAddrs.end()) return it->second;
return _varToVAddrs[id];
if (!inVarToValTable(lhs) || !inVarToValTable(rhs)) return false;
return eq((*this)[lhs], (*this)[rhs]);
}

virtual VAddrs &loadVAddrs(u32_t addr) override
/// Whether state is null state (uninitialized state)
inline bool isNullState() const
{
return _varToVal.size() == 1 && eq((*_varToVal.begin()).second, -1) && _locToVal.empty();
}

/// Print values of all expressions
void printExprValues() const;

/// Print values of all expressions
void printExprValues(std::ostream &oss) const override;

std::string toString() const override;

std::string pcToString() const;

std::string varToString(u32_t varId) const;

std::string locToString(u32_t objId) const;

bool applySelect(u32_t res, u32_t cond, u32_t top, u32_t fop);

bool applyPhi(u32_t res, std::vector<u32_t> &ops);

virtual Addrs &loadAddrs(u32_t addr) override
{
assert(isVirtualMemAddress(addr) && "not virtual address?");
u32_t objId = getInternalID(addr);
auto it = _locToVAddrs.find(objId);
if (it != _locToVAddrs.end())
auto it = _locToAddrs.find(objId);
if (it != _locToAddrs.end())
{
return it->second;
}
else
{
auto globIt = globalConsES._locToVAddrs.find(objId);
if (globIt != globalConsES._locToVAddrs.end())
auto globIt = globalConsES._locToAddrs.find(objId);
if (globIt != globalConsES._locToAddrs.end())
{
return globIt->second;
}
else
{
return getVAddrs(0);
return getAddrs(0);
}
}
}

virtual std::string varToAddrs(u32_t varId) const override
{
std::stringstream exprName;
auto it = _varToVAddrs.find(varId);
if (it == _varToVAddrs.end())
auto it = _varToAddrs.find(varId);
if (it == _varToAddrs.end())
{
auto git = globalConsES._varToVAddrs.find(varId);
if (git == globalConsES._varToVAddrs.end())
auto git = globalConsES._varToAddrs.find(varId);
if (git == globalConsES._varToAddrs.end())
exprName << "Var not in varToAddrs!\n";
else
{
const VAddrs &vaddrs = git->second;
const Addrs &vaddrs = git->second;
if (vaddrs.size() == 1)
{
exprName << "addr: {" << std::dec << getInternalID(*vaddrs.begin()) << "}\n";
Expand All @@ -254,7 +277,7 @@ class ConsExeState final : public ExeState
}
else
{
const VAddrs &vaddrs = it->second;
const Addrs &vaddrs = it->second;
if (vaddrs.size() == 1)
{
exprName << "addr: {" << std::dec << getInternalID(*vaddrs.begin()) << "}\n";
Expand All @@ -275,15 +298,15 @@ class ConsExeState final : public ExeState
virtual std::string locToAddrs(u32_t objId) const override
{
std::stringstream exprName;
auto it = _locToVAddrs.find(objId);
if (it == _locToVAddrs.end())
auto it = _locToAddrs.find(objId);
if (it == _locToAddrs.end())
{
auto git = globalConsES._locToVAddrs.find(objId);
if (git == globalConsES._locToVAddrs.end())
auto git = globalConsES._locToAddrs.find(objId);
if (git == globalConsES._locToAddrs.end())
exprName << "Obj not in locToVal!\n";
else
{
const VAddrs &vaddrs = git->second;
const Addrs &vaddrs = git->second;
if (vaddrs.size() == 1)
{
exprName << "addr: {" << std::dec << getInternalID(*vaddrs.begin()) << "}\n";
Expand All @@ -301,7 +324,7 @@ class ConsExeState final : public ExeState
}
else
{
const VAddrs &vaddrs = it->second;
const Addrs &vaddrs = it->second;
if (vaddrs.size() == 1)
{
exprName << "addr: {" << std::dec << getInternalID(*vaddrs.begin()) << "}\n";
Expand Down Expand Up @@ -338,22 +361,10 @@ class ConsExeState final : public ExeState

public:

inline const VarToValMap &getVarToVal() const
{
return _varToVal;
}

inline const LocToValMap &getLocToVal() const
{
return _locToVal;
}


s64_t getNumber(u32_t lhs);

public:


static inline SingleAbsValue getIntOneZ3Expr()
{
return getContext().int_val(1);
Expand All @@ -375,14 +386,6 @@ class ConsExeState final : public ExeState
}

public:
inline SingleAbsValue &operator[](u32_t varId)
{
auto it = globalConsES._varToVal.find(varId);
if (it != globalConsES._varToVal.end())
return it->second;
else
return _varToVal[varId];
}

/// Store value to location
bool store(const SingleAbsValue &loc, const SingleAbsValue &value);
Expand Down
Loading

0 comments on commit 7a3e537

Please sign in to comment.