Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

replace int64 with s64 in IntervalValue/Z3Expr #1195

Merged
merged 13 commits into from
Sep 11, 2023
+54 −83
Merged

replace int64 with s64 in IntervalValue/Z3Expr #1195

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
32572a6
add reshapeValue() to getOffsetfromGepPair
Sep 8, 2023
8fe5417
Merge branch 'master' into 0821
bjjwwang Sep 9, 2023
216c4cb
refactor getGepByteOffset and accumulateConstantByteOffset
Sep 9, 2023
83f6327
add reshapeValue() to getOffsetfromGepPair
Sep 9, 2023
b5d9790
fix SVF CI compile err
Sep 9, 2023
eabc637
replace int64 with s64 to IntervalValue
Sep 11, 2023
66a8291
replace more int64 with s64
Sep 11, 2023
406323f
replace more int64 with s64
Sep 11, 2023
61022c8
replace more int64 with s64
Sep 11, 2023
02db8b7
replace more int64 with s64
Sep 11, 2023
b929b39
replace more int64 with s64
Sep 11, 2023
3b36520
replace more int64 with s64
Sep 11, 2023
b579fa4
Merge branch 'master' into 0821
bjjwwang Sep 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions svf/include/AbstractExecution/BoundedZ3Expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,11 +51,10 @@ class BoundedZ3Expr : public Z3Expr

BoundedZ3Expr(s32_t i) : Z3Expr(i) {}

BoundedZ3Expr(int64_t i) : Z3Expr(getContext().int_val(i)) {}
BoundedZ3Expr(s64_t i) : Z3Expr(getContext().int_val((int64_t)i)) {}

BoundedZ3Expr(const BoundedZ3Expr &z3Expr) : Z3Expr(z3Expr) {}


inline BoundedZ3Expr &operator=(const BoundedZ3Expr &rhs)
{
Z3Expr::operator=(rhs);
Expand Down Expand Up @@ -347,13 +346,13 @@ class BoundedZ3Expr : public Z3Expr
}

/// Return Numeral
inline int64_t getNumeral() const
inline s64_t getNumeral() const
{
if (is_numeral())
{
int64_t i;
if (getExpr().is_numeral_i64(i))
return get_numeral_int64();
return (s64_t)get_numeral_int64();
else
{
return (getExpr() < 0).simplify().is_true() ? INT64_MIN : INT64_MAX;
Expand All @@ -374,7 +373,7 @@ class BoundedZ3Expr : public Z3Expr
}
}

int64_t bvLen() const;
s64_t bvLen() const;
//%}
}; // end class ConZ3Expr
} // end namespace SVF
Expand Down
38 changes: 19 additions & 19 deletions svf/include/AbstractExecution/IntervalValue.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,29 +95,29 @@ class IntervalValue final : public AbstractValue
explicit IntervalValue() : AbstractValue(AbstractValue::IntervalK), _lb(minus_infinity()), _ub(plus_infinity()) {}

/// Create the IntervalValue [n, n]
explicit IntervalValue(int64_t n) : AbstractValue(AbstractValue::IntervalK), _lb(n), _ub(n) {}
explicit IntervalValue(s64_t n) : AbstractValue(AbstractValue::IntervalK), _lb(n), _ub(n) {}

explicit IntervalValue(s32_t n) : IntervalValue((int64_t) n) {}
explicit IntervalValue(s32_t n) : IntervalValue((s64_t) n) {}

explicit IntervalValue(u32_t n) : IntervalValue((int64_t) n) {}
explicit IntervalValue(u32_t n) : IntervalValue((s64_t) n) {}

explicit IntervalValue(double n) : IntervalValue((int64_t) n) {}
explicit IntervalValue(double n) : IntervalValue((s64_t) n) {}

explicit IntervalValue(NumericLiteral n) : IntervalValue(n, n) {}

/// Create the IntervalValue [lb, ub]
explicit IntervalValue(NumericLiteral lb, NumericLiteral ub) : AbstractValue(AbstractValue::IntervalK),
_lb(std::move(lb)), _ub(std::move(ub)) {}

explicit IntervalValue(int64_t lb, int64_t ub) : IntervalValue(NumericLiteral(lb), NumericLiteral(ub)) {}
explicit IntervalValue(s64_t lb, s64_t ub) : IntervalValue(NumericLiteral(lb), NumericLiteral(ub)) {}

