diff options
| -rw-r--r-- | llvm/include/llvm/Support/SMTAPI.h | 42 | ||||
| -rw-r--r-- | llvm/lib/Support/Z3Solver.cpp | 70 |
2 files changed, 112 insertions, 0 deletions
diff --git a/llvm/include/llvm/Support/SMTAPI.h b/llvm/include/llvm/Support/SMTAPI.h index 8891faa998e..24dcd124593 100644 --- a/llvm/include/llvm/Support/SMTAPI.h +++ b/llvm/include/llvm/Support/SMTAPI.h @@ -279,6 +279,48 @@ public: virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + /// Creates a predicate that checks for overflow in a bitvector addition + /// operation + virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, + const SMTExprRef &RHS, + bool isSigned) = 0; + + /// Creates a predicate that checks for underflow in a signed bitvector + /// addition operation + virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) = 0; + + /// Creates a predicate that checks for overflow in a signed bitvector + /// subtraction operation + virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) = 0; + + /// Creates a predicate that checks for underflow in a bitvector subtraction + /// operation + virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, + const SMTExprRef &RHS, + bool isSigned) = 0; + + /// Creates a predicate that checks for overflow in a signed bitvector + /// division/modulus operation + virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) = 0; + + /// Creates a predicate that checks for overflow in a bitvector negation + /// operation + virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0; + + /// Creates a predicate that checks for overflow in a bitvector multiplication + /// operation + virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, + const SMTExprRef &RHS, + bool isSigned) = 0; + + /// Creates a predicate that checks for underflow in a signed bitvector + /// multiplication operation + virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) = 0; + /// Creates a floating-point negation operation virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp index 5e40831db9e..f1a6fdf87cf 100644 --- a/llvm/lib/Support/Z3Solver.cpp +++ b/llvm/lib/Support/Z3Solver.cpp @@ -603,6 +603,76 @@ public: toZ3Expr(*Exp).AST))); } + /// Creates a predicate that checks for overflow in a bitvector addition + /// operation + SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, + bool isSigned) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, isSigned))); + } + + /// Creates a predicate that checks for underflow in a signed bitvector + /// addition operation + SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + /// Creates a predicate that checks for overflow in a signed bitvector + /// subtraction operation + SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + /// Creates a predicate that checks for underflow in a bitvector subtraction + /// operation + SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, + bool isSigned) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, isSigned))); + } + + /// Creates a predicate that checks for overflow in a signed bitvector + /// division/modulus operation + SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + /// Creates a predicate that checks for overflow in a bitvector negation + /// operation + SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST))); + } + + /// Creates a predicate that checks for overflow in a bitvector multiplication + /// operation + SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, + bool isSigned) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, isSigned))); + } + + /// Creates a predicate that checks for underflow in a signed bitvector + /// multiplication operation + SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, + const SMTExprRef &RHS) override { + return newExprRef(Z3Expr( + Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override { return newExprRef( Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, |
