diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-29 17:48:46 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-29 17:48:46 +0000 |
commit | 4801f553640a7005eb26e89a1635f16669a13631 (patch) | |
tree | 8368cff83b51a6bfe0541962c8239b7e0d365d26 /src | |
parent | 304bdf18169ab0070ddbd6d4c9ebea8be46314b1 (diff) |
Fix a few segfaults in driver.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src')
-rw-r--r-- | src/main/command_executor.h | 2 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 193 | ||||
-rwxr-xr-x | src/options/mkoptions | 2 |
3 files changed, 103 insertions, 94 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index a5bd78abe..38a20b1cb 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -40,6 +40,8 @@ protected: public: CommandExecutor(ExprManager &exprMgr, Options &options); + virtual ~CommandExecutor() {} + /** * Executes a command. Recursively handles if cmd is a command * sequence. Eventually uses doCommandSingleton (which can be diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 3eba7ff6a..8f8e19f81 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -63,7 +63,7 @@ namespace CVC4 { const char *progName; /** A pointer to the CommandExecutor (the signal handlers need it) */ - CVC4::main::CommandExecutor* pExecutor; + CVC4::main::CommandExecutor* pExecutor = NULL; }/* CVC4::main namespace */ }/* CVC4 namespace */ @@ -185,24 +185,21 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Create the expression manager using appropriate options # ifndef PORTFOLIO_BUILD - ExprManager exprMgr(opts); + ExprManager* exprMgr = new ExprManager(opts); # else vector<Options> threadOpts = parseThreadSpecificOptions(opts); - ExprManager exprMgr(threadOpts[0]); + ExprManager* exprMgr = new ExprManager(threadOpts[0]); # endif # ifndef PORTFOLIO_BUILD - CommandExecutor cmdExecutor(exprMgr, opts); + pExecutor = new CommandExecutor(*exprMgr, opts); # else - CommandExecutorPortfolio cmdExecutor(exprMgr, opts, threadOpts); + pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); # endif - // give access to the signal handlers for stats output - pExecutor = &cmdExecutor; - Parser* replayParser = NULL; if( opts[options::replayFilename] != "" ) { - ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts); + ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts); if( opts[options::replayFilename] == "-") { if( inputFromStdin ) { @@ -217,114 +214,122 @@ int runCvc4(int argc, char* argv[], Options& opts) { *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1); } - // Timer statistic - RegisterStatistic statTotalTime(&cmdExecutor.getStatisticsRegistry(), &s_totalTime); - - // Filename statistics - ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(&cmdExecutor.getStatisticsRegistry(), &s_statFilename); - - // Parse and execute commands until we are done - Command* cmd; - bool status = true; - if( opts[options::interactive] ) { - InteractiveShell shell(exprMgr, opts); - Message() << Configuration::getPackageName() - << " " << Configuration::getVersionString(); - if(Configuration::isSubversionBuild()) { - Message() << " [" << Configuration::getSubversionId() << "]"; - } - Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") - << " assertions:" - << (Configuration::isAssertionBuild() ? "on" : "off") - << endl; - if(replayParser != NULL) { - // have the replay parser use the declarations input interactively - replayParser->useDeclarationsFrom(shell.getParser()); - } - while((cmd = shell.readCommand())) { - status = cmdExecutor.doCommand(cmd) && status; - delete cmd; - } - } else { - ParserBuilder parserBuilder(&exprMgr, filename, opts); + int returnValue = 0; + { + // Timer statistic + RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), &s_totalTime); + + // Filename statistics + ReferenceStat< const char* > s_statFilename("filename", filename); + RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename); + + // Parse and execute commands until we are done + Command* cmd; + bool status = true; + if( opts[options::interactive] ) { + InteractiveShell shell(*exprMgr, opts); + Message() << Configuration::getPackageName() + << " " << Configuration::getVersionString(); + if(Configuration::isSubversionBuild()) { + Message() << " [" << Configuration::getSubversionId() << "]"; + } + Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") + << " assertions:" + << (Configuration::isAssertionBuild() ? "on" : "off") + << endl; + if(replayParser != NULL) { + // have the replay parser use the declarations input interactively + replayParser->useDeclarationsFrom(shell.getParser()); + } + while((cmd = shell.readCommand())) { + status = pExecutor->doCommand(cmd) && status; + delete cmd; + } + } else { + ParserBuilder parserBuilder(exprMgr, filename, opts); - if( inputFromStdin ) { + if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) - parserBuilder.withStreamInput(cin); + parserBuilder.withStreamInput(cin); #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ - parserBuilder.withLineBufferedStreamInput(cin); + parserBuilder.withLineBufferedStreamInput(cin); #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ - } + } - Parser *parser = parserBuilder.build(); - if(replayParser != NULL) { - // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser); - } - while(status && (cmd = parser->nextCommand())) { - if(dynamic_cast<QuitCommand*>(cmd) != NULL) { + Parser *parser = parserBuilder.build(); + if(replayParser != NULL) { + // have the replay parser use the file's declarations + replayParser->useDeclarationsFrom(parser); + } + while(status && (cmd = parser->nextCommand())) { + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { + delete cmd; + break; + } + status = pExecutor->doCommand(cmd); delete cmd; - break; } - status = cmdExecutor.doCommand(cmd); - delete cmd; + // Remove the parser + delete parser; } - // Remove the parser - delete parser; - } - if( opts[options::replayStream] != NULL ) { - // this deletes the expression parser too - delete opts[options::replayStream]; - opts.set(options::replayStream, NULL); - } + if( opts[options::replayStream] != NULL ) { + // this deletes the expression parser too + delete opts[options::replayStream]; + opts.set(options::replayStream, NULL); + } - int returnValue; - string result = "unknown"; - if(status) { - result = cmdExecutor.getSmtEngineStatus(); + string result = "unknown"; + if(status) { + result = pExecutor->getSmtEngineStatus(); - if(result == "sat") { - returnValue = 10; - } else if(result == "unsat") { - returnValue = 20; + if(result == "sat") { + returnValue = 10; + } else if(result == "unsat") { + returnValue = 20; + } else { + returnValue = 0; + } } else { - returnValue = 0; + // there was some kind of error + returnValue = 1; } - } else { - // there was some kind of error - returnValue = 1; - } #ifdef CVC4_COMPETITION_MODE - // exit, don't return (don't want destructors to run) - // _exit() from unistd.h doesn't run global destructors - // or other on_exit/atexit stuff. - _exit(returnValue); + // exit, don't return (don't want destructors to run) + // _exit() from unistd.h doesn't run global destructors + // or other on_exit/atexit stuff. + _exit(returnValue); #endif /* CVC4_COMPETITION_MODE */ - ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(&cmdExecutor.getStatisticsRegistry(), &s_statSatResult); + ReferenceStat< Result > s_statSatResult("sat/unsat", result); + RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult); - s_totalTime.stop(); + s_totalTime.stop(); - // Set the global executor pointer to NULL first. If we get a - // signal while dumping statistics, we don't want to try again. - pExecutor = NULL; - if(opts[options::statistics]) { - cmdExecutor.flushStatistics(*opts[options::err]); - } + // Set the global executor pointer to NULL first. If we get a + // signal while dumping statistics, we don't want to try again. + if(opts[options::statistics]) { + pExecutor->flushStatistics(*opts[options::err]); + } #ifdef CVC4_DEBUG - if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) { - _exit(returnValue); - } + if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) { + _exit(returnValue); + } #else /* CVC4_DEBUG */ - if(opts[options::earlyExit]) { - _exit(returnValue); - } + if(opts[options::earlyExit]) { + _exit(returnValue); + } #endif /* CVC4_DEBUG */ + } + + // On exceptional exit, these are leaked, but that's okay... they + // need to be around in that case for main() to print statistics. + delete pExecutor; + delete exprMgr; + + pExecutor = NULL; return returnValue; } diff --git a/src/options/mkoptions b/src/options/mkoptions index 79ef35f5b..ffaff9927 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -852,6 +852,8 @@ function handle_alias { # false positive: =SOMETHING, where SOMETHING != ARG linkarg= fi + else + linkarg= fi links="$links #line $lineno \"$kf\" |