From: Brian Norris <banorris@uci.edu>
Date: Tue, 20 Nov 2012 03:32:22 +0000 (-0800)
Subject: main/model: move full user-program execution to ModelChecker::run
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1a2fb82a5c26ec83fb05d0fa208662cf98f4758b;p=cdsspec-compiler.git

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.
---

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(&params);
@@ -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;