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

git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@357088 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/include/llvm/Support/SMTAPI.h b/include/llvm/Support/SMTAPI.h
index 8891faa998ec622668792a904c91f5d384e9e632..24dcd124593ee54444a7b12ded166ff3e10025e6 100644 (file)
--- a/include/llvm/Support/SMTAPI.h
+++ b/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/lib/Support/Z3Solver.cpp b/lib/Support/Z3Solver.cpp
index 5e40831db9eee2bcee5740238129349821638dbc..f1a6fdf87cf2b7f6dbec12d22801bdcfd6e98c8f 100644 (file)
--- a/lib/Support/Z3Solver.cpp
+++ b/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,