Merge branch 'master' of /home/git/random-fuzzer into thread-switch

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 090743a49ff0ce6da1a1627acdd1367ebdc5c0ac..a37e00521ea7761608db62b32cec81faadbcf5c4 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -26,6 +26,37 @@ void placeholder(void *) {
        ASSERT(0);
 }
 
+#include <signal.h>
+
+#define SIGSTACKSIZE 65536
+static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
+{
+       model_print("Segmentation fault at %p\n", si->si_addr);
+       model_print("For debugging, place breakpoint at: %s:%d\n",
+                                                       __FILE__, __LINE__);
+       print_trace();  // Trace printing may cause dynamic memory allocation
+       while(1)
+               ;
+}
+
+void install_handler() {
+       stack_t ss;
+       ss.ss_sp = model_malloc(SIGSTACKSIZE);
+       ss.ss_size = SIGSTACKSIZE;
+       ss.ss_flags = 0;
+       sigaltstack(&ss, NULL);
+       struct sigaction sa;
+       sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
+       sigemptyset(&sa.sa_mask);
+       sa.sa_sigaction = mprot_handle_pf;
+
+       if (sigaction(SIGSEGV, &sa, NULL) == -1) {
+               perror("sigaction(SIGSEGV)");
+               exit(EXIT_FAILURE);
+       }
+
+}
+
 /** @brief Constructor */
 ModelChecker::ModelChecker() :
        /* Initialize default scheduler */
@@ -54,8 +85,7 @@ ModelChecker::ModelChecker() :
        parse_options(&params);
        initRaceDetector();
        /* Configure output redirection for the model-checker */
-       redirect_output();
-       install_trace_analyses(get_execution());
+       install_handler();
 }
 
 /** @brief Destructor */
@@ -262,6 +292,7 @@ void ModelChecker::finish_execution(bool more_executions)
        execution_number ++;
        if (more_executions)
                reset_to_initial_state();
+
        history->set_new_exec_flag();
 }
 
@@ -346,7 +377,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 
 void ModelChecker::startRunExecution(Thread *old) 
 {
-
        if (params.traceminsize != 0 &&
                        execution->get_curr_seq_num() > checkfree) {
                checkfree += params.checkthreshold;
@@ -390,12 +420,12 @@ Thread* ModelChecker::getNextThread()
                if (act && execution->is_enabled(thr) && !execution->check_action_enabled(act)) {
                        scheduler->sleep(thr);
                }
-
-       chooseThread(act, thr);
+               chooseThread(act, thr);
        }
        return nextThread;
 }
 
+/* Swap back to system_context and terminate this execution */
 void ModelChecker::finishRunExecution(Thread *old) 
 {
        scheduler->set_current_thread(NULL);
@@ -515,9 +545,9 @@ void ModelChecker::handleChosenThread(Thread *old)
                chosen_thread->set_pending(NULL);
                chosen_thread = NULL;
                // Allow this thread to stash the next pending action
-               if (should_terminate_execution())
-                       finishRunExecution(th);
-               else
+//             if (should_terminate_execution())
+//                     finishRunExecution(th);
+//             else
                        startRunExecution(th);
        } else {
                /* Consume the next action for a Thread */
@@ -538,6 +568,9 @@ static void runChecker() {
 void ModelChecker::startChecker() {
        startExecution(get_system_context(), runChecker);
        snapshot = take_snapshot();
+
+       install_trace_analyses(get_execution());
+       redirect_output();
        initMainThread();
 }
 
@@ -566,8 +599,6 @@ void ModelChecker::run()
                        if (break_execution)
                                break;
 
-                       thread_chosen = false;
-                       curr_thread_num = 1;
                        startRunExecution(NULL);
                } while (!should_terminate_execution());