Remove mixed atomic-non-atomic and 'read from initial value' support.

Author: Patrick-6

genmc-sys/src_cpp/MiriInterface.cpp

@@ -105,18 +105,8 @@ auto MiriGenMCShim::createHandle(const GenmcParams &config)
 	auto *driverPtr = driver.get();
 	auto initValGetter = [driverPtr](const AAccess &access)
 	{
-		const auto addr = access.getAddr();
-		if (!driverPtr->initVals_.contains(addr))
-		{
-			return SVal(0xCC00CC00);
-			// BUG_ON(!driverPtr->initVals_.contains(addr));
-		}
-		auto result = driverPtr->initVals_[addr];
-		if (!result.is_init)
-		{
-			return SVal(0xFF00FF00);
-		}
-		return result.toSVal();
+		// FIXME(genmc): Add proper support for initial values.
+		return SVal(0xff);
 	};
 	driver->getExec().getGraph().setInitValGetter(initValGetter);
 
@@ -214,9 +204,7 @@ void MiriGenMCShim::handleThreadKill(ThreadId thread_id) {
 
 	auto newLab = std::make_unique<ReadLabel>(pos, ord, loc, aSize, type);
 
-	auto oldValSetter = [this, old_val](SAddr loc)
-	{ this->handleOldVal(loc, old_val); };
-	auto result = GenMCDriver::handleLoad(std::move(newLab), oldValSetter);
+	auto result = GenMCDriver::handleLoad(std::move(newLab));
 	return result;
 }
 
@@ -236,13 +224,7 @@ void MiriGenMCShim::handleThreadKill(ThreadId thread_id) {
 
 	std::unique_ptr<WriteLabel> wLab = std::make_unique<WriteLabel>(pos, ord, loc, aSize, type, val);
 
-	auto oldValSetter = [this, old_val](SAddr loc)
-	{
-		this->handleOldVal(loc,
-						   old_val); // TODO GENMC(HACK): is this the correct way to do it?
-	};
-
-	return GenMCDriver::handleStore(std::move(wLab), oldValSetter);
+	return GenMCDriver::handleStore(std::move(wLab));
 }
 
 /**** Memory (de)allocation ****/

genmc-sys/src_cpp/MiriInterface.hpp

@@ -106,42 +106,6 @@ struct MiriGenMCShim : private GenMCDriver
 	static std::unique_ptr<MiriGenMCShim> createHandle(const GenmcParams &config);
 
 private:
-	/**
-	 * @brief Try to insert the initial value of a memory location.
-	 * @param addr
-	 * @param value
-	 * */
-	void handleOldVal(const SAddr addr, GenmcScalar value)
-	{
-		// TODO GENMC(CLEANUP): Pass this as a parameter:
-		auto &g = getExec().getGraph();
-		auto *coLab = g.co_max(addr);
-		if (auto *wLab = llvm::dyn_cast<WriteLabel>(coLab))
-		{
-			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));
-				BUG_ON(result.second &&
-					   (*result.first).second !=
-						   value); /* Attempt to replace initial value */
-			}
-		}
-		else
-		{
-			BUG(); /* Invalid label */
-		}
-		// either initLabel	==> update initValGetter
-		// or WriteLabel    ==> Update its value in place (only if non-atomic)
-	}
-
-	// TODO GENMC(mixed-size accesses):
-	std::unordered_map<SAddr, GenmcScalar> initVals_{};
-
 	std::vector<Action> globalInstructions;
 };