From b92880a5cfb374f4650052ba93919f473075926a Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 6 Nov 2016 22:27:00 -0800 Subject: [PATCH] Adds a C++05 version of unique_ptr. Used this to solve a garbage collection problem caused by memory leaks of heap allocated Parsers. --- src/base/Makefile.am | 1 + src/base/cvc4_unique_ptr.h | 70 +++++++++++++++++++++++++++++++++++++ src/main/driver_unified.cpp | 25 ++++++------- 3 files changed, 82 insertions(+), 14 deletions(-) create mode 100644 src/base/cvc4_unique_ptr.h diff --git a/src/base/Makefile.am b/src/base/Makefile.am index bda063176..94e45c542 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -20,6 +20,7 @@ libbase_la_SOURCES = \ configuration_private.h \ cvc4_assert.cpp \ cvc4_assert.h \ + cvc4_unique_ptr.h \ exception.cpp \ exception.h \ listener.cpp \ diff --git a/src/base/cvc4_unique_ptr.h b/src/base/cvc4_unique_ptr.h new file mode 100644 index 000000000..9642d0185 --- /dev/null +++ b/src/base/cvc4_unique_ptr.h @@ -0,0 +1,70 @@ +/********************* */ +/*! \file cvc4_unique_ptr.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A CVC4 variant of unique_ptr for C++05. + ** + ** A CVC4 variant of unique_ptr for C++05. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__UNIQUE_PTR_H +#define __CVC4__UNIQUE_PTR_H + +namespace CVC4 { + +/** + * A CVC4 variant of unique_ptr for C++05. + * + * This is a variant of unique_ptr that is not designed for move semantics. + * These are appropriate to own pointer allocations on the stack that should be + * deleted when an exception is thrown. These should be used with care within + * heap based data structures, and never as the return value of a function. + */ +template +class UniquePtr { + public: + UniquePtr() : d_pointer(NULL) {} + UniquePtr(T* pointer) : d_pointer(pointer) {} + ~UniquePtr() { delete d_pointer; } + + void reset(T* pointer) { + delete d_pointer; + d_pointer = pointer; + } + + /** Gives up ownership of the pointer to the caller. */ + T* release() { + T* copy = d_pointer; + d_pointer = NULL; + return copy; + } + + /** Returns the pointer. */ + T* get() const { return d_pointer; } + + /** Returns the pointer. Undefined if the pointer is null. */ + T* operator->() const { return d_pointer; } + + /** Returns true if the pointer is not-null. */ + operator bool() const { return d_pointer != NULL; } + + private: + UniquePtr(const UniquePtr*) CVC4_UNDEFINED; + UniquePtr& operator=(const UniquePtr&) CVC4_UNDEFINED; + + /** An owned pointer object allocated by `new` or NULL. */ + T* d_pointer; +}; /* class UniquePtr */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__UNIQUE_PTR_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index bab70e98f..e9e703b5f 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -26,6 +26,7 @@ #include "cvc4autoconfig.h" #include "base/configuration.h" +#include "base/cvc4_unique_ptr.h" #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" @@ -241,7 +242,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } # endif - Parser* replayParser = NULL; + UniquePtr replayParser; if( opts.getReplayInputFilename() != "" ) { std::string replayFilename = opts.getReplayInputFilename(); ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts); @@ -252,8 +253,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { } replayParserBuilder.withStreamInput(cin); } - replayParser = replayParserBuilder.build(); - pExecutor->setReplayStream(new Parser::ExprStream(replayParser)); + replayParser.reset(replayParserBuilder.build()); + pExecutor->setReplayStream(new Parser::ExprStream(replayParser.get())); } int returnValue = 0; @@ -297,7 +298,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { << (Configuration::isAssertionBuild() ? "on" : "off") << endl; } - if(replayParser != NULL) { + if(replayParser) { // have the replay parser use the declarations input interactively replayParser->useDeclarationsFrom(shell.getParser()); } @@ -347,10 +348,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { vector< vector > allCommands; allCommands.push_back(vector()); - Parser *parser = parserBuilder.build(); - if(replayParser != NULL) { + UniquePtr parser(parserBuilder.build()); + if(replayParser) { // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser); + replayParser->useDeclarationsFrom(parser.get()); } int needReset = 0; // true if one of the commands was interrupted @@ -484,8 +485,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { } delete cmd; } - // Remove the parser - delete parser; } else { if(!opts.wasSetByUserIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(false)); @@ -504,10 +503,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ } - Parser *parser = parserBuilder.build(); - if(replayParser != NULL) { + UniquePtr parser(parserBuilder.build()); + if(replayParser) { // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser); + replayParser->useDeclarationsFrom(parser.get()); } bool interrupted = false; while(status || opts.getContinuedExecution()) { @@ -536,8 +535,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { } delete cmd; } - // Remove the parser - delete parser; } Result result; -- 2.30.2