From: Brian Norris <banorris@uci.edu>
Date: Thu, 15 Nov 2012 21:50:40 +0000 (-0800)
Subject: assert bugs through common interface
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=1798c510e77f37e3d79cba6a1fdad3b13ccc9674

assert bugs through common interface

- User-provied assertions (MODEL_ASSERT())
- Data races
- Deadlocks
- Unlock before lock

Notably, I have not yet converted the "uninitialized load" bug, because
it actually isn't correct yet. It needs to handle future values and lazy
synchronization better.
---

diff --git a/common.cc b/common.cc
index f4aa7ece..8b5c9971 100644
--- a/common.cc
+++ b/common.cc
@@ -46,9 +46,9 @@ void assert_hook(void)
 void model_assert(bool expr, const char *file, int line)
 {
 	if (!expr) {
-		printf("  [BUG] Program has hit assertion in file %s at line %d\n",
+		char msg[100];
+		sprintf(msg, "Program has hit assertion in file %s at line %d\n",
 				file, line);
-		model->set_assert();
-		model->switch_to_master(NULL);
+		model->assert_bug(msg, true);
 	}
 }
diff --git a/datarace.cc b/datarace.cc
index ac364d79..c2921330 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -102,10 +102,8 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 	unrealizedraces.push_back(race);
 
 	/* If the race is realized, bail out now. */
-	if (checkDataRaces()) {
-		model->set_assert();
-		model->switch_to_master(NULL);
-	}
+	if (checkDataRaces())
+		model->assert_bug("Datarace", true);
 }
 
 /** This function goes through the list of unrealized data races,
diff --git a/model.cc b/model.cc
index a2a0a6d4..417252c3 100644
--- a/model.cc
+++ b/model.cc
@@ -417,7 +417,7 @@ bool ModelChecker::next_execution()
 		num_feasible_executions++;
 
 		if (is_deadlocked())
-			assert_bug("Deadlock detected", false);
+			assert_bug("Deadlock detected");
 
 		print_bugs();
 		checkDataRaces();
@@ -677,10 +677,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 	}
 		//otherwise fall into the lock case
 	case ATOMIC_LOCK: {
-		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
-			printf("Lock access before initialization\n");
-			set_assert();
-		}
+		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+			assert_bug("Lock access before initialization");
 		state->islocked = true;
 		ModelAction *unlock = get_last_unlock(curr);
 		//synchronize with the previous unlock statement
@@ -890,7 +888,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 
 	/* See if we have realized a data race */
 	if (checkDataRaces())
-		set_assert();
+		assert_bug("Datarace");
 }
 
 /**
@@ -1821,9 +1819,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 	}
 
 	// If we resolved promises or data races, see if we have realized a data race.
-	if (checkDataRaces()) {
-		set_assert();
-	}
+	if (checkDataRaces())
+		assert_bug("Datarace");
 
 	return updated;
 }