explicit IntervalValue(double lb, double ub) : IntervalValue(NumericLiteral((int64_t) lb), NumericLiteral((int64_t) ub)) {}
explicit IntervalValue(double lb, double ub) : IntervalValue(NumericLiteral((s64_t) lb), NumericLiteral((s64_t) ub)) {}

explicit IntervalValue(s32_t lb, s32_t ub) : IntervalValue((int64_t) lb, (int64_t) ub) {}
explicit IntervalValue(s32_t lb, s32_t ub) : IntervalValue((s64_t) lb, (s64_t) ub) {}

explicit IntervalValue(u32_t lb, u32_t ub) : IntervalValue((int64_t) lb, (int64_t) ub) {}
explicit IntervalValue(u32_t lb, u32_t ub) : IntervalValue((s64_t) lb, (s64_t) ub) {}

explicit IntervalValue(u64_t lb, u64_t ub) : IntervalValue((int64_t) lb, (int64_t) ub) {}
explicit IntervalValue(u64_t lb, u64_t ub) : IntervalValue((s64_t) lb, (s64_t) ub) {}

/// Copy constructor
IntervalValue(const IntervalValue &) = default;
Expand Down Expand Up @@ -260,7 +260,7 @@ class IntervalValue final : public AbstractValue
}

/// Return
int64_t getNumeral() const
s64_t getNumeral() const
{
assert(is_numeral() && "this IntervalValue is not numeral");
return _lb.getNumeral();
Expand Down Expand Up @@ -800,15 +800,15 @@ inline IntervalValue operator&(const IntervalValue &lhs, const IntervalValue &rh
}
else if (lhs.lb().getNumeral() >= 0 && rhs.lb().getNumeral() >= 0)
{
return IntervalValue((int64_t) 0, min(lhs.ub(), rhs.ub()));
return IntervalValue((s64_t) 0, min(lhs.ub(), rhs.ub()));
}
else if (lhs.lb().getNumeral() >= 0)
{
return IntervalValue((int64_t) 0, lhs.ub());
return IntervalValue((s64_t) 0, lhs.ub());
}
else if (rhs.lb().getNumeral() >= 0)
{
return IntervalValue((int64_t) 0, rhs.ub());
return IntervalValue((s64_t) 0, rhs.ub());
}
else
{
Expand All @@ -835,9 +835,9 @@ inline IntervalValue operator|(const IntervalValue &lhs, const IntervalValue &rh
else if (lhs.lb().getNumeral() >= 0 && !lhs.ub().is_infinity() &&
rhs.lb().getNumeral() >= 0 && !rhs.ub().is_infinity())
{
int64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
int64_t ub = next_power_of_2(s64_t(m+1));
return IntervalValue((int64_t) 0, (int64_t) ub);
s64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
s64_t ub = next_power_of_2(s64_t(m+1));
return IntervalValue((s64_t) 0, (s64_t) ub);
}
else
{
Expand All @@ -864,9 +864,9 @@ inline IntervalValue operator^(const IntervalValue &lhs, const IntervalValue &rh
else if (lhs.lb().getNumeral() >= 0 && !lhs.ub().is_infinity() &&
rhs.lb().getNumeral() >= 0 && !rhs.ub().is_infinity())
{
int64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
int64_t ub = next_power_of_2(s64_t(m+1));
return IntervalValue((int64_t) 0, (int64_t) ub);
s64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
s64_t ub = next_power_of_2(s64_t(m+1));
return IntervalValue((s64_t) 0, (s64_t) ub);
}
else
{
Expand Down
4 changes: 2 additions & 2 deletions svf/include/AbstractExecution/NumericLiteral.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ class NumericLiteral

NumericLiteral(s32_t i) : _n(i) {}

NumericLiteral(int64_t i) : _n(i) {}
NumericLiteral(s64_t i) : _n(i) {}

NumericLiteral(BoundedZ3Expr z3Expr) : _n(std::move(z3Expr)) {}

Expand Down Expand Up @@ -117,7 +117,7 @@ class NumericLiteral
}

/// Return Numeral
inline int64_t getNumeral() const
inline s64_t getNumeral() const
{
return _n.getNumeral();
}
Expand Down
10 changes: 5 additions & 5 deletions svf/lib/AbstractExecution/BoundedZ3Expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,11 @@

using namespace SVF;

int64_t BoundedZ3Expr::bvLen() const
s64_t BoundedZ3Expr::bvLen() const
{
if(is_infinite()) return Options::MaxBVLen();
if(is_infinite()) return (s64_t)Options::MaxBVLen();
// No overflow
if(getNumeral() != INT64_MIN && getNumeral() != INT64_MAX) return Options::MaxBVLen();
if(getNumeral() != INT64_MIN && getNumeral() != INT64_MAX) return (s64_t)Options::MaxBVLen();
// Create a symbolic variable
Z3Expr x = getContext().real_const("x");
Z3Expr y = getContext().real_const("y");
Expand All @@ -54,11 +54,11 @@ int64_t BoundedZ3Expr::bvLen() const
z3::model model = solver->get_model();
Z3Expr log2_x = model.eval(y.getExpr(), true);
Z3Expr::getSolver().pop();
return BoundedZ3Expr(log2_x + 1).simplify().getNumeral();
return (s64_t)BoundedZ3Expr(log2_x + 1).simplify().getNumeral();
}
else
{
Z3Expr::getSolver().pop();
return Options::MaxBVLen();
return (s64_t)Options::MaxBVLen();
}
}
76 changes: 24 additions & 52 deletions svf/lib/AbstractExecution/SVFIR2ItvExeState.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,8 +173,7 @@ SVFIR2ItvExeState::VAddrs SVFIR2ItvExeState::getGepObjAddress(u32_t pointer, APO
return ret;
}

std::pair<APOffset, APOffset> SVFIR2ItvExeState::getBytefromGepTypePair(const AccessPath::VarAndGepTypePair& gep_pair, const GepStmt *gep, APOffset elemBytesize)
{
std::pair<APOffset, APOffset> SVFIR2ItvExeState::getBytefromGepTypePair(const AccessPath::VarAndGepTypePair& gep_pair, const GepStmt *gep, APOffset elemBytesize) {
const SVFValue *value = gep_pair.first->getValue();
const SVFType *type = gep_pair.second;
const SVFConstantInt *op = SVFUtil::dyn_cast<SVFConstantInt>(value);
Expand All @@ -183,30 +182,22 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getBytefromGepTypePair(const Ac
/// set largest byte offset is 0xFFFFFF in case of int32 overflow
APOffset maxByteLimit = 99999;
APOffset minByteLimit = -99999;
auto valueReshape = [&](s64_t offset)
{
if (offset < (s64_t)minByteLimit)
{
auto valueReshape = [&](s64_t offset) {
if (offset < (s64_t)minByteLimit) {
return minByteLimit;
}
else if (offset > (s64_t)maxByteLimit)
{
} else if (offset > (s64_t)maxByteLimit) {
return maxByteLimit;
}
else
{
} else {
return offset;
}
};
/// offset is constant but stored in variable
if (op)
{
offsetLb = offsetUb = op->getSExtValue() > maxByteLimit
? maxByteLimit
: op->getSExtValue();
}
else
{
? maxByteLimit
: op->getSExtValue();
} else {
u32_t idx = _svfir->getValueNode(value);
IntervalValue &idxVal = _es[idx];
if (idxVal.isBottom() || idxVal.isTop())
Expand All @@ -215,9 +206,7 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getBytefromGepTypePair(const Ac
if (idxVal.is_numeral())
{
offsetLb = offsetUb = valueReshape(idxVal.lb().getNumeral());
}
else
{
} else {
offsetLb = valueReshape(idxVal.lb().getNumeral());
offsetUb = valueReshape(idxVal.ub().getNumeral());
}
Expand All @@ -240,37 +229,28 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getBytefromGepTypePair(const Ac
}


std::pair<APOffset, APOffset> SVFIR2ItvExeState::getIndexfromGepTypePair(const AccessPath::VarAndGepTypePair& gep_pair, const GepStmt *gep)
{
std::pair<APOffset, APOffset> SVFIR2ItvExeState::getIndexfromGepTypePair(const AccessPath::VarAndGepTypePair& gep_pair, const GepStmt *gep) {
const SVFValue *value = gep_pair.first->getValue();
const SVFType *type = gep_pair.second;
const SVFConstantInt *op = SVFUtil::dyn_cast<SVFConstantInt>(value);
APOffset offsetLb = 0;
APOffset offsetUb = 0;
APOffset maxFieldLimit = (APOffset)Options::MaxFieldLimit();
APOffset minFieldLimit = 0;
auto valueReshape = [&](s64_t offset)
{
if (offset < minFieldLimit)
{
auto valueReshape = [&](s64_t offset) {
if (offset < minFieldLimit) {
return minFieldLimit;
}
else if (offset > maxFieldLimit)
{
} else if (offset > maxFieldLimit) {
return maxFieldLimit;
}
else
{
} else {
return offset;
}
};
/// offset is constant but stored in variable
/// offset is constant but stored in variable
if (op)
{
offsetLb = offsetUb = valueReshape(op->getSExtValue());
}
else
{
} else {
u32_t idx = _svfir->getValueNode(value);
//if (!inVarToIValTable(idx)) return std::make_pair(-1, -1);
IntervalValue &idxVal = _es[idx];
Expand All @@ -280,9 +260,7 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getIndexfromGepTypePair(const A
if (idxVal.is_numeral())
{
offsetLb = offsetUb = valueReshape(idxVal.lb().getNumeral());
}
else
{
} else {
offsetLb = valueReshape(idxVal.lb().getNumeral());
offsetUb = valueReshape(idxVal.ub().getNumeral());
}
Expand All @@ -298,10 +276,10 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getIndexfromGepTypePair(const A
else
{
const std::vector<u32_t>& so = SymbolTableInfo::SymbolInfo()
->getTypeInfo(type)
->getFlattenedElemIdxVec();
->getTypeInfo(type)
->getFlattenedElemIdxVec();
if (so.empty() || offsetUb >= (APOffset)so.size() ||
offsetLb >= (APOffset)so.size())
offsetLb >= (APOffset)so.size())
{
offsetLb = 0;
offsetUb = maxFieldLimit;
Expand All @@ -321,8 +299,7 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getIndexfromGepTypePair(const A
}


std::pair<APOffset, APOffset> SVFIR2ItvExeState::getGepByteOffset(const GepStmt *gep, APOffset elemBytesize)
{
std::pair<APOffset, APOffset> SVFIR2ItvExeState::getGepByteOffset(const GepStmt *gep, APOffset elemBytesize) {
/// for instant constant index, e.g. gep arr, 1
if (gep->getOffsetVarAndGepTypePairVec().empty())
return std::make_pair(gep->getConstantFieldIdx(), gep->getConstantFieldIdx());
Expand All @@ -333,7 +310,7 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getGepByteOffset(const GepStmt
for (int i = gep->getOffsetVarAndGepTypePairVec().size() - 1; i >= 0; i--)
{
std::pair<APOffset, APOffset> offsetIdx = getBytefromGepTypePair(
gep->getOffsetVarAndGepTypePairVec()[i], gep, elemBytesize);
gep->getOffsetVarAndGepTypePairVec()[i], gep, elemBytesize);
APOffset offsetLb = offsetIdx.first;
APOffset offsetUb = offsetIdx.second;
if (totalOffsetLb + offsetLb > maxFieldLimit)
Expand All @@ -349,8 +326,7 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getGepByteOffset(const GepStmt
}


std::pair<APOffset, APOffset> SVFIR2ItvExeState::getGepOffset(const GepStmt *gep)
{
std::pair<APOffset , APOffset> SVFIR2ItvExeState::getGepOffset(const GepStmt *gep) {
/// for instant constant index, e.g. gep arr, 1
if (gep->getOffsetVarAndGepTypePairVec().empty())
return std::make_pair(gep->getConstantFieldIdx(), gep->getConstantFieldIdx());
Expand All @@ -361,7 +337,7 @@ std::pair<APOffset, APOffset> SVFIR2ItvExeState::getGepOffset(const GepStmt *gep
for (int i = gep->getOffsetVarAndGepTypePairVec().size() - 1; i >= 0; i--)
{
std::pair<APOffset, APOffset> offsetIdx = getIndexfromGepTypePair(
gep->getOffsetVarAndGepTypePairVec()[i], gep);
gep->getOffsetVarAndGepTypePairVec()[i], gep);
APOffset offsetLb = offsetIdx.first;
APOffset offsetUb = offsetIdx.second;
if ((long long) (totalOffsetLb + offsetLb) > maxFieldLimit)
Expand Down Expand Up @@ -632,10 +608,6 @@ void SVFIR2ItvExeState::translateCmp(const CmpStmt *cmp)
{
IntervalValue resVal;
VAddrs &lhs = getVAddrs(op0), &rhs = getVAddrs(op1);
// if (lhs.empty() || rhs.empty()) {
// outs() << "empty address cmp?\n";
// return;
// }
assert(!lhs.empty() && !rhs.empty() && "empty address?");
auto predicate = cmp->getPredicate();
switch (predicate)
Expand Down