replace int64 with s64 in IntervalValue/Z3Expr (SVF-tools#1195)

* add reshapeValue() to getOffsetfromGepPair * refactor getGepByteOffset and accumulateConstantByteOffset * fix SVF CI compile err * replace int64 with s64 to IntervalValue * replace more int64 with s64 * replace more int64 with s64 * replace more int64 with s64 * replace more int64 with s64 * replace more int64 with s64 * replace more int64 with s64 --------- Co-authored-by: jiawei.wang <[email protected]>
JasonZhongZexin · Sep 13, 2023 · ae326b2 · ae326b2
1 parent 4167863
commit ae326b2
Show file tree

Hide file tree

Showing 5 changed files with 54 additions and 83 deletions.
diff --git a/svf/include/AbstractExecution/BoundedZ3Expr.h b/svf/include/AbstractExecution/BoundedZ3Expr.h
@@ -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);
@@ -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;
@@ -374,7 +373,7 @@ class BoundedZ3Expr : public Z3Expr
         }
     }
 
-    int64_t bvLen() const;
+    s64_t bvLen() const;
     //%}
 }; // end class ConZ3Expr
 } // end namespace SVF

diff --git a/svf/include/AbstractExecution/IntervalValue.h b/svf/include/AbstractExecution/IntervalValue.h
@@ -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;
@@ -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();
@@ -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
     {
@@ -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
     {
@@ -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
     {

diff --git a/svf/include/AbstractExecution/NumericLiteral.h b/svf/include/AbstractExecution/NumericLiteral.h
@@ -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)) {}
 
@@ -117,7 +117,7 @@ class NumericLiteral
     }
 
     /// Return Numeral
-    inline int64_t getNumeral() const
+    inline s64_t getNumeral() const
     {
         return _n.getNumeral();
     }

diff --git a/svf/lib/AbstractExecution/BoundedZ3Expr.cpp b/svf/lib/AbstractExecution/BoundedZ3Expr.cpp
@@ -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");
@@ -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();
     }
 }
diff --git a/svf/lib/AbstractExecution/SVFIR2ItvExeState.cpp b/svf/lib/AbstractExecution/SVFIR2ItvExeState.cpp
@@ -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);
@@ -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())
@@ -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());
         }
@@ -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];
@@ -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());
         }
@@ -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;
@@ -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());
@@ -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)
@@ -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());
@@ -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)
@@ -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)