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 { _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits