From: weiyu <weiyuluo1232@gmail.com>
Date: Thu, 11 Jul 2019 23:48:50 +0000 (-0700)
Subject: Merge branch 'new_fuzzer' into branch-weiyu
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=7db53a974507e129e6b32980c97f9759d1390711;hp=080c029c02600d44ad7d797c8e373d4df899f9b0

Merge branch 'new_fuzzer' into branch-weiyu
---

diff --git a/cmodelint.cc b/cmodelint.cc
index f71c0f7e..c42ffe41 100644
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -363,7 +363,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) {
 
 void cds_func_entry(const char * funcName) {
 	if (!model) return;
-
+	/*
 	Thread * th = thread_current();
 	uint32_t func_id;
 
@@ -384,11 +384,12 @@ void cds_func_entry(const char * funcName) {
 	}
 
 	history->enter_function(func_id, th->get_id());
+	*/
 }
 
 void cds_func_exit(const char * funcName) {
 	if (!model) return;
-
+	/*
 	Thread * th = thread_current();
 	uint32_t func_id;
 
@@ -396,4 +397,5 @@ void cds_func_exit(const char * funcName) {
 	func_id = history->getFuncMap()->get(funcName);
 
 	history->exit_function(func_id, th->get_id());
+	*/
 }
diff --git a/librace.cc b/librace.cc
index a9bb7052..64133304 100644
--- a/librace.cc
+++ b/librace.cc
@@ -6,6 +6,7 @@
 #include "datarace.h"
 #include "model.h"
 #include "threads-model.h"
+#include "snapshot-interface.h"
 
 void store_8(void *addr, uint8_t val)
 {
@@ -101,6 +102,8 @@ uint64_t load_64(const void *addr)
 void cds_store8(void *addr)
 {
 	//DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
+	if (!model)
+		return;
 	thread_id_t tid = thread_current()->get_id();
 	raceCheckWrite(tid, addr);
 }
@@ -108,6 +111,8 @@ void cds_store8(void *addr)
 void cds_store16(void *addr)
 {
 	//DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
+	if (!model)
+		return;
 	thread_id_t tid = thread_current()->get_id();
 	raceCheckWrite(tid, addr);
 	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
@@ -116,6 +121,8 @@ void cds_store16(void *addr)
 void cds_store32(void *addr)
 {
 	//DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
+	if (!model)
+		return;
 	thread_id_t tid = thread_current()->get_id();
 	raceCheckWrite(tid, addr);
 	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
@@ -126,6 +133,8 @@ void cds_store32(void *addr)
 void cds_store64(void *addr)
 {
 	//DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
+	if (!model)
+		return;
 	thread_id_t tid = thread_current()->get_id();
 	raceCheckWrite(tid, addr);
 	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
@@ -137,7 +146,41 @@ void cds_store64(void *addr)
 	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 7));
 }
 
-void cds_load8(const void *addr) { load_8(addr); }
-void cds_load16(const void *addr) { load_16(addr); }
-void cds_load32(const void *addr) { load_32(addr); }
-void cds_load64(const void *addr) { load_64(addr); }
+void cds_load8(const void *addr) {
+	if (!model)
+		return;
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckRead(tid, addr);
+}
+
+void cds_load16(const void *addr) {
+	if (!model)
+		return;
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckRead(tid, addr);
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 1));
+}
+
+void cds_load32(const void *addr) {
+	if (!model)
+		return;
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckRead(tid, addr);
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 1));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 2));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 3));
+}
+
+void cds_load64(const void *addr) {
+	if (!model)
+		return;
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckRead(tid, addr);
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 1));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 2));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 3));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 4));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 5));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 6));
+	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 7));
+}
diff --git a/main.cc b/main.cc
index a484f497..80ac52ac 100644
--- a/main.cc
+++ b/main.cc
@@ -198,8 +198,6 @@ int main(int argc, char **argv)
 	model_params *params = model->getParams();
 	parse_options(params, main_argc, main_argv);
 
-	//Initialize race detector
-	initRaceDetector();
 
 	snapshot_stack_init();
 	install_trace_analyses(model->get_execution());
diff --git a/model.cc b/model.cc
index 17916954..6214e9bc 100644
--- a/model.cc
+++ b/model.cc
@@ -45,6 +45,7 @@ ModelChecker::ModelChecker() :
 	scheduler->set_current_thread(init_thread);
 	execution->setParams(&params);
 	param_defaults(&params);
+	initRaceDetector();
 }
 
 /** @brief Destructor */