f73377062c7a09b6e4108d56cb5421b7674785a2
[c11tester.git] / model.cc
1 #include <stdio.h>
2 #include <algorithm>
3 #include <new>
4 #include <stdarg.h>
5 #include <string.h>
6 #include <cstdlib>
7
8 #include "model.h"
9 #include "action.h"
10 #include "schedule.h"
11 #include "snapshot-interface.h"
12 #include "common.h"
13 #include "datarace.h"
14 #include "threads-model.h"
15 #include "output.h"
16 #include "traceanalysis.h"
17 #include "execution.h"
18 #include "history.h"
19 #include "bugmessage.h"
20 #include "params.h"
21 #include "plugins.h"
22
23 ModelChecker *model = NULL;
24 int inside_model = 0;
25
26 void placeholder(void *) {
27         ASSERT(0);
28 }
29
30 #include <signal.h>
31
32 #define SIGSTACKSIZE 65536
33 static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
34 {
35         model_print("Segmentation fault at %p\n", si->si_addr);
36         model_print("For debugging, place breakpoint at: %s:%d\n",
37                                                         __FILE__, __LINE__);
38         print_trace();  // Trace printing may cause dynamic memory allocation
39         while(1)
40                 ;
41 }
42
43 void install_handler() {
44         stack_t ss;
45         ss.ss_sp = model_malloc(SIGSTACKSIZE);
46         ss.ss_size = SIGSTACKSIZE;
47         ss.ss_flags = 0;
48         sigaltstack(&ss, NULL);
49         struct sigaction sa;
50         sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
51         sigemptyset(&sa.sa_mask);
52         sa.sa_sigaction = mprot_handle_pf;
53
54         if (sigaction(SIGSEGV, &sa, NULL) == -1) {
55                 perror("sigaction(SIGSEGV)");
56                 exit(EXIT_FAILURE);
57         }
58 }
59
60 void createModelIfNotExist() {
61         if (!model) {
62                 ENTER_MODEL_FLAG;
63                 snapshot_system_init(100000);
64                 model = new ModelChecker();
65                 model->startChecker();
66                 EXIT_MODEL_FLAG;
67         }
68 }
69
70 /** @brief Constructor */
71 ModelChecker::ModelChecker() :
72         /* Initialize default scheduler */
73         params(),
74         scheduler(new Scheduler()),
75         history(new ModelHistory()),
76         execution(new ModelExecution(this, scheduler)),
77         execution_number(1),
78         curr_thread_num(MAIN_THREAD_ID),
79         trace_analyses(),
80         inspect_plugin(NULL)
81 {
82         model_print("C11Tester\n"
83                                                         "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
84                                                         "Distributed under the GPLv2\n"
85                                                         "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
86         init_memory_ops();
87         real_memset(&stats,0,sizeof(struct execution_stats));
88         init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL);
89 #ifdef TLS
90         init_thread->setTLS((char *)get_tls_addr());
91 #endif
92         execution->add_thread(init_thread);
93         scheduler->set_current_thread(init_thread);
94         register_plugins();
95         execution->setParams(&params);
96         param_defaults(&params);
97         parse_options(&params);
98         initRaceDetector();
99         /* Configure output redirection for the model-checker */
100         install_handler();
101 }
102
103 /** @brief Destructor */
104 ModelChecker::~ModelChecker()
105 {
106         delete scheduler;
107 }
108
109 /** Method to set parameters */
110 model_params * ModelChecker::getParams() {
111         return &params;
112 }
113
114 /**
115  * Restores user program to initial state and resets all model-checker data
116  * structures.
117  */
118 void ModelChecker::reset_to_initial_state()
119 {
120
121         /**
122          * FIXME: if we utilize partial rollback, we will need to free only
123          * those pending actions which were NOT pending before the rollback
124          * point
125          */
126         for (unsigned int i = 0;i < get_num_threads();i++)
127                 delete get_thread(int_to_id(i))->get_pending();
128
129         snapshot_roll_back(snapshot);
130 }
131
132 /** @return the number of user threads created during this execution */
133 unsigned int ModelChecker::get_num_threads() const
134 {
135         return execution->get_num_threads();
136 }
137
138 /**
139  * Must be called from user-thread context (e.g., through the global
140  * thread_current() interface)
141  *
142  * @return The currently executing Thread.
143  */
144 Thread * ModelChecker::get_current_thread() const
145 {
146         return scheduler->get_current_thread();
147 }
148
149 /**
150  * Must be called from user-thread context (e.g., through the global
151  * thread_current_id() interface)
152  *
153  * @return The id of the currently executing Thread.
154  */
155 thread_id_t ModelChecker::get_current_thread_id() const
156 {
157         ASSERT(int_to_id(curr_thread_num) == get_current_thread()->get_id());
158         return int_to_id(curr_thread_num);
159 }
160
161 /**
162  * @brief Choose the next thread to execute.
163  *
164  * This function chooses the next thread that should execute. It can enforce
165  * execution replay/backtracking or, if the model-checker has no preference
166  * regarding the next thread (i.e., when exploring a new execution ordering),
167  * we defer to the scheduler.
168  *
169  * @return The next chosen thread to run, if any exist. Or else if the current
170  * execution should terminate, return NULL.
171  */
172 Thread * ModelChecker::get_next_thread()
173 {
174
175         /*
176          * Have we completed exploring the preselected path? Then let the
177          * scheduler decide
178          */
179         return scheduler->select_next_thread();
180 }
181
182 /**
183  * @brief Assert a bug in the executing program.
184  *
185  * Use this function to assert any sort of bug in the user program. If the
186  * current trace is feasible (actually, a prefix of some feasible execution),
187  * then this execution will be aborted, printing the appropriate message. If
188  * the current trace is not yet feasible, the error message will be stashed and
189  * printed if the execution ever becomes feasible.
190  *
191  * @param msg Descriptive message for the bug (do not include newline char)
192  * @return True if bug is immediately-feasible
193  */
194 void ModelChecker::assert_bug(const char *msg, ...)
195 {
196         char str[800];
197
198         va_list ap;
199         va_start(ap, msg);
200         vsnprintf(str, sizeof(str), msg, ap);
201         va_end(ap);
202
203         execution->assert_bug(str);
204 }
205
206 /**
207  * @brief Assert a bug in the executing program, asserted by a user thread
208  * @see ModelChecker::assert_bug
209  * @param msg Descriptive message for the bug (do not include newline char)
210  */
211 void ModelChecker::assert_user_bug(const char *msg)
212 {
213         /* If feasible bug, bail out now */
214         assert_bug(msg);
215         switch_thread(NULL);
216 }
217
218 /** @brief Print bug report listing for this execution (if any bugs exist) */
219 void ModelChecker::print_bugs() const
220 {
221         SnapVector<bug_message *> *bugs = execution->get_bugs();
222
223         model_print("Bug report: %zu bug%s detected\n",
224                                                         bugs->size(),
225                                                         bugs->size() > 1 ? "s" : "");
226         for (unsigned int i = 0;i < bugs->size();i++)
227                 (*bugs)[i] -> print();
228 }
229
230 /**
231  * @brief Record end-of-execution stats
232  *
233  * Must be run when exiting an execution. Records various stats.
234  * @see struct execution_stats
235  */
236 void ModelChecker::record_stats()
237 {
238         stats.num_total ++;
239         if (execution->have_bug_reports())
240                 stats.num_buggy_executions ++;
241         else if (execution->is_complete_execution())
242                 stats.num_complete ++;
243         else {
244                 //All threads are sleeping
245                 /**
246                  * @todo We can violate this ASSERT() when fairness/sleep sets
247                  * conflict to cause an execution to terminate, e.g. with:
248                  * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
249                  */
250                 //ASSERT(scheduler->all_threads_sleeping());
251         }
252 }
253
254 /** @brief Print execution stats */
255 void ModelChecker::print_stats() const
256 {
257         model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
258         model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
259         model_print("Total executions: %d\n", stats.num_total);
260 }
261
262 /**
263  * @brief End-of-exeuction print
264  * @param printbugs Should any existing bugs be printed?
265  */
266 void ModelChecker::print_execution(bool printbugs) const
267 {
268         model_print("Program output from execution %d:\n",
269                                                         get_execution_number());
270         print_program_output();
271
272         if (params.verbose >= 3) {
273                 print_stats();
274         }
275
276         /* Don't print invalid bugs */
277         if (printbugs && execution->have_bug_reports()) {
278                 model_print("\n");
279                 print_bugs();
280         }
281
282         model_print("\n");
283         execution->print_summary();
284 }
285
286 /**
287  * Queries the model-checker for more executions to explore and, if one
288  * exists, resets the model-checker state to execute a new execution.
289  *
290  * @return If there are more executions to explore, return true. Otherwise,
291  * return false.
292  */
293 void ModelChecker::finish_execution(bool more_executions)
294 {
295         DBG();
296         /* Is this execution a feasible execution that's worth bug-checking? */
297         bool complete = (execution->is_complete_execution() ||
298                                                                          execution->have_bug_reports());
299
300         /* End-of-execution bug checks */
301         if (complete) {
302                 if (execution->is_deadlocked())
303                         assert_bug("Deadlock detected");
304
305                 run_trace_analyses();
306         }
307
308         record_stats();
309         /* Output */
310         if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
311                 print_execution(complete);
312         else
313                 clear_program_output();
314
315         execution_number ++;
316         history->set_new_exec_flag();
317
318         if (more_executions)
319                 reset_to_initial_state();
320 }
321
322 /** @brief Run trace analyses on complete trace */
323 void ModelChecker::run_trace_analyses() {
324         for (unsigned int i = 0;i < trace_analyses.size();i ++)
325                 trace_analyses[i] -> analyze(execution->get_action_trace());
326 }
327
328 /**
329  * @brief Get a Thread reference by its ID
330  * @param tid The Thread's ID
331  * @return A Thread reference
332  */
333 Thread * ModelChecker::get_thread(thread_id_t tid) const
334 {
335         return execution->get_thread(tid);
336 }
337
338 /**
339  * @brief Get a reference to the Thread in which a ModelAction was executed
340  * @param act The ModelAction
341  * @return A Thread reference
342  */
343 Thread * ModelChecker::get_thread(const ModelAction *act) const
344 {
345         return execution->get_thread(act);
346 }
347
348 void ModelChecker::startRunExecution(Thread *old) {
349         while (true) {
350                 if (params.traceminsize != 0 &&
351                                 execution->get_curr_seq_num() > checkfree) {
352                         checkfree += params.checkthreshold;
353                         execution->collectActions();
354                 }
355
356                 curr_thread_num = MAIN_THREAD_ID;
357                 Thread *thr = getNextThread(old);
358                 if (thr != nullptr) {
359                         scheduler->set_current_thread(thr);
360                         EXIT_MODEL_FLAG;
361                         if (Thread::swap(old, thr) < 0) {
362                                 perror("swap threads");
363                                 exit(EXIT_FAILURE);
364                         }
365                         return;
366                 }
367
368                 if (!handleChosenThread(old)) {
369                         return;
370                 }
371         }
372 }
373
374 Thread* ModelChecker::getNextThread(Thread *old)
375 {
376         Thread *nextThread = nullptr;
377         for (unsigned int i = curr_thread_num;i < get_num_threads();i++) {
378                 thread_id_t tid = int_to_id(i);
379                 Thread *thr = get_thread(tid);
380
381                 if (!thr->is_complete()) {
382                         if (!thr->get_pending()) {
383                                 curr_thread_num = i;
384                                 nextThread = thr;
385                                 break;
386                         }
387                 } else if (thr != old && !thr->is_freed()) {
388                         thr->freeResources();
389                 }
390
391                 ModelAction *act = thr->get_pending();
392                 if (act && scheduler->is_enabled(tid)){
393                         /* Don't schedule threads which should be disabled */
394                         if (!execution->check_action_enabled(act)) {
395                                 scheduler->sleep(thr);
396                         }
397
398                         /* Allow pending relaxed/release stores or thread actions to perform first */
399                         else if (!chosen_thread) {
400                                 if (act->is_write()) {
401                                         std::memory_order order = act->get_mo();
402                                         if (order == std::memory_order_relaxed || \
403                                                         order == std::memory_order_release) {
404                                                 chosen_thread = thr;
405                                         }
406                                 } else if (act->get_type() == THREAD_CREATE || \
407                                                                          act->get_type() == PTHREAD_CREATE || \
408                                                                          act->get_type() == THREAD_START || \
409                                                                          act->get_type() == THREAD_FINISH) {
410                                         chosen_thread = thr;
411                                 }
412                         }
413                 }
414         }
415         return nextThread;
416 }
417
418 /* Swap back to system_context and terminate this execution */
419 void ModelChecker::finishRunExecution(Thread *old)
420 {
421         scheduler->set_current_thread(NULL);
422
423         /** Reset curr_thread_num to initial value for next execution. */
424         curr_thread_num = MAIN_THREAD_ID;
425
426         /** If we have more executions, we won't make it past this call. */
427         finish_execution(execution_number < params.maxexecutions);
428
429
430         /** We finished the final execution.  Print stuff and exit. */
431         model_print("******* Model-checking complete: *******\n");
432         print_stats();
433
434         /* Have the trace analyses dump their output. */
435         for (unsigned int i = 0;i < trace_analyses.size();i++)
436                 trace_analyses[i]->finish();
437
438         /* unlink tmp file created by last child process */
439         char filename[256];
440         snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
441         unlink(filename);
442
443         /* Exit. */
444         _Exit(0);
445 }
446
447 uint64_t ModelChecker::switch_thread(ModelAction *act)
448 {
449         if (modellock) {
450                 static bool fork_message_printed = false;
451
452                 if (!fork_message_printed) {
453                         model_print("Fork handler or dead thread trying to call into model checker...\n");
454                         fork_message_printed = true;
455                 }
456                 delete act;
457                 return 0;
458         }
459         ENTER_MODEL_FLAG;
460
461         DBG();
462         Thread *old = thread_current();
463         old->set_state(THREAD_READY);
464
465         ASSERT(!old->get_pending());
466
467         if (inspect_plugin != NULL) {
468                 inspect_plugin->inspectModelAction(act);
469         }
470
471         old->set_pending(act);
472
473         if (old->is_waiting_on(old))
474                 assert_bug("Deadlock detected (thread %u)", curr_thread_num);
475
476         Thread* next = getNextThread(old);
477         if (next != nullptr) {
478                 scheduler->set_current_thread(next);
479                 if (Thread::swap(old, next) < 0) {
480                         perror("swap threads");
481                         exit(EXIT_FAILURE);
482                 }
483         } else {
484                 if (handleChosenThread(old)) {
485                         startRunExecution(old);
486                 }
487         }
488         return old->get_return_value();
489 }
490
491 bool ModelChecker::handleChosenThread(Thread *old)
492 {
493         if (execution->has_asserted()) {
494                 finishRunExecution(old);
495                 return false;
496         }
497         if (!chosen_thread) {
498                 chosen_thread = get_next_thread();
499         }
500         if (!chosen_thread) {
501                 finishRunExecution(old);
502                 return false;
503         }
504         if (chosen_thread->just_woken_up()) {
505                 chosen_thread->set_wakeup_state(false);
506                 chosen_thread->set_pending(NULL);
507                 chosen_thread = NULL;
508                 // Allow this thread to stash the next pending action
509                 return true;
510         }
511
512         // Consume the next action for a Thread
513         ModelAction *curr = chosen_thread->get_pending();
514         chosen_thread->set_pending(NULL);
515         chosen_thread = execution->take_step(curr);
516
517         if (should_terminate_execution()) {
518                 finishRunExecution(old);
519                 return false;
520         } else {
521                 return true;
522         }
523 }
524
525 void ModelChecker::startChecker() {
526         startExecution();
527         //Need to initial random number generator state to avoid resets on rollback
528         initstate(423121, random_state, sizeof(random_state));
529
530         snapshot = take_snapshot();
531
532         //reset random number generator state
533         setstate(random_state);
534
535         install_trace_analyses(get_execution());
536         redirect_output();
537         initMainThread();
538 }
539
540 bool ModelChecker::should_terminate_execution()
541 {
542         if (execution->have_bug_reports()) {
543                 execution->set_assert();
544                 return true;
545         } else if (execution->isFinished()) {
546                 return true;
547         }
548         return false;
549 }