contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h

   1 //== SMTSort.h --------------------------------------------------*- C++ -*--==//
   2 //
   3 //                     The LLVM Compiler Infrastructure
   4 //
   5 // This file is distributed under the University of Illinois Open Source
   6 // License. See LICENSE.TXT for details.
   7 //
   8 //===----------------------------------------------------------------------===//
   9 //
  10 //  This file defines a SMT generic Sort API, which will be the base class
  11 //  for every SMT solver sort specific class.
  12 //
  13 //===----------------------------------------------------------------------===//
  14
  15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
  16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
  17
  18 #include "clang/Basic/TargetInfo.h"
  19
  20 namespace clang {
  21 namespace ento {
  22
  23 /// Generic base class for SMT sorts
  24 class SMTSort {
  25 public:
  26   SMTSort() = default;
  27   virtual ~SMTSort() = default;
  28
  29   /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
  30   virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
  31
  32   /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
  33   virtual bool isFloatSort() const { return isFloatSortImpl(); }
  34
  35   /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
  36   virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
  37
  38   /// Returns the bitvector size, fails if the sort is not a bitvector
  39   /// Calls getBitvectorSortSizeImpl().
  40   virtual unsigned getBitvectorSortSize() const {
  41     assert(isBitvectorSort() && "Not a bitvector sort!");
  42     unsigned Size = getBitvectorSortSizeImpl();
  43     assert(Size && "Size is zero!");
  44     return Size;
  45   };
  46
  47   /// Returns the floating-point size, fails if the sort is not a floating-point
  48   /// Calls getFloatSortSizeImpl().
  49   virtual unsigned getFloatSortSize() const {
  50     assert(isFloatSort() && "Not a floating-point sort!");
  51     unsigned Size = getFloatSortSizeImpl();
  52     assert(Size && "Size is zero!");
  53     return Size;
  54   };
  55
  56   friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
  57     return LHS.equal_to(RHS);
  58   }
  59
  60   virtual void print(raw_ostream &OS) const = 0;
  61
  62   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
  63
  64 protected:
  65   /// Query the SMT solver and returns true if two sorts are equal (same kind
  66   /// and bit width). This does not check if the two sorts are the same objects.
  67   virtual bool equal_to(SMTSort const &other) const = 0;
  68
  69   /// Query the SMT solver and checks if a sort is bitvector.
  70   virtual bool isBitvectorSortImpl() const = 0;
  71
  72   /// Query the SMT solver and checks if a sort is floating-point.
  73   virtual bool isFloatSortImpl() const = 0;
  74
  75   /// Query the SMT solver and checks if a sort is boolean.
  76   virtual bool isBooleanSortImpl() const = 0;
  77
  78   /// Query the SMT solver and returns the sort bit width.
  79   virtual unsigned getBitvectorSortSizeImpl() const = 0;
  80
  81   /// Query the SMT solver and returns the sort bit width.
  82   virtual unsigned getFloatSortSizeImpl() const = 0;
  83 };
  84
  85 /// Shared pointer for SMTSorts, used by SMTSolver API.
  86 using SMTSortRef = std::shared_ptr<SMTSort>;
  87
  88 } // namespace ento
  89 } // namespace clang
  90
  91 #endif