diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/main | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 89 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 2 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 3 |
3 files changed, 83 insertions, 11 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index df71f13c9..9035ed8b8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -298,8 +298,21 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the declarations input interactively replayParser->useDeclarationsFrom(shell.getParser()); } - while((cmd = shell.readCommand())) { + + while(true) { + try { + cmd = shell.readCommand(); + } catch(UnsafeInterruptException& e) { + *opts[options::out] << CommandInterrupted(); + break; + } + if (cmd == NULL) + break; status = pExecutor->doCommand(cmd) && status; + if (cmd->interrupted()) { + delete cmd; + break; + } delete cmd; } } else if(opts[options::tearDownIncremental]) { @@ -332,15 +345,34 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool needReset = false; - while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { + // true if one of the commands was interrupted + bool interrupted = false; + while (status || opts[options::continuedExecution]) { + if (interrupted) { + *opts[options::out] << CommandInterrupted(); + break; + } + + try { + cmd = parser->nextCommand(); + if (cmd == NULL) break; + } catch (UnsafeInterruptException& e) { + interrupted = true; + continue; + } + if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + if (interrupted) break; + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } @@ -351,29 +383,44 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if(dynamic_cast<PopCommand*>(cmd) != NULL) { allCommands.pop_back(); // fixme leaks cmds here pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } + if (interrupted) continue; *opts[options::out] << CommandSuccess(); } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || dynamic_cast<QueryCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } } + if (interrupted) { + continue; + } + status = pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + continue; + } needReset = true; } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) { pExecutor->doCommand(cmd); @@ -396,6 +443,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { allCommands.back().push_back(copy); } status = pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + continue; + } + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; break; @@ -428,8 +480,27 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { + bool interrupted = false; + while(status || opts[options::continuedExecution]) { + if (interrupted) { + *opts[options::out] << CommandInterrupted(); + pExecutor->reset(); + break; + } + try { + cmd = parser->nextCommand(); + if (cmd == NULL) break; + } catch (UnsafeInterruptException& e) { + interrupted = true; + continue; + } + status = pExecutor->doCommand(cmd); + if (cmd->interrupted() && status == 0) { + interrupted = true; + break; + } + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; break; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 0aee195e4..3b237f6a4 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -172,7 +172,7 @@ InteractiveShell::~InteractiveShell() { #endif /* HAVE_LIBREADLINE */ } -Command* InteractiveShell::readCommand() { +Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) { char* lineBuf = NULL; string line = ""; diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 43054f980..ef55919a1 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -19,6 +19,7 @@ #include <string> #include "util/language.h" +#include "util/unsafe_interrupt_exception.h" #include "options/options.h" namespace CVC4 { @@ -56,7 +57,7 @@ public: * Read a command from the interactive shell. This will read as * many lines as necessary to parse a well-formed command. */ - Command* readCommand(); + Command* readCommand() throw (UnsafeInterruptException); /** * Return the internal parser being used. |