Remove GenMC verbosity level settings from Miri, remove MIRI_LOG debug prints

Author: Patrick-6

genmc-sys/src/lib.rs

@@ -26,8 +26,6 @@ impl Default for GenmcParams {
     fn default() -> Self {
         Self {
             print_random_schedule_seed: false,
-            quiet: true,
-            log_level_trace: false,
             do_symmetry_reduction: false,
         }
     }
@@ -41,8 +39,6 @@ mod ffi {
     struct GenmcParams {
         // pub genmc_seed: u64; // OR: Option<u64>
         pub print_random_schedule_seed: bool,
-        pub quiet: bool, // TODO GENMC: maybe make log-level more fine grained
-        pub log_level_trace: bool,
         pub do_symmetry_reduction: bool,
     }
 

genmc-sys/src_cpp/MiriInterface.cpp

@@ -71,21 +71,10 @@ auto MiriGenMCShim::createHandle(const GenmcParams &config)
 	// FIXME(genmc): expose this setting to Miri
 	conf->randomScheduleSeed = "42";
 	conf->printRandomScheduleSeed = config.print_random_schedule_seed;
-	if (config.quiet)
-	{
-		// logLevel = VerbosityLevel::Quiet;
-		// TODO GENMC: error might be better (or new level for `BUG`)
-		// logLevel = VerbosityLevel::Quiet;
-		logLevel = VerbosityLevel::Error;
-	}
-	else if (config.log_level_trace)
-	{
-		logLevel = VerbosityLevel::Trace;
-	}
-	else
-	{
-		logLevel = VerbosityLevel::Tip;
-	}
+
+	// FIXME(genmc): Add support for setting this from the Miri side.
+	// FIXME(genmc): Decide on what to do about warnings from GenMC (keep them disabled until then).
+	logLevel = VerbosityLevel::Error;
 
 	// FIXME(genmc): check if we can enable IPR:
 	conf->ipr = false;
@@ -127,20 +116,14 @@ auto MiriGenMCShim::createHandle(const GenmcParams &config)
 		const auto addr = access.getAddr();
 		if (!driverPtr->initVals_.contains(addr))
 		{
-			MIRI_LOG() << "WARNING: TODO GENMC: requested initial value for address "
-					   << addr << ", but there is none.\n";
 			return SVal(0xCC00CC00);
 			// BUG_ON(!driverPtr->initVals_.contains(addr));
 		}
 		auto result = driverPtr->initVals_[addr];
 		if (!result.is_init)
 		{
-			MIRI_LOG() << "WARNING: TODO GENMC: requested initial value for address "
-					   << addr << ", but the memory is uninitialized.\n";
 			return SVal(0xFF00FF00);
 		}
-		MIRI_LOG() << "MiriGenMCShim: requested initial value for address " << addr
-				   << " == " << addr.get() << ", returning: " << result << "\n";
 		return result.toSVal();
 	};
 	driver->getExec().getGraph().setInitValGetter(initValGetter);
@@ -211,8 +194,6 @@ void MiriGenMCShim::handleThreadJoin(ThreadId thread_id, ThreadId child_id)
 
 void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 {
-	MIRI_LOG() << "GenMC:   handleThreadFinish: thread id: " << thread_id << "\n";
-
 	auto pos = incPos(thread_id);
 	auto retVal = SVal(ret_val);
 
@@ -228,9 +209,7 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 											 MemOrdering ord, GenmcScalar old_val) -> LoadResult
 {
 	auto pos = incPos(thread_id);
-	MIRI_LOG() << "Received Load from Miri at address: " << address << ", size " << size
-			   << " with ordering " << ord << ", event: " << pos << "\n";
-
+	
 	auto loc = SAddr(address);
 	auto aSize = ASize(size);
 	auto type = AType::Unsigned; // FIXME(genmc): get correct type from Miri(?)
@@ -249,10 +228,6 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 														GenmcScalar rhs_value, GenmcScalar old_val)
 	-> ReadModifyWriteResult
 {
-	MIRI_LOG() << "Received Read-Modify-Write from Miri at address: " << address << ", size "
-			   << size << " with orderings (" << loadOrd << ", " << store_ordering
-			   << "), rmw op: " << static_cast<uint64_t>(rmw_op) << "\n";
-
 	auto pos = incPos(thread_id);
 
 	auto loc = SAddr(address);
@@ -288,14 +263,6 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 	MemOrdering success_store_ordering, MemOrdering fail_load_ordering,
 	bool can_fail_spuriously) -> CompareExchangeResult
 {
-
-	MIRI_LOG() << "Received Compare-Exchange from Miri (value: " << expected_value << " --> "
-			   << new_value << ", old value: " << old_val << ") at address: " << address
-			   << ", size " << size << " with success orderings (" << success_load_ordering
-			   << ", " << success_store_ordering
-			   << "), fail load ordering: " << fail_load_ordering
-			   << ", is weak (can fail spuriously): " << can_fail_spuriously << "\n";
-
 	auto pos = incPos(thread_id);
 
 	auto loc = SAddr(address);
@@ -335,10 +302,6 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 											  MemOrdering ord, StoreEventType store_event_type)
 	-> StoreResult
 {
-	MIRI_LOG() << "Received Store from Miri at address " << address << ", size " << size
-			   << " with ordering " << ord << ", is part of rmw: ("
-			   << static_cast<uint64_t>(store_event_type) << ")\n";
-
 	auto pos = incPos(thread_id);
 
 	auto loc = SAddr(address);

genmc-sys/src_cpp/MiriInterface.hpp

@@ -123,52 +123,23 @@ struct MiriGenMCShim : private GenMCDriver
 	 * */
 	void handleOldVal(const SAddr addr, GenmcScalar value)
 	{
-		MIRI_LOG() << "handleOldVal: " << addr << ", " << value.value << ", " << value.extra
-				   << ", " << value.is_init << "\n";
-		// if (!value.is_init) {
-		// 	// // TODO GENMC(uninit value handling)
-		// 	// MIRI_LOG() << "WARNING: got uninitialized old value, ignoring ...\n";
-		// 	// return;
-		// 	MIRI_LOG() << "WARNING: got uninitialized old value, converting to dummy "
-		// 		      "value ...\n";
-		// 	value.is_init = true;
-		// 	value.value = 0xAAFFAAFF;
-		// }
-
 		// TODO GENMC(CLEANUP): Pass this as a parameter:
 		auto &g = getExec().getGraph();
 		auto *coLab = g.co_max(addr);
-		MIRI_LOG() << "handleOldVal: coLab: " << *coLab << "\n";
 		if (auto *wLab = llvm::dyn_cast<WriteLabel>(coLab))
 		{
-			MIRI_LOG()
-				<< "handleOldVal: got WriteLabel, atomic: " << !wLab->isNotAtomic()
-				<< "\n";
-			if (!value.is_init)
-				MIRI_LOG() << "WARNING: TODO GENMC: handleOldVal tried to "
-							  "overwrite value of NA "
-							  "reads-from label, but old value is `uninit`\n";
-			else if (wLab->isNotAtomic())
+			if (value.is_init && wLab->isNotAtomic())
 				wLab->setVal(value.toSVal());
 		}
 		else if (const auto *wLab = llvm::dyn_cast<InitLabel>(coLab))
 		{
 			if (value.is_init)
 			{
 				auto result = initVals_.insert(std::make_pair(addr, value));
-				MIRI_LOG() << "handleOldVal: got InitLabel, insertion result: "
-						   << result.first->second << ", " << result.second << "\n";
 				BUG_ON(result.second &&
 					   (*result.first).second !=
 						   value); /* Attempt to replace initial value */
 			}
-			else
-			{
-				// LOG(VerbosityLevel::Error) <<
-				MIRI_LOG() << "WARNING: TODO GENMC: handleOldVal tried set initial "
-							  "value, but old "
-							  "value is `uninit`\n";
-			}
 		}
 		else
 		{

src/concurrency/genmc/config.rs

@@ -9,11 +9,6 @@ pub struct GenmcConfig {
 }
 
 impl GenmcConfig {
-    fn set_log_level_trace(&mut self) {
-        self.params.quiet = false;
-        self.params.log_level_trace = true;
-    }
-
     /// Function for parsing command line options for GenMC mode.
     ///
     /// All GenMC arguments start with the string "-Zmiri-genmc".
@@ -36,10 +31,7 @@ impl GenmcConfig {
         let Some(trimmed_arg) = trimmed_arg.strip_prefix("-") else {
             return Err(format!("Invalid GenMC argument \"-Zmiri-genmc{trimmed_arg}\""));
         };
-        if trimmed_arg == "log-trace" {
-            // TODO GENMC: maybe expand to allow more control over log level?
-            genmc_config.set_log_level_trace();
-        } else if trimmed_arg == "symmetry-reduction" {
+        if trimmed_arg == "symmetry-reduction" {
             // TODO GENMC (PERFORMANCE): maybe make this the default, have an option to turn it off instead
             genmc_config.params.do_symmetry_reduction = true;
         } else {