Index: cfe/trunk/CMakeLists.txt =================================================================== --- cfe/trunk/CMakeLists.txt +++ cfe/trunk/CMakeLists.txt @@ -186,6 +186,8 @@ set(CLANG_HAVE_LIBXML 1) endif() +find_package(Z3 4.5) + include(CheckIncludeFile) check_include_file(sys/resource.h CLANG_HAVE_RLIMITS) @@ -330,10 +332,6 @@ endif() endif() -configure_file( - ${CLANG_SOURCE_DIR}/include/clang/Config/config.h.cmake - ${CLANG_BINARY_DIR}/include/clang/Config/config.h) - include(CMakeParseArguments) include(AddClang) @@ -371,8 +369,19 @@ option(CLANG_ENABLE_ARCMT "Build ARCMT." ON) option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON) -if (NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT) - message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT") +option(CLANG_ANALYZER_BUILD_Z3 + "Build the static analyzer with the Z3 constraint manager." OFF) + +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_BUILD_Z3)) + message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") +endif() + +if(CLANG_ANALYZER_BUILD_Z3) + if(Z3_FOUND) + set(CLANG_ANALYZER_WITH_Z3 1) + else() + message(FATAL_ERROR "Cannot find Z3 header file or shared library") + endif() endif() if(CLANG_ENABLE_ARCMT) @@ -687,3 +696,7 @@ if (LLVM_ADD_NATIVE_VISUALIZERS_TO_SOLUTION) add_subdirectory(utils/ClangVisualizers) endif() + +configure_file( + ${CLANG_SOURCE_DIR}/include/clang/Config/config.h.cmake + ${CLANG_BINARY_DIR}/include/clang/Config/config.h) Index: cfe/trunk/cmake/modules/FindZ3.cmake =================================================================== --- cfe/trunk/cmake/modules/FindZ3.cmake +++ cfe/trunk/cmake/modules/FindZ3.cmake @@ -0,0 +1,28 @@ +find_path(Z3_INCLUDE_DIR NAMES z3.h + PATH_SUFFIXES libz3 + ) + +find_library(Z3_LIBRARIES NAMES z3 libz3 + ) + +find_program(Z3_EXECUTABLE z3) + +if(Z3_INCLUDE_DIR AND Z3_EXECUTABLE) + execute_process (COMMAND ${Z3_EXECUTABLE} -version + OUTPUT_VARIABLE libz3_version_str + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + + string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1" + Z3_VERSION_STRING "${libz3_version_str}") + unset(libz3_version_str) +endif() + +# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if +# all listed variables are TRUE +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 + REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR + VERSION_VAR Z3_VERSION_STRING) + +mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) Index: cfe/trunk/include/clang/Config/config.h.cmake =================================================================== --- cfe/trunk/include/clang/Config/config.h.cmake +++ cfe/trunk/include/clang/Config/config.h.cmake @@ -38,6 +38,9 @@ /* Define if we have libxml2 */ #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML} +/* Define if we have z3 and want to build it */ +#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3} + /* Define if we have sys/resource.h (rlimits) */ #cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS} Index: cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def +++ cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def @@ -22,6 +22,7 @@ #endif ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager) +ANALYSIS_CONSTRAINTS(Z3Constraints, "z3", "Use Z3 contraint solver", CreateZ3ConstraintManager) #ifndef ANALYSIS_DIAGNOSTICS #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN) Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -184,6 +184,9 @@ CreateRangeConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine); +std::unique_ptr +CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine); + } // end GR namespace } // end clang namespace Index: cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt +++ cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt @@ -1,5 +1,12 @@ set(LLVM_LINK_COMPONENTS support) +# Link Z3 if the user wants to build it. +if(CLANG_ANALYZER_WITH_Z3) + set(Z3_LINK_FILES ${Z3_LIBRARIES}) +else() + set(Z3_LINK_FILES "") +endif() + add_clang_library(clangStaticAnalyzerCore APSIntType.cpp AnalysisManager.cpp @@ -43,6 +50,7 @@ Store.cpp SubEngine.cpp SymbolManager.cpp + Z3ConstraintManager.cpp LINK_LIBS clangAST @@ -50,4 +58,12 @@ clangBasic clangLex clangRewrite + ${Z3_LINK_FILES} ) + +if(CLANG_ANALYZER_WITH_Z3) + target_include_directories(clangStaticAnalyzerCore SYSTEM + PRIVATE + ${Z3_INCLUDE_DIR} + ) +endif() Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -0,0 +1,1618 @@ +//== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "clang/Basic/TargetInfo.h" +#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" + +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; + +// 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 + +class Z3Sort { + friend class Z3Expr; + + Z3_sort Sort; + + Z3Sort() : Sort(nullptr) {} + Z3Sort(Z3_sort ZS) : Sort(ZS) { + Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); + } + +public: + /// Override implicit copy constructor for correct reference counting. + Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) { + Z3_inc_ref(Z3Context::ZC, reinterpret_cast(Sort)); + } + + /// Provide move constructor + Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); } + + /// 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() { + if (Sort) + Z3_dec_ref(Z3Context::ZC, reinterpret_cast(Sort)); + } + + // 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; + + 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); + } + + // Return an appropriate sort for the given AST. + static Z3Sort getSort(Z3_ast AST) { + return Z3Sort(Z3_get_sort(Z3Context::ZC, AST)); + } + + Z3_sort_kind getSortKind() const { + return Z3_get_sort_kind(Z3Context::ZC, Sort); + } + + unsigned getBitvectorSortSize() const { + assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!"); + return Z3_get_bv_sort_size(Z3Context::ZC, 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); + } + + bool operator==(const Z3Sort &Other) const { + return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.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; + } + + void print(raw_ostream &OS) const { + OS << Z3_sort_to_string(Z3Context::ZC, Sort); + } + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } +}; // end class Z3Sort + +class Z3Expr { + friend class Z3Model; + friend class Z3Solver; + + Z3_ast AST; + + Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); } + + // 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)); + } + + // 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)); + } + +public: + /// Override implicit copy constructor for correct reference counting. + Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); } + + /// Provide move constructor + Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); } + + /// 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() { + if (AST) + Z3_dec_ref(Z3Context::ZC, AST); + } + + /// 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(); + } + } + + /// Construct a Z3Expr from a unary operator, given a Z3_context. + static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) { + Z3_ast AST; + + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; + + case UO_Minus: + AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST); + break; + + case UO_Not: + AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST); + break; + + case UO_LNot: + AST = Z3_mk_not(Z3Context::ZC, Exp.AST); + break; + } + + return Z3Expr(AST); + } + + /// 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; + + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; + + case UO_Minus: + AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST); + break; + + case UO_LNot: + return Z3Expr::fromUnOp(Op, Exp); + } + + return Z3Expr(AST); + } + + /// Construct a Z3Expr from a n-ary binary operator. + static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op, + const std::vector &ASTs) { + Z3_ast AST; + + switch (Op) { + default: + llvm_unreachable("Unimplemented opcode"); + break; + + case BO_LAnd: + AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data()); + break; + + case BO_LOr: + AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data()); + break; + } + + return Z3Expr(AST); + } + + /// 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; + + // 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); + } + + /// 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); + } + + /// 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; + + 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); + } + + /// 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); + } + + /// 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!"); + } + + 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); + } + + /// 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())); + + 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); + } + + /// 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); + } + + /// 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); + } + + /// 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)) { + return false; + } + + if (useSemantics && + !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) { + assert(false && "Floating-point types don't match!"); + 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; + } + } + + 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); + } + + /// 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; + } + + void print(raw_ostream &OS) const { + OS << Z3_ast_to_string(Z3Context::ZC, AST); + } + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } +}; // end class Z3Expr + +class Z3Model { + Z3_model Model; + +public: + Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); } + + /// Override implicit copy constructor for correct reference counting. + Z3Model(const Z3Model &Copy) : Model(Copy.Model) { + Z3_model_inc_ref(Z3Context::ZC, Model); + } + + /// Provide move constructor + Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); } + + /// 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() { + if (Model) + Z3_model_dec_ref(Z3Context::ZC, Model); + } + + /// 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; + + Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func); + Z3Sort Sort = Z3Sort::getSort(Assign); + return Z3Expr::toAPFloat(Sort, Assign, Float, true); + } + + void print(raw_ostream &OS) const { + OS << Z3_model_to_string(Z3Context::ZC, Model); + } + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } +}; // end class Z3Model + +class Z3Solver { + friend class Z3ConstraintManager; + + Z3_solver Solver; + + Z3Solver(Z3_solver ZS) : Solver(ZS) { + Z3_solver_inc_ref(Z3Context::ZC, Solver); + } + +public: + /// Override implicit copy constructor for correct reference counting. + Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) { + Z3_solver_inc_ref(Z3Context::ZC, Solver); + } + + /// Provide move constructor + Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); } + + /// 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() { + if (Solver) + Z3_solver_dec_ref(Z3Context::ZC, Solver); + } + + /// 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; + + while (I != IE) + ASTs.push_back(I++->second.AST); + + Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs); + addConstraint(Conj); + } + } + + /// Check if the constraints are satisfiable + Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); } + + /// Push the current solver state + void push() { return Z3_solver_push(Z3Context::ZC, Solver); } + + /// 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); + } + + /// Get a model from the solver. Caller should check the model is + /// satisfiable. + Z3Model getModel() { + return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver)); + } + + /// Reset the solver and remove all constraints. + void reset() { Z3_solver_reset(Z3Context::ZC, Solver); } +}; // end class Z3Solver + +void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { + llvm::report_fatal_error("Z3 error: " + + llvm::Twine(Z3_get_error_msg_ex(Context, Error))); +} + +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); + } + + //===------------------------------------------------------------------===// + // Implementation for interface from ConstraintManager. + //===------------------------------------------------------------------===// + + bool canReasonAbout(SVal X) const override; + + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; + + const llvm::APSInt *getSymVal(ProgramStateRef State, + SymbolRef Sym) const override; + + ProgramStateRef removeDeadBindings(ProgramStateRef St, + SymbolReaper &SymReaper) override; + + 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; + + // 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 + +Z3_context Z3Context::ZC; + +} // end anonymous namespace + +ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State, + SymbolRef Sym, bool Assumption) { + QualType RetTy; + bool hasComparison; + + Z3Expr 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)); + + return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp)); +} + +ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange( + ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, + const llvm::APSInt &To, bool InRange) { + QualType RetTy; + // The expression may be casted, so we cannot call getZ3DataExpr() directly + Z3Expr Exp = getZ3Expr(Sym, &RetTy); + + assert((getAPSIntType(From) == getAPSIntType(To)) && + "Range values have different types!"); + QualType RTy = getAPSIntType(From); + bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType(); + Z3Expr FromExp = Z3Expr::fromAPSInt(From); + Z3Expr ToExp = Z3Expr::fromAPSInt(To); + + // Construct single (in)equality + if (From == To) + return assumeZ3Expr(State, Sym, + getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE, + FromExp, RTy, nullptr)); + + // Construct two (in)equalities, and a logical and/or + Z3Expr LHS = + getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr); + Z3Expr RHS = + getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr); + return assumeZ3Expr( + State, Sym, + Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy)); +} + +ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State, + SymbolRef Sym, + bool Assumption) { + // Skip anything that is unsupported + return State; +} + +bool Z3ConstraintManager::canReasonAbout(SVal X) const { + const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); + + Optional SymVal = X.getAs(); + if (!SymVal) + return true; + + const SymExpr *Sym = SymVal->getSymbol(); + do { + QualType Ty = Sym->getType(); + + // Complex types are not modeled + if (Ty->isComplexType() || Ty->isComplexIntegerType()) + return false; + + // Non-IEEE 754 floating-point types are not modeled + if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && + (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || + &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble()))) + return false; + + if (isa(Sym)) { + break; + } else if (const SymbolCast *SC = dyn_cast(Sym)) { + Sym = SC->getOperand(); + } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + if (const SymIntExpr *SIE = dyn_cast(BSE)) { + Sym = SIE->getLHS(); + } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { + Sym = ISE->getRHS(); + } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { + return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) && + canReasonAbout(nonloc::SymbolVal(SSM->getRHS())); + } else { + llvm_unreachable("Unsupported binary expression to reason about!"); + } + } else { + llvm_unreachable("Unsupported expression to reason about!"); + } + } while (Sym); + + return true; +} + +ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State, + 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); + // Negate the constraint + Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false); + + Solver.reset(); + Solver.addStateConstraints(State); + + Solver.push(); + Solver.addConstraint(Exp); + Z3_lbool isSat = Solver.check(); + + Solver.pop(); + Solver.addConstraint(NotExp); + Z3_lbool isNotSat = Solver.check(); + + // Zero is the only possible solution + if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE) + return true; + // Zero is not a solution + else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE) + return false; + + // Zero may be a solution + return ConditionTruthVal(); +} + +const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State, + SymbolRef Sym) const { + BasicValueFactory &BV = getBasicVals(); + ASTContext &Ctx = BV.getContext(); + + if (const SymbolData *SD = dyn_cast(Sym)) { + QualType Ty = Sym->getType(); + assert(!Ty->isRealFloatingType()); + llvm::APSInt Value(Ctx.getTypeSize(Ty), + !Ty->isSignedIntegerOrEnumerationType()); + + Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty); + + Solver.reset(); + Solver.addStateConstraints(State); + + // Constraints are unsatisfiable + if (Solver.check() != Z3_L_TRUE) + return nullptr; + + Z3Model Model = Solver.getModel(); + // Model does not assign interpretation + if (!Model.getInterpretation(Exp, Value)) + return nullptr; + + // A value has been obtained, check if it is the only value + Z3Expr NotExp = Z3Expr::fromBinOp( + Exp, BO_NE, + Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.getBoolValue()) + : Z3Expr::fromAPSInt(Value), + false); + + Solver.addConstraint(NotExp); + if (Solver.check() == Z3_L_TRUE) + return nullptr; + + // This is the only solution, store it + return &BV.getValue(Value); + } else if (const SymbolCast *SC = dyn_cast(Sym)) { + SymbolRef CastSym = SC->getOperand(); + QualType CastTy = SC->getType(); + // Skip the void type + if (CastTy->isVoidType()) + return nullptr; + + const llvm::APSInt *Value; + if (!(Value = getSymVal(State, CastSym))) + return nullptr; + return &BV.Convert(SC->getType(), *Value); + } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + const llvm::APSInt *LHS, *RHS; + if (const SymIntExpr *SIE = dyn_cast(BSE)) { + LHS = getSymVal(State, SIE->getLHS()); + RHS = &SIE->getRHS(); + } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { + LHS = &ISE->getLHS(); + RHS = getSymVal(State, ISE->getRHS()); + } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { + // Early termination to avoid expensive call + LHS = getSymVal(State, SSM->getLHS()); + RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr; + } else { + llvm_unreachable("Unsupported binary expression to get symbol value!"); + } + + if (!LHS || !RHS) + return nullptr; + + llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS; + QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS); + doIntTypeConversion( + ConvertedLHS, LTy, ConvertedRHS, RTy); + return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); + } + + llvm_unreachable("Unsupported expression to get symbol value!"); +} + +ProgramStateRef +Z3ConstraintManager::removeDeadBindings(ProgramStateRef State, + SymbolReaper &SymReaper) { + ConstraintZ3Ty CZ = State->get(); + ConstraintZ3Ty::Factory &CZFactory = State->get_context(); + + for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) { + if (SymReaper.maybeDead(I->first)) + CZ = CZFactory.remove(CZ, *I); + } + + return State->set(CZ); +} + +//===------------------------------------------------------------------===// +// Internal implementation. +//===------------------------------------------------------------------===// + +ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State, + SymbolRef Sym, + const Z3Expr &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)); + + return nullptr; +} + +Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State, + const Z3Expr &Exp) const { + Solver.reset(); + Solver.addConstraint(Exp); + Solver.addStateConstraints(State); + return Solver.check(); +} + +Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy, + bool *hasComparison) const { + if (hasComparison) { + *hasComparison = false; + } + + return getZ3SymExpr(Sym, RetTy, hasComparison); +} + +Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const { + return Z3Expr::fromUnOp(UO_LNot, Exp); +} + +Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty, + bool Assumption) const { + ASTContext &Ctx = getBasicVals().getContext(); + if (Ty->isRealFloatingType()) { + llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); + return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE, + Z3Expr::fromAPFloat(Zero)); + } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() || + Ty->isBlockPointerType() || Ty->isReferenceType()) { + bool isSigned = Ty->isSignedIntegerOrEnumerationType(); + // Skip explicit comparison for boolean types + if (Ty->isBooleanType()) + return Assumption ? getZ3NotExpr(Exp) : Exp; + return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE, + Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)), + isSigned); + } + + llvm_unreachable("Unsupported type for zero value!"); +} + +Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy, + bool *hasComparison) const { + if (const SymbolData *SD = dyn_cast(Sym)) { + if (RetTy) + *RetTy = Sym->getType(); + + return getZ3DataExpr(SD->getSymbolID(), Sym->getType()); + } else if (const SymbolCast *SC = dyn_cast(Sym)) { + if (RetTy) + *RetTy = Sym->getType(); + + QualType FromTy; + Z3Expr 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) + if (hasComparison) + *hasComparison = false; + return getZ3CastExpr(Exp, FromTy, Sym->getType()); + } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy); + // Set the hasComparison parameter, in post-order traversal order. + if (hasComparison) + *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode()); + return Exp; + } + + llvm_unreachable("Unsupported SymbolRef type!"); +} + +Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID, + QualType Ty) const { + ASTContext &Ctx = getBasicVals().getContext(); + return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(), + Ctx.getTypeSize(Ty)); +} + +Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, + QualType ToTy) const { + ASTContext &Ctx = getBasicVals().getContext(); + return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, + Ctx.getTypeSize(FromTy)); +} + +Z3Expr 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)) { + RTy = getAPSIntType(SIE->getRHS()); + Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison); + Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS()); + return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); + } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { + LTy = getAPSIntType(ISE->getLHS()); + Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS()); + Z3Expr 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); + 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; + doTypeConversion(NewLHS, NewRHS, LTy, RTy); + // Update the return type parameter if the output type has changed. + if (RetTy) { + // A boolean result can be represented as an integer type in C/C++, but at + // this point we only care about the Z3 type. Set it as a boolean type to + // avoid subsequent Z3 errors. + if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) { + ASTContext &Ctx = getBasicVals().getContext(); + *RetTy = Ctx.BoolTy; + } else { + *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 (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) { + ASTContext &Ctx = getBasicVals().getContext(); + *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true); + } + } + + return LTy->isRealFloatingType() + ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS) + : Z3Expr::fromBinOp(NewLHS, Op, NewRHS, + LTy->isSignedIntegerOrEnumerationType()); +} + +//===------------------------------------------------------------------===// +// Helper functions. +//===------------------------------------------------------------------===// + +QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const { + ASTContext &Ctx = getBasicVals().getContext(); + return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()); +} + +void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, + QualType <y, QualType &RTy) const { + ASTContext &Ctx = getBasicVals().getContext(); + + // Perform type conversion + if (LTy->isIntegralOrEnumerationType() && + RTy->isIntegralOrEnumerationType()) { + if (LTy->isArithmeticType() && RTy->isArithmeticType()) + return doIntTypeConversion(LHS, LTy, RHS, RTy); + } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { + return doFloatTypeConversion(LHS, LTy, RHS, RTy); + } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) || + (LTy->isBlockPointerType() || RTy->isBlockPointerType()) || + (LTy->isReferenceType() || RTy->isReferenceType())) { + // TODO: Refactor to Sema::FindCompositePointerType(), and + // Sema::CheckCompareOperands(). + + uint64_t LBitWidth = Ctx.getTypeSize(LTy); + uint64_t RBitWidth = Ctx.getTypeSize(RTy); + + // Cast the non-pointer type to the pointer type. + // TODO: Be more strict about this. + if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) || + (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) || + (LTy->isReferenceType() ^ RTy->isReferenceType())) { + if (LTy->isNullPtrType() || LTy->isBlockPointerType() || + LTy->isReferenceType()) { + LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } else { + RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } + } + + // 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. + if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) { + assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) && + "Pointer types have different bitwidths!"); + if (RTy->isVoidPointerType()) + RTy = LTy; + else + LTy = RTy; + } + + if (LTy == RTy) + return; + } + + // Fallback: for the solver, assume that these types don't really matter + if ((LTy.getCanonicalType() == RTy.getCanonicalType()) || + (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) { + LTy = RTy; + return; + } + + // TODO: Refine behavior for invalid type casts +} + +template +void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType <y, T &RHS, + QualType &RTy) const { + ASTContext &Ctx = getBasicVals().getContext(); + + uint64_t LBitWidth = Ctx.getTypeSize(LTy); + uint64_t RBitWidth = Ctx.getTypeSize(RTy); + + // Always perform integer promotion before checking type equality. + // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion + if (LTy->isPromotableIntegerType()) { + QualType NewTy = Ctx.getPromotedIntegerType(LTy); + uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); + LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth); + LTy = NewTy; + LBitWidth = NewBitWidth; + } + if (RTy->isPromotableIntegerType()) { + QualType NewTy = Ctx.getPromotedIntegerType(RTy); + uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); + RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth); + RTy = NewTy; + RBitWidth = NewBitWidth; + } + + if (LTy == RTy) + return; + + // Perform integer type conversion + // Note: Safe to skip updating bitwidth because this must terminate + bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType(); + bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType(); + + int order = Ctx.getIntegerTypeOrder(LTy, RTy); + if (isLSignedTy == isRSignedTy) { + // Same signedness; use the higher-ranked type + if (order == 1) { + RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else { + LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } + } else if (order != (isLSignedTy ? 1 : -1)) { + // The unsigned type has greater than or equal rank to the + // signed type, so use the unsigned type + if (isRSignedTy) { + RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else { + LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } + } else if (LBitWidth != RBitWidth) { + // The two types are different widths; if we are here, that + // means the signed type is larger than the unsigned type, so + // use the signed type. + if (isLSignedTy) { + RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else { + LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } + } else { + // The signed type is higher-ranked than the unsigned type, + // but isn't actually any bigger (like unsigned int and long + // on most 32-bit systems). Use the unsigned type corresponding + // to the signed type. + QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy); + RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = NewTy; + LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = NewTy; + } +} + +template +void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType <y, T &RHS, + QualType &RTy) const { + ASTContext &Ctx = getBasicVals().getContext(); + + uint64_t LBitWidth = Ctx.getTypeSize(LTy); + uint64_t RBitWidth = Ctx.getTypeSize(RTy); + + // Perform float-point type promotion + if (!LTy->isRealFloatingType()) { + LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + LBitWidth = RBitWidth; + } + if (!RTy->isRealFloatingType()) { + RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + RBitWidth = LBitWidth; + } + + if (LTy == RTy) + return; + + // If we have two real floating types, convert the smaller operand to the + // bigger result + // Note: Safe to skip updating bitwidth because this must terminate + int order = Ctx.getFloatingTypeOrder(LTy, RTy); + if (order > 0) { + RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else if (order == 0) { + LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } else { + llvm_unreachable("Unsupported floating-point type cast!"); + } +} + +llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V, + QualType ToTy, uint64_t ToWidth, + QualType FromTy, + uint64_t FromWidth) { + APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType()); + return TargetType.convert(V); +} + +//==------------------------------------------------------------------------==/ +// Pretty-printing. +//==------------------------------------------------------------------------==/ + +void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS, + const char *nl, const char *sep) { + + ConstraintZ3Ty CZ = St->get(); + + OS << nl << sep << "Constraints:"; + for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) { + OS << nl << ' ' << I->first << " : "; + I->second.print(OS); + } + OS << nl; +} + +#endif + +std::unique_ptr +ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { +#if CLANG_ANALYZER_WITH_Z3 + return llvm::make_unique(Eng, StMgr.getSValBuilder()); +#else + llvm::report_fatal_error("Clang was not compiled with Z3 support!", false); + return nullptr; +#endif +} Index: cfe/trunk/test/Analysis/expr-inspection.c =================================================================== --- cfe/trunk/test/Analysis/expr-inspection.c +++ cfe/trunk/test/Analysis/expr-inspection.c @@ -19,4 +19,4 @@ // CHECK: Expressions: // CHECK-NEXT: clang_analyzer_printState : &code{clang_analyzer_printState} -// CHECK-NEXT: Ranges are empty. +// CHECK-NEXT: {{(Ranges are empty.)|(Constraints:[[:space:]]*$)}} Index: cfe/trunk/test/Analysis/lit.local.cfg =================================================================== --- cfe/trunk/test/Analysis/lit.local.cfg +++ cfe/trunk/test/Analysis/lit.local.cfg @@ -10,6 +10,10 @@ if result.code == lit.Test.FAIL: return result + # If z3 backend available, add an additional run line for it + if test.config.clang_staticanalyzer_z3 == '1': + result = self.executeWithAnalyzeSubstitution(test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3') + return result def executeWithAnalyzeSubstitution(self, test, litConfig, substitution): Index: cfe/trunk/test/Analysis/unsupported-types.c =================================================================== --- cfe/trunk/test/Analysis/unsupported-types.c +++ cfe/trunk/test/Analysis/unsupported-types.c @@ -0,0 +1,31 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -triple x86_64-unknown-linux -verify %s +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -triple powerpc64-linux-gnu -verify %s + +#define _Complex_I (__extension__ 1.0iF) + +void clang_analyzer_eval(int); + +void complex_float(double _Complex x, double _Complex y) { + clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}} + if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I) + return + clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); // expected-warning{{UNKNOWN}} +} + +void complex_int(int _Complex x, int _Complex y) { + clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}} + if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I) + return + clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); // expected-warning{{UNKNOWN}} +} + +void longdouble_float(long double x, long double y) { + clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}} + if (x != 0.0L && y != 1.0L) + return + clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x + y == 1.0L); // expected-warning{{UNKNOWN}} +} Index: cfe/trunk/test/lit.cfg =================================================================== --- cfe/trunk/test/lit.cfg +++ cfe/trunk/test/lit.cfg @@ -361,6 +361,9 @@ if config.clang_staticanalyzer: config.available_features.add("staticanalyzer") + if config.clang_staticanalyzer_z3 == '1': + config.available_features.add("z3") + # As of 2011.08, crash-recovery tests still do not pass on FreeBSD. if platform.system() not in ['FreeBSD']: config.available_features.add('crash-recovery') Index: cfe/trunk/test/lit.site.cfg.in =================================================================== --- cfe/trunk/test/lit.site.cfg.in +++ cfe/trunk/test/lit.site.cfg.in @@ -18,6 +18,7 @@ config.clang_arcmt = @CLANG_ENABLE_ARCMT@ config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@" config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@ +config.clang_staticanalyzer_z3 = "@CLANG_ANALYZER_WITH_Z3@" config.clang_examples = @CLANG_BUILD_EXAMPLES@ config.enable_shared = @ENABLE_SHARED@ config.enable_backtrace = @ENABLE_BACKTRACES@