Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h =================================================================== --- /dev/null +++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -0,0 +1,244 @@ +//== 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/SMTContext.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" + +namespace clang { +namespace ento { + +using SMTExprRef = std::shared_ptr; +using SMTSortRef = std::shared_ptr; + +class SMTSolver { +public: + SMTSolver() = default; + virtual ~SMTSolver() = default; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + + // 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; + + /// Given a constraint, add it to the solver + virtual void addConstraint(const SMTExprRef &Exp) = 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 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; +}; + +} // namespace ento +} // namespace clang + +#endif Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -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" @@ -49,7 +50,9 @@ namespace { class Z3Expr; +class Z3Sort; static const Z3Expr &toZ3Expr(const SMTExpr &E); +static const Z3Sort &toZ3Sort(const SMTSort &S); class Z3Config { friend class Z3Context; @@ -98,11 +101,11 @@ Z3_sort Sort; +public: Z3Sort(SMTContext &C, Z3_sort ZS) : SMTSort(C), Sort(ZS) { Z3_inc_ref(toZ3Context(Context).Context, reinterpret_cast(Sort)); } -public: /// Override implicit copy constructor for correct reference counting. Z3Sort(const Z3Sort &Copy) : SMTSort(Copy.Context), Sort(Copy.Sort) { Z3_inc_ref(toZ3Context(Context).Context, reinterpret_cast(Sort)); @@ -171,16 +174,20 @@ } }; // end class Z3Sort +static const Z3Sort &toZ3Sort(const SMTSort &S) { + return static_cast(S); +} + class Z3Expr : public SMTExpr { friend class Z3Solver; Z3_ast AST; +public: Z3Expr(SMTContext &C, Z3_ast ZA) : SMTExpr(C), AST(ZA) { Z3_inc_ref(toZ3Context(Context).Context, AST); } -public: /// Override implicit copy constructor for correct reference counting. Z3Expr(const Z3Expr &Copy) : SMTExpr(Copy.Context), AST(Copy.AST) { Z3_inc_ref(toZ3Context(Context).Context, AST); @@ -314,25 +321,27 @@ 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); } @@ -352,47 +361,37 @@ 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); + void addConstraint(const SMTExprRef &Exp) override { + Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); } - // Return a boolean sort. - Z3Sort getBoolSort() { - return Z3Sort(Context, Z3_mk_bool_sort(Context.Context)); + SMTSortRef getBoolSort() override { + return std::make_shared(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)); + SMTSortRef getBitvectorSort(unsigned BitWidth) override { + return std::make_shared(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; - + SMTSortRef getFloatSort(unsigned BitWidth) { switch (BitWidth) { - default: - llvm_unreachable("Unsupported floating-point bitwidth!"); - break; case 16: - Sort = Z3_mk_fpa_sort_16(Context.Context); - break; + return getFloat16Sort(); case 32: - Sort = Z3_mk_fpa_sort_32(Context.Context); - break; + return getFloat32Sort(); case 64: - Sort = Z3_mk_fpa_sort_64(Context.Context); - break; + return getFloat64Sort(); case 128: - Sort = Z3_mk_fpa_sort_128(Context.Context); - break; + return getFloat128Sort(); + default:; } - return Z3Sort(Context, Sort); + llvm_unreachable("Unsupported floating-point bitwidth!"); } // Return an appropriate sort, given a QualType - Z3Sort MkSort(const QualType &Ty, unsigned BitWidth) { + SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) { if (Ty->isBooleanType()) return getBoolSort(); @@ -402,9 +401,388 @@ return getBitvectorSort(BitWidth); } - // Return an appropriate sort for the given AST. - Z3Sort getSort(Z3_ast AST) { - return Z3Sort(Context, Z3_get_sort(Context.Context, AST)); + SMTSortRef getSort(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTSortRef getFloat16Sort() override { + return std::make_shared(Context, + Z3_mk_fpa_sort_16(Context.Context)); + } + + SMTSortRef getFloat32Sort() override { + return std::make_shared(Context, + Z3_mk_fpa_sort_32(Context.Context)); + } + + SMTSortRef getFloat64Sort() override { + return std::make_shared(Context, + Z3_mk_fpa_sort_64(Context.Context)); + } + + SMTSortRef getFloat128Sort() override { + return std::make_shared(Context, + Z3_mk_fpa_sort_128(Context.Context)); + } + + SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkBVNot(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkNot(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + 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 std::make_shared(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 std::make_shared(Context, + Z3_mk_or(Context.Context, 2, Args)); + } + + SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkFPNeg(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + SMTExprRef RoundingMode = getFloatRoundingMode(); + return std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + Context, + Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST, + toZ3Expr(*RoundingMode).AST)); + } + + SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + Context, + Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)); + } + + SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + 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 std::make_shared( + Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST, + toZ3Expr(*T).AST, toZ3Expr(*F).AST)); + } + + SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkExtract(unsigned High, unsigned Low, + const SMTExprRef &Exp) override { + return std::make_shared( + Context, Z3_mk_extract(Context.Context, High, Low, toZ3Expr(*Exp).AST)); + } + + SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override { + return std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + 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 std::make_shared( + Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, + toZ3Expr(*From).AST, ToWidth)); + } + + SMTExprRef mkBoolean(const bool b) override { + return std::make_shared(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 std::make_shared( + 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 std::make_shared( + Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, + toZ3Sort(*Sort).Sort)); + } + + SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override { + return std::make_shared( + 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; } /// Given a program state, construct the logical conjunction and add it to @@ -416,406 +794,325 @@ // Construct the logical AND of all the constraints if (I != IE) { - std::vector ASTs; + std::vector ASTs; while (I != IE) - ASTs.push_back(I++->second.AST); + ASTs.push_back(std::make_shared(I++->second)); - Z3Expr Conj = fromNBinOp(BO_LAnd, ASTs); - addConstraint(Conj); + addConstraint(fromNBinOp(BO_LAnd, ASTs)); } } // Return an appropriate floating-point rounding mode. - Z3Expr getFloatRoundingMode() { + SMTExprRef getFloatRoundingMode() override { // TODO: Don't assume nearest ties to even rounding mode - return Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)); + return std::make_shared(Context, Z3_mk_fpa_rne(Context.Context)); } /// Construct a Z3Expr from a unary operator, given a Z3_context. - Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) { - Z3_ast AST; - + SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) { switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - case UO_Minus: - AST = Z3_mk_bvneg(Context.Context, Exp.AST); - break; + return mkBVNeg(Exp); case UO_Not: - AST = Z3_mk_bvnot(Context.Context, Exp.AST); - break; + return mkBVNot(Exp); case UO_LNot: - AST = Z3_mk_not(Context.Context, Exp.AST); - break; - } + return mkNot(Exp); - return Z3Expr(Context, AST); + default:; + } + llvm_unreachable("Unimplemented opcode"); } /// 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 fromFloatUnOp(const UnaryOperator::Opcode Op, + const SMTExprRef &Exp) { switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - case UO_Minus: - AST = Z3_mk_fpa_neg(Context.Context, Exp.AST); - break; + return mkFPNeg(Exp); case UO_LNot: return fromUnOp(Op, Exp); - } - return Z3Expr(Context, AST); + default:; + } + llvm_unreachable("Unimplemented opcode"); } /// Construct a Z3Expr from a n-ary binary operator. - Z3Expr fromNBinOp(const BinaryOperator::Opcode Op, - const std::vector &ASTs) { - Z3_ast AST; + SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op, + const std::vector &ASTs) { + assert(!ASTs.empty()); - switch (Op) { - default: + if (Op != BO_LAnd && Op != BO_LOr) 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; - } - - return Z3Expr(Context, AST); + SMTExprRef res = ASTs.front(); + for (std::size_t i = 0; 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. - 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!"); + 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) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - - // Multiplicative operators + // Multiplicative operators case BO_Mul: - AST = Z3_mk_bvmul(Context.Context, LHS.AST, RHS.AST); - break; + return mkBVMul(LHS, RHS); + case BO_Div: - AST = isSigned ? Z3_mk_bvsdiv(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvudiv(Context.Context, LHS.AST, RHS.AST); - break; + return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS); + case BO_Rem: - AST = isSigned ? Z3_mk_bvsrem(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvurem(Context.Context, LHS.AST, RHS.AST); - break; + return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS); // Additive operators case BO_Add: - AST = Z3_mk_bvadd(Context.Context, LHS.AST, RHS.AST); - break; + return mkBVAdd(LHS, RHS); + case BO_Sub: - AST = Z3_mk_bvsub(Context.Context, LHS.AST, RHS.AST); - break; + return mkBVSub(LHS, RHS); // Bitwise shift operators case BO_Shl: - AST = Z3_mk_bvshl(Context.Context, LHS.AST, RHS.AST); - break; + return mkBVShl(LHS, RHS); + case BO_Shr: - AST = isSigned ? Z3_mk_bvashr(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvlshr(Context.Context, LHS.AST, RHS.AST); - break; + return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS); // 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; + return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS); + case BO_GT: - AST = isSigned ? Z3_mk_bvsgt(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvugt(Context.Context, LHS.AST, RHS.AST); - break; + return isSigned ? mkBVSgt(LHS, RHS) : mkBVUgt(LHS, RHS); + case BO_LE: - AST = isSigned ? Z3_mk_bvsle(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvule(Context.Context, LHS.AST, RHS.AST); - break; + return isSigned ? mkBVSle(LHS, RHS) : mkBVUle(LHS, RHS); + case BO_GE: - AST = isSigned ? Z3_mk_bvsge(Context.Context, LHS.AST, RHS.AST) - : Z3_mk_bvuge(Context.Context, LHS.AST, RHS.AST); - break; + return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS); // Equality operators case BO_EQ: - AST = Z3_mk_eq(Context.Context, LHS.AST, RHS.AST); - break; + return mkEqual(LHS, RHS); + 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; + return mkBVAnd(LHS, RHS); + case BO_Xor: - AST = Z3_mk_bvxor(Context.Context, LHS.AST, RHS.AST); - break; + return mkBVXor(LHS, RHS); + case BO_Or: - AST = Z3_mk_bvor(Context.Context, LHS.AST, RHS.AST); - break; + return mkBVOr(LHS, RHS); // Logical operators case BO_LAnd: - case BO_LOr: { - std::vector Args = {LHS.AST, RHS.AST}; - return fromNBinOp(Op, Args); - } - } + return mkAnd(LHS, RHS); - return Z3Expr(Context, AST); + 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. - Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS, - const BinaryOperator::Opcode Op, - const llvm::APFloat::fltCategory &RHS) { - Z3_ast AST; - + SMTExprRef fromFloatSpecialBinOp(const SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const llvm::APFloat::fltCategory &RHS) { switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; - - // Equality operators + // Equality operators case BO_EQ: switch (RHS) { case llvm::APFloat::fcInfinity: - AST = Z3_mk_fpa_is_infinite(Context.Context, LHS.AST); - break; + return mkFPIsInfinite(LHS); + case llvm::APFloat::fcNaN: - AST = Z3_mk_fpa_is_nan(Context.Context, LHS.AST); - break; + return mkFPIsNaN(LHS); + case llvm::APFloat::fcNormal: - AST = Z3_mk_fpa_is_normal(Context.Context, LHS.AST); - break; + return mkFPIsNormal(LHS); + case llvm::APFloat::fcZero: - AST = Z3_mk_fpa_is_zero(Context.Context, LHS.AST); - break; + return mkFPIsZero(LHS); } break; + case BO_NE: return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS)); - break; + + default:; } - return Z3Expr(Context, AST); + llvm_unreachable("Unimplemented opcode"); } /// 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!"); + 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) { - default: - llvm_unreachable("Unimplemented opcode"); - break; + // Multiplicative operators + case BO_Mul: + return mkFPMul(LHS, RHS); + + case BO_Div: + return mkFPDiv(LHS, RHS); - // 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; + return mkFPRem(LHS, RHS); // 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; - } + case BO_Add: + return mkFPAdd(LHS, RHS); + + case BO_Sub: + return mkFPSub(LHS, RHS); // Relational operators case BO_LT: - AST = Z3_mk_fpa_lt(Context.Context, LHS.AST, RHS.AST); - break; + return mkFPLt(LHS, RHS); + case BO_GT: - AST = Z3_mk_fpa_gt(Context.Context, LHS.AST, RHS.AST); - break; + return mkFPGt(LHS, RHS); + case BO_LE: - AST = Z3_mk_fpa_leq(Context.Context, LHS.AST, RHS.AST); - break; + return mkFPLe(LHS, RHS); + case BO_GE: - AST = Z3_mk_fpa_geq(Context.Context, LHS.AST, RHS.AST); - break; + return mkFPGe(LHS, RHS); // Equality operators case BO_EQ: - AST = Z3_mk_fpa_eq(Context.Context, LHS.AST, RHS.AST); - break; + return mkFPEqual(LHS, RHS); + 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); + + default:; } - return Z3Expr(Context, AST); + llvm_unreachable("Unimplemented opcode"); } /// Construct a Z3Expr from a SymbolData, given a Z3_context. - Z3Expr fromData(const SymbolID ID, const QualType &Ty, uint64_t BitWidth) { + SMTExprRef fromData(const SymbolID ID, const QualType &Ty, + uint64_t BitWidth) override { llvm::Twine Name = "$" + llvm::Twine(ID); - - Z3Sort Sort = MkSort(Ty, BitWidth); - - 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); + return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth)); } /// 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; - + 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())) { - // 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; + return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth), + mkBitvector(llvm::APSInt("0"), ToBitWidth)); } - } 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!"); + + 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); } - return Z3Expr(Context, AST); + if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) + return ToTy->isSignedIntegerOrEnumerationType() + ? mkSBVtoFP(Exp, ToBitWidth) + : mkUBVtoFP(Exp, ToBitWidth); + + llvm_unreachable("Unsupported explicit type cast!"); } /// Construct a Z3Expr from a boolean, given a Z3_context. - Z3Expr fromBoolean(const bool Bool) { + SMTExprRef fromBoolean(const bool Bool) { Z3_ast AST = Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context); - return Z3Expr(Context, AST); + return std::make_shared(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) { + 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 std::make_shared( + 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) { + SMTSortRef Sort = getBitvectorSort(Int.getBitWidth()); + Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(), + toZ3Sort(*Sort).Sort); + return std::make_shared(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) { + SMTSortRef Sort = getBitvectorSort(BitWidth); + Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort); + return std::make_shared(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; } @@ -829,11 +1126,10 @@ 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; } @@ -842,15 +1138,14 @@ // 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()); @@ -861,17 +1156,14 @@ 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; } @@ -880,31 +1172,31 @@ /// 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 = std::make_shared( + 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 = std::make_shared( + Context, Z3_model_get_const_interp(Context.Context, Model.Model, Func)); + SMTSortRef Sort = getSort(Assign); return toAPFloat(Sort, Assign, Float, true); } @@ -917,13 +1209,22 @@ } /// 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); } @@ -935,13 +1236,11 @@ } /// 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 { @@ -1000,52 +1299,54 @@ // 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. @@ -1061,7 +1362,7 @@ // 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. @@ -1087,7 +1388,7 @@ 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)); @@ -1155,27 +1456,29 @@ 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); 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 @@ -1193,29 +1496,31 @@ 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); // 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 @@ -1282,9 +1587,9 @@ 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 @@ -1297,10 +1602,7 @@ } 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(); } @@ -1311,24 +1613,25 @@ 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(std::make_pair(Sym, Exp)); + if (checkZ3Model(State, Exp).isConstrainedTrue()) + return State->add(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); 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; } @@ -1336,12 +1639,13 @@ 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)); @@ -1360,8 +1664,8 @@ 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(Sym)) { if (RetTy) *RetTy = Sym->getType(); @@ -1372,7 +1676,7 @@ *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) @@ -1380,7 +1684,7 @@ *hasComparison = false; return getZ3CastExpr(Exp, FromTy, Sym->getType()); } else if (const BinarySymExpr *BSE = dyn_cast(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()); @@ -1390,52 +1694,52 @@ 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(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(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(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) { @@ -1462,19 +1766,19 @@ 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) @@ -1484,14 +1788,15 @@ 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()); @@ -1522,7 +1827,7 @@ 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(); @@ -1531,11 +1836,11 @@ if (LTy->isIntegralOrEnumerationType() && RTy->isIntegralOrEnumerationType()) { if (LTy->isArithmeticType() && RTy->isArithmeticType()) - return doIntTypeConversion(LHS, LTy, RHS, - RTy); + return doIntTypeConversion(LHS, LTy, RHS, + RTy); } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { - return doFloatTypeConversion(LHS, LTy, RHS, - RTy); + return doFloatTypeConversion(LHS, LTy, RHS, + RTy); } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) || (LTy->isBlockPointerType() || RTy->isBlockPointerType()) || (LTy->isReferenceType() || RTy->isReferenceType())) {