r337914 - [analyzer] Create generic SMT Context class

[Mikhail R. Gadelha via cfe-commits]

Author: mramalho
Date: Wed Jul 25 05:49:07 2018
New Revision: 337914

URL: http://llvm.org/viewvc/llvm-project?rev=337914&view=rev
Log:
[analyzer] Create generic SMT Context class

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 `SMTConstraintManager`s. 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 `SMTSolverContext`object, which can access the specific context by calling `getContext()`.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

Differential Revision: https://reviews.llvm.org/D49233

Added:
    cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
Modified:
    cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h?rev=337914&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h (added)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h Wed Jul 25 05:49:07 2018
@@ -0,0 +1,30 @@
+//== 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;
+};
+
+} // namespace ento
+} // namespace clang
+
+#endif

Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337914&r1=337913&r2=337914&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:07 2018
@@ -11,6 +11,7 @@
 #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"
 
@@ -63,19 +64,22 @@ public:
   ~Z3Config() { Z3_del_config(Config); }
 }; // end class Z3Config
 
-class Z3Context {
-  Z3_context ZC_P;
-
+class Z3Context : public SMTContext {
 public:
   static Z3_context ZC;
 
-  Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
+  Z3Context() : SMTContext() {
+    Context = Z3_mk_context_rc(Z3Config().Config);
+    ZC = Context;
+  }
 
   ~Z3Context() {
     Z3_del_context(ZC);
-    Z3_finalize_memory();
-    ZC_P = nullptr;
+    Context = nullptr;
   }
+
+protected:
+  Z3_context Context;
 }; // end class Z3Context
 
 class Z3Sort {