Author: mramalho Date: Wed Jul 25 05:49:15 2018 New Revision: 337916 URL: http://llvm.org/viewvc/llvm-project?rev=337916&view=rev Log: [analyzer] Create generic SMT Sort Class
Summary: New base class for all future SMT sorts. The only change is that the class implements methods `isBooleanSort()`, `isBitvectorSort()` and `isFloatSort()` so it doesn't rely on `Z3`'s enum. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49550 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=337916&view=auto ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Wed Jul 25 05:49:15 2018 @@ -0,0 +1,71 @@ +//== SMTSort.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 Sort API, which will be the base class +// for every SMT solver sort specific class. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H + +namespace clang { +namespace ento { + +class SMTSort { +public: + SMTSort() = default; + virtual ~SMTSort() = default; + + virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); } + virtual bool isFloatSort() const { return isFloatSortImpl(); } + virtual bool isBooleanSort() const { return isBooleanSortImpl(); } + + virtual unsigned getBitvectorSortSize() const { + assert(isBitvectorSort() && "Not a bitvector sort!"); + unsigned Size = getBitvectorSortSizeImpl(); + assert(Size && "Size is zero!"); + return Size; + }; + + virtual unsigned getFloatSortSize() const { + assert(isFloatSort() && "Not a floating-point sort!"); + unsigned Size = getFloatSortSizeImpl(); + assert(Size && "Size is zero!"); + return Size; + }; + + friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) { + return LHS.equal_to(RHS); + } + + virtual void print(raw_ostream &OS) const = 0; + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } + +protected: + virtual bool equal_to(SMTSort const &other) const = 0; + + virtual bool isBitvectorSortImpl() const = 0; + + virtual bool isFloatSortImpl() const = 0; + + virtual bool isBooleanSortImpl() const = 0; + + virtual unsigned getBitvectorSortSizeImpl() const = 0; + + virtual unsigned getFloatSortSizeImpl() const = 0; +}; + +using SMTSortRef = std::shared_ptr<SMTSort>; + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337916&r1=337915&r2=337916&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:15 2018 @@ -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/SMTSort.h" #include "clang/Config/config.h" @@ -84,27 +85,26 @@ public: } }; // end class Z3Context -class Z3Sort { - friend class Z3Expr; +class Z3Sort : public SMTSort { friend class Z3Solver; Z3Context &Context; Z3_sort Sort; - Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { - assert(C.Context != nullptr); + Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) { Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); } public: /// Override implicit copy constructor for correct reference counting. - Z3Sort(const Z3Sort &Copy) : Context(Copy.Context), Sort(Copy.Sort) { + Z3Sort(const Z3Sort &Copy) + : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) { Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); } /// Provide move constructor - Z3Sort(Z3Sort &&Move) : Context(Move.Context), Sort(nullptr) { + Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) { *this = std::move(Move); } @@ -124,24 +124,30 @@ public: Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); } - Z3_sort_kind getSortKind() const { - return Z3_get_sort_kind(Context.Context, Sort); + bool isBitvectorSortImpl() const override { + return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT); + } + + bool isFloatSortImpl() const override { + return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT); } - unsigned getBitvectorSortSize() const { - assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!"); + bool isBooleanSortImpl() const override { + return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT); + } + + unsigned getBitvectorSortSizeImpl() const override { return Z3_get_bv_sort_size(Context.Context, Sort); } - unsigned getFloatSortSize() const { - assert(getSortKind() == Z3_FLOATING_POINT_SORT && - "Not a floating-point sort!"); + unsigned getFloatSortSizeImpl() const override { return Z3_fpa_get_ebits(Context.Context, Sort) + Z3_fpa_get_sbits(Context.Context, Sort); } - bool operator==(const Z3Sort &Other) const { - return Z3_is_eq_sort(Context.Context, Sort, Other.Sort); + bool equal_to(SMTSort const &Other) const override { + return Z3_is_eq_sort(Context.Context, Sort, + static_cast<const Z3Sort &>(Other).Sort); } Z3Sort &operator=(const Z3Sort &Move) { @@ -151,11 +157,9 @@ public: return *this; } - void print(raw_ostream &OS) const { + void print(raw_ostream &OS) const override { OS << Z3_sort_to_string(Context.Context, Sort); } - - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } }; // end class Z3Sort class Z3Expr { @@ -804,8 +808,7 @@ public: /// Construct an APFloat from a Z3Expr, given the AST representation bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, llvm::APFloat &Float, bool useSemantics = true) { - assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT && - "Unsupported sort to floating-point!"); + assert(Sort.isFloatSort() && "Unsupported sort to floating-point!"); llvm::APSInt Int(Sort.getFloatSortSize(), true); const llvm::fltSemantics &Semantics = @@ -828,10 +831,7 @@ public: /// Construct an APSInt from a Z3Expr, given the AST representation bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int, bool useSemantics = true) { - switch (Sort.getSortKind()) { - default: - llvm_unreachable("Unsupported sort to integer!"); - case Z3_BV_SORT: { + if (Sort.isBitvectorSort()) { if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) { assert(false && "Bitvector types don't match!"); return false; @@ -859,11 +859,13 @@ public: } return true; } - case Z3_BOOL_SORT: + + if (Sort.isBooleanSort()) { if (useSemantics && Int.getBitWidth() < 1) { assert(false && "Boolean type doesn't match!"); return false; } + Int = llvm::APSInt( llvm::APInt(Int.getBitWidth(), Z3_get_bool_value(Context.Context, AST) == Z3_L_TRUE ? 1 @@ -871,6 +873,8 @@ public: Int.isUnsigned()); return true; } + + llvm_unreachable("Unsupported sort to integer!"); } /// Given an expression and a model, extract the value of this operand in _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
