Author: mramalho Date: Wed Jul 25 05:49:23 2018 New Revision: 337918 URL: http://llvm.org/viewvc/llvm-project?rev=337918&view=rev Log: [analyzer] Implemented SMT generic API
Summary: Created new SMT generic API. Small changes to `Z3ConstraintManager` because of the new generic objects (`SMTSort` and `SMTExpr`) returned by `SMTSolver`. Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: mgorny, xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49495 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337918&view=auto ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 05:49:23 2018 @@ -0,0 +1,546 @@ +//== SMTSolver.h ------------------------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// This file defines a SMT generic Solver API, which will be the base class +// for every SMT solver specific class. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" + +namespace clang { +namespace ento { + +class SMTSolver { +public: + SMTSolver() = default; + virtual ~SMTSolver() = default; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + + // Return an appropriate floating-point sort for the given bitwidth. + SMTSortRef getFloatSort(unsigned BitWidth) { + switch (BitWidth) { + case 16: + return getFloat16Sort(); + case 32: + return getFloat32Sort(); + case 64: + return getFloat64Sort(); + case 128: + return getFloat128Sort(); + default:; + } + llvm_unreachable("Unsupported floating-point bitwidth!"); + } + + // Return an appropriate sort, given a QualType + SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) { + if (Ty->isBooleanType()) + return getBoolSort(); + + if (Ty->isRealFloatingType()) + return getFloatSort(BitWidth); + + return getBitvectorSort(BitWidth); + } + + /// Construct a Z3Expr from a unary operator, given a Z3_context. + SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) { + switch (Op) { + case UO_Minus: + return mkBVNeg(Exp); + + case UO_Not: + return mkBVNot(Exp); + + case UO_LNot: + return mkNot(Exp); + + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a floating-point unary operator, given a + /// Z3_context. + SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op, + const SMTExprRef &Exp) { + switch (Op) { + case UO_Minus: + return mkFPNeg(Exp); + + case UO_LNot: + return fromUnOp(Op, Exp); + + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a n-ary binary operator. + SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op, + const std::vector<SMTExprRef> &ASTs) { + assert(!ASTs.empty()); + + if (Op != BO_LAnd && Op != BO_LOr) + llvm_unreachable("Unimplemented opcode"); + + SMTExprRef res = ASTs.front(); + for (std::size_t i = 1; i < ASTs.size(); ++i) + res = (Op == BO_LAnd) ? mkAnd(res, ASTs[i]) : mkOr(res, ASTs[i]); + return res; + } + + /// Construct a Z3Expr from a binary operator, given a Z3_context. + SMTExprRef fromBinOp(const SMTExprRef &LHS, const BinaryOperator::Opcode Op, + const SMTExprRef &RHS, bool isSigned) { + assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!"); + + switch (Op) { + // Multiplicative operators + case BO_Mul: + return mkBVMul(LHS, RHS); + + case BO_Div: + return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS); + + case BO_Rem: + return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS); + + // Additive operators + case BO_Add: + return mkBVAdd(LHS, RHS); + + case BO_Sub: + return mkBVSub(LHS, RHS); + + // Bitwise shift operators + case BO_Shl: + return mkBVShl(LHS, RHS); + + case BO_Shr: + return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS); + + // Relational operators + case BO_LT: + return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS); + + case BO_GT: + return isSigned ? mkBVSgt(LHS, RHS) : mkBVUgt(LHS, RHS); + + case BO_LE: + return isSigned ? mkBVSle(LHS, RHS) : mkBVUle(LHS, RHS); + + case BO_GE: + return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS); + + // Equality operators + case BO_EQ: + return mkEqual(LHS, RHS); + + case BO_NE: + return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned)); + + // Bitwise operators + case BO_And: + return mkBVAnd(LHS, RHS); + + case BO_Xor: + return mkBVXor(LHS, RHS); + + case BO_Or: + return mkBVOr(LHS, RHS); + + // Logical operators + case BO_LAnd: + return mkAnd(LHS, RHS); + + case BO_LOr: + return mkOr(LHS, RHS); + + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a special floating-point binary operator, given + /// a Z3_context. + SMTExprRef fromFloatSpecialBinOp(const SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const llvm::APFloat::fltCategory &RHS) { + switch (Op) { + // Equality operators + case BO_EQ: + switch (RHS) { + case llvm::APFloat::fcInfinity: + return mkFPIsInfinite(LHS); + + case llvm::APFloat::fcNaN: + return mkFPIsNaN(LHS); + + case llvm::APFloat::fcNormal: + return mkFPIsNormal(LHS); + + case llvm::APFloat::fcZero: + return mkFPIsZero(LHS); + } + break; + + case BO_NE: + return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS)); + + default:; + } + + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a floating-point binary operator, given a + /// Z3_context. + SMTExprRef fromFloatBinOp(const SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const SMTExprRef &RHS) { + assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!"); + + switch (Op) { + // Multiplicative operators + case BO_Mul: + return mkFPMul(LHS, RHS); + + case BO_Div: + return mkFPDiv(LHS, RHS); + + case BO_Rem: + return mkFPRem(LHS, RHS); + + // Additive operators + case BO_Add: + return mkFPAdd(LHS, RHS); + + case BO_Sub: + return mkFPSub(LHS, RHS); + + // Relational operators + case BO_LT: + return mkFPLt(LHS, RHS); + + case BO_GT: + return mkFPGt(LHS, RHS); + + case BO_LE: + return mkFPLe(LHS, RHS); + + case BO_GE: + return mkFPGe(LHS, RHS); + + // Equality operators + case BO_EQ: + return mkFPEqual(LHS, RHS); + + case BO_NE: + return fromFloatUnOp(UO_LNot, fromFloatBinOp(LHS, BO_EQ, RHS)); + + // Logical operators + case BO_LAnd: + case BO_LOr: + return fromBinOp(LHS, Op, RHS, false); + + default:; + } + + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct a Z3Expr from a SymbolCast, given a Z3_context. + SMTExprRef fromCast(const SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, + QualType FromTy, uint64_t FromBitWidth) { + if ((FromTy->isIntegralOrEnumerationType() && + ToTy->isIntegralOrEnumerationType()) || + (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) || + (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) || + (FromTy->isReferenceType() ^ ToTy->isReferenceType())) { + + if (FromTy->isBooleanType()) { + assert(ToBitWidth > 0 && "BitWidth must be positive!"); + return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth), + mkBitvector(llvm::APSInt("0"), ToBitWidth)); + } + + if (ToBitWidth > FromBitWidth) + return FromTy->isSignedIntegerOrEnumerationType() + ? mkSignExt(ToBitWidth - FromBitWidth, Exp) + : mkZeroExt(ToBitWidth - FromBitWidth, Exp); + + if (ToBitWidth < FromBitWidth) + return mkExtract(ToBitWidth - 1, 0, Exp); + + // Both are bitvectors with the same width, ignore the type cast + return Exp; + } + + if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) { + if (ToBitWidth != FromBitWidth) + return mkFPtoFP(Exp, getFloatSort(ToBitWidth)); + + return Exp; + } + + if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { + SMTSortRef Sort = getFloatSort(ToBitWidth); + return FromTy->isSignedIntegerOrEnumerationType() ? mkFPtoSBV(Exp, Sort) + : mkFPtoUBV(Exp, Sort); + } + + if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) + return ToTy->isSignedIntegerOrEnumerationType() + ? mkSBVtoFP(Exp, ToBitWidth) + : mkUBVtoFP(Exp, ToBitWidth); + + llvm_unreachable("Unsupported explicit type cast!"); + } + + // Callback function for doCast parameter on APSInt type. + llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy, + uint64_t ToWidth, QualType FromTy, + uint64_t FromWidth) { + APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType()); + return TargetType.convert(V); + } + + // Return a boolean sort. + virtual SMTSortRef getBoolSort() = 0; + + // Return an appropriate bitvector sort for the given bitwidth. + virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0; + + // Return a floating-point sort of width 16 + virtual SMTSortRef getFloat16Sort() = 0; + + // Return a floating-point sort of width 32 + virtual SMTSortRef getFloat32Sort() = 0; + + // Return a floating-point sort of width 64 + virtual SMTSortRef getFloat64Sort() = 0; + + // Return a floating-point sort of width 128 + virtual SMTSortRef getFloat128Sort() = 0; + + // Return an appropriate sort for the given AST. + virtual SMTSortRef getSort(const SMTExprRef &AST) = 0; + + // Return a new SMTExprRef from an SMTExpr + virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0; + + /// Given a constraint, add it to the solver + virtual void addConstraint(const SMTExprRef &Exp) const = 0; + + /// Create a bitvector addition operation + virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector subtraction operation + virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector multiplication operation + virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector signed modulus operation + virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector unsigned modulus operation + virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector signed division operation + virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector unsigned division operation + virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector logical shift left operation + virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector arithmetic shift right operation + virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector logical shift right operation + virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector negation operation + virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0; + + /// Create a bitvector not operation + virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0; + + /// Create a bitvector xor operation + virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector or operation + virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector and operation + virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector unsigned less-than operation + virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector signed less-than operation + virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector unsigned greater-than operation + virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector signed greater-than operation + virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector unsigned less-equal-than operation + virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector signed less-equal-than operation + virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector unsigned greater-equal-than operation + virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a bitvector signed greater-equal-than operation + virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + /// Create a boolean not operation + virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0; + + /// Create a bitvector equality operation + virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, + const SMTExprRef &F) = 0; + + virtual SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkExtract(unsigned High, unsigned Low, + const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0; + + virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, + const SMTExprRef &RHS) = 0; + + virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; + + virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, + const SMTSortRef &To) = 0; + + virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, + const SMTSortRef &To) = 0; + + virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0; + + virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0; + + virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0; + + // Return an appropriate floating-point rounding mode. + virtual SMTExprRef getFloatRoundingMode() = 0; + + virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0; + + virtual bool getBoolean(const SMTExprRef &Exp) = 0; + + /// Construct a const SMTExprRef &From a boolean. + virtual SMTExprRef mkBoolean(const bool b) = 0; + + /// Construct a const SMTExprRef &From a finite APFloat. + virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0; + + /// Construct a const SMTExprRef &From an APSInt. + virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0; + + SMTExprRef mkBitvector(const llvm::APSInt Int) { + return mkBitvector(Int, Int.getBitWidth()); + } + + /// Given an expression, extract the value of this operand in the model. + virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0; + + /// Given an expression extract the value of this operand in the model. + virtual bool getInterpretation(const SMTExprRef &Exp, + llvm::APFloat &Float) = 0; + + /// Construct a Z3Expr from a boolean, given a Z3_context. + virtual SMTExprRef fromBoolean(const bool Bool) = 0; + /// Construct a Z3Expr from a finite APFloat, given a Z3_context. + virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0; + + /// Construct a Z3Expr from an APSInt, given a Z3_context. + virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0; + + /// Construct a Z3Expr from an integer, given a Z3_context. + virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0; + + /// Construct a const SMTExprRef &From a SymbolData, given a SMT_context. + virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty, + uint64_t BitWidth) = 0; + + /// Check if the constraints are satisfiable + virtual ConditionTruthVal check() const = 0; + + /// Push the current solver state + virtual void push() = 0; + + /// Pop the previous solver state + virtual void pop(unsigned NumStates = 1) = 0; + + /// Reset the solver and remove all constraints. + virtual void reset() const = 0; + + virtual void print(raw_ostream &OS) const = 0; +}; + +using SMTSolverRef = std::shared_ptr<SMTSolver>; + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337918&r1=337917&r2=337918&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:23 2018 @@ -13,6 +13,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" #include "clang/Config/config.h" @@ -93,11 +94,11 @@ class Z3Sort : public SMTSort { Z3_sort Sort; +public: Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) { Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); } -public: /// Override implicit copy constructor for correct reference counting. Z3Sort(const Z3Sort &Copy) : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) { @@ -163,6 +164,10 @@ public: } }; // end class Z3Sort +static const Z3Sort &toZ3Sort(const SMTSort &S) { + return static_cast<const Z3Sort &>(S); +} + class Z3Expr : public SMTExpr { friend class Z3Solver; @@ -170,11 +175,11 @@ class Z3Expr : public SMTExpr { Z3_ast AST; +public: Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) { Z3_inc_ref(Context.Context, AST); } -public: /// Override implicit copy constructor for correct reference counting. Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) { Z3_inc_ref(Context.Context, AST); @@ -228,6 +233,10 @@ public: } }; // end class Z3Expr +static const Z3Expr &toZ3Expr(const SMTExpr &E) { + return static_cast<const Z3Expr &>(E); +} + class Z3Model { friend class Z3Solver; @@ -304,25 +313,27 @@ static bool areEquivalent(const llvm::fl llvm::APFloat::semanticsSizeInBits(RHS)); } -class Z3Solver { +class Z3Solver : public SMTSolver { friend class Z3ConstraintManager; Z3Context Context; Z3_solver Solver; - Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { + Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) { Z3_solver_inc_ref(Context.Context, Solver); } public: /// Override implicit copy constructor for correct reference counting. - Z3Solver(const Z3Solver &Copy) : Context(Copy.Context), Solver(Copy.Solver) { + Z3Solver(const Z3Solver &Copy) + : SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) { Z3_solver_inc_ref(Context.Context, Solver); } /// Provide move constructor - Z3Solver(Z3Solver &&Move) : Context(Move.Context), Solver(nullptr) { + Z3Solver(Z3Solver &&Move) + : SMTSolver(), Context(Move.Context), Solver(nullptr) { *this = std::move(Move); } @@ -342,470 +353,460 @@ public: Z3_solver_dec_ref(Context.Context, Solver); } - /// Given a constraint, add it to the solver - void addConstraint(const Z3Expr &Exp) { - Z3_solver_assert(Context.Context, Solver, Exp.AST); - } - - // Return a boolean sort. - Z3Sort getBoolSort() { - return Z3Sort(Context, Z3_mk_bool_sort(Context.Context)); - } - - // Return an appropriate bitvector sort for the given bitwidth. - Z3Sort getBitvectorSort(unsigned BitWidth) { - return Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)); - } - - // Return an appropriate floating-point sort for the given bitwidth. - Z3Sort getFloatSort(unsigned BitWidth) { - Z3_sort Sort; - - switch (BitWidth) { - default: - llvm_unreachable("Unsupported floating-point bitwidth!"); - break; - case 16: - Sort = Z3_mk_fpa_sort_16(Context.Context); - break; - case 32: - Sort = Z3_mk_fpa_sort_32(Context.Context); - break; - case 64: - Sort = Z3_mk_fpa_sort_64(Context.Context); - break; - case 128: - Sort = Z3_mk_fpa_sort_128(Context.Context); - break; - } - return Z3Sort(Context, Sort); + void addConstraint(const SMTExprRef &Exp) const override { + Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); } - // Return an appropriate sort, given a QualType - Z3Sort MkSort(const QualType &Ty, unsigned BitWidth) { - if (Ty->isBooleanType()) - return getBoolSort(); + SMTSortRef getBoolSort() override { + return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context)); + } - if (Ty->isRealFloatingType()) - return getFloatSort(BitWidth); + SMTSortRef getBitvectorSort(unsigned BitWidth) override { + return std::make_shared<Z3Sort>(Context, + Z3_mk_bv_sort(Context.Context, BitWidth)); + } - return getBitvectorSort(BitWidth); + SMTSortRef getSort(const SMTExprRef &Exp) override { + return std::make_shared<Z3Sort>( + Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)); } - // Return an appropriate sort for the given AST. - Z3Sort getSort(Z3_ast AST) { - return Z3Sort(Context, Z3_get_sort(Context.Context, AST)); + SMTSortRef getFloat16Sort() override { + return std::make_shared<Z3Sort>(Context, + Z3_mk_fpa_sort_16(Context.Context)); } - /// Given a program state, construct the logical conjunction and add it to - /// the solver - void addStateConstraints(ProgramStateRef State) { - // TODO: Don't add all the constraints, only the relevant ones - ConstraintZ3Ty CZ = State->get<ConstraintZ3>(); - ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end(); - - // Construct the logical AND of all the constraints - if (I != IE) { - std::vector<Z3_ast> ASTs; + SMTSortRef getFloat32Sort() override { + return std::make_shared<Z3Sort>(Context, + Z3_mk_fpa_sort_32(Context.Context)); + } - while (I != IE) - ASTs.push_back(I++->second.AST); + SMTSortRef getFloat64Sort() override { + return std::make_shared<Z3Sort>(Context, + Z3_mk_fpa_sort_64(Context.Context)); + } - Z3Expr Conj = fromNBinOp(BO_LAnd, ASTs); - addConstraint(Conj); - } + SMTSortRef getFloat128Sort() override { + return std::make_shared<Z3Sort>(Context, + Z3_mk_fpa_sort_128(Context.Context)); } - // Return an appropriate floating-point rounding mode. - Z3Expr getFloatRoundingMode() { - // TODO: Don't assume nearest ties to even rounding mode - return Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)); + SMTExprRef newExprRef(const SMTExpr &E) const override { + return std::make_shared<Z3Expr>(toZ3Expr(E)); } - /// Construct a Z3Expr from a unary operator, given a Z3_context. - Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) { - Z3_ast AST; + SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); + } - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; + SMTExprRef mkBVNot(const SMTExprRef &Exp) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); + } - case UO_Minus: - AST = Z3_mk_bvneg(Context.Context, Exp.AST); - break; + SMTExprRef mkNot(const SMTExprRef &Exp) override { + return newExprRef( + Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); + } - case UO_Not: - AST = Z3_mk_bvnot(Context.Context, Exp.AST); - break; + SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - case UO_LNot: - AST = Z3_mk_not(Context.Context, Exp.AST); - break; - } + SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); } - /// Construct a Z3Expr from a floating-point unary operator, given a - /// Z3_context. - Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) { - Z3_ast AST; + SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; + SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - case UO_Minus: - AST = Z3_mk_fpa_neg(Context.Context, Exp.AST); - break; + SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - case UO_LNot: - return fromUnOp(Op, Exp); - } + SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); } - /// Construct a Z3Expr from a n-ary binary operator. - Z3Expr fromNBinOp(const BinaryOperator::Opcode Op, - const std::vector<Z3_ast> &ASTs) { - Z3_ast AST; - - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - - case BO_LAnd: - AST = Z3_mk_and(Context.Context, ASTs.size(), ASTs.data()); - break; - - case BO_LOr: - AST = Z3_mk_or(Context.Context, ASTs.size(), ASTs.data()); - break; - } + SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); } - /// Construct a Z3Expr from a binary operator, given a Z3_context. - Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op, - const Z3Expr &RHS, bool isSigned) { - Z3_ast AST; - - assert(getSort(LHS.AST) == getSort(RHS.AST) && - "AST's must have the same sort!"); - - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - - // Multiplicative operators - case BO_Mul: - AST = Z3_mk_bvmul(Context.Context, LHS.AST, RHS.AST); - break; - case BO_Div: - AST = isSigned ? Z3_mk_bvsdiv(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvudiv(Context.Context, LHS.AST, RHS.AST); - break; - case BO_Rem: - AST = isSigned ? Z3_mk_bvsrem(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvurem(Context.Context, LHS.AST, RHS.AST); - break; - - // Additive operators - case BO_Add: - AST = Z3_mk_bvadd(Context.Context, LHS.AST, RHS.AST); - break; - case BO_Sub: - AST = Z3_mk_bvsub(Context.Context, LHS.AST, RHS.AST); - break; - - // Bitwise shift operators - case BO_Shl: - AST = Z3_mk_bvshl(Context.Context, LHS.AST, RHS.AST); - break; - case BO_Shr: - AST = isSigned ? Z3_mk_bvashr(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvlshr(Context.Context, LHS.AST, RHS.AST); - break; - - // Relational operators - case BO_LT: - AST = isSigned ? Z3_mk_bvslt(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvult(Context.Context, LHS.AST, RHS.AST); - break; - case BO_GT: - AST = isSigned ? Z3_mk_bvsgt(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvugt(Context.Context, LHS.AST, RHS.AST); - break; - case BO_LE: - AST = isSigned ? Z3_mk_bvsle(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvule(Context.Context, LHS.AST, RHS.AST); - break; - case BO_GE: - AST = isSigned ? Z3_mk_bvsge(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvuge(Context.Context, LHS.AST, RHS.AST); - break; - - // Equality operators - case BO_EQ: - AST = Z3_mk_eq(Context.Context, LHS.AST, RHS.AST); - break; - case BO_NE: - return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned)); - break; - - // Bitwise operators - case BO_And: - AST = Z3_mk_bvand(Context.Context, LHS.AST, RHS.AST); - break; - case BO_Xor: - AST = Z3_mk_bvxor(Context.Context, LHS.AST, RHS.AST); - break; - case BO_Or: - AST = Z3_mk_bvor(Context.Context, LHS.AST, RHS.AST); - break; - - // Logical operators - case BO_LAnd: - case BO_LOr: { - std::vector<Z3_ast> Args = {LHS.AST, RHS.AST}; - return fromNBinOp(Op, Args); - } - } + SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); } - /// Construct a Z3Expr from a special floating-point binary operator, given - /// a Z3_context. - Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS, - const BinaryOperator::Opcode Op, - const llvm::APFloat::fltCategory &RHS) { - Z3_ast AST; - - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - - // Equality operators - case BO_EQ: - switch (RHS) { - case llvm::APFloat::fcInfinity: - AST = Z3_mk_fpa_is_infinite(Context.Context, LHS.AST); - break; - case llvm::APFloat::fcNaN: - AST = Z3_mk_fpa_is_nan(Context.Context, LHS.AST); - break; - case llvm::APFloat::fcNormal: - AST = Z3_mk_fpa_is_normal(Context.Context, LHS.AST); - break; - case llvm::APFloat::fcZero: - AST = Z3_mk_fpa_is_zero(Context.Context, LHS.AST); - break; - } - break; - case BO_NE: - return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS)); - break; - } + SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); } - /// Construct a Z3Expr from a floating-point binary operator, given a - /// Z3_context. - Z3Expr fromFloatBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op, - const Z3Expr &RHS) { - Z3_ast AST; - - assert(getSort(LHS.AST) == getSort(RHS.AST) && - "AST's must have the same sort!"); - - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - - // Multiplicative operators - case BO_Mul: { - Z3Expr RoundingMode = getFloatRoundingMode(); - AST = Z3_mk_fpa_mul(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST); - break; - } - case BO_Div: { - Z3Expr RoundingMode = getFloatRoundingMode(); - AST = Z3_mk_fpa_div(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST); - break; - } - case BO_Rem: - AST = Z3_mk_fpa_rem(Context.Context, LHS.AST, RHS.AST); - break; - - // Additive operators - case BO_Add: { - Z3Expr RoundingMode = getFloatRoundingMode(); - AST = Z3_mk_fpa_add(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST); - break; - } - case BO_Sub: { - Z3Expr RoundingMode = getFloatRoundingMode(); - AST = Z3_mk_fpa_sub(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST); - break; - } + SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - // Relational operators - case BO_LT: - AST = Z3_mk_fpa_lt(Context.Context, LHS.AST, RHS.AST); - break; - case BO_GT: - AST = Z3_mk_fpa_gt(Context.Context, LHS.AST, RHS.AST); - break; - case BO_LE: - AST = Z3_mk_fpa_leq(Context.Context, LHS.AST, RHS.AST); - break; - case BO_GE: - AST = Z3_mk_fpa_geq(Context.Context, LHS.AST, RHS.AST); - break; - - // Equality operators - case BO_EQ: - AST = Z3_mk_fpa_eq(Context.Context, LHS.AST, RHS.AST); - break; - case BO_NE: - return fromFloatUnOp(UO_LNot, fromFloatBinOp(LHS, BO_EQ, RHS)); - break; - - // Logical operators - case BO_LAnd: - case BO_LOr: - return fromBinOp(LHS, Op, RHS, false); - } + SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); } - /// Construct a Z3Expr from a SymbolData, given a Z3_context. - Z3Expr fromData(const SymbolID ID, const QualType &Ty, uint64_t BitWidth) { - llvm::Twine Name = "$" + llvm::Twine(ID); + SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - Z3Sort Sort = MkSort(Ty, BitWidth); + SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } - Z3_symbol Symbol = Z3_mk_string_symbol(Context.Context, Name.str().c_str()); - Z3_ast AST = Z3_mk_const(Context.Context, Symbol, Sort.Sort); - return Z3Expr(Context, AST); - } - - /// Construct a Z3Expr from a SymbolCast, given a Z3_context. - Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth, - QualType FromTy, uint64_t FromBitWidth) { - Z3_ast AST; - - if ((FromTy->isIntegralOrEnumerationType() && - ToTy->isIntegralOrEnumerationType()) || - (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) || - (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) || - (FromTy->isReferenceType() ^ ToTy->isReferenceType())) { - // Special case: Z3 boolean type is distinct from bitvector type, so - // must use if-then-else expression instead of direct cast - if (FromTy->isBooleanType()) { - assert(ToBitWidth > 0 && "BitWidth must be positive!"); - Z3Expr Zero = fromInt("0", ToBitWidth); - Z3Expr One = fromInt("1", ToBitWidth); - AST = Z3_mk_ite(Context.Context, Exp.AST, One.AST, Zero.AST); - } else if (ToBitWidth > FromBitWidth) { - AST = FromTy->isSignedIntegerOrEnumerationType() - ? Z3_mk_sign_ext(Context.Context, ToBitWidth - FromBitWidth, - Exp.AST) - : Z3_mk_zero_ext(Context.Context, ToBitWidth - FromBitWidth, - Exp.AST); - } else if (ToBitWidth < FromBitWidth) { - AST = Z3_mk_extract(Context.Context, ToBitWidth - 1, 0, Exp.AST); - } else { - // Both are bitvectors with the same width, ignore the type cast - return Exp; - } - } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) { - if (ToBitWidth != FromBitWidth) { - Z3Expr RoundingMode = getFloatRoundingMode(); - Z3Sort Sort = getFloatSort(ToBitWidth); - AST = Z3_mk_fpa_to_fp_float(Context.Context, RoundingMode.AST, Exp.AST, - Sort.Sort); - } else { - return Exp; - } - } else if (FromTy->isIntegralOrEnumerationType() && - ToTy->isRealFloatingType()) { - Z3Expr RoundingMode = getFloatRoundingMode(); - Z3Sort Sort = getFloatSort(ToBitWidth); - AST = FromTy->isSignedIntegerOrEnumerationType() - ? Z3_mk_fpa_to_fp_signed(Context.Context, RoundingMode.AST, - Exp.AST, Sort.Sort) - : Z3_mk_fpa_to_fp_unsigned(Context.Context, RoundingMode.AST, - Exp.AST, Sort.Sort); - } else if (FromTy->isRealFloatingType() && - ToTy->isIntegralOrEnumerationType()) { - Z3Expr RoundingMode = getFloatRoundingMode(); - AST = ToTy->isSignedIntegerOrEnumerationType() - ? Z3_mk_fpa_to_sbv(Context.Context, RoundingMode.AST, Exp.AST, - ToBitWidth) - : Z3_mk_fpa_to_ubv(Context.Context, RoundingMode.AST, Exp.AST, - ToBitWidth); - } else { - llvm_unreachable("Unsupported explicit type cast!"); - } + SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; + return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args))); + } + + SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; + return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args))); + } + + SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPNeg(const SMTExprRef &Exp) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override { + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override { + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override { + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef( + Z3Expr(Context, + Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST))); + } + + SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef( + Z3Expr(Context, + Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST))); + } + + SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef( + Z3Expr(Context, + Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST))); + } + + SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef( + Z3Expr(Context, + Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST))); + } - return Z3Expr(Context, AST); + SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, + const SMTExprRef &F) override { + return newExprRef( + Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST, + toZ3Expr(*T).AST, toZ3Expr(*F).AST))); + } + + SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) override { + return newExprRef(Z3Expr( + Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) override { + return newExprRef(Z3Expr( + Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkExtract(unsigned High, unsigned Low, + const SMTExprRef &Exp) override { + return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low, + toZ3Expr(*Exp).AST))); + } + + SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return newExprRef( + Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, + toZ3Expr(*RHS).AST))); + } + + SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef(Z3Expr( + Context, + Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST, + toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); + } + + SMTExprRef mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef(Z3Expr( + Context, + Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST, + toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); + } + + SMTExprRef mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef(Z3Expr( + Context, + Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST, + toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); + } + + SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST, + toZ3Expr(*From).AST, ToWidth))); + } + + SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, + toZ3Expr(*From).AST, ToWidth))); + } + + SMTExprRef mkBoolean(const bool b) override { + return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context) + : Z3_mk_false(Context.Context))); + } + + SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override { + const SMTSortRef Sort = getBitvectorSort(BitWidth); + return newExprRef( + Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(), + toZ3Sort(*Sort).Sort))); + } + + SMTExprRef mkFloat(const llvm::APFloat Float) override { + SMTSortRef Sort = + getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics())); + + llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false); + SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth()); + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, + toZ3Sort(*Sort).Sort))); + } + + SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override { + return newExprRef( + Z3Expr(Context, Z3_mk_const(Context.Context, + Z3_mk_string_symbol(Context.Context, Name), + toZ3Sort(*Sort).Sort))); + } + + const llvm::APSInt getBitvector(const SMTExprRef &Exp) override { + // FIXME: this returns a string and the bitWidth is overridden + return llvm::APSInt( + Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST)); + } + + bool getBoolean(const SMTExprRef &Exp) override { + return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE; + } + + // Return an appropriate floating-point rounding mode. + SMTExprRef getFloatRoundingMode() override { + // TODO: Don't assume nearest ties to even rounding mode + return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context))); + } + + /// Construct a Z3Expr from a SymbolData, given a Z3_context. + SMTExprRef fromData(const SymbolID ID, const QualType &Ty, + uint64_t BitWidth) override { + llvm::Twine Name = "$" + llvm::Twine(ID); + return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth)); } /// Construct a Z3Expr from a boolean, given a Z3_context. - Z3Expr fromBoolean(const bool Bool) { + SMTExprRef fromBoolean(const bool Bool) override { Z3_ast AST = Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context); - return Z3Expr(Context, AST); + return newExprRef(Z3Expr(Context, AST)); } /// Construct a Z3Expr from a finite APFloat, given a Z3_context. - Z3Expr fromAPFloat(const llvm::APFloat &Float) { - Z3_ast AST; - Z3Sort Sort = + SMTExprRef fromAPFloat(const llvm::APFloat &Float) override { + SMTSortRef Sort = getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics())); llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false); - Z3Expr Z3Int = fromAPSInt(Int); - AST = Z3_mk_fpa_to_fp_bv(Context.Context, Z3Int.AST, Sort.Sort); - return Z3Expr(Context, AST); + SMTExprRef Z3Int = fromAPSInt(Int); + return newExprRef(Z3Expr( + Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, + toZ3Sort(*Sort).Sort))); } /// Construct a Z3Expr from an APSInt, given a Z3_context. - Z3Expr fromAPSInt(const llvm::APSInt &Int) { - Z3Sort Sort = getBitvectorSort(Int.getBitWidth()); - Z3_ast AST = - Z3_mk_numeral(Context.Context, Int.toString(10).c_str(), Sort.Sort); - return Z3Expr(Context, AST); + SMTExprRef fromAPSInt(const llvm::APSInt &Int) override { + SMTSortRef Sort = getBitvectorSort(Int.getBitWidth()); + Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(), + toZ3Sort(*Sort).Sort); + return newExprRef(Z3Expr(Context, AST)); } /// Construct a Z3Expr from an integer, given a Z3_context. - Z3Expr fromInt(const char *Int, uint64_t BitWidth) { - Z3Sort Sort = getBitvectorSort(BitWidth); - Z3_ast AST = Z3_mk_numeral(Context.Context, Int, Sort.Sort); - return Z3Expr(Context, AST); + SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override { + SMTSortRef Sort = getBitvectorSort(BitWidth); + Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort); + return newExprRef(Z3Expr(Context, AST)); } - /// Construct an APFloat from a Z3Expr, given the AST representation - bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, llvm::APFloat &Float, - bool useSemantics = true) { - assert(Sort.isFloatSort() && "Unsupported sort to floating-point!"); + bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST, + llvm::APFloat &Float, bool useSemantics) { + assert(Sort->isFloatSort() && "Unsupported sort to floating-point!"); - llvm::APSInt Int(Sort.getFloatSortSize(), true); + llvm::APSInt Int(Sort->getFloatSortSize(), true); const llvm::fltSemantics &Semantics = - getFloatSemantics(Sort.getFloatSortSize()); - Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize()); + getFloatSemantics(Sort->getFloatSortSize()); + SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize()); if (!toAPSInt(BVSort, AST, Int, true)) { return false; } @@ -819,11 +820,10 @@ public: return true; } - /// Construct an APSInt from a Z3Expr, given the AST representation - bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int, - bool useSemantics = true) { - if (Sort.isBitvectorSort()) { - if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) { + bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST, + llvm::APSInt &Int, bool useSemantics) { + if (Sort->isBitvectorSort()) { + if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) { assert(false && "Bitvector types don't match!"); return false; } @@ -832,15 +832,14 @@ public: // Force cast because Z3 defines __uint64 to be a unsigned long long // type, which isn't compatible with a unsigned long type, even if they // are the same size. - Z3_get_numeral_uint64(Context.Context, AST, + Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST, reinterpret_cast<__uint64 *>(&Value[0])); - if (Sort.getBitvectorSortSize() <= 64) { + if (Sort->getBitvectorSortSize() <= 64) { Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), Int.isUnsigned()); - } else if (Sort.getBitvectorSortSize() == 128) { - Z3Expr ASTHigh = - Z3Expr(Context, Z3_mk_extract(Context.Context, 127, 64, AST)); - Z3_get_numeral_uint64(Context.Context, AST, + } else if (Sort->getBitvectorSortSize() == 128) { + SMTExprRef ASTHigh = mkExtract(127, 64, AST); + Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST, reinterpret_cast<__uint64 *>(&Value[1])); Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), Int.isUnsigned()); @@ -851,17 +850,14 @@ public: return true; } - if (Sort.isBooleanSort()) { + if (Sort->isBooleanSort()) { if (useSemantics && Int.getBitWidth() < 1) { assert(false && "Boolean type doesn't match!"); return false; } - Int = llvm::APSInt( - llvm::APInt(Int.getBitWidth(), - Z3_get_bool_value(Context.Context, AST) == Z3_L_TRUE ? 1 - : 0), - Int.isUnsigned()); + Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)), + Int.isUnsigned()); return true; } @@ -870,50 +866,53 @@ public: /// Given an expression and a model, extract the value of this operand in /// the model. - bool getInterpretation(const Z3Model Model, const Z3Expr &Exp, - llvm::APSInt &Int) { - Z3_func_decl Func = - Z3_get_app_decl(Context.Context, Z3_to_app(Context.Context, Exp.AST)); + bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override { + Z3Model Model = getModel(); + Z3_func_decl Func = Z3_get_app_decl( + Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) return false; - Z3_ast Assign = - Z3_model_get_const_interp(Context.Context, Model.Model, Func); - Z3Sort Sort = getSort(Assign); + SMTExprRef Assign = newExprRef( + Z3Expr(Context, + Z3_model_get_const_interp(Context.Context, Model.Model, Func))); + SMTSortRef Sort = getSort(Assign); return toAPSInt(Sort, Assign, Int, true); } /// Given an expression and a model, extract the value of this operand in /// the model. - bool getInterpretation(const Z3Model Model, const Z3Expr &Exp, - llvm::APFloat &Float) { - Z3_func_decl Func = - Z3_get_app_decl(Context.Context, Z3_to_app(Context.Context, Exp.AST)); + bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override { + Z3Model Model = getModel(); + Z3_func_decl Func = Z3_get_app_decl( + Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) return false; - Z3_ast Assign = - Z3_model_get_const_interp(Context.Context, Model.Model, Func); - Z3Sort Sort = getSort(Assign); + SMTExprRef Assign = newExprRef( + Z3Expr(Context, + Z3_model_get_const_interp(Context.Context, Model.Model, Func))); + SMTSortRef Sort = getSort(Assign); return toAPFloat(Sort, Assign, Float, true); } - // Callback function for doCast parameter on APSInt type. - llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy, - uint64_t ToWidth, QualType FromTy, - uint64_t FromWidth) { - APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType()); - return TargetType.convert(V); - } - /// Check if the constraints are satisfiable - Z3_lbool check() { return Z3_solver_check(Context.Context, Solver); } + ConditionTruthVal check() const override { + Z3_lbool res = Z3_solver_check(Context.Context, Solver); + if (res == Z3_L_TRUE) + return true; + + if (res == Z3_L_FALSE) + return false; + + return ConditionTruthVal(); + } /// Push the current solver state - void push() { return Z3_solver_push(Context.Context, Solver); } + void push() override { return Z3_solver_push(Context.Context, Solver); } /// Pop the previous solver state - void pop(unsigned NumStates = 1) { + void pop(unsigned NumStates = 1) override { assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates); return Z3_solver_pop(Context.Context, Solver, NumStates); } @@ -925,13 +924,11 @@ public: } /// Reset the solver and remove all constraints. - void reset() { Z3_solver_reset(Context.Context, Solver); } + void reset() const override { Z3_solver_reset(Context.Context, Solver); } - void print(raw_ostream &OS) const { + void print(raw_ostream &OS) const override { OS << Z3_solver_to_string(Context.Context, Solver); } - - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } }; // end class Z3Solver class Z3ConstraintManager : public SMTConstraintManager { @@ -988,54 +985,60 @@ private: // Internal implementation. //===------------------------------------------------------------------===// + /// Given a program state, construct the logical conjunction and add it to + /// the solver + void addStateConstraints(ProgramStateRef State) const; + // Check whether a new model is satisfiable, and update the program state. ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym, - const Z3Expr &Exp); + const SMTExprRef &Exp); // Generate and check a Z3 model, using the given constraint. - Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const; + ConditionTruthVal checkZ3Model(ProgramStateRef State, + const SMTExprRef &Exp) const; // Generate a Z3Expr that represents the given symbolic expression. // Sets the hasComparison parameter if the expression has a comparison // operator. // Sets the RetTy parameter to the final return type after promotions and // casts. - Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr, - bool *hasComparison = nullptr) const; + SMTExprRef getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr, + bool *hasComparison = nullptr) const; // Generate a Z3Expr that takes the logical not of an expression. - Z3Expr getZ3NotExpr(const Z3Expr &Exp) const; + SMTExprRef getZ3NotExpr(const SMTExprRef &Exp) const; // Generate a Z3Expr that compares the expression to zero. - Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy, - bool Assumption) const; + SMTExprRef getZ3ZeroExpr(const SMTExprRef &Exp, QualType RetTy, + bool Assumption) const; // Recursive implementation to unpack and generate symbolic expression. // Sets the hasComparison and RetTy parameters. See getZ3Expr(). - Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy, - bool *hasComparison) const; + SMTExprRef getZ3SymExpr(SymbolRef Sym, QualType *RetTy, + bool *hasComparison) const; // Wrapper to generate Z3Expr from SymbolData. - Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const; + SMTExprRef getZ3DataExpr(const SymbolID ID, QualType Ty) const; // Wrapper to generate Z3Expr from SymbolCast. - Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const; + SMTExprRef getZ3CastExpr(const SMTExprRef &Exp, QualType FromTy, + QualType Ty) const; // Wrapper to generate Z3Expr from BinarySymExpr. // Sets the hasComparison and RetTy parameters. See getZ3Expr(). - Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison, - QualType *RetTy) const; + SMTExprRef getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison, + QualType *RetTy) const; // Wrapper to generate Z3Expr from unpacked binary symbolic expression. // Sets the RetTy parameter. See getZ3Expr(). - Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy, - BinaryOperator::Opcode Op, const Z3Expr &RHS, - QualType RTy, QualType *RetTy) const; + SMTExprRef getZ3BinExpr(const SMTExprRef &LHS, QualType LTy, + BinaryOperator::Opcode Op, const SMTExprRef &RHS, + QualType RTy, QualType *RetTy) const; // Wrapper to generate Z3Expr from a range. If From == To, an equality will // be created instead. - Z3Expr getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, bool InRange); + SMTExprRef getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From, + const llvm::APSInt &To, bool InRange); //===------------------------------------------------------------------===// // Helper functions. @@ -1051,33 +1054,49 @@ private: // Perform implicit type conversion on binary symbolic expressions. // May modify all input parameters. // TODO: Refactor to use built-in conversion functions - void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType <y, + void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType <y, QualType &RTy) const; // Perform implicit integer type conversion. // May modify all input parameters. // TODO: Refactor to use Sema::handleIntegerConversion() - template <typename T, T (Z3Solver::*doCast)(const T &, QualType, uint64_t, - QualType, uint64_t)> + template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t, + QualType, uint64_t)> void doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const; // Perform implicit floating-point type conversion. // May modify all input parameters. // TODO: Refactor to use Sema::handleFloatConversion() - template <typename T, T (Z3Solver::*doCast)(const T &, QualType, uint64_t, - QualType, uint64_t)> + template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t, + QualType, uint64_t)> void doFloatTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const; }; // end class Z3ConstraintManager } // end anonymous namespace +void Z3ConstraintManager::addStateConstraints(ProgramStateRef State) const { + // TODO: Don't add all the constraints, only the relevant ones + ConstraintZ3Ty CZ = State->get<ConstraintZ3>(); + ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end(); + + // Construct the logical AND of all the constraints + if (I != IE) { + std::vector<SMTExprRef> ASTs; + + while (I != IE) + ASTs.push_back(Solver.newExprRef(Z3Expr(I++->second))); + + Solver.addConstraint(Solver.fromNBinOp(BO_LAnd, ASTs)); + } +} + ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) { QualType RetTy; bool hasComparison; - Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison); + SMTExprRef Exp = getZ3Expr(Sym, &RetTy, &hasComparison); // Create zero comparison for implicit boolean cast, with reversed assumption if (!hasComparison && !RetTy->isBooleanType()) return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption)); @@ -1145,27 +1164,29 @@ ConditionTruthVal Z3ConstraintManager::c SymbolRef Sym) { QualType RetTy; // The expression may be casted, so we cannot call getZ3DataExpr() directly - Z3Expr VarExp = getZ3Expr(Sym, &RetTy); - Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true); + SMTExprRef VarExp = getZ3Expr(Sym, &RetTy); + SMTExprRef Exp = getZ3ZeroExpr(VarExp, RetTy, true); + // Negate the constraint - Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false); + SMTExprRef NotExp = getZ3ZeroExpr(VarExp, RetTy, false); Solver.reset(); - Solver.addStateConstraints(State); + addStateConstraints(State); Solver.push(); Solver.addConstraint(Exp); - Z3_lbool isSat = Solver.check(); + ConditionTruthVal isSat = Solver.check(); Solver.pop(); Solver.addConstraint(NotExp); - Z3_lbool isNotSat = Solver.check(); + ConditionTruthVal isNotSat = Solver.check(); // Zero is the only possible solution - if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE) + if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) return true; + // Zero is not a solution - else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE) + if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) return false; // Zero may be a solution @@ -1183,29 +1204,31 @@ const llvm::APSInt *Z3ConstraintManager: llvm::APSInt Value(Ctx.getTypeSize(Ty), !Ty->isSignedIntegerOrEnumerationType()); - Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty); + SMTExprRef Exp = getZ3DataExpr(SD->getSymbolID(), Ty); Solver.reset(); - Solver.addStateConstraints(State); + addStateConstraints(State); // Constraints are unsatisfiable - if (Solver.check() != Z3_L_TRUE) + ConditionTruthVal isSat = Solver.check(); + if (!isSat.isConstrainedTrue()) return nullptr; - Z3Model Model = Solver.getModel(); // Model does not assign interpretation - if (!Solver.getInterpretation(Model, Exp, Value)) + if (!Solver.getInterpretation(Exp, Value)) return nullptr; // A value has been obtained, check if it is the only value - Z3Expr NotExp = Solver.fromBinOp( + SMTExprRef NotExp = Solver.fromBinOp( Exp, BO_NE, Ty->isBooleanType() ? Solver.fromBoolean(Value.getBoolValue()) : Solver.fromAPSInt(Value), false); Solver.addConstraint(NotExp); - if (Solver.check() == Z3_L_TRUE) + + ConditionTruthVal isNotSat = Solver.check(); + if (isNotSat.isConstrainedTrue()) return nullptr; // This is the only solution, store it @@ -1244,8 +1267,8 @@ const llvm::APSInt *Z3ConstraintManager: QualType LTy, RTy; std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS); std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS); - doIntTypeConversion<llvm::APSInt, &Z3Solver::castAPSInt>(ConvertedLHS, LTy, - ConvertedRHS, RTy); + doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>( + ConvertedLHS, LTy, ConvertedRHS, RTy); return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); } @@ -1272,9 +1295,9 @@ void Z3ConstraintManager::addRangeConstr for (const auto &I : CR) { SymbolRef Sym = I.first; - Z3Expr Constraints = Solver.fromBoolean(false); + SMTExprRef Constraints = Solver.fromBoolean(false); for (const auto &Range : I.second) { - Z3Expr SymRange = + SMTExprRef SymRange = getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true); // FIXME: the last argument (isSigned) is not used when generating the @@ -1287,10 +1310,7 @@ void Z3ConstraintManager::addRangeConstr } clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() { - if (Solver.check() == Z3_L_FALSE) - return false; - - return ConditionTruthVal(); + return Solver.check(); } LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const { Solver.dump(); } @@ -1301,24 +1321,25 @@ LLVM_DUMP_METHOD void Z3ConstraintManage ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State, SymbolRef Sym, - const Z3Expr &Exp) { + const SMTExprRef &Exp) { // Check the model, avoid simplifying AST to save time - if (checkZ3Model(State, Exp) == Z3_L_TRUE) - return State->add<ConstraintZ3>(std::make_pair(Sym, Exp)); + if (checkZ3Model(State, Exp).isConstrainedTrue()) + return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp))); return nullptr; } -Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State, - const Z3Expr &Exp) const { +ConditionTruthVal +Z3ConstraintManager::checkZ3Model(ProgramStateRef State, + const SMTExprRef &Exp) const { Solver.reset(); Solver.addConstraint(Exp); - Solver.addStateConstraints(State); + addStateConstraints(State); return Solver.check(); } -Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy, - bool *hasComparison) const { +SMTExprRef Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy, + bool *hasComparison) const { if (hasComparison) { *hasComparison = false; } @@ -1326,12 +1347,13 @@ Z3Expr Z3ConstraintManager::getZ3Expr(Sy return getZ3SymExpr(Sym, RetTy, hasComparison); } -Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const { +SMTExprRef Z3ConstraintManager::getZ3NotExpr(const SMTExprRef &Exp) const { return Solver.fromUnOp(UO_LNot, Exp); } -Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty, - bool Assumption) const { +SMTExprRef Z3ConstraintManager::getZ3ZeroExpr(const SMTExprRef &Exp, + QualType Ty, + bool Assumption) const { ASTContext &Ctx = getBasicVals().getContext(); if (Ty->isRealFloatingType()) { llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); @@ -1350,8 +1372,8 @@ Z3Expr Z3ConstraintManager::getZ3ZeroExp llvm_unreachable("Unsupported type for zero value!"); } -Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy, - bool *hasComparison) const { +SMTExprRef Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy, + bool *hasComparison) const { if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { if (RetTy) *RetTy = Sym->getType(); @@ -1362,7 +1384,7 @@ Z3Expr Z3ConstraintManager::getZ3SymExpr *RetTy = Sym->getType(); QualType FromTy; - Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison); + SMTExprRef Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison); // Casting an expression with a comparison invalidates it. Note that this // must occur after the recursive call above. // e.g. (signed char) (x > 0) @@ -1370,7 +1392,7 @@ Z3Expr Z3ConstraintManager::getZ3SymExpr *hasComparison = false; return getZ3CastExpr(Exp, FromTy, Sym->getType()); } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { - Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy); + SMTExprRef Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy); // Set the hasComparison parameter, in post-order traversal order. if (hasComparison) *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode()); @@ -1380,52 +1402,52 @@ Z3Expr Z3ConstraintManager::getZ3SymExpr llvm_unreachable("Unsupported SymbolRef type!"); } -Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID, - QualType Ty) const { +SMTExprRef Z3ConstraintManager::getZ3DataExpr(const SymbolID ID, + QualType Ty) const { ASTContext &Ctx = getBasicVals().getContext(); return Solver.fromData(ID, Ty, Ctx.getTypeSize(Ty)); } -Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, - QualType ToTy) const { +SMTExprRef Z3ConstraintManager::getZ3CastExpr(const SMTExprRef &Exp, + QualType FromTy, + QualType ToTy) const { ASTContext &Ctx = getBasicVals().getContext(); return Solver.fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, Ctx.getTypeSize(FromTy)); } -Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE, - bool *hasComparison, - QualType *RetTy) const { +SMTExprRef Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE, + bool *hasComparison, + QualType *RetTy) const { QualType LTy, RTy; BinaryOperator::Opcode Op = BSE->getOpcode(); if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { - Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison); + SMTExprRef LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison); llvm::APSInt NewRInt; std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS()); - Z3Expr RHS = Solver.fromAPSInt(NewRInt); + SMTExprRef RHS = Solver.fromAPSInt(NewRInt); return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { llvm::APSInt NewLInt; std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS()); - Z3Expr LHS = Solver.fromAPSInt(NewLInt); - Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison); + SMTExprRef LHS = Solver.fromAPSInt(NewLInt); + SMTExprRef RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison); return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { - Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison); - Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison); + SMTExprRef LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison); + SMTExprRef RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison); return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); } else { llvm_unreachable("Unsupported BinarySymExpr type!"); } } -Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy, - BinaryOperator::Opcode Op, - const Z3Expr &RHS, QualType RTy, - QualType *RetTy) const { - Z3Expr NewLHS = LHS; - Z3Expr NewRHS = RHS; +SMTExprRef Z3ConstraintManager::getZ3BinExpr( + const SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, + const SMTExprRef &RHS, QualType RTy, QualType *RetTy) const { + SMTExprRef NewLHS = LHS; + SMTExprRef NewRHS = RHS; doTypeConversion(NewLHS, NewRHS, LTy, RTy); // Update the return type parameter if the output type has changed. if (RetTy) { @@ -1452,19 +1474,19 @@ Z3Expr Z3ConstraintManager::getZ3BinExpr LTy->isSignedIntegerOrEnumerationType()); } -Z3Expr Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym, - const llvm::APSInt &From, - const llvm::APSInt &To, - bool InRange) { +SMTExprRef Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym, + const llvm::APSInt &From, + const llvm::APSInt &To, + bool InRange) { // Convert lower bound QualType FromTy; llvm::APSInt NewFromInt; std::tie(NewFromInt, FromTy) = fixAPSInt(From); - Z3Expr FromExp = Solver.fromAPSInt(NewFromInt); + SMTExprRef FromExp = Solver.fromAPSInt(NewFromInt); // Convert symbol QualType SymTy; - Z3Expr Exp = getZ3Expr(Sym, &SymTy); + SMTExprRef Exp = getZ3Expr(Sym, &SymTy); // Construct single (in)equality if (From == To) @@ -1474,14 +1496,15 @@ Z3Expr Z3ConstraintManager::getZ3RangeEx QualType ToTy; llvm::APSInt NewToInt; std::tie(NewToInt, ToTy) = fixAPSInt(To); - Z3Expr ToExp = Solver.fromAPSInt(NewToInt); + SMTExprRef ToExp = Solver.fromAPSInt(NewToInt); assert(FromTy == ToTy && "Range values have different types!"); // Construct two (in)equalities, and a logical and/or - Z3Expr LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, - FromTy, /*RetTy=*/nullptr); - Z3Expr RHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, - /*RetTy=*/nullptr); + SMTExprRef LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, + FromTy, /*RetTy=*/nullptr); + SMTExprRef RHS = + getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, + /*RetTy=*/nullptr); return Solver.fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, SymTy->isSignedIntegerOrEnumerationType()); @@ -1512,7 +1535,7 @@ Z3ConstraintManager::fixAPSInt(const llv return std::make_pair(NewInt, getAPSIntType(NewInt)); } -void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, +void Z3ConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType <y, QualType &RTy) const { ASTContext &Ctx = getBasicVals().getContext(); @@ -1520,12 +1543,13 @@ void Z3ConstraintManager::doTypeConversi // Perform type conversion if (LTy->isIntegralOrEnumerationType() && RTy->isIntegralOrEnumerationType()) { - if (LTy->isArithmeticType() && RTy->isArithmeticType()) - return doIntTypeConversion<Z3Expr, &Z3Solver::fromCast>(LHS, LTy, RHS, - RTy); + if (LTy->isArithmeticType() && RTy->isArithmeticType()) { + doIntTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS, RTy); + return; + } } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { - return doFloatTypeConversion<Z3Expr, &Z3Solver::fromCast>(LHS, LTy, RHS, - RTy); + doFloatTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS, RTy); + return; } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) || (LTy->isBlockPointerType() || RTy->isBlockPointerType()) || (LTy->isReferenceType() || RTy->isReferenceType())) { @@ -1576,8 +1600,8 @@ void Z3ConstraintManager::doTypeConversi // TODO: Refine behavior for invalid type casts } -template <typename T, T (Z3Solver::*doCast)(const T &, QualType, uint64_t, - QualType, uint64_t)> +template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t, + QualType, uint64_t)> void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const { ASTContext &Ctx = getBasicVals().getContext(); @@ -1654,8 +1678,8 @@ void Z3ConstraintManager::doIntTypeConve } } -template <typename T, T (Z3Solver::*doCast)(const T &, QualType, uint64_t, - QualType, uint64_t)> +template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t, + QualType, uint64_t)> void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const { ASTContext &Ctx = getBasicVals().getContext(); _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
