Index: include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h =================================================================== --- /dev/null +++ include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h @@ -0,0 +1,408 @@ +//== Z3ConstraintManager.h -------------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_Z3CONSTRAINTMANAGER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_Z3CONSTRAINTMANAGER_H + +#include "clang/Basic/TargetInfo.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" + +#include "clang/Config/config.h" + +#if CLANG_ANALYZER_WITH_Z3 + +#include + +class Z3Config { + friend class Z3Context; + + Z3_config Config; + +public: + Z3Config(); + ~Z3Config(); +}; // end class Z3Config + +class Z3Context { + Z3_context ZC_P; + +public: + static Z3_context ZC; + + Z3Context(); + ~Z3Context(); +}; // end class Z3Context + +class Z3Sort { + friend class Z3Expr; + + Z3_sort Sort; + + Z3Sort(); + Z3Sort(Z3_sort ZS); + +public: + /// Override implicit copy constructor for correct reference counting. + Z3Sort(const Z3Sort &Copy); + + /// Provide move constructor + Z3Sort(Z3Sort &&Move); + + /// Provide move assignment constructor + Z3Sort &operator=(Z3Sort &&Move); + + ~Z3Sort(); + + // Return a boolean sort. + static Z3Sort getBoolSort(); + + // Return an appropriate bitvector sort for the given bitwidth. + static Z3Sort getBitvectorSort(unsigned BitWidth); + + // Return an appropriate floating-point sort for the given bitwidth. + static Z3Sort getFloatSort(unsigned BitWidth); + + // Return an appropriate sort for the given AST. + static Z3Sort getSort(Z3_ast AST); + + Z3_sort_kind getSortKind() const; + + unsigned getBitvectorSortSize() const; + + unsigned getFloatSortSize() const; + + bool operator==(const Z3Sort &Other) const; + + Z3Sort &operator=(const Z3Sort &Move); + + void print(llvm::raw_ostream &OS) const; + + LLVM_DUMP_METHOD void dump() const; +}; // end class Z3Sort + +class Z3Expr { + friend class Z3Model; + friend class Z3Solver; + + Z3_ast AST; + + Z3Expr(Z3_ast ZA); + + // Return an appropriate floating-point rounding mode. + static Z3Expr getFloatRoundingMode(); + + // Determine whether two float semantics are equivalent + static bool areEquivalent(const llvm::fltSemantics &LHS, + const llvm::fltSemantics &RHS); + +public: + /// Override implicit copy constructor for correct reference counting. + Z3Expr(const Z3Expr &Copy); + + /// Provide move constructor + Z3Expr(Z3Expr &&Move); + + /// Provide move assignment constructor + Z3Expr &operator=(Z3Expr &&Move); + + ~Z3Expr(); + + /// Get the corresponding IEEE floating-point type for a given bitwidth. + static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth); + + /// Construct a Z3Expr from a unary operator, given a Z3_context. + static Z3Expr fromUnOp(const clang::UnaryOperator::Opcode Op, + const Z3Expr &Exp); + + /// Construct a Z3Expr from a floating-point unary operator, given a + /// Z3_context. + static Z3Expr fromFloatUnOp(const clang::UnaryOperator::Opcode Op, + const Z3Expr &Exp); + + /// Construct a Z3Expr from a n-ary binary operator. + static Z3Expr fromNBinOp(const clang::BinaryOperator::Opcode Op, + const std::vector &ASTs); + + /// Construct a Z3Expr from a binary operator, given a Z3_context. + static Z3Expr fromBinOp(const Z3Expr &LHS, + const clang::BinaryOperator::Opcode Op, + const Z3Expr &RHS, bool isSigned); + + /// Construct a Z3Expr from a special floating-point binary operator, given + /// a Z3_context. + static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS, + const clang::BinaryOperator::Opcode Op, + const llvm::APFloat::fltCategory &RHS); + + /// Construct a Z3Expr from a floating-point binary operator, given a + /// Z3_context. + static Z3Expr fromFloatBinOp(const Z3Expr &LHS, + const clang::BinaryOperator::Opcode Op, + const Z3Expr &RHS); + + /// Construct a Z3Expr from a SymbolData, given a Z3_context. + static Z3Expr fromData(const clang::ento::SymbolID ID, bool isBool, + bool isFloat, uint64_t BitWidth); + + /// Construct a Z3Expr from a SymbolCast, given a Z3_context. + static Z3Expr fromCast(const Z3Expr &Exp, clang::QualType ToTy, + uint64_t ToBitWidth, clang::QualType FromTy, + uint64_t FromBitWidth); + + /// Construct a Z3Expr from a boolean, given a Z3_context. + static Z3Expr fromBoolean(const bool Bool); + + /// Construct a Z3Expr from a finite APFloat, given a Z3_context. + static Z3Expr fromAPFloat(const llvm::APFloat &Float); + + /// Construct a Z3Expr from an APSInt, given a Z3_context. + static Z3Expr fromAPSInt(const llvm::APSInt &Int); + + /// Construct a Z3Expr from an integer, given a Z3_context. + static Z3Expr fromInt(const char *Int, uint64_t BitWidth); + + /// Construct an APFloat from a Z3Expr, given the AST representation + static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, + llvm::APFloat &Float, bool useSemantics = true); + + /// Construct an APSInt from a Z3Expr, given the AST representation + static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int, + bool useSemantics = true); + + void Profile(llvm::FoldingSetNodeID &ID) const; + + bool operator<(const Z3Expr &Other) const; + + /// Comparison of AST equality, not model equivalence. + bool operator==(const Z3Expr &Other) const; + + /// Override implicit move constructor for correct reference counting. + Z3Expr &operator=(const Z3Expr &Move); + + void print(llvm::raw_ostream &OS) const; + + LLVM_DUMP_METHOD void dump() const; +}; // end class Z3Expr + +class Z3Model { + Z3_model Model; + +public: + Z3Model(Z3_model ZM); + + /// Override implicit copy constructor for correct reference counting. + Z3Model(const Z3Model &Copy); + + /// Provide move constructor + Z3Model(Z3Model &&Move); + + /// Provide move assignment constructor + Z3Model &operator=(Z3Model &&Move); + + ~Z3Model(); + + /// Given an expression, extract the value of this operand in the model. + bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const; + + /// Given an expression, extract the value of this operand in the model. + bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const; + + void print(llvm::raw_ostream &OS) const; + + LLVM_DUMP_METHOD void dump() const; +}; // end class Z3Model + +class Z3Solver { + friend class Z3ConstraintManager; + + Z3_solver Solver; + + Z3Solver(Z3_solver ZS); + +public: + /// Override implicit copy constructor for correct reference counting. + Z3Solver(const Z3Solver &Copy); + + /// Provide move constructor + Z3Solver(Z3Solver &&Move); + + /// Provide move assignment constructor + Z3Solver &operator=(Z3Solver &&Move); + + ~Z3Solver(); + + /// Given a constraint, add it to the solver + void addConstraint(const Z3Expr &Exp); + + /// Given a program state, construct the logical conjunction and add it to + /// the solver + void addStateConstraints(clang::ento::ProgramStateRef State); + + /// Check if the constraints are satisfiable + Z3_lbool check(); + + /// Push the current solver state + void push(); + + /// Pop the previous solver state + void pop(unsigned NumStates = 1); + + /// Get a model from the solver. Caller should check the model is + /// satisfiable. + Z3Model getModel(); + + /// Reset the solver and remove all constraints. + void reset(); + + void print(llvm::raw_ostream &OS) const; + + LLVM_DUMP_METHOD void dump() const; +}; // end class Z3Solver + +class Z3ConstraintManager : public clang::ento::SimpleConstraintManager { + Z3Context Context; + mutable Z3Solver Solver; + +public: + Z3ConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB); + + //===------------------------------------------------------------------===// + // Implementation for interface from ConstraintManager. + //===------------------------------------------------------------------===// + + bool canReasonAbout(clang::ento::SVal X) const override; + + clang::ento::ConditionTruthVal checkNull(clang::ento::ProgramStateRef State, + clang::ento::SymbolRef Sym) override; + + const llvm::APSInt *getSymVal(clang::ento::ProgramStateRef State, + clang::ento::SymbolRef Sym) const override; + + clang::ento::ProgramStateRef + removeDeadBindings(clang::ento::ProgramStateRef St, + clang::ento::SymbolReaper &SymReaper) override; + + void print(clang::ento::ProgramStateRef St, llvm::raw_ostream &Out, + const char *nl, const char *sep) override; + + //===------------------------------------------------------------------===// + // Implementation for interface from SimpleConstraintManager. + //===------------------------------------------------------------------===// + + clang::ento::ProgramStateRef assumeSym(clang::ento::ProgramStateRef state, + clang::ento::SymbolRef Sym, + bool Assumption) override; + + clang::ento::ProgramStateRef + assumeSymInclusiveRange(clang::ento::ProgramStateRef State, + clang::ento::SymbolRef Sym, const llvm::APSInt &From, + const llvm::APSInt &To, bool InRange) override; + + clang::ento::ProgramStateRef + assumeSymUnsupported(clang::ento::ProgramStateRef State, + clang::ento::SymbolRef Sym, bool Assumption) override; + +private: + //===------------------------------------------------------------------===// + // Internal implementation. + //===------------------------------------------------------------------===// + + // Check whether a new model is satisfiable, and update the program state. + clang::ento::ProgramStateRef assumeZ3Expr(clang::ento::ProgramStateRef State, + clang::ento::SymbolRef Sym, + const Z3Expr &Exp); + + // Generate and check a Z3 model, using the given constraint. + Z3_lbool checkZ3Model(clang::ento::ProgramStateRef State, + const Z3Expr &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(clang::ento::SymbolRef Sym, clang::QualType *RetTy = nullptr, + bool *hasComparison = nullptr) const; + + // Generate a Z3Expr that takes the logical not of an expression. + Z3Expr getZ3NotExpr(const Z3Expr &Exp) const; + + // Generate a Z3Expr that compares the expression to zero. + Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, clang::QualType RetTy, + bool Assumption) const; + + // Recursive implementation to unpack and generate symbolic expression. + // Sets the hasComparison and RetTy parameters. See getZ3Expr(). + Z3Expr getZ3SymExpr(clang::ento::SymbolRef Sym, clang::QualType *RetTy, + bool *hasComparison) const; + + // Wrapper to generate Z3Expr from SymbolData. + Z3Expr getZ3DataExpr(const clang::ento::SymbolID ID, + clang::QualType Ty) const; + + // Wrapper to generate Z3Expr from SymbolCast. + Z3Expr getZ3CastExpr(const Z3Expr &Exp, clang::QualType FromTy, + clang::QualType Ty) const; + + // Wrapper to generate Z3Expr from BinarySymExpr. + // Sets the hasComparison and RetTy parameters. See getZ3Expr(). + Z3Expr getZ3SymBinExpr(const clang::ento::BinarySymExpr *BSE, + bool *hasComparison, clang::QualType *RetTy) const; + + // Wrapper to generate Z3Expr from unpacked binary symbolic expression. + // Sets the RetTy parameter. See getZ3Expr(). + Z3Expr getZ3BinExpr(const Z3Expr &LHS, clang::QualType LTy, + clang::BinaryOperator::Opcode Op, const Z3Expr &RHS, + clang::QualType RTy, clang::QualType *RetTy) const; + + //===------------------------------------------------------------------===// + // Helper functions. + //===------------------------------------------------------------------===// + + // Recover the QualType of an APSInt. + // TODO: Refactor to put elsewhere + clang::QualType getAPSIntType(const llvm::APSInt &Int) const; + + // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1. + std::pair + fixAPSInt(const llvm::APSInt &Int) const; + + // 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, clang::QualType <y, + clang::QualType &RTy) const; + + // Perform implicit integer type conversion. + // May modify all input parameters. + // TODO: Refactor to use Sema::handleIntegerConversion() + template + void doIntTypeConversion(T &LHS, clang::QualType <y, T &RHS, + clang::QualType &RTy) const; + + // Perform implicit floating-point type conversion. + // May modify all input parameters. + // TODO: Refactor to use Sema::handleFloatConversion() + template + void doFloatTypeConversion(T &LHS, clang::QualType <y, T &RHS, + clang::QualType &RTy) const; + + // Callback function for doCast parameter on APSInt type. + static llvm::APSInt castAPSInt(const llvm::APSInt &V, clang::QualType ToTy, + uint64_t ToWidth, clang::QualType FromTy, + uint64_t FromWidth); +}; // end class Z3ConstraintManager + +#endif + +#endif Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -12,10 +12,10 @@ // //===----------------------------------------------------------------------===// -#include "RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/ImmutableSet.h" #include "llvm/Support/raw_ostream.h" Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp +++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -12,8 +12,8 @@ // //===----------------------------------------------------------------------===// -#include "RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" namespace clang { Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -11,1016 +11,789 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" - -#include "clang/Config/config.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h" using namespace clang; using namespace ento; #if CLANG_ANALYZER_WITH_Z3 -#include - -// Forward declarations -namespace { -class Z3Expr; -class ConstraintZ3 {}; -} // end anonymous namespace - typedef llvm::ImmutableSet> ConstraintZ3Ty; +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty) + +Z3Config::Z3Config() : Config(Z3_mk_config()) { + // Enable model finding + Z3_set_param_value(Config, "model", "true"); + // Disable proof generation + Z3_set_param_value(Config, "proof", "false"); + // Set timeout to 15000ms = 15s + Z3_set_param_value(Config, "timeout", "15000"); +} -// Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair) -namespace clang { -namespace ento { -template <> -struct ProgramStateTrait - : public ProgramStatePartialTrait { - static void *GDMIndex() { - static int Index; - return &Index; - } -}; -} // end namespace ento -} // end namespace clang - -namespace { - -class Z3Config { - friend class Z3Context; - - Z3_config Config; - -public: - Z3Config() : Config(Z3_mk_config()) { - // Enable model finding - Z3_set_param_value(Config, "model", "true"); - // Disable proof generation - Z3_set_param_value(Config, "proof", "false"); - // Set timeout to 15000ms = 15s - Z3_set_param_value(Config, "timeout", "15000"); - } - - ~Z3Config() { Z3_del_config(Config); } -}; // end class Z3Config - -class Z3Context { - Z3_context ZC_P; - -public: - static Z3_context ZC; - - Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; } - - ~Z3Context() { - Z3_del_context(ZC); - Z3_finalize_memory(); - ZC_P = nullptr; - } -}; // end class Z3Context +Z3Config::~Z3Config() { Z3_del_config(Config); } -class Z3Sort { - friend class Z3Expr; +Z3Context::Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { + ZC = ZC_P; +} - Z3_sort Sort; +Z3Context::~Z3Context() { + Z3_del_context(ZC); + Z3_finalize_memory(); + ZC_P = nullptr; +} - Z3Sort() : Sort(nullptr) {} - Z3Sort(Z3_sort ZS) : Sort(ZS) { - Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); - } +Z3Sort::Z3Sort() : Sort(nullptr) {} -public: - /// Override implicit copy constructor for correct reference counting. - Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) { - Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); - } +Z3Sort::Z3Sort(Z3_sort ZS) : Sort(ZS) { + Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); +} - /// Provide move constructor - Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); } +Z3Sort::Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) { + Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); +} - /// Provide move assignment constructor - Z3Sort &operator=(Z3Sort &&Move) { - if (this != &Move) { - if (Sort) - Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); - Sort = Move.Sort; - Move.Sort = nullptr; - } - return *this; - } +Z3Sort::Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); } - ~Z3Sort() { +Z3Sort &Z3Sort::operator=(Z3Sort &&Move) { + if (this != &Move) { if (Sort) Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); + Sort = Move.Sort; + Move.Sort = nullptr; } + return *this; +} - // Return a boolean sort. - static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); } - - // Return an appropriate bitvector sort for the given bitwidth. - static Z3Sort getBitvectorSort(unsigned BitWidth) { - return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth)); - } - - // Return an appropriate floating-point sort for the given bitwidth. - static Z3Sort getFloatSort(unsigned BitWidth) { - Z3_sort Sort; +Z3Sort::~Z3Sort() { + if (Sort) + Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); +} - switch (BitWidth) { - default: - llvm_unreachable("Unsupported floating-point bitwidth!"); - break; - case 16: - Sort = Z3_mk_fpa_sort_16(Z3Context::ZC); - break; - case 32: - Sort = Z3_mk_fpa_sort_32(Z3Context::ZC); - break; - case 64: - Sort = Z3_mk_fpa_sort_64(Z3Context::ZC); - break; - case 128: - Sort = Z3_mk_fpa_sort_128(Z3Context::ZC); - break; - } - return Z3Sort(Sort); - } +Z3Sort Z3Sort::getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); } - // Return an appropriate sort for the given AST. - static Z3Sort getSort(Z3_ast AST) { - return Z3Sort(Z3_get_sort(Z3Context::ZC, AST)); - } +Z3Sort Z3Sort::getBitvectorSort(unsigned BitWidth) { + return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth)); +} - Z3_sort_kind getSortKind() const { - return Z3_get_sort_kind(Z3Context::ZC, Sort); - } +Z3Sort Z3Sort::getFloatSort(unsigned BitWidth) { + Z3_sort Sort; - unsigned getBitvectorSortSize() const { - assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!"); - return Z3_get_bv_sort_size(Z3Context::ZC, Sort); - } + switch (BitWidth) { + default: + llvm_unreachable("Unsupported floating-point bitwidth!"); + break; + case 16: + Sort = Z3_mk_fpa_sort_16(Z3Context::ZC); + break; + case 32: + Sort = Z3_mk_fpa_sort_32(Z3Context::ZC); + break; + case 64: + Sort = Z3_mk_fpa_sort_64(Z3Context::ZC); + break; + case 128: + Sort = Z3_mk_fpa_sort_128(Z3Context::ZC); + break; + } + return Z3Sort(Sort); +} - unsigned getFloatSortSize() const { - assert(getSortKind() == Z3_FLOATING_POINT_SORT && - "Not a floating-point sort!"); - return Z3_fpa_get_ebits(Z3Context::ZC, Sort) + - Z3_fpa_get_sbits(Z3Context::ZC, Sort); - } +Z3Sort Z3Sort::getSort(Z3_ast AST) { + return Z3Sort(Z3_get_sort(Z3Context::ZC, AST)); +} - bool operator==(const Z3Sort &Other) const { - return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort); - } +Z3_sort_kind Z3Sort::getSortKind() const { + return Z3_get_sort_kind(Z3Context::ZC, Sort); +} - Z3Sort &operator=(const Z3Sort &Move) { - Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Move.Sort)); - Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); - Sort = Move.Sort; - return *this; - } +unsigned Z3Sort::getBitvectorSortSize() const { + assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!"); + return Z3_get_bv_sort_size(Z3Context::ZC, Sort); +} - void print(raw_ostream &OS) const { - OS << Z3_sort_to_string(Z3Context::ZC, Sort); - } +unsigned Z3Sort::getFloatSortSize() const { + assert(getSortKind() == Z3_FLOATING_POINT_SORT && + "Not a floating-point sort!"); + return Z3_fpa_get_ebits(Z3Context::ZC, Sort) + + Z3_fpa_get_sbits(Z3Context::ZC, Sort); +} - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } -}; // end class Z3Sort +bool Z3Sort::operator==(const Z3Sort &Other) const { + return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort); +} -class Z3Expr { - friend class Z3Model; - friend class Z3Solver; +Z3Sort &Z3Sort::operator=(const Z3Sort &Move) { + Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Move.Sort)); + Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); + Sort = Move.Sort; + return *this; +} - Z3_ast AST; +void Z3Sort::print(raw_ostream &OS) const { + OS << Z3_sort_to_string(Z3Context::ZC, Sort); +} - Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); } +LLVM_DUMP_METHOD void Z3Sort::dump() const { print(llvm::errs()); } - // Return an appropriate floating-point rounding mode. - static Z3Expr getFloatRoundingMode() { - // TODO: Don't assume nearest ties to even rounding mode - return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC)); - } +Z3Expr::Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); } - // Determine whether two float semantics are equivalent - static bool areEquivalent(const llvm::fltSemantics &LHS, - const llvm::fltSemantics &RHS) { - return (llvm::APFloat::semanticsPrecision(LHS) == - llvm::APFloat::semanticsPrecision(RHS)) && - (llvm::APFloat::semanticsMinExponent(LHS) == - llvm::APFloat::semanticsMinExponent(RHS)) && - (llvm::APFloat::semanticsMaxExponent(LHS) == - llvm::APFloat::semanticsMaxExponent(RHS)) && - (llvm::APFloat::semanticsSizeInBits(LHS) == - llvm::APFloat::semanticsSizeInBits(RHS)); - } +Z3Expr Z3Expr::getFloatRoundingMode() { + // TODO: Don't assume nearest ties to even rounding mode + return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC)); +} -public: - /// Override implicit copy constructor for correct reference counting. - Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); } +bool Z3Expr::areEquivalent(const llvm::fltSemantics &LHS, + const llvm::fltSemantics &RHS) { + return (llvm::APFloat::semanticsPrecision(LHS) == + llvm::APFloat::semanticsPrecision(RHS)) && + (llvm::APFloat::semanticsMinExponent(LHS) == + llvm::APFloat::semanticsMinExponent(RHS)) && + (llvm::APFloat::semanticsMaxExponent(LHS) == + llvm::APFloat::semanticsMaxExponent(RHS)) && + (llvm::APFloat::semanticsSizeInBits(LHS) == + llvm::APFloat::semanticsSizeInBits(RHS)); +} - /// Provide move constructor - Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); } +Z3Expr::Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { + Z3_inc_ref(Z3Context::ZC, AST); +} - /// Provide move assignment constructor - Z3Expr &operator=(Z3Expr &&Move) { - if (this != &Move) { - if (AST) - Z3_dec_ref(Z3Context::ZC, AST); - AST = Move.AST; - Move.AST = nullptr; - } - return *this; - } +Z3Expr::Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); } - ~Z3Expr() { +Z3Expr &Z3Expr::operator=(Z3Expr &&Move) { + if (this != &Move) { if (AST) Z3_dec_ref(Z3Context::ZC, AST); + AST = Move.AST; + Move.AST = nullptr; } + return *this; +} - /// Get the corresponding IEEE floating-point type for a given bitwidth. - static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) { - switch (BitWidth) { - default: - llvm_unreachable("Unsupported floating-point semantics!"); - break; - case 16: - return llvm::APFloat::IEEEhalf(); - case 32: - return llvm::APFloat::IEEEsingle(); - case 64: - return llvm::APFloat::IEEEdouble(); - case 128: - return llvm::APFloat::IEEEquad(); - } - } +Z3Expr::~Z3Expr() { + if (AST) + Z3_dec_ref(Z3Context::ZC, AST); +} - /// Construct a Z3Expr from a unary operator, given a Z3_context. - static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) { - Z3_ast AST; +const llvm::fltSemantics &Z3Expr::getFloatSemantics(unsigned BitWidth) { + switch (BitWidth) { + default: + llvm_unreachable("Unsupported floating-point semantics!"); + break; + case 16: + return llvm::APFloat::IEEEhalf(); + case 32: + return llvm::APFloat::IEEEsingle(); + case 64: + return llvm::APFloat::IEEEdouble(); + case 128: + return llvm::APFloat::IEEEquad(); + } +} - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; +Z3Expr Z3Expr::fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) { + Z3_ast AST; - case UO_Minus: - AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST); - break; + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; - case UO_Not: - AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST); - break; + case UO_Minus: + AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST); + break; - case UO_LNot: - AST = Z3_mk_not(Z3Context::ZC, Exp.AST); - break; - } + case UO_Not: + AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST); + break; - return Z3Expr(AST); + case UO_LNot: + AST = Z3_mk_not(Z3Context::ZC, Exp.AST); + break; } - /// Construct a Z3Expr from a floating-point unary operator, given a - /// Z3_context. - static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op, - const Z3Expr &Exp) { - Z3_ast AST; + return Z3Expr(AST); +} - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; +Z3Expr Z3Expr::fromFloatUnOp(const UnaryOperator::Opcode Op, + const Z3Expr &Exp) { + Z3_ast AST; - case UO_Minus: - AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST); - break; + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; - case UO_LNot: - return Z3Expr::fromUnOp(Op, Exp); - } + case UO_Minus: + AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST); + break; - return Z3Expr(AST); + case UO_LNot: + return Z3Expr::fromUnOp(Op, Exp); } - /// Construct a Z3Expr from a n-ary binary operator. - static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op, - const std::vector &ASTs) { - Z3_ast AST; + return Z3Expr(AST); +} - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; +Z3Expr Z3Expr::fromNBinOp(const BinaryOperator::Opcode Op, + const std::vector &ASTs) { + Z3_ast AST; - case BO_LAnd: - AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data()); - break; + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; - case BO_LOr: - AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data()); - break; - } + case BO_LAnd: + AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data()); + break; - return Z3Expr(AST); + case BO_LOr: + AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data()); + break; } - /// Construct a Z3Expr from a binary operator, given a Z3_context. - static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op, - const Z3Expr &RHS, bool isSigned) { - Z3_ast AST; - - assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) && - "AST's must have the same sort!"); - - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; + return Z3Expr(AST); +} - // Multiplicative operators - case BO_Mul: - AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_Div: - AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_Rem: - AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST); - break; +Z3Expr Z3Expr::fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op, + const Z3Expr &RHS, bool isSigned) { + Z3_ast AST; - // Additive operators - case BO_Add: - AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_Sub: - AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST); - break; + assert(Z3Sort::getSort(LHS.AST) == Z3Sort::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(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_Div: + AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_Rem: + AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Additive operators + case BO_Add: + AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_Sub: + AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Bitwise shift operators + case BO_Shl: + AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_Shr: + AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Relational operators + case BO_LT: + AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_GT: + AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_LE: + AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_GE: + AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST) + : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Equality operators + case BO_EQ: + AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_NE: + return Z3Expr::fromUnOp(UO_LNot, + Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned)); + break; + + // Bitwise operators + case BO_And: + AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_Xor: + AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_Or: + AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Logical operators + case BO_LAnd: + case BO_LOr: { + std::vector Args = {LHS.AST, RHS.AST}; + return Z3Expr::fromNBinOp(Op, Args); + } + } + + return Z3Expr(AST); +} - // Bitwise shift operators - case BO_Shl: - AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_Shr: - AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST); - break; +Z3Expr Z3Expr::fromFloatSpecialBinOp(const Z3Expr &LHS, + const BinaryOperator::Opcode Op, + const llvm::APFloat::fltCategory &RHS) { + Z3_ast AST; - // Relational operators - case BO_LT: - AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_GT: - AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_LE: - AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_GE: - AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST) - : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST); - break; + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; - // Equality operators - case BO_EQ: - AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_NE: - return Z3Expr::fromUnOp(UO_LNot, - Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned)); + // Equality operators + case BO_EQ: + switch (RHS) { + case llvm::APFloat::fcInfinity: + AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST); break; - - // Bitwise operators - case BO_And: - AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST); + case llvm::APFloat::fcNaN: + AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST); break; - case BO_Xor: - AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST); + case llvm::APFloat::fcNormal: + AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST); break; - case BO_Or: - AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST); + case llvm::APFloat::fcZero: + AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST); break; - - // Logical operators - case BO_LAnd: - case BO_LOr: { - std::vector Args = {LHS.AST, RHS.AST}; - return Z3Expr::fromNBinOp(Op, Args); } - } - - return Z3Expr(AST); + break; + case BO_NE: + return Z3Expr::fromFloatUnOp( + UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS)); + break; } - /// Construct a Z3Expr from a special floating-point binary operator, given - /// a Z3_context. - static 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(Z3Context::ZC, LHS.AST); - break; - case llvm::APFloat::fcNaN: - AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST); - break; - case llvm::APFloat::fcNormal: - AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST); - break; - case llvm::APFloat::fcZero: - AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST); - break; - } - break; - case BO_NE: - return Z3Expr::fromFloatUnOp( - UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS)); - break; - } - - return Z3Expr(AST); - } + return Z3Expr(AST); +} - /// Construct a Z3Expr from a floating-point binary operator, given a - /// Z3_context. - static Z3Expr fromFloatBinOp(const Z3Expr &LHS, - const BinaryOperator::Opcode Op, - const Z3Expr &RHS) { - Z3_ast AST; +Z3Expr Z3Expr::fromFloatBinOp(const Z3Expr &LHS, + const BinaryOperator::Opcode Op, + const Z3Expr &RHS) { + Z3_ast AST; - assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) && - "AST's must have the same sort!"); + assert(Z3Sort::getSort(LHS.AST) == Z3Sort::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 = Z3Expr::getFloatRoundingMode(); + AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); + break; + } + case BO_Div: { + Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); + AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); + break; + } + case BO_Rem: + AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Additive operators + case BO_Add: { + Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); + AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); + break; + } + case BO_Sub: { + Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); + AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); + break; + } + + // Relational operators + case BO_LT: + AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_GT: + AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_LE: + AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_GE: + AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST); + break; + + // Equality operators + case BO_EQ: + AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST); + break; + case BO_NE: + return Z3Expr::fromFloatUnOp(UO_LNot, + Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS)); + break; + + // Logical operators + case BO_LAnd: + case BO_LOr: + return Z3Expr::fromBinOp(LHS, Op, RHS, false); + } + + return Z3Expr(AST); +} - switch (Op) { - default: - llvm_unreachable("Unimplemented opcode"); - break; +Z3Expr Z3Expr::fromData(const SymbolID ID, bool isBool, bool isFloat, + uint64_t BitWidth) { + llvm::Twine Name = "$" + llvm::Twine(ID); + + Z3Sort Sort; + if (isBool) + Sort = Z3Sort::getBoolSort(); + else if (isFloat) + Sort = Z3Sort::getFloatSort(BitWidth); + else + Sort = Z3Sort::getBitvectorSort(BitWidth); + + Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str()); + Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort); + return Z3Expr(AST); +} - // Multiplicative operators - case BO_Mul: { - Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); - AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); - break; - } - case BO_Div: { - Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); - AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); - break; - } - case BO_Rem: - AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST); - break; +Z3Expr Z3Expr::fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth, + QualType FromTy, uint64_t FromBitWidth) { + Z3_ast AST; - // Additive operators - case BO_Add: { - Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); - AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); - break; + 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 = Z3Expr::fromInt("0", ToBitWidth); + Z3Expr One = Z3Expr::fromInt("1", ToBitWidth); + AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST); + } else if (ToBitWidth > FromBitWidth) { + AST = FromTy->isSignedIntegerOrEnumerationType() + ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth, + Exp.AST) + : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth, + Exp.AST); + } else if (ToBitWidth < FromBitWidth) { + AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST); + } else { + // Both are bitvectors with the same width, ignore the type cast + return Exp; } - case BO_Sub: { + } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) { + if (ToBitWidth != FromBitWidth) { Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); - AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST); - break; + Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth); + AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST, + Sort.Sort); + } else { + return Exp; } + } else if (FromTy->isIntegralOrEnumerationType() && + ToTy->isRealFloatingType()) { + Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); + Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth); + AST = FromTy->isSignedIntegerOrEnumerationType() + ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST, Exp.AST, + Sort.Sort) + : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST, + Exp.AST, Sort.Sort); + } else if (FromTy->isRealFloatingType() && + ToTy->isIntegralOrEnumerationType()) { + Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); + AST = ToTy->isSignedIntegerOrEnumerationType() + ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST, + ToBitWidth) + : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST, + ToBitWidth); + } else { + llvm_unreachable("Unsupported explicit type cast!"); + } - // Relational operators - case BO_LT: - AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_GT: - AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_LE: - AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_GE: - AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST); - break; - - // Equality operators - case BO_EQ: - AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST); - break; - case BO_NE: - return Z3Expr::fromFloatUnOp(UO_LNot, - Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS)); - break; - - // Logical operators - case BO_LAnd: - case BO_LOr: - return Z3Expr::fromBinOp(LHS, Op, RHS, false); - } + return Z3Expr(AST); +} - return Z3Expr(AST); - } +Z3Expr Z3Expr::fromBoolean(const bool Bool) { + Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC); + return Z3Expr(AST); +} - /// Construct a Z3Expr from a SymbolData, given a Z3_context. - static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat, - uint64_t BitWidth) { - llvm::Twine Name = "$" + llvm::Twine(ID); - - Z3Sort Sort; - if (isBool) - Sort = Z3Sort::getBoolSort(); - else if (isFloat) - Sort = Z3Sort::getFloatSort(BitWidth); - else - Sort = Z3Sort::getBitvectorSort(BitWidth); - - Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str()); - Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort); - return Z3Expr(AST); - } +Z3Expr Z3Expr::fromAPFloat(const llvm::APFloat &Float) { + Z3_ast AST; + Z3Sort Sort = Z3Sort::getFloatSort( + llvm::APFloat::semanticsSizeInBits(Float.getSemantics())); - /// Construct a Z3Expr from a SymbolCast, given a Z3_context. - static 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 = Z3Expr::fromInt("0", ToBitWidth); - Z3Expr One = Z3Expr::fromInt("1", ToBitWidth); - AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST); - } else if (ToBitWidth > FromBitWidth) { - AST = FromTy->isSignedIntegerOrEnumerationType() - ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth, - Exp.AST) - : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth, - Exp.AST); - } else if (ToBitWidth < FromBitWidth) { - AST = Z3_mk_extract(Z3Context::ZC, 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 = Z3Expr::getFloatRoundingMode(); - Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth); - AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST, - Sort.Sort); - } else { - return Exp; - } - } else if (FromTy->isIntegralOrEnumerationType() && - ToTy->isRealFloatingType()) { - Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); - Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth); - AST = FromTy->isSignedIntegerOrEnumerationType() - ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST, - Exp.AST, Sort.Sort) - : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST, - Exp.AST, Sort.Sort); - } else if (FromTy->isRealFloatingType() && - ToTy->isIntegralOrEnumerationType()) { - Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode(); - AST = ToTy->isSignedIntegerOrEnumerationType() - ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST, - ToBitWidth) - : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST, - ToBitWidth); - } else { - llvm_unreachable("Unsupported explicit type cast!"); - } + llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true); + Z3Expr Z3Int = Z3Expr::fromAPSInt(Int); + AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort); - return Z3Expr(AST); - } + return Z3Expr(AST); +} - /// Construct a Z3Expr from a boolean, given a Z3_context. - static Z3Expr fromBoolean(const bool Bool) { - Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC); - return Z3Expr(AST); - } +Z3Expr Z3Expr::fromAPSInt(const llvm::APSInt &Int) { + Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth()); + Z3_ast AST = + Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort); + return Z3Expr(AST); +} - /// Construct a Z3Expr from a finite APFloat, given a Z3_context. - static Z3Expr fromAPFloat(const llvm::APFloat &Float) { - Z3_ast AST; - Z3Sort Sort = Z3Sort::getFloatSort( - llvm::APFloat::semanticsSizeInBits(Float.getSemantics())); +Z3Expr Z3Expr::fromInt(const char *Int, uint64_t BitWidth) { + Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth); + Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort); + return Z3Expr(AST); +} - llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true); - Z3Expr Z3Int = Z3Expr::fromAPSInt(Int); - AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort); +bool Z3Expr::toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, + llvm::APFloat &Float, bool useSemantics) { + assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT && + "Unsupported sort to floating-point!"); - return Z3Expr(AST); + llvm::APSInt Int(Sort.getFloatSortSize(), true); + const llvm::fltSemantics &Semantics = + Z3Expr::getFloatSemantics(Sort.getFloatSortSize()); + Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize()); + if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) { + return false; } - /// Construct a Z3Expr from an APSInt, given a Z3_context. - static Z3Expr fromAPSInt(const llvm::APSInt &Int) { - Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth()); - Z3_ast AST = - Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort); - return Z3Expr(AST); + if (useSemantics && !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) { + assert(false && "Floating-point types don't match!"); + return false; } - /// Construct a Z3Expr from an integer, given a Z3_context. - static Z3Expr fromInt(const char *Int, uint64_t BitWidth) { - Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth); - Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort); - return Z3Expr(AST); - } + Float = llvm::APFloat(Semantics, Int); + return true; +} - /// Construct an APFloat from a Z3Expr, given the AST representation - static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, - llvm::APFloat &Float, bool useSemantics = true) { - assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT && - "Unsupported sort to floating-point!"); - - llvm::APSInt Int(Sort.getFloatSortSize(), true); - const llvm::fltSemantics &Semantics = - Z3Expr::getFloatSemantics(Sort.getFloatSortSize()); - Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize()); - if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) { +bool Z3Expr::toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int, + bool useSemantics) { + switch (Sort.getSortKind()) { + default: + llvm_unreachable("Unsupported sort to integer!"); + case Z3_BV_SORT: { + if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) { + assert(false && "Bitvector types don't match!"); return false; } - if (useSemantics && - !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) { - assert(false && "Floating-point types don't match!"); + uint64_t Value[2]; + // 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(Z3Context::ZC, AST, + reinterpret_cast<__uint64 *>(&Value[0])); + if (Sort.getBitvectorSortSize() <= 64) { + Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true); + } else if (Sort.getBitvectorSortSize() == 128) { + Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST)); + Z3_get_numeral_uint64(Z3Context::ZC, AST, + reinterpret_cast<__uint64 *>(&Value[1])); + Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true); + } else { + assert(false && "Bitwidth not supported!"); return false; } - - Float = llvm::APFloat(Semantics, Int); return true; } - - /// Construct an APSInt from a Z3Expr, given the AST representation - static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int, - bool useSemantics = true) { - switch (Sort.getSortKind()) { - default: - llvm_unreachable("Unsupported sort to integer!"); - case Z3_BV_SORT: { - if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) { - assert(false && "Bitvector types don't match!"); - return false; - } - - uint64_t Value[2]; - // 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(Z3Context::ZC, AST, - reinterpret_cast<__uint64 *>(&Value[0])); - if (Sort.getBitvectorSortSize() <= 64) { - Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true); - } else if (Sort.getBitvectorSortSize() == 128) { - Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST)); - Z3_get_numeral_uint64(Z3Context::ZC, AST, - reinterpret_cast<__uint64 *>(&Value[1])); - Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true); - } else { - assert(false && "Bitwidth not supported!"); - return false; - } - return true; - } - case Z3_BOOL_SORT: - 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(Z3Context::ZC, AST) == Z3_L_TRUE ? 1 - : 0), - true); - return true; + case Z3_BOOL_SORT: + 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(Z3Context::ZC, AST) == Z3_L_TRUE ? 1 : 0), + true); + return true; } +} - void Profile(llvm::FoldingSetNodeID &ID) const { - ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST)); - } - - bool operator<(const Z3Expr &Other) const { - llvm::FoldingSetNodeID ID1, ID2; - Profile(ID1); - Other.Profile(ID2); - return ID1 < ID2; - } - - /// Comparison of AST equality, not model equivalence. - bool operator==(const Z3Expr &Other) const { - assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST), - Z3_get_sort(Z3Context::ZC, Other.AST)) && - "AST's must have the same sort"); - return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST); - } +void Z3Expr::Profile(llvm::FoldingSetNodeID &ID) const { + ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST)); +} - /// Override implicit move constructor for correct reference counting. - Z3Expr &operator=(const Z3Expr &Move) { - Z3_inc_ref(Z3Context::ZC, Move.AST); - Z3_dec_ref(Z3Context::ZC, AST); - AST = Move.AST; - return *this; - } +bool Z3Expr::operator<(const Z3Expr &Other) const { + llvm::FoldingSetNodeID ID1, ID2; + Profile(ID1); + Other.Profile(ID2); + return ID1 < ID2; +} - void print(raw_ostream &OS) const { - OS << Z3_ast_to_string(Z3Context::ZC, AST); - } +bool Z3Expr::operator==(const Z3Expr &Other) const { + assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST), + Z3_get_sort(Z3Context::ZC, Other.AST)) && + "AST's must have the same sort"); + return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST); +} - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } -}; // end class Z3Expr +Z3Expr &Z3Expr::operator=(const Z3Expr &Move) { + Z3_inc_ref(Z3Context::ZC, Move.AST); + Z3_dec_ref(Z3Context::ZC, AST); + AST = Move.AST; + return *this; +} -class Z3Model { - Z3_model Model; +void Z3Expr::print(raw_ostream &OS) const { + OS << Z3_ast_to_string(Z3Context::ZC, AST); +} -public: - Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); } +LLVM_DUMP_METHOD void Z3Expr::dump() const { print(llvm::errs()); } - /// Override implicit copy constructor for correct reference counting. - Z3Model(const Z3Model &Copy) : Model(Copy.Model) { - Z3_model_inc_ref(Z3Context::ZC, Model); - } +Z3Model::Z3Model(Z3_model ZM) : Model(ZM) { + Z3_model_inc_ref(Z3Context::ZC, Model); +} - /// Provide move constructor - Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); } +Z3Model::Z3Model(const Z3Model &Copy) : Model(Copy.Model) { + Z3_model_inc_ref(Z3Context::ZC, Model); +} - /// Provide move assignment constructor - Z3Model &operator=(Z3Model &&Move) { - if (this != &Move) { - if (Model) - Z3_model_dec_ref(Z3Context::ZC, Model); - Model = Move.Model; - Move.Model = nullptr; - } - return *this; - } +Z3Model::Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); } - ~Z3Model() { +Z3Model &Z3Model::operator=(Z3Model &&Move) { + if (this != &Move) { if (Model) Z3_model_dec_ref(Z3Context::ZC, Model); + Model = Move.Model; + Move.Model = nullptr; } + return *this; +} - /// Given an expression, extract the value of this operand in the model. - bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const { - Z3_func_decl Func = - Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST)); - if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE) - return false; - - Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func); - Z3Sort Sort = Z3Sort::getSort(Assign); - return Z3Expr::toAPSInt(Sort, Assign, Int, true); - } - - /// Given an expression, extract the value of this operand in the model. - bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const { - Z3_func_decl Func = - Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST)); - if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE) - return false; +Z3Model::~Z3Model() { + if (Model) + Z3_model_dec_ref(Z3Context::ZC, Model); +} - Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func); - Z3Sort Sort = Z3Sort::getSort(Assign); - return Z3Expr::toAPFloat(Sort, Assign, Float, true); - } +bool Z3Model::getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const { + Z3_func_decl Func = + Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST)); + if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE) + return false; - void print(raw_ostream &OS) const { - OS << Z3_model_to_string(Z3Context::ZC, Model); - } + Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func); + Z3Sort Sort = Z3Sort::getSort(Assign); + return Z3Expr::toAPSInt(Sort, Assign, Int, true); +} - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } -}; // end class Z3Model +bool Z3Model::getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const { + Z3_func_decl Func = + Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST)); + if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE) + return false; -class Z3Solver { - friend class Z3ConstraintManager; + Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func); + Z3Sort Sort = Z3Sort::getSort(Assign); + return Z3Expr::toAPFloat(Sort, Assign, Float, true); +} - Z3_solver Solver; +void Z3Model::print(raw_ostream &OS) const { + OS << Z3_model_to_string(Z3Context::ZC, Model); +} - Z3Solver(Z3_solver ZS) : Solver(ZS) { - Z3_solver_inc_ref(Z3Context::ZC, Solver); - } +LLVM_DUMP_METHOD void Z3Model::dump() const { print(llvm::errs()); } -public: - /// Override implicit copy constructor for correct reference counting. - Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) { - Z3_solver_inc_ref(Z3Context::ZC, Solver); - } +Z3Solver::Z3Solver(Z3_solver ZS) : Solver(ZS) { + Z3_solver_inc_ref(Z3Context::ZC, Solver); +} - /// Provide move constructor - Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); } +Z3Solver::Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) { + Z3_solver_inc_ref(Z3Context::ZC, Solver); +} - /// Provide move assignment constructor - Z3Solver &operator=(Z3Solver &&Move) { - if (this != &Move) { - if (Solver) - Z3_solver_dec_ref(Z3Context::ZC, Solver); - Solver = Move.Solver; - Move.Solver = nullptr; - } - return *this; - } +Z3Solver::Z3Solver(Z3Solver &&Move) : Solver(nullptr) { + *this = std::move(Move); +} - ~Z3Solver() { +Z3Solver &Z3Solver::operator=(Z3Solver &&Move) { + if (this != &Move) { if (Solver) Z3_solver_dec_ref(Z3Context::ZC, Solver); + Solver = Move.Solver; + Move.Solver = nullptr; } + return *this; +} - /// Given a constraint, add it to the solver - void addConstraint(const Z3Expr &Exp) { - Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST); - } - - /// 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(); - ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end(); - - // Construct the logical AND of all the constraints - if (I != IE) { - std::vector ASTs; +Z3Solver::~Z3Solver() { + if (Solver) + Z3_solver_dec_ref(Z3Context::ZC, Solver); +} - while (I != IE) - ASTs.push_back(I++->second.AST); +void Z3Solver::addConstraint(const Z3Expr &Exp) { + Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST); +} - Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs); - addConstraint(Conj); - } - } +void Z3Solver::addStateConstraints(ProgramStateRef State) { + // TODO: Don't add all the constraints, only the relevant ones + ConstraintZ3Ty CZ = State->get(); + ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end(); - /// Check if the constraints are satisfiable - Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); } + // Construct the logical AND of all the constraints + if (I != IE) { + std::vector ASTs; - /// Push the current solver state - void push() { return Z3_solver_push(Z3Context::ZC, Solver); } + while (I != IE) + ASTs.push_back(I++->second.AST); - /// Pop the previous solver state - void pop(unsigned NumStates = 1) { - assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates); - return Z3_solver_pop(Z3Context::ZC, Solver, NumStates); + Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs); + addConstraint(Conj); } +} - /// Get a model from the solver. Caller should check the model is - /// satisfiable. - Z3Model getModel() { - return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver)); - } +Z3_lbool Z3Solver::check() { return Z3_solver_check(Z3Context::ZC, Solver); } - /// Reset the solver and remove all constraints. - void reset() { Z3_solver_reset(Z3Context::ZC, Solver); } -}; // end class Z3Solver +void Z3Solver::push() { return Z3_solver_push(Z3Context::ZC, Solver); } -void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { - llvm::report_fatal_error("Z3 error: " + - llvm::Twine(Z3_get_error_msg_ex(Context, Error))); +void Z3Solver::pop(unsigned NumStates) { + assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates); + return Z3_solver_pop(Z3Context::ZC, Solver, NumStates); } -class Z3ConstraintManager : public SimpleConstraintManager { - Z3Context Context; - mutable Z3Solver Solver; - -public: - Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) - : SimpleConstraintManager(SE, SB), - Solver(Z3_mk_simple_solver(Z3Context::ZC)) { - Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler); - } +Z3Model Z3Solver::getModel() { + return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver)); +} - //===------------------------------------------------------------------===// - // Implementation for interface from ConstraintManager. - //===------------------------------------------------------------------===// +void Z3Solver::reset() { Z3_solver_reset(Z3Context::ZC, Solver); } - bool canReasonAbout(SVal X) const override; +void Z3Solver::print(raw_ostream &OS) const { + OS << Z3_solver_to_string(Z3Context::ZC, Solver); +} - ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; +LLVM_DUMP_METHOD void Z3Solver::dump() const { print(llvm::errs()); } - const llvm::APSInt *getSymVal(ProgramStateRef State, - SymbolRef Sym) const override; - - ProgramStateRef removeDeadBindings(ProgramStateRef St, - SymbolReaper &SymReaper) override; +void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { + llvm::report_fatal_error("Z3 error: " + + llvm::Twine(Z3_get_error_msg_ex(Context, Error))); +} - void print(ProgramStateRef St, raw_ostream &Out, const char *nl, - const char *sep) override; - - //===------------------------------------------------------------------===// - // Implementation for interface from SimpleConstraintManager. - //===------------------------------------------------------------------===// - - ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym, - bool Assumption) override; - - ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &From, - const llvm::APSInt &To, - bool InRange) override; - - ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, - bool Assumption) override; - -private: - //===------------------------------------------------------------------===// - // Internal implementation. - //===------------------------------------------------------------------===// - - // Check whether a new model is satisfiable, and update the program state. - ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym, - const Z3Expr &Exp); - - // Generate and check a Z3 model, using the given constraint. - Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &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; - - // Generate a Z3Expr that takes the logical not of an expression. - Z3Expr getZ3NotExpr(const Z3Expr &Exp) const; - - // Generate a Z3Expr that compares the expression to zero. - Z3Expr getZ3ZeroExpr(const Z3Expr &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; - - // Wrapper to generate Z3Expr from SymbolData. - Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const; - - // Wrapper to generate Z3Expr from SymbolCast. - Z3Expr getZ3CastExpr(const Z3Expr &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; - - // 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; - - //===------------------------------------------------------------------===// - // Helper functions. - //===------------------------------------------------------------------===// - - // Recover the QualType of an APSInt. - // TODO: Refactor to put elsewhere - QualType getAPSIntType(const llvm::APSInt &Int) const; - - // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1. - std::pair fixAPSInt(const llvm::APSInt &Int) const; - - // 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, - QualType &RTy) const; - - // Perform implicit integer type conversion. - // May modify all input parameters. - // TODO: Refactor to use Sema::handleIntegerConversion() - template - 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 - void doFloatTypeConversion(T &LHS, QualType <y, T &RHS, - QualType &RTy) const; - - // Callback function for doCast parameter on APSInt type. - static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy, - uint64_t ToWidth, QualType FromTy, - uint64_t FromWidth); -}; // end class Z3ConstraintManager +Z3ConstraintManager::Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) + : SimpleConstraintManager(SE, SB), + Solver(Z3_mk_simple_solver(Z3Context::ZC)) { + Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler); +} Z3_context Z3Context::ZC; -} // end anonymous namespace - ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) { QualType RetTy; @@ -1388,8 +1161,8 @@ *RetTy = LTy; } - // If the two operands are pointers and the operation is a subtraction, the - // result is of type ptrdiff_t, which is signed + // If the two operands are pointers and the operation is a subtraction, + // the result is of type ptrdiff_t, which is signed if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) { ASTContext &Ctx = getBasicVals().getContext(); *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true); @@ -1464,8 +1237,9 @@ } // Cast the void pointer type to the non-void pointer type. - // For void types, this assumes that the casted value is equal to the value - // of the original pointer, and does not account for alignment requirements. + // For void types, this assumes that the casted value is equal to the + // value of the original pointer, and does not account for alignment + // requirements. if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) { assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) && "Pointer types have different bitwidths!"); @@ -1631,10 +1405,9 @@ OS << nl; } -#endif - -std::unique_ptr -ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { +std::unique_ptr +clang::ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, + SubEngine *Eng) { #if CLANG_ANALYZER_WITH_Z3 return llvm::make_unique(Eng, StMgr.getSValBuilder()); #else @@ -1644,3 +1417,5 @@ return nullptr; #endif } + +#endif