From 5f3a8d4376e1ed065532d9b70733ee7fc775119a Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Wed, 25 Jul 2018 12:49:07 +0000 Subject: [PATCH] [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` 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 git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@337914 91177308-0d34-0410-b5e6-96231b3b80d8 --- .../Core/PathSensitive/SMTContext.h | 30 +++++++++++++++++++ .../Core/Z3ConstraintManager.cpp | 16 ++++++---- 2 files changed, 40 insertions(+), 6 deletions(-) create mode 100644 include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h new file mode 100644 index 0000000000..01aa1c8b6d --- /dev/null +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h @@ -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 diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 66a6cf5bad..c124159cd0 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -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 { -- 2.40.0