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().
isBitvectorSort()30   virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
31 
32   /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
isFloatSort()33   virtual bool isFloatSort() const { return isFloatSortImpl(); }
34 
35   /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
isBooleanSort()36   virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
37 
38   /// Returns the bitvector size, fails if the sort is not a bitvector
39   /// Calls getBitvectorSortSizeImpl().
getBitvectorSortSize()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().
getFloatSortSize()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 
dump()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
92