[llvm] r357088 - New methods to check for under-/overflow in the SMT API
Mikhail R. Gadelha via llvm-commits
llvm-commits at lists.llvm.org
Wed Mar 27 09:54:12 PDT 2019
Author: mramalho
Date: Wed Mar 27 09:54:12 2019
New Revision: 357088
URL: http://llvm.org/viewvc/llvm-project?rev=357088&view=rev
Log:
New methods to check for under-/overflow in the SMT API
Summary: Added methods to check for under-/overflow in additions, subtractions, signed divisions/modulus, negations, and multiplications.
Reviewers: ddcc, gou4shi1
Reviewed By: ddcc, gou4shi1
Subscribers: hiraditya, llvm-commits
Tags: #llvm
Differential Revision: https://reviews.llvm.org/D59796
Modified:
llvm/trunk/include/llvm/Support/SMTAPI.h
llvm/trunk/lib/Support/Z3Solver.cpp
Modified: llvm/trunk/include/llvm/Support/SMTAPI.h
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/include/llvm/Support/SMTAPI.h?rev=357088&r1=357087&r2=357088&view=diff
==============================================================================
--- llvm/trunk/include/llvm/Support/SMTAPI.h (original)
+++ llvm/trunk/include/llvm/Support/SMTAPI.h Wed Mar 27 09:54:12 2019
@@ -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;
Modified: llvm/trunk/lib/Support/Z3Solver.cpp
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Support/Z3Solver.cpp?rev=357088&r1=357087&r2=357088&view=diff
==============================================================================
--- llvm/trunk/lib/Support/Z3Solver.cpp (original)
+++ llvm/trunk/lib/Support/Z3Solver.cpp Wed Mar 27 09:54:12 2019
@@ -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,
More information about the llvm-commits
mailing list