From 1a2fb82a5c26ec83fb05d0fa208662cf98f4758b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 19 Nov 2012 19:32:22 -0800 Subject: [PATCH] main/model: move full user-program execution to ModelChecker::run We don't really need the top-level ModelChecker execution loop to be in main.cc; it should be exposed simply as a run() method. --- main.cc | 19 +------------------ model.cc | 22 ++++++++++++++++++++++ model.h | 4 ++++ 3 files changed, 27 insertions(+), 18 deletions(-) diff --git a/main.cc b/main.cc index a577ed2..6456401 100644 --- a/main.cc +++ b/main.cc @@ -104,15 +104,8 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) int main_argc; char **main_argv; -/** Wrapper to run the user's main function, with appropriate arguments */ -void wrapper_user_main(void *) -{ - user_main(main_argc, main_argv); -} - /** The model_main function contains the main model checking loop. */ static void model_main() { - thrd_t user_thread; struct model_params params; param_defaults(¶ms); @@ -130,18 +123,8 @@ static void model_main() { snapshotObject = new SnapshotStack(); model = new ModelChecker(params); - snapshotObject->snapshotStep(0); - do { - /* Start user program */ - model->add_thread(new Thread(&user_thread, &wrapper_user_main, NULL)); - - /* Wait for all threads to complete */ - model->finish_execution(); - } while (model->next_execution()); - - model->print_stats(); - + model->run(); delete model; DEBUG("Exiting\n"); diff --git a/model.cc b/model.cc index fd893c7..4370098 100644 --- a/model.cc +++ b/model.cc @@ -2516,3 +2516,25 @@ void ModelChecker::finish_execution() { while (take_step()); } + +/** Wrapper to run the user's main function, with appropriate arguments */ +void user_main_wrapper(void *) +{ + user_main(model->params.argc, model->params.argv); +} + +/** @brief Run ModelChecker for the user program */ +void ModelChecker::run() +{ + do { + thrd_t user_thread; + + /* Start user program */ + add_thread(new Thread(&user_thread, &user_main_wrapper, NULL)); + + /* Wait for all threads to complete */ + finish_execution(); + } while (next_execution()); + + print_stats(); +} diff --git a/model.h b/model.h index 04e191b..5f389c5 100644 --- a/model.h +++ b/model.h @@ -91,6 +91,8 @@ public: ModelChecker(struct model_params params); ~ModelChecker(); + void run(); + /** @returns the context for the main model-checking system thread */ ucontext_t * get_system_context() { return &system_context; } @@ -252,6 +254,8 @@ private: bool have_bug_reports() const; void print_bugs() const; void print_execution(bool printbugs) const; + + friend void user_main_wrapper(); }; extern ModelChecker *model; -- 2.34.1