[analyzer] Create generic SMT Expr class

[mikhail.ramalho]

Summary

New base class for all future SMT Exprs.

No major changes except moving areEquivalent and getFloatSemantics outside of Z3Expr to keep the class minimal.

[mikhail.ramalho]

Make some methods pure virtual

[george.karpenkov]

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

52 ↗

(On Diff #156496)

same nit: could we not store anything in the abstract class?

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

52 ↗

(On Diff #156496)

do we need this forward class/function declaration?

[mikhail.ramalho]

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

52 ↗

(On Diff #156496)

It's used on equal_to, but I guess I can do like on Z3Sort and cast it directly.

[mikhail.ramalho]

Removed SMTContext from SMExpr.

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h

+//== 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"
+
+namespace clang {
+namespace ento {
+
+class SMTExpr {
+public:
+  SMTExpr() = default;
+  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 = 0;
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+
+protected:
+  virtual bool equal_to(SMTExpr const &other) const = 0;
+};
+
+using SMTExprRef = std::shared_ptr<SMTExpr>;
+
+} // namespace ento
+} // namespace clang
+
+#endif

cfe/trunk/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/SMTExpr.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
 
 #include "clang/Config/config.h"
 
 using namespace clang;
 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
Z3Sort &operator=(const Z3Sort &Move) {
     return *this;
   }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_sort_to_string(Context.Context, Sort);
   }
 }; // 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);
+  Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
     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));
-  }
-
 public:
   /// Override implicit copy constructor for correct reference counting.
-  Z3Expr(const Z3Expr &Copy) : Context(Copy.Context), AST(Copy.AST) {
+  Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
     Z3_inc_ref(Context.Context, AST);
   }
 
   /// Provide move constructor
-  Z3Expr(Z3Expr &&Move) : Context(Move.Context), AST(nullptr) {
+  Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {
     *this = std::move(Move);
   }
 
   /// Provide move assignment constructor
   Z3Expr &operator=(Z3Expr &&Move) {
     if (this != &Move) {
       if (AST)
         Z3_dec_ref(Context.Context, AST);
       AST = Move.AST;
       Move.AST = nullptr;
     }
     return *this;
   }
 
   ~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 {
+  void Profile(llvm::FoldingSetNodeID &ID) const override {
     ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
   }
 
-  bool operator<(const Z3Expr &Other) const {
-    llvm::FoldingSetNodeID ID1, ID2;
-    Profile(ID1);
-    Other.Profile(ID2);
-    return ID1 < ID2;
-  }
-
   /// Comparison of AST equality, not model equivalence.
-  bool operator==(const Z3Expr &Other) const {
+  bool equal_to(SMTExpr const &Other) const override {
     assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
-                         Z3_get_sort(Context.Context, Other.AST)) &&
+                         Z3_get_sort(Context.Context,
+                                     static_cast<const Z3Expr &>(Other).AST)) &&
            "AST's must have the same sort");
-    return Z3_is_eq_ast(Context.Context, AST, Other.AST);
+    return Z3_is_eq_ast(Context.Context, AST,
+                        static_cast<const Z3Expr &>(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);
     AST = Move.AST;
     return *this;
   }
 
-  void print(raw_ostream &OS) const {
+  void print(raw_ostream &OS) const override {
     OS << Z3_ast_to_string(Context.Context, AST);
   }
-
-  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Expr
 
 class Z3Model {
   friend class Z3Solver;
 
   Z3Context &Context;
 
   Z3_model Model;
public:
 
   void print(raw_ostream &OS) const {
     OS << Z3_model_to_string(Context.Context, Model);
   }
 
   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;
 
   Z3Context Context;
 
   Z3_solver Solver;
 
   Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
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.isFloatSort() && "Unsupported sort to floating-point!");
 
     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;
     }
 
     Float = llvm::APFloat(Semantics, Int);
     return true;
   }