diff options
author | Tim King <taking@cs.nyu.edu> | 2016-11-09 17:04:02 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-11-09 17:04:02 -0800 |
commit | fd24718e1d1127e648f789920fb413da3118d998 (patch) | |
tree | 3cef485dbe92e5b0d200d314e844545de1714692 | |
parent | 9db0ef7df43a067a0063a3652f0acd54e982ba13 (diff) | |
parent | 831f2b7176bc3db49e2fb354918a71df896ad63a (diff) |
Merge pull request #103 from timothy-king/uniq-ptr
Adds a C++05 version of unique_ptr. Used this to solve a garbage coll…
-rw-r--r-- | src/base/Makefile.am | 3 | ||||
-rw-r--r-- | src/base/ptr_closer.h | 73 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 2 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 25 |
4 files changed, 87 insertions, 16 deletions
diff --git a/src/base/Makefile.am b/src/base/Makefile.am index bda063176..bf919cd81 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -26,7 +26,8 @@ libbase_la_SOURCES = \ listener.h \ modal_exception.h \ output.cpp \ - output.h + output.h \ + ptr_closer.h diff --git a/src/base/ptr_closer.h b/src/base/ptr_closer.h new file mode 100644 index 000000000..9c40eee4b --- /dev/null +++ b/src/base/ptr_closer.h @@ -0,0 +1,73 @@ +/********************* */ +/*! \file ptr_closer.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 class to close owned pointers in the destructor. + ** + ** A class to close owned pointers in the destructor. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PTR_CLOSER_H +#define __CVC4__PTR_CLOSER_H + +namespace CVC4 { + +/** + * A class to close owned pointers in the destructor. This plays a similar role + * to unique_ptr, but without move semantics. This is designed to overcome the + * lack of having unique_ptr in 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 T> +class PtrCloser { + public: + PtrCloser() : d_pointer(NULL) {} + explicit PtrCloser(T* pointer) : d_pointer(pointer) {} + ~PtrCloser() { delete d_pointer; } + + /** Deletes the currently owned copy and takes ownership of pointer. */ + void reset(T* pointer = NULL) { + 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: + PtrCloser(const PtrCloser*) CVC4_UNDEFINED; + PtrCloser& operator=(const PtrCloser&) CVC4_UNDEFINED; + + /** An owned pointer object allocated by `new`. Or NULL. */ + T* d_pointer; +}; /* class PtrCloser */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__PTR_CLOSER_H */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 75521e901..1c03cf407 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -338,7 +338,7 @@ ${metakind_operatorKinds} }/* CVC4::kind namespace */ -#line 341 "${template}" +#line 342 "${template}" namespace theory { diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index bab70e98f..e43c8a6ee 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -27,6 +27,7 @@ #include "base/configuration.h" #include "base/output.h" +#include "base/ptr_closer.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" #include "main/command_executor.h" @@ -241,7 +242,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } # endif - Parser* replayParser = NULL; + PtrCloser<Parser> 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<Command*> > allCommands; allCommands.push_back(vector<Command*>()); - Parser *parser = parserBuilder.build(); - if(replayParser != NULL) { + PtrCloser<Parser> 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) { + PtrCloser<Parser> 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; |