Fix snapshot code

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 5625f30ca8b637e362ebe49203394e52fe9d9e11..3bac9039b4822475bb0226adcf4fd85cc8008ea1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2,6 +2,7 @@
 #include <algorithm>
 #include <new>
 #include <stdarg.h>
+#include <string.h>
 
 #include "model.h"
 #include "action.h"
@@ -22,14 +23,18 @@ ModelChecker *model;
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
        params(params),
+       restart_flag(false),
+       exit_flag(false),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
        execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),
-       trace_analyses()
+       trace_analyses(),
+       inspect_plugin(NULL)
 {
+       memset(&stats,0,sizeof(struct execution_stats));
 }
 
 /** @brief Destructor */
@@ -241,7 +246,8 @@ void ModelChecker::print_stats() const
        model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
        model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
        model_print("Total executions: %d\n", stats.num_total);
-       model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
+       if (params.verbose)
+               model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
 }
 
 /**
@@ -254,7 +260,7 @@ void ModelChecker::print_execution(bool printbugs) const
                        get_execution_number());
        print_program_output();
 
-       if (params.verbose >= 2) {
+       if (params.verbose >= 3) {
                model_print("\nEarliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
                        earliest_diverge->print();
@@ -297,12 +303,15 @@ bool ModelChecker::next_execution()
 
                checkDataRaces();
                run_trace_analyses();
+       } else if (inspect_plugin && !execution->is_complete_execution() &&
+               (execution->too_many_steps())) {
+                inspect_plugin->analyze(execution->get_action_trace());
        }
 
        record_stats();
 
        /* Output */
-       if (params.verbose || (complete && execution->have_bug_reports()))
+       if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
                print_execution(complete);
        else
                clear_program_output();
@@ -310,6 +319,14 @@ bool ModelChecker::next_execution()
        if (complete)
                earliest_diverge = NULL;
 
+       if (restart_flag) {
+               do_restart();
+               return true;
+       }
+
+       if (exit_flag)
+               return false;
+
        if ((diverge = execution->get_next_backtrack()) == NULL)
                return false;
 
@@ -320,6 +337,9 @@ bool ModelChecker::next_execution()
 
        execution_number++;
 
+       if (params.maxexecutions != 0 && stats.num_complete >= params.maxexecutions)
+               return false;
+
        reset_to_initial_state();
        return true;
 }
@@ -380,6 +400,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
+       if (inspect_plugin != NULL) {
+               inspect_plugin->inspectModelAction(act);
+       }
        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
@@ -409,9 +432,35 @@ bool ModelChecker::should_terminate_execution()
        return false;
 }
 
+/** @brief Exit ModelChecker upon returning to the run loop of the
+ *     model checker. */
+void ModelChecker::exit_model_checker()
+{
+       exit_flag = true;
+}
+
+/** @brief Restart ModelChecker upon returning to the run loop of the
+ *     model checker. */
+void ModelChecker::restart()
+{
+       restart_flag = true;
+}
+
+void ModelChecker::do_restart()
+{
+       restart_flag = false;
+       diverge = NULL;
+       earliest_diverge = NULL;
+       reset_to_initial_state();
+       node_stack->full_reset();
+       memset(&stats,0,sizeof(struct execution_stats));
+       execution_number = 1;
+}
+
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
+       bool has_next;
        do {
                thrd_t user_thread;
                Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL);
@@ -459,7 +508,17 @@ void ModelChecker::run()
                        t = execution->take_step(curr);
                } while (!should_terminate_execution());
 
-       } while (next_execution());
+               has_next = next_execution();
+               if (inspect_plugin != NULL && !has_next) {
+                       inspect_plugin->actionAtModelCheckingFinish();
+                       // Check if the inpect plugin set the restart flag
+                       if (restart_flag) {
+                               model_print("******* Model-checking RESTART: *******\n");
+                               has_next = true;
+                               do_restart();
+                       }
+               }
+       } while (has_next);
 
        execution->fixup_release_sequences();