[analyzer] Create generic SMT Context class

[mikhail.ramalho]

Summary

This patch creates SMTContext which will wrap a specific SMT context, through SMTSolverContext.

The templated SMTSolverContext class it's a simple wrapper around a SMT specific context (currently only used in the Z3 backend), while Z3Context inherits SMTSolverContext<Z3_context> and implements solver specific operations like initialization and destruction of the context.

This separation was done because:

1. We might want to keep one single context, shared across different SMTConstraintManagers. It can be achieved by constructing a SMTContext, through a function like CreateSMTContext(Z3), CreateSMTContext(BOOLECTOR), etc. The rest of the CSA only need to know about SMTContext, so maybe it's a good idea moving SMTSolverContext to a separate header in the future.

2. Any generic SMT operation will only require one SMTSolverContextobject, which can access the specific context by calling getContext().

[george.karpenkov]

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

76

Could we remove this method?

78

Let's not do this. This invalidates all Z3 objects, and all future calls to any Z3 objects will segfault.

[mikhail.ramalho]

Removed reset method and call to Z3_finalize_memory().

[george.karpenkov]

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

22

What's the point of this base class?

[mikhail.ramalho]

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

22

SMTContext will be used around the CSA, since it doesn't know anything about the specific SMT context, e.g., Z3_Context.

SMTSolverContext<Z3_context> will be used in the solver specific implementation.

[mikhail.ramalho]

Simplify SMTContext class

[george.karpenkov]

LGTM with a nit

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

24

Probably should do =0 to indicate that this is a pure virtual class.

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

+//== SMTContext.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 Context API, which will be the base class
+//  for every SMT solver context specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H
+
+namespace clang {
+namespace ento {
+
+class SMTContext {
+public:
+  SMTContext() = default;
+  virtual ~SMTContext() = default;
+};
+
+template <typename C> class SMTSolverContext : public SMTContext {
+public:
+  SMTSolverContext() : SMTContext() {}
+  virtual ~SMTSolverContext() = default;
+
+  C getContext() const { return Context; }
+
+  virtual void reset(){};
+
+protected:
+  C 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/Config/config.h"
 
 using namespace clang;
 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
 
Z3Config() : Config(Z3_mk_config()) {
     Z3_set_param_value(Config, "proof", "false");
     // Set timeout to 15000ms = 15s
     Z3_set_param_value(Config, "timeout", "15000");
   }
 
   ~Z3Config() { Z3_del_config(Config); }
 }; // end class Z3Config
 
-class Z3Context {
-  Z3_context ZC_P;
-
+class Z3Context : public SMTSolverContext<Z3_context> {
 public:
   static Z3_context ZC;
 
-  Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
+  Z3Context() : SMTSolverContext<Z3_context>() {
+    Context = Z3_mk_context_rc(Z3Config().Config);
+    ZC = Context;
+  }
 
-  ~Z3Context() {
+  void reset() override {
     Z3_del_context(ZC);
     Z3_finalize_memory();
-    ZC_P = nullptr;
+    Context = nullptr;
   }
+
+  ~Z3Context() { reset(); }
 }; // end class Z3Context
 
 class Z3Sort {
   friend class Z3Expr;
 
   Z3_sort Sort;
 
   Z3Sort() : Sort(nullptr) {}