-
-/** @brief Run ModelChecker for the user program */
-void ModelChecker::run()
-{
- //Need to initial random number generator state to avoid resets on rollback
- char random_state[256];
- initstate(423121, random_state, sizeof(random_state));
- checkfree = params.checkthreshold;
- for(int exec = 0;exec < params.maxexecutions;exec++) {
- chosen_thread = init_thread;
- break_execution = false;
- do {
- if (params.traceminsize != 0 &&
- execution->get_curr_seq_num() > checkfree) {
- checkfree += params.checkthreshold;
- execution->collectActions();
- }
-
- thread_chosen = false;
- curr_thread_num = 1;
- Thread *thr = getNextThread();
- if (thr != nullptr) {
- switch_from_master(thr);
- continue;
- }
-
- if (break_execution)
- break;
- if (execution->has_asserted())
- break;
- if (!chosen_thread)
- chosen_thread = get_next_thread();
- if (!chosen_thread || chosen_thread->is_model_thread())
- break;
- if (chosen_thread->just_woken_up()) {
- chosen_thread->set_wakeup_state(false);
- chosen_thread->set_pending(NULL);
- chosen_thread = NULL;
- continue;
- }
-
- /* Consume the next action for a Thread */
- ModelAction *curr = chosen_thread->get_pending();
- chosen_thread->set_pending(NULL);
- chosen_thread = execution->take_step(curr);
- } while (!should_terminate_execution());
-
- finish_execution((exec+1) < params.maxexecutions);
- //restore random number generator state after rollback
- setstate(random_state);
- }
-
- model_print("******* Model-checking complete: *******\n");
- print_stats();
-
- /* Have the trace analyses dump their output. */
- for (unsigned int i = 0;i < trace_analyses.size();i++)
- trace_analyses[i]->finish();
-
- /* unlink tmp file created by last child process */
- char filename[256];
- snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
- unlink(filename);
-}