From: weiyu Date: Tue, 15 Sep 2020 23:08:44 +0000 (-0700) Subject: Fix a bug in memcpy, implement memset, and remove model_thread X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=448991da4be411c39be8ce3a56615a8eae2811d3 Fix a bug in memcpy, implement memset, and remove model_thread --- diff --git a/datarace.cc b/datarace.cc index 13aa4655..11811a1a 100644 --- a/datarace.cc +++ b/datarace.cc @@ -865,6 +865,9 @@ Exit: void raceCheckRead64(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT @@ -893,6 +896,7 @@ void raceCheckRead64(thread_id_t thread, const void *location) if (shadow[7]==old_shadowval) shadow[7] = new_shadowval; else goto L7; + RESTORE_MODEL_FLAG(old_flag); return; } @@ -910,10 +914,14 @@ L6: raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 6)); L7: raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 7)); + RESTORE_MODEL_FLAG(old_flag); } void raceCheckRead32(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT @@ -930,6 +938,7 @@ void raceCheckRead32(thread_id_t thread, const void *location) if (shadow[3]==old_shadowval) shadow[3] = new_shadowval; else goto L3; + RESTORE_MODEL_FLAG(old_flag); return; } @@ -939,10 +948,14 @@ L2: raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 2)); L3: raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 3)); + RESTORE_MODEL_FLAG(old_flag); } void raceCheckRead16(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT @@ -952,20 +965,26 @@ void raceCheckRead16(thread_id_t thread, const void *location) if (CHECKBOUNDARY(location, 1)) { if (shadow[1]==old_shadowval) { shadow[1] = new_shadowval; + RESTORE_MODEL_FLAG(old_flag); return; } } raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1)); + RESTORE_MODEL_FLAG(old_flag); } void raceCheckRead8(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT load8_count++; #endif raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval); + RESTORE_MODEL_FLAG(old_flag); } static inline uint64_t * raceCheckWrite_firstIt(thread_id_t thread, const void * location, uint64_t *old_val, uint64_t *new_val) @@ -1110,6 +1129,8 @@ Exit: void raceCheckWrite64(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT @@ -1138,6 +1159,7 @@ void raceCheckWrite64(thread_id_t thread, const void *location) if (shadow[7]==old_shadowval) shadow[7] = new_shadowval; else goto L7; + RESTORE_MODEL_FLAG(old_flag); return; } @@ -1155,10 +1177,14 @@ L6: raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 6)); L7: raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 7)); + RESTORE_MODEL_FLAG(old_flag); } void raceCheckWrite32(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT @@ -1175,6 +1201,7 @@ void raceCheckWrite32(thread_id_t thread, const void *location) if (shadow[3]==old_shadowval) shadow[3] = new_shadowval; else goto L3; + RESTORE_MODEL_FLAG(old_flag); return; } @@ -1184,10 +1211,14 @@ L2: raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 2)); L3: raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 3)); + RESTORE_MODEL_FLAG(old_flag); } void raceCheckWrite16(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT @@ -1198,20 +1229,26 @@ void raceCheckWrite16(thread_id_t thread, const void *location) if (CHECKBOUNDARY(location, 1)) { if (shadow[1]==old_shadowval) { shadow[1] = new_shadowval; + RESTORE_MODEL_FLAG(old_flag); return; } } raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 1)); + RESTORE_MODEL_FLAG(old_flag); } void raceCheckWrite8(thread_id_t thread, const void *location) { + int old_flag = GET_MODEL_FLAG; + ENTER_MODEL_FLAG; + uint64_t old_shadowval, new_shadowval; old_shadowval = new_shadowval = INVALIDSHADOWVAL; #ifdef COLLECT_STAT store8_count++; #endif raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval); + RESTORE_MODEL_FLAG(old_flag); } #ifdef COLLECT_STAT diff --git a/execution.cc b/execution.cc index 4953718d..61d33cb9 100644 --- a/execution.cc +++ b/execution.cc @@ -18,8 +18,6 @@ #include "fuzzer.h" #include "newfuzzer.h" -#define INITIAL_THREAD_ID 0 - #ifdef COLLECT_STAT static unsigned int atomic_load_count = 0; static unsigned int atomic_store_count = 0; @@ -89,8 +87,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ - model_thread = new Thread(get_next_id()); - add_thread(model_thread); fuzzer->register_engine(m, this); scheduler->register_engine(this); #ifdef TLS diff --git a/execution.h b/execution.h index 82d629ce..b8bfb035 100644 --- a/execution.h +++ b/execution.h @@ -19,6 +19,8 @@ #include #include "classlist.h" +#define INITIAL_THREAD_ID 0 + struct PendingFutureValue { PendingFutureValue(ModelAction *writer, ModelAction *reader) : writer(writer), reader(reader) diff --git a/hashtable.h b/hashtable.h index b7cac674..22563a01 100644 --- a/hashtable.h +++ b/hashtable.h @@ -113,7 +113,7 @@ public: /** @brief Reset the table to its initial state. */ void reset() { - memset(table, 0, capacity * sizeof(struct hashlistnode<_Key, _Val>)); + real_memset(table, 0, capacity * sizeof(struct hashlistnode<_Key, _Val>)); if (zero) { _free(zero); zero = NULL; diff --git a/model.cc b/model.cc index 450aac5a..4b94d75a 100644 --- a/model.cc +++ b/model.cc @@ -59,9 +59,11 @@ void install_handler() { void createModelIfNotExist() { if (!model) { + ENTER_MODEL_FLAG; snapshot_system_init(100000); model = new ModelChecker(); model->startChecker(); + EXIT_MODEL_FLAG; } } @@ -73,7 +75,7 @@ ModelChecker::ModelChecker() : history(new ModelHistory()), execution(new ModelExecution(this, scheduler)), execution_number(1), - curr_thread_num(1), + curr_thread_num(INITIAL_THREAD_ID), trace_analyses(), inspect_plugin(NULL) { @@ -82,7 +84,7 @@ ModelChecker::ModelChecker() : "Distributed under the GPLv2\n" "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n"); init_memory_ops(); - memset(&stats,0,sizeof(struct execution_stats)); + real_memset(&stats,0,sizeof(struct execution_stats)); init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL); #ifdef TLS init_thread->setTLS((char *)get_tls_addr()); @@ -351,11 +353,11 @@ void ModelChecker::startRunExecution(Thread *old) { execution->collectActions(); } - curr_thread_num = 1; + curr_thread_num = INITIAL_THREAD_ID; Thread *thr = getNextThread(old); if (thr != nullptr) { scheduler->set_current_thread(thr); - inside_model = 0; + EXIT_MODEL_FLAG; if (Thread::swap(old, thr) < 0) { perror("swap threads"); exit(EXIT_FAILURE); @@ -419,7 +421,7 @@ void ModelChecker::finishRunExecution(Thread *old) scheduler->set_current_thread(NULL); /** Reset curr_thread_num to initial value for next execution. */ - curr_thread_num = 1; + curr_thread_num = INITIAL_THREAD_ID; /** If we have more executions, we won't make it past this call. */ finish_execution(execution_number < params.maxexecutions); @@ -454,7 +456,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act) delete act; return 0; } - inside_model = 1; + ENTER_MODEL_FLAG; DBG(); Thread *old = thread_current(); diff --git a/model.h b/model.h index 331ea18a..9e52f537 100644 --- a/model.h +++ b/model.h @@ -18,6 +18,11 @@ #include "classlist.h" #include "snapshot-interface.h" +#define ENTER_MODEL_FLAG (inside_model = 1) +#define EXIT_MODEL_FLAG (inside_model = 0) +#define GET_MODEL_FLAG (inside_model) +#define RESTORE_MODEL_FLAG(f) (inside_model = f) + /** @brief Model checker execution stats */ struct execution_stats { int num_total; /**< @brief Total number of executions */ diff --git a/mymemory.cc b/mymemory.cc index e82f8d2e..cda63dcc 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -137,31 +137,32 @@ void init_memory_ops() } void * memcpy(void * dst, const void * src, size_t n) { - if (false && model && !inside_model) { + if (model && !inside_model) { + //model_print("memcpy intercepted\n"); thread_id_t tid = thread_current_id(); if (((uintptr_t)src&7) == 0 && ((uintptr_t)dst&7) == 0 && (n&7) == 0) { for (uint i = 0; i < (n>>3); i++) { - raceCheckRead64(tid, (void *)(((char *)src) + i)); + raceCheckRead64(tid, (void *)(((uint64_t *)src) + i)); ((volatile uint64_t *)dst)[i] = ((uint64_t *)src)[i]; - raceCheckWrite64(tid, (void *)(((char *)src) + i)); + raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i)); } } else if (((uintptr_t)src&3) == 0 && ((uintptr_t)dst&3) == 0 && (n&3) == 0) { for (uint i = 0; i < (n>>2); i++) { - raceCheckRead32(tid, (void *)(((char *)src) + i)); + raceCheckRead32(tid, (void *)(((uint32_t *)src) + i)); ((volatile uint32_t *)dst)[i] = ((uint32_t *)src)[i]; - raceCheckWrite32(tid, (void *)(((char *)src) + i)); + raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i)); } } else if (((uintptr_t)src&1) == 0 && ((uintptr_t)dst&1) == 0 && (n&1) == 0) { for (uint i = 0; i < (n>>1); i++) { - raceCheckRead16(tid, (void *)(((char *)src) + i)); + raceCheckRead16(tid, (void *)(((uint16_t *)src) + i)); ((volatile uint16_t *)dst)[i] = ((uint16_t *)src)[i]; - raceCheckWrite16(tid, (void *)(((char *)src) + i)); + raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i)); } } else { for(uint i=0;i>3); i++) { + uint16_t cs2 = cs << 8 | cs; + uint64_t cs3 = cs2 << 16 | cs2; + uint64_t cs4 = cs3 << 32 | cs3; + ((volatile uint64_t *)dst)[i] = cs4; + raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i)); + } + } else if (((uintptr_t)dst&3) == 0 && (n&3) == 0) { + for (uint i = 0; i < (n>>2); i++) { + uint16_t cs2 = cs << 8 | cs; + uint32_t cs3 = cs2 << 16 | cs2; + ((volatile uint32_t *)dst)[i] = cs3; + raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i)); + } + } else if (((uintptr_t)dst&1) == 0 && (n&1) == 0) { + for (uint i = 0; i < (n>>1); i++) { + uint16_t cs2 = cs << 8 | cs; + ((volatile uint16_t *)dst)[i] = cs2; + raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i)); + } + } else { + for (uint i=0;iget_id()); if (threadid >= enabled_len) { enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1)); - memset(&new_enabled[enabled_len], 0, (threadid + 1 - enabled_len) * sizeof(enabled_type_t)); + real_memset(&new_enabled[enabled_len], 0, (threadid + 1 - enabled_len) * sizeof(enabled_type_t)); if (enabled != NULL) { real_memcpy(new_enabled, enabled, enabled_len * sizeof(enabled_type_t)); snapshot_free(enabled); diff --git a/threads.cc b/threads.cc index faa49fc5..024f6ea5 100644 --- a/threads.cc +++ b/threads.cc @@ -419,7 +419,7 @@ Thread::Thread(thread_id_t tid) : last_action_val(0), model_thread(true) { - memset(&context, 0, sizeof(context)); + real_memset(&context, 0, sizeof(context)); } /**