Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h =================================================================== --- /dev/null +++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h @@ -0,0 +1,58 @@ +//== SMTExpr.h --------------------------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// This file defines a SMT generic Expr API, which will be the base class +// for every SMT solver expr specific class. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" + +namespace clang { +namespace ento { + +class SMTExpr { +public: + SMTExpr(SMTContext &C) : Context(C) {} + virtual ~SMTExpr() = default; + + bool operator<(const SMTExpr &Other) const { + llvm::FoldingSetNodeID ID1, ID2; + Profile(ID1); + Other.Profile(ID2); + return ID1 < ID2; + } + + virtual void Profile(llvm::FoldingSetNodeID &ID) const { + static int Tag = 0; + ID.AddPointer(&Tag); + } + + friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) { + return LHS.equal_to(RHS); + } + + virtual void print(raw_ostream &OS) const {}; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + +protected: + virtual bool equal_to(SMTExpr const &other) const { return false; } + + SMTContext &Context; +}; + +} // namespace ento +} // namespace clang + +#endif Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -12,6 +12,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" #include "clang/Config/config.h" @@ -47,6 +48,9 @@ namespace { +class Z3Expr; +static const Z3Expr &toZ3Expr(const SMTExpr &E); + class Z3Config { friend class Z3Context; @@ -167,40 +171,23 @@ } }; // end class Z3Sort -class Z3Expr { - friend class Z3Model; +class Z3Expr : public SMTExpr { friend class Z3Solver; - Z3Context &Context; - Z3_ast AST; - Z3Expr(Z3Context &C, Z3_ast ZA) : Context(C), AST(ZA) { - assert(C.Context != nullptr); - Z3_inc_ref(Context.Context, 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(SMTContext &C, Z3_ast ZA) : SMTExpr(C), AST(ZA) { + Z3_inc_ref(toZ3Context(Context).Context, AST); } public: /// Override implicit copy constructor for correct reference counting. - Z3Expr(const Z3Expr &Copy) : Context(Copy.Context), AST(Copy.AST) { - Z3_inc_ref(Context.Context, AST); + Z3Expr(const Z3Expr &Copy) : SMTExpr(Copy.Context), AST(Copy.AST) { + Z3_inc_ref(toZ3Context(Context).Context, AST); } /// Provide move constructor - Z3Expr(Z3Expr &&Move) : Context(Move.Context), AST(nullptr) { + Z3Expr(Z3Expr &&Move) : SMTExpr(Move.Context), AST(nullptr) { *this = std::move(Move); } @@ -208,7 +195,7 @@ Z3Expr &operator=(Z3Expr &&Move) { if (this != &Move) { if (AST) - Z3_dec_ref(Context.Context, AST); + Z3_dec_ref(toZ3Context(Context).Context, AST); AST = Move.AST; Move.AST = nullptr; } @@ -217,60 +204,40 @@ ~Z3Expr() { if (AST) - Z3_dec_ref(Context.Context, 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(); - } - } - - void Profile(llvm::FoldingSetNodeID &ID) const { - ID.AddInteger(Z3_get_ast_hash(Context.Context, AST)); + Z3_dec_ref(toZ3Context(Context).Context, AST); } - bool operator<(const Z3Expr &Other) const { - llvm::FoldingSetNodeID ID1, ID2; - Profile(ID1); - Other.Profile(ID2); - return ID1 < ID2; + void Profile(llvm::FoldingSetNodeID &ID) const override { + ID.AddInteger(Z3_get_ast_hash(toZ3Context(Context).Context, AST)); } /// Comparison of AST equality, not model equivalence. - bool operator==(const Z3Expr &Other) const { - assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST), - Z3_get_sort(Context.Context, Other.AST)) && + bool equal_to(SMTExpr const &Other) const override { + assert(Z3_is_eq_sort(toZ3Context(Context).Context, + Z3_get_sort(toZ3Context(Context).Context, AST), + Z3_get_sort(toZ3Context(Context).Context, + toZ3Expr(Other).AST)) && "AST's must have the same sort"); - return Z3_is_eq_ast(Context.Context, AST, Other.AST); + return Z3_is_eq_ast(toZ3Context(Context).Context, AST, toZ3Expr(Other).AST); } /// Override implicit move constructor for correct reference counting. Z3Expr &operator=(const Z3Expr &Move) { - Z3_inc_ref(Context.Context, Move.AST); - Z3_dec_ref(Context.Context, AST); + Z3_inc_ref(toZ3Context(Context).Context, Move.AST); + Z3_dec_ref(toZ3Context(Context).Context, AST); AST = Move.AST; return *this; } - void print(raw_ostream &OS) const { - OS << Z3_ast_to_string(Context.Context, AST); + void print(raw_ostream &OS) const override { + OS << Z3_ast_to_string(toZ3Context(Context).Context, AST); } - - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } }; // end class Z3Expr +static const Z3Expr &toZ3Expr(const SMTExpr &E) { + return static_cast(E); +} + class Z3Model { friend class Z3Solver; @@ -317,6 +284,36 @@ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } }; // end class Z3Model +/// 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(); + } +} + +// 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)); +} + class Z3Solver { friend class Z3ConstraintManager; @@ -817,14 +814,13 @@ llvm::APSInt Int(Sort.getFloatSortSize(), true); const llvm::fltSemantics &Semantics = - Z3Expr::getFloatSemantics(Sort.getFloatSortSize()); + getFloatSemantics(Sort.getFloatSortSize()); Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize()); if (!toAPSInt(BVSort, AST, Int, true)) { return false; } - if (useSemantics && - !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) { + if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) { assert(false && "Floating-point types don't match!"); return false; }