[analyzer] Create generic SMT Sort Class

[mikhail.ramalho]

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.

[mikhail.ramalho]

Make some methods pure virtual

[george.karpenkov]

Small change requested. Otherwise, good to go.

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h

64

A reference to a generic SMTContext is not very useful.
Could we just remove that, then you can remove the constructor of SMTContext,
just store Z3Context in a subclass, and then you won't need casts everywhere as well?

[mikhail.ramalho]

Removed SMTContext reference from SMTSort.

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h

+//== 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
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
+
+namespace clang {
+namespace ento {
+
+class SMTSort {
+public:
+  SMTSort(SMTContext &C) : Context(C) {}
+  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;
+
+  SMTContext &Context;
+};
+
+} // namespace ento
+} // namespace clang
+
+#endif

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 //== 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/SMTConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
 
 #include "clang/Config/config.h"
 
 using namespace clang;
 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
 
public:
   }
 
   virtual ~Z3Context() {
     Z3_del_context(Context);
     Context = nullptr;
   }
 }; // end class Z3Context
 
-class Z3Sort {
-  friend class Z3Expr;
-  friend class Z3Solver;
+static Z3Context &toZ3Context(SMTContext &C) {
+  return static_cast<Z3Context &>(C);
+}
 
-  Z3Context &Context;
+class Z3Sort : public SMTSort {
+  friend class Z3Solver;
 
   Z3_sort Sort;
 
-  Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
-    assert(C.Context != nullptr);
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+  Z3Sort(SMTContext &C, Z3_sort ZS) : SMTSort(C), Sort(ZS) {
+    Z3_inc_ref(toZ3Context(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) {
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+  Z3Sort(const Z3Sort &Copy) : SMTSort(Copy.Context), Sort(Copy.Sort) {
+    Z3_inc_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
   /// Provide move constructor
-  Z3Sort(Z3Sort &&Move) : Context(Move.Context), Sort(nullptr) {
+  Z3Sort(Z3Sort &&Move) : SMTSort(Move.Context), Sort(nullptr) {
     *this = std::move(Move);
   }
 
   /// Provide move assignment constructor
   Z3Sort &operator=(Z3Sort &&Move) {
     if (this != &Move) {
       if (Sort)
-        Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+        Z3_dec_ref(toZ3Context(Context).Context,
+                   reinterpret_cast<Z3_ast>(Sort));
       Sort = Move.Sort;
       Move.Sort = nullptr;
     }
     return *this;
   }
 
   ~Z3Sort() {
     if (Sort)
-      Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+      Z3_dec_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
+  }
+
+  bool isBitvectorSortImpl() const override {
+    return (Z3_get_sort_kind(toZ3Context(Context).Context, Sort) == Z3_BV_SORT);
+  }
+
+  bool isFloatSortImpl() const override {
+    return (Z3_get_sort_kind(toZ3Context(Context).Context, Sort) ==
+            Z3_FLOATING_POINT_SORT);
   }
 
-  Z3_sort_kind getSortKind() const {
-    return Z3_get_sort_kind(Context.Context, Sort);
+  bool isBooleanSortImpl() const override {
+    return (Z3_get_sort_kind(toZ3Context(Context).Context, Sort) ==
+            Z3_BOOL_SORT);
   }
 
-  unsigned getBitvectorSortSize() const {
-    assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
-    return Z3_get_bv_sort_size(Context.Context, Sort);
+  unsigned getBitvectorSortSizeImpl() const override {
+    return Z3_get_bv_sort_size(toZ3Context(Context).Context, Sort);
   }
 
-  unsigned getFloatSortSize() const {
-    assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
-           "Not a floating-point sort!");
-    return Z3_fpa_get_ebits(Context.Context, Sort) +
-           Z3_fpa_get_sbits(Context.Context, Sort);
+  unsigned getFloatSortSizeImpl() const override {
+    return Z3_fpa_get_ebits(toZ3Context(Context).Context, Sort) +
+           Z3_fpa_get_sbits(toZ3Context(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(toZ3Context(Context).Context, Sort,
+                         static_cast<const Z3Sort *>(&Other)->Sort);
   }
 
   Z3Sort &operator=(const Z3Sort &Move) {
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Move.Sort));
-    Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+    Z3_inc_ref(toZ3Context(Context).Context,
+               reinterpret_cast<Z3_ast>(Move.Sort));
+    Z3_dec_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
     Sort = Move.Sort;
     return *this;
   }
 
-  void print(raw_ostream &OS) const {
-    OS << Z3_sort_to_string(Context.Context, Sort);
+  void print(raw_ostream &OS) const override {
+    OS << Z3_sort_to_string(toZ3Context(Context).Context, Sort);
   }
-
-  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Sort
 
 class Z3Expr {
   friend class Z3Model;
   friend class Z3Solver;
 
   Z3Context &Context;
 
Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
     Z3Sort Sort = getBitvectorSort(BitWidth);
     Z3_ast AST = Z3_mk_numeral(Context.Context, Int, Sort.Sort);
     return Z3Expr(Context, AST);
   }
 
   /// 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 =
         Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
     Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize());
     if (!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
   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;
       }
 
       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
if (Sort.isBitvectorSort()) {
         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
                            Int.isUnsigned());
       } else {
         assert(false && "Bitwidth not supported!");
         return false;
       }
       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
                                                                            : 0),
           Int.isUnsigned());
       return true;
     }
+
+    llvm_unreachable("Unsupported sort to integer!");
   }
 
   /// Given an expression and a model, extract the value of this operand in
   /// the model.
   bool getInterpretation(const Z3Model Model, const Z3Expr &Exp,
                          llvm::APSInt &Int) {
     Z3_func_decl Func =
         Z3_get_app_decl(Context.Context, Z3_to_app(Context.Context, Exp.AST));