From 86a3d313e816d31c3d24f1e13e991803aa5c1c0a Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Wed, 27 Mar 2019 16:54:12 +0000 Subject: [PATCH] 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 --- include/llvm/Support/SMTAPI.h | 42 +++++++++++++++++++++ lib/Support/Z3Solver.cpp | 70 +++++++++++++++++++++++++++++++++++ 2 files changed, 112 insertions(+) diff --git a/include/llvm/Support/SMTAPI.h b/include/llvm/Support/SMTAPI.h index 8891faa998e..24dcd124593 100644 --- 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 5e40831db9e..f1a6fdf87cf 100644 --- 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, -- 2.40.0