From 753e7cc77743cf0689735094345a634e87f662e1 Mon Sep 17 00:00:00 2001 From: "jiawei.wang" Date: Tue, 25 Jul 2023 00:53:53 +0000 Subject: [PATCH 1/2] fix bitvec err for sse --- svf/include/AbstractExecution/BoundedZ3Expr.h | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/svf/include/AbstractExecution/BoundedZ3Expr.h b/svf/include/AbstractExecution/BoundedZ3Expr.h index d69d72543..8d9904eae 100644 --- a/svf/include/AbstractExecution/BoundedZ3Expr.h +++ b/svf/include/AbstractExecution/BoundedZ3Expr.h @@ -248,19 +248,19 @@ class BoundedZ3Expr : public Z3Expr friend BoundedZ3Expr operator^(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - const auto &maxBvLen = std::max(lhs.bvLen(), rhs.bvLen()); + s64_t maxBvLen = 64; return bv2int(int2bv(maxBvLen, lhs.getExpr()) ^ int2bv(maxBvLen, rhs.getExpr()), true); } friend BoundedZ3Expr operator&(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - const auto &maxBvLen = std::max(lhs.bvLen(), rhs.bvLen()); + s64_t maxBvLen = 64; return bv2int(int2bv(maxBvLen, lhs.getExpr()) & int2bv(maxBvLen, rhs.getExpr()), true); } friend BoundedZ3Expr operator|(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - const auto &maxBvLen = std::max(lhs.bvLen(), rhs.bvLen()); + s64_t maxBvLen = 64; return bv2int(int2bv(maxBvLen, lhs.getExpr()) | int2bv(maxBvLen, rhs.getExpr()), true); } @@ -274,7 +274,7 @@ class BoundedZ3Expr : public Z3Expr return ite(lhs.getExpr() >= 0, BoundedZ3Expr(0), BoundedZ3Expr(-1)); else { - const auto &maxBvLen = std::max(lhs.bvLen(), rhs.bvLen()); + s64_t maxBvLen = 64; return bv2int(ashr(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true); } } @@ -289,14 +289,14 @@ class BoundedZ3Expr : public Z3Expr return ite(lhs.getExpr() >= 0, plus_infinity(), minus_infinity()); else { - const auto &maxBvLen = std::max(lhs.bvLen(), rhs.bvLen()); + s64_t maxBvLen = 64; return bv2int(shl(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true); } } friend BoundedZ3Expr lshr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - const auto &maxBvLen = std::max(lhs.bvLen(), rhs.bvLen()); + s64_t maxBvLen = 64; return bv2int(lshr(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true); } @@ -394,3 +394,4 @@ struct std::hash } }; #endif //SVF_BOUNDEDZ3EXPR_H + From 3aec7a35d091e34d4230a344eadbf624c5e9b4a3 Mon Sep 17 00:00:00 2001 From: "jiawei.wang" Date: Tue, 25 Jul 2023 02:35:30 +0000 Subject: [PATCH 2/2] fix bitvec err for sse --- svf/include/AbstractExecution/BoundedZ3Expr.h | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/svf/include/AbstractExecution/BoundedZ3Expr.h b/svf/include/AbstractExecution/BoundedZ3Expr.h index 8d9904eae..f83e9c050 100644 --- a/svf/include/AbstractExecution/BoundedZ3Expr.h +++ b/svf/include/AbstractExecution/BoundedZ3Expr.h @@ -29,6 +29,7 @@ #ifndef SVF_BOUNDEDZ3EXPR_H #define SVF_BOUNDEDZ3EXPR_H +#define MaxBvLen 64 #include "Util/Z3Expr.h" @@ -248,20 +249,17 @@ class BoundedZ3Expr : public Z3Expr friend BoundedZ3Expr operator^(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - s64_t maxBvLen = 64; - return bv2int(int2bv(maxBvLen, lhs.getExpr()) ^ int2bv(maxBvLen, rhs.getExpr()), true); + return bv2int(int2bv(MaxBvLen, lhs.getExpr()) ^ int2bv(MaxBvLen, rhs.getExpr()), true); } friend BoundedZ3Expr operator&(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - s64_t maxBvLen = 64; - return bv2int(int2bv(maxBvLen, lhs.getExpr()) & int2bv(maxBvLen, rhs.getExpr()), true); + return bv2int(int2bv(MaxBvLen, lhs.getExpr()) & int2bv(MaxBvLen, rhs.getExpr()), true); } friend BoundedZ3Expr operator|(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - s64_t maxBvLen = 64; - return bv2int(int2bv(maxBvLen, lhs.getExpr()) | int2bv(maxBvLen, rhs.getExpr()), true); + return bv2int(int2bv(MaxBvLen, lhs.getExpr()) | int2bv(MaxBvLen, rhs.getExpr()), true); } friend BoundedZ3Expr ashr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) @@ -274,8 +272,7 @@ class BoundedZ3Expr : public Z3Expr return ite(lhs.getExpr() >= 0, BoundedZ3Expr(0), BoundedZ3Expr(-1)); else { - s64_t maxBvLen = 64; - return bv2int(ashr(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true); + return bv2int(ashr(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true); } } @@ -289,15 +286,13 @@ class BoundedZ3Expr : public Z3Expr return ite(lhs.getExpr() >= 0, plus_infinity(), minus_infinity()); else { - s64_t maxBvLen = 64; - return bv2int(shl(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true); + return bv2int(shl(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true); } } friend BoundedZ3Expr lshr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) { - s64_t maxBvLen = 64; - return bv2int(lshr(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true); + return bv2int(lshr(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true); } friend BoundedZ3Expr int2bv(u32_t n, const BoundedZ3Expr &e)