user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #4733 from michaliskok/genmc-bug-fixes

Browse source 
genmc: Bug fixes
This commit is contained in:
Ralf Jung 2025-11-29 12:45:50 +00:00 • committed by GitHub
commit a121102003
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
13 changed files with 530 additions and 509 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/tools/miri/genmc-sys/build.rs
View file

@ -28,7 +28,7 @@ mod downloading {
/// The GenMC repository the we get our commit from.
pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
/// The GenMC commit we depend on. It must be available on the specified GenMC repository.
pub(crate) const GENMC_COMMIT: &str = "aa10ed65117c3291524efc19253b5d443a4602ac";
pub(crate) const GENMC_COMMIT: &str = "22d3d0b44dedb4e8e1aae3330e546465e4664529";
/// Ensure that a local GenMC repo is present and set to the correct commit.
/// Return the path of the GenMC repo and whether the checked out commit was changed.
@ -178,14 +178,8 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
// These are all the C++ files we need to compile, which needs to be updated if more C++ files are added to Miri.
// We use absolute paths since relative paths can confuse IDEs when attempting to go-to-source on a path in a compiler error.
let cpp_files_base_path = Path::new("cpp/src/");
let cpp_files = [
"MiriInterface/EventHandling.cpp",
"MiriInterface/Exploration.cpp",
"MiriInterface/Mutex.cpp",
"MiriInterface/Setup.cpp",
"MiriInterface/ThreadManagement.cpp",
]
.map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
let cpp_files = ["MiriInterface/Exploration.cpp", "MiriInterface/Setup.cpp"]
.map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
let mut bridge = cxx_build::bridge("src/lib.rs");
// FIXME(genmc,cmake): Remove once the GenMC debug setting is available in the config.h file.

5
src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
View file

@ -125,8 +125,11 @@ struct MiriGenmcShim : private GenMCDriver {
void handle_fence(ThreadId thread_id, MemOrdering ord);
/**** Memory (de)allocation ****/
auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
auto handle_free(ThreadId thread_id, uint64_t address) -> bool;
/** Returns null on success, or an error string if an error occurs. */
auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr<std::string>;
/**** Thread management ****/
void handle_thread_create(ThreadId thread_id, ThreadId parent_id);

265
src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
View file

@ -1,265 +0,0 @@
/** This file contains functionality related to handling events encountered
* during an execution, such as loads, stores or memory (de)allocation. */
#include "MiriInterface.hpp"
// CXX.rs generated headers:
#include "genmc-sys/src/lib.rs.h"
// GenMC headers:
#include "ADT/value_ptr.hpp"
#include "ExecutionGraph/EventLabel.hpp"
#include "ExecutionGraph/LoadAnnotation.hpp"
#include "Runtime/InterpreterEnumAPI.hpp"
#include "Static/ModuleID.hpp"
#include "Support/ASize.hpp"
#include "Support/Error.hpp"
#include "Support/Logger.hpp"
#include "Support/MemAccess.hpp"
#include "Support/RMWOps.hpp"
#include "Support/SAddr.hpp"
#include "Support/SVal.hpp"
#include "Support/ThreadInfo.hpp"
#include "Support/Verbosity.hpp"
#include "Verification/GenMCDriver.hpp"
#include "Verification/MemoryModel.hpp"
// C++ headers:
#include <cstddef>
#include <cstdint>
#include <memory>
#include <utility>
/**** Blocking instructions ****/
void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
}
/**** Memory access handling ****/
[[nodiscard]] auto MiriGenmcShim::handle_load(
ThreadId thread_id,
uint64_t address,
uint64_t size,
MemOrdering ord,
GenmcScalar old_val
) -> LoadResult {
// `type` is only used for printing.
const auto type = AType::Unsigned;
const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
thread_id,
GenmcScalarExt::try_to_sval(old_val),
ord,
SAddr(address),
ASize(size),
type
);
if (const auto* err = std::get_if<VerificationError>(&ret))
return LoadResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
if (ret_val == nullptr)
ERROR("Unimplemented: load returned unexpected result.");
return LoadResultExt::from_value(*ret_val);
}
[[nodiscard]] auto MiriGenmcShim::handle_store(
ThreadId thread_id,
uint64_t address,
uint64_t size,
GenmcScalar value,
GenmcScalar old_val,
MemOrdering ord
) -> StoreResult {
const auto pos = inc_pos(thread_id);
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
nullptr,
pos,
GenmcScalarExt::try_to_sval(old_val),
ord,
SAddr(address),
ASize(size),
/* type */ AType::Unsigned, // `type` is only used for printing.
GenmcScalarExt::to_sval(value),
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&ret))
return StoreResultExt::from_error(format_error(*err));
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(
nullptr == is_coherence_order_maximal_write,
"Unimplemented: Store returned unexpected result."
);
return StoreResultExt::ok(*is_coherence_order_maximal_write);
}
void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
const auto pos = inc_pos(thread_id);
GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
}
[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
ThreadId thread_id,
uint64_t address,
uint64_t size,
RMWBinOp rmw_op,
MemOrdering ordering,
GenmcScalar rhs_value,
GenmcScalar old_val
) -> ReadModifyWriteResult {
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
// into a load and a store component. This means we can have for example `AcqRel` loads and
// stores, but this is intended for RMW operations.
// Somewhat confusingly, the GenMC term for RMW read/write labels is
// `FaiRead` and `FaiWrite`.
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
thread_id,
GenmcScalarExt::try_to_sval(old_val),
ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
rmw_op,
GenmcScalarExt::to_sval(rhs_value),
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return ReadModifyWriteResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&load_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
if (nullptr == ret_val) {
ERROR("Unimplemented: read-modify-write returned unexpected result.");
}
const auto read_old_val = *ret_val;
const auto new_value =
executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
const auto storePos = inc_pos(thread_id);
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
nullptr,
storePos,
GenmcScalarExt::try_to_sval(old_val),
ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
new_value
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return ReadModifyWriteResultExt::from_error(format_error(*err));
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(
nullptr == is_coherence_order_maximal_write,
"Unimplemented: RMW store returned unexpected result."
);
return ReadModifyWriteResultExt::ok(
/* old_value: */ read_old_val,
new_value,
*is_coherence_order_maximal_write
);
}
[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange(
ThreadId thread_id,
uint64_t address,
uint64_t size,
GenmcScalar expected_value,
GenmcScalar new_value,
GenmcScalar old_val,
MemOrdering success_ordering,
MemOrdering fail_load_ordering,
bool can_fail_spuriously
) -> CompareExchangeResult {
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
// into a load and a store component. This means we can have for example `AcqRel` loads and
// stores, but this is intended for CAS operations.
// FIXME(GenMC): properly handle failure memory ordering.
auto expectedVal = GenmcScalarExt::to_sval(expected_value);
auto new_val = GenmcScalarExt::to_sval(new_value);
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
thread_id,
GenmcScalarExt::try_to_sval(old_val),
success_ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
expectedVal,
new_val
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return CompareExchangeResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&load_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
const auto read_old_val = *ret_val;
if (read_old_val != expectedVal)
return CompareExchangeResultExt::failure(read_old_val);
// FIXME(GenMC): Add support for modelling spurious failures.
const auto storePos = inc_pos(thread_id);
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
nullptr,
storePos,
GenmcScalarExt::try_to_sval(old_val),
success_ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
new_val
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return CompareExchangeResultExt::from_error(format_error(*err));
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(
nullptr == is_coherence_order_maximal_write,
"Unimplemented: compare-exchange store returned unexpected result."
);
return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write);
}
/**** Memory (de)allocation ****/
auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
-> uint64_t {
const auto pos = inc_pos(thread_id);
// These are only used for printing and features Miri-GenMC doesn't support (yet).
const auto storage_duration = StorageDuration::SD_Heap;
// Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots)
const auto storage_type = StorageType::ST_Volatile;
const auto address_space = AddressSpace::AS_User;
const SVal ret_val = GenMCDriver::handleMalloc(
nullptr,
pos,
size,
alignment,
storage_duration,
storage_type,
address_space,
EventDeps()
);
return ret_val.get();
}
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
const auto pos = inc_pos(thread_id);
GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
// FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
return getResult().status.has_value();
}

435
src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
View file

@ -1,4 +1,5 @@
/** This file contains functionality related to exploration, such as scheduling. */
/** This file contains functionality related to exploration events
* such as loads, stores and memory (de)allocation. */
#include "MiriInterface.hpp"
@ -6,13 +7,32 @@
#include "genmc-sys/src/lib.rs.h"
// GenMC headers:
#include "ADT/value_ptr.hpp"
#include "ExecutionGraph/EventLabel.hpp"
#include "ExecutionGraph/LoadAnnotation.hpp"
#include "Runtime/InterpreterEnumAPI.hpp"
#include "Static/ModuleID.hpp"
#include "Support/ASize.hpp"
#include "Support/Error.hpp"
#include "Support/Logger.hpp"
#include "Support/MemAccess.hpp"
#include "Support/RMWOps.hpp"
#include "Support/SAddr.hpp"
#include "Support/SVal.hpp"
#include "Support/ThreadInfo.hpp"
#include "Support/Verbosity.hpp"
#include "Verification/GenMCDriver.hpp"
#include "Verification/MemoryModel.hpp"
// C++ headers:
#include <cmath>
#include <cstddef>
#include <cstdint>
#include <limits>
#include <memory>
#include <utility>
/** Scheduling */
auto MiriGenmcShim::schedule_next(
const int curr_thread_id,
@ -41,8 +61,6 @@ auto MiriGenmcShim::schedule_next(
);
}
/**** Execution start/end handling ****/
void MiriGenmcShim::handle_execution_start() {
threads_action_.clear();
threads_action_.push_back(Action(ActionKind::Load, Event::getInit()));
@ -50,9 +68,230 @@ void MiriGenmcShim::handle_execution_start() {
}
auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr<std::string> {
// FIXME(genmc): add error handling once GenMC returns an error here.
GenMCDriver::handleExecutionEnd();
return {};
auto ret = GenMCDriver::handleExecutionEnd();
return ret.has_value() ? format_error(*ret) : nullptr;
}
/**** Blocking instructions ****/
void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
}
/**** Memory access handling ****/
[[nodiscard]] auto MiriGenmcShim::handle_load(
ThreadId thread_id,
uint64_t address,
uint64_t size,
MemOrdering ord,
GenmcScalar old_val
) -> LoadResult {
// `type` is only used for printing.
const auto type = AType::Unsigned;
const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
thread_id,
GenmcScalarExt::try_to_sval(old_val),
ord,
SAddr(address),
ASize(size),
type
);
if (const auto* err = std::get_if<VerificationError>(&ret))
return LoadResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(!ret_val, "Unimplemented: load returned unexpected result.");
return LoadResultExt::from_value(*ret_val);
}
[[nodiscard]] auto MiriGenmcShim::handle_store(
ThreadId thread_id,
uint64_t address,
uint64_t size,
GenmcScalar value,
GenmcScalar old_val,
MemOrdering ord
) -> StoreResult {
const auto pos = inc_pos(thread_id);
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
nullptr,
pos,
GenmcScalarExt::try_to_sval(old_val),
ord,
SAddr(address),
ASize(size),
/* type */ AType::Unsigned, // `type` is only used for printing.
GenmcScalarExt::to_sval(value),
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&ret))
return StoreResultExt::from_error(format_error(*err));
const auto* is_co_max = std::get_if<bool>(&ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(!is_co_max, "Unimplemented: Store returned unexpected result.");
return StoreResultExt::ok(*is_co_max);
}
void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
const auto pos = inc_pos(thread_id);
GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
}
[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
ThreadId thread_id,
uint64_t address,
uint64_t size,
RMWBinOp rmw_op,
MemOrdering ordering,
GenmcScalar rhs_value,
GenmcScalar old_val
) -> ReadModifyWriteResult {
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
// into a load and a store component. This means we can have for example `AcqRel` loads and
// stores, but this is intended for RMW operations.
// Somewhat confusingly, the GenMC term for RMW read/write labels is
// `FaiRead` and `FaiWrite`.
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
thread_id,
GenmcScalarExt::try_to_sval(old_val),
ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
rmw_op,
GenmcScalarExt::to_sval(rhs_value),
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return ReadModifyWriteResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&load_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(!ret_val, "Unimplemented: read-modify-write returned unexpected result.");
const auto read_old_val = *ret_val;
const auto new_value =
executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
const auto storePos = inc_pos(thread_id);
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
nullptr,
storePos,
GenmcScalarExt::try_to_sval(old_val),
ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
new_value
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return ReadModifyWriteResultExt::from_error(format_error(*err));
const auto* is_co_max = std::get_if<bool>(&store_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(!is_co_max, "Unimplemented: RMW store returned unexpected result.");
return ReadModifyWriteResultExt::ok(
/* old_value: */ read_old_val,
new_value,
*is_co_max
);
}
[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange(
ThreadId thread_id,
uint64_t address,
uint64_t size,
GenmcScalar expected_value,
GenmcScalar new_value,
GenmcScalar old_val,
MemOrdering success_ordering,
MemOrdering fail_load_ordering,
bool can_fail_spuriously
) -> CompareExchangeResult {
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
// into a load and a store component. This means we can have for example `AcqRel` loads and
// stores, but this is intended for CAS operations.
// FIXME(GenMC): properly handle failure memory ordering.
auto expectedVal = GenmcScalarExt::to_sval(expected_value);
auto new_val = GenmcScalarExt::to_sval(new_value);
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
thread_id,
GenmcScalarExt::try_to_sval(old_val),
success_ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
expectedVal,
new_val
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return CompareExchangeResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&load_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
const auto read_old_val = *ret_val;
if (read_old_val != expectedVal)
return CompareExchangeResultExt::failure(read_old_val);
// FIXME(GenMC): Add support for modelling spurious failures.
const auto storePos = inc_pos(thread_id);
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
nullptr,
storePos,
GenmcScalarExt::try_to_sval(old_val),
success_ordering,
SAddr(address),
ASize(size),
AType::Unsigned, // The type is only used for printing.
new_val
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return CompareExchangeResultExt::from_error(format_error(*err));
const auto* is_co_max = std::get_if<bool>(&store_ret);
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
ERROR_ON(!is_co_max, "Unimplemented: compare-exchange store returned unexpected result.");
return CompareExchangeResultExt::success(read_old_val, *is_co_max);
}
/**** Memory (de)allocation ****/
auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
-> uint64_t {
const auto pos = inc_pos(thread_id);
// These are only used for printing and features Miri-GenMC doesn't support (yet).
const auto storage_duration = StorageDuration::SD_Heap;
// Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots)
const auto storage_type = StorageType::ST_Volatile;
const auto address_space = AddressSpace::AS_User;
const SVal ret_val = GenMCDriver::handleMalloc(
nullptr,
pos,
size,
alignment,
storage_duration,
storage_type,
address_space,
EventDeps()
);
return ret_val.get();
}
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address)
-> std::unique_ptr<std::string> {
auto pos = inc_pos(thread_id);
auto ret = GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
return ret.has_value() ? format_error(*ret) : nullptr;
}
/**** Estimation mode result ****/
@ -66,3 +305,187 @@ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult {
.blocked_execs = static_cast<uint64_t>(res.exploredBlocked),
};
}
/** Mutexes */
struct MutexState {
static constexpr SVal UNLOCKED { 0 };
static constexpr SVal LOCKED { 1 };
static constexpr bool isValid(SVal v) {
return v == UNLOCKED || v == LOCKED;
}
};
auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
-> MutexLockResult {
// This annotation informs GenMC about the condition required to make this lock call succeed.
// It stands for `value_read_by_load != MUTEX_LOCKED`.
const auto size_bits = size * 8;
const auto annot = std::move(Annotation(
AssumeType::Spinloop,
Annotation::ExprVP(
NeExpr<ModuleID::ID>::create(
// `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
// The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
// other variables from previous expressions that may be used here.
RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
ConcreteExpr<ModuleID::ID>::create(size_bits, MutexState::LOCKED)
)
.release()
)
));
// As usual, we need to tell GenMC which value was stored at this location before this atomic
// access, if there previously was a non-atomic initializing access. We set the initial state of
// a mutex to be "unlocked".
const auto old_val = MutexState::UNLOCKED;
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
thread_id,
old_val,
address,
size,
annot,
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return MutexLockResultExt::from_error(format_error(*err));
// If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it
// would not acquire the mutex. Like the handling of the case further down where we read a `1`
// ("Mutex already locked"), Miri should call the handle function again once the current thread
// is scheduled by GenMC the next time.
if (std::holds_alternative<Reset>(load_ret))
return MutexLockResultExt::reset();
const auto* ret_val = std::get_if<SVal>(&load_ret);
ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1");
if (*ret_val == MutexState::LOCKED) {
// We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
// it. GenMC determines this based on the annotation we pass with the load further up in
// this function, namely when that load will read a value other than `MutexState::LOCKED`.
this->handle_assume_block(thread_id, AssumeType::Spinloop);
return MutexLockResultExt::ok(false);
}
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
nullptr,
inc_pos(thread_id),
old_val,
address,
size,
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return MutexLockResultExt::from_error(format_error(*err));
// We don't update Miri's memory for this operation so we don't need to know if the store
// was the co-maximal store, but we still check that we at least get a boolean as the result
// of the store.
const auto* is_co_max = std::get_if<bool>(&store_ret);
ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result.");
return MutexLockResultExt::ok(true);
}
auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
-> MutexLockResult {
auto& currPos = threads_action_[thread_id].event;
// As usual, we need to tell GenMC which value was stored at this location before this atomic
// access, if there previously was a non-atomic initializing access. We set the initial state of
// a mutex to be "unlocked".
const auto old_val = MutexState::UNLOCKED;
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
nullptr,
++currPos,
old_val,
SAddr(address),
ASize(size)
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return MutexLockResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&load_ret);
ERROR_ON(!ret_val, "Unimplemented: mutex trylock load returned unexpected result.");
ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1");
if (*ret_val == MutexState::LOCKED)
return MutexLockResultExt::ok(false); /* Lock already held. */
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
nullptr,
++currPos,
old_val,
SAddr(address),
ASize(size)
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return MutexLockResultExt::from_error(format_error(*err));
// We don't update Miri's memory for this operation so we don't need to know if the store was
// co-maximal, but we still check that we get a boolean result.
const auto* is_co_max = std::get_if<bool>(&store_ret);
ERROR_ON(!is_co_max, "Unimplemented: store part of mutex try_lock returned unexpected result.");
return MutexLockResultExt::ok(true);
}
auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
-> StoreResult {
const auto pos = inc_pos(thread_id);
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
nullptr,
pos,
// As usual, we need to tell GenMC which value was stored at this location before this
// atomic access, if there previously was a non-atomic initializing access. We set the
// initial state of a mutex to be "unlocked".
/* old_val */ MutexState::UNLOCKED,
MemOrdering::Release,
SAddr(address),
ASize(size),
AType::Signed,
/* store_value */ MutexState::UNLOCKED,
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&ret))
return StoreResultExt::from_error(format_error(*err));
const auto* is_co_max = std::get_if<bool>(&ret);
ERROR_ON(!is_co_max, "Unimplemented: store part of mutex unlock returned unexpected result.");
return StoreResultExt::ok(*is_co_max);
}
/** Thread creation/joining */
void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) {
// NOTE: The threadCreate event happens in the parent:
const auto pos = inc_pos(parent_id);
// FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
const unsigned fun_id = 0;
const SVal arg = SVal(0);
const ThreadInfo child_info =
ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
// Sanity check the thread id, which is the index in the `threads_action_` array.
BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
}
void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
// The thread join event happens in the parent.
const auto pos = inc_pos(thread_id);
const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
// If the join failed, decrease the event index again:
if (!std::holds_alternative<SVal>(ret)) {
dec_pos(thread_id);
}
// FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
// NOTE: Thread return value is ignored, since Miri doesn't need it.
}
void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
const auto pos = inc_pos(thread_id);
GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
}
void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
const auto pos = inc_pos(thread_id);
GenMCDriver::handleThreadKill(nullptr, pos);
}

163
src/tools/miri/genmc-sys/cpp/src/MiriInterface/Mutex.cpp
View file

@ -1,163 +0,0 @@
/** This file contains functionality related to handling mutexes. */
#include "MiriInterface.hpp"
// GenMC headers:
#include "Static/ModuleID.hpp"
// CXX.rs generated headers:
#include "genmc-sys/src/lib.rs.h"
#define MUTEX_UNLOCKED SVal(0)
#define MUTEX_LOCKED SVal(1)
auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
-> MutexLockResult {
// This annotation informs GenMC about the condition required to make this lock call succeed.
// It stands for `value_read_by_load != MUTEX_LOCKED`.
const auto size_bits = size * 8;
const auto annot = std::move(Annotation(
AssumeType::Spinloop,
Annotation::ExprVP(
NeExpr<ModuleID::ID>::create(
// `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
// The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
// other variables from previous expressions that may be used here.
RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED)
)
.release()
)
));
// As usual, we need to tell GenMC which value was stored at this location before this atomic
// access, if there previously was a non-atomic initializing access. We set the initial state of
// a mutex to be "unlocked".
const auto old_val = MUTEX_UNLOCKED;
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
thread_id,
old_val,
address,
size,
annot,
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return MutexLockResultExt::from_error(format_error(*err));
// If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it
// would not acquire the mutex. Like the handling of the case further down where we read a `1`
// ("Mutex already locked"), Miri should call the handle function again once the current thread
// is scheduled by GenMC the next time.
if (std::holds_alternative<Reset>(load_ret))
return MutexLockResultExt::reset();
const auto* ret_val = std::get_if<SVal>(&load_ret);
ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
ERROR_ON(
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
"Mutex read value was neither 0 nor 1"
);
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
if (is_lock_acquired) {
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
nullptr,
inc_pos(thread_id),
old_val,
address,
size,
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return MutexLockResultExt::from_error(format_error(*err));
// We don't update Miri's memory for this operation so we don't need to know if the store
// was the co-maximal store, but we still check that we at least get a boolean as the result
// of the store.
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
ERROR_ON(
nullptr == is_coherence_order_maximal_write,
"Unimplemented: store part of mutex try_lock returned unexpected result."
);
} else {
// We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
// it. GenMC determines this based on the annotation we pass with the load further up in
// this function, namely when that load will read a value other than `MUTEX_LOCKED`.
this->handle_assume_block(thread_id, AssumeType::Spinloop);
}
return MutexLockResultExt::ok(is_lock_acquired);
}
auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
-> MutexLockResult {
auto& currPos = threads_action_[thread_id].event;
// As usual, we need to tell GenMC which value was stored at this location before this atomic
// access, if there previously was a non-atomic initializing access. We set the initial state of
// a mutex to be "unlocked".
const auto old_val = MUTEX_UNLOCKED;
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
nullptr,
++currPos,
old_val,
SAddr(address),
ASize(size)
);
if (const auto* err = std::get_if<VerificationError>(&load_ret))
return MutexLockResultExt::from_error(format_error(*err));
const auto* ret_val = std::get_if<SVal>(&load_ret);
if (nullptr == ret_val) {
ERROR("Unimplemented: mutex trylock load returned unexpected result.");
}
ERROR_ON(
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
"Mutex read value was neither 0 nor 1"
);
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
if (!is_lock_acquired) {
return MutexLockResultExt::ok(false); /* Lock already held. */
}
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
nullptr,
++currPos,
old_val,
SAddr(address),
ASize(size)
);
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return MutexLockResultExt::from_error(format_error(*err));
// We don't update Miri's memory for this operation so we don't need to know if the store was
// co-maximal, but we still check that we get a boolean result.
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
ERROR_ON(
nullptr == is_coherence_order_maximal_write,
"Unimplemented: store part of mutex try_lock returned unexpected result."
);
return MutexLockResultExt::ok(true);
}
auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
-> StoreResult {
const auto pos = inc_pos(thread_id);
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
nullptr,
pos,
// As usual, we need to tell GenMC which value was stored at this location before this
// atomic access, if there previously was a non-atomic initializing access. We set the
// initial state of a mutex to be "unlocked".
/* old_val */ MUTEX_UNLOCKED,
MemOrdering::Release,
SAddr(address),
ASize(size),
AType::Signed,
/* store_value */ MUTEX_UNLOCKED,
EventDeps()
);
if (const auto* err = std::get_if<VerificationError>(&ret))
return StoreResultExt::from_error(format_error(*err));
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
ERROR_ON(
nullptr == is_coherence_order_maximal_write,
"Unimplemented: store part of mutex unlock returned unexpected result."
);
return StoreResultExt::ok(*is_coherence_order_maximal_write);
}

56
src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp
View file

@ -1,56 +0,0 @@
/** This file contains functionality related thread management (creation, finishing, join, etc.) */
#include "MiriInterface.hpp"
// CXX.rs generated headers:
#include "genmc-sys/src/lib.rs.h"
// GenMC headers:
#include "Support/Error.hpp"
#include "Support/Verbosity.hpp"
// C++ headers:
#include <cstdint>
void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) {
// NOTE: The threadCreate event happens in the parent:
const auto pos = inc_pos(parent_id);
// FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
const unsigned fun_id = 0;
const SVal arg = SVal(0);
const ThreadInfo child_info =
ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
// NOTE: Default memory ordering (`Release`) used here.
const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
// Sanity check the thread id, which is the index in the `threads_action_` array.
BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
}
void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
// The thread join event happens in the parent.
const auto pos = inc_pos(thread_id);
// NOTE: Default memory ordering (`Acquire`) used here.
const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
// If the join failed, decrease the event index again:
if (!std::holds_alternative<SVal>(ret)) {
dec_pos(thread_id);
}
// FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
// NOTE: Thread return value is ignored, since Miri doesn't need it.
}
void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
const auto pos = inc_pos(thread_id);
// NOTE: Default memory ordering (`Release`) used here.
GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
}
void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
const auto pos = inc_pos(thread_id);
GenMCDriver::handleThreadKill(nullptr, pos);
}

6
src/tools/miri/genmc-sys/src/lib.rs
View file

@ -438,7 +438,11 @@ mod ffi {
alignment: u64,
) -> u64;
/// Returns true if an error was found.
fn handle_free(self: Pin<&mut MiriGenmcShim>, thread_id: i32, address: u64) -> bool;
fn handle_free(
self: Pin<&mut MiriGenmcShim>,
thread_id: i32,
address: u64,
) -> UniquePtr<CxxString>;
/**** Thread management ****/
fn handle_thread_create(self: Pin<&mut MiriGenmcShim>, thread_id: i32, parent_id: i32);

15
src/tools/miri/src/concurrency/genmc/mod.rs
View file

@ -592,9 +592,11 @@ impl GenmcCtx {
genmc_size,
alignment.bytes(),
);
if chosen_address == 0 {
throw_exhaust!(AddressSpaceFull);
}
// Non-global addresses should not be in the global address space or null.
assert_ne!(0, chosen_address, "GenMC malloc returned nullptr.");
// Non-global addresses should not be in the global address space.
assert_eq!(0, chosen_address & GENMC_GLOBAL_ADDRESSES_MASK);
// Sanity check the address alignment:
assert!(
@ -622,15 +624,14 @@ impl GenmcCtx {
!self.get_alloc_data_races(),
"memory deallocation with data race checking disabled."
);
if self
let free_result = self
.handle
.borrow_mut()
.pin_mut()
.handle_free(self.active_thread_genmc_tid(machine), address.bytes())
{
.handle_free(self.active_thread_genmc_tid(machine), address.bytes());
if let Some(error) = free_result.as_ref() {
// FIXME(genmc): improve error handling.
// An error was detected, so we get the error string from GenMC.
throw_ub_format!("{}", self.try_get_error().unwrap());
throw_ub_format!("{}", error.to_string_lossy());
}
interp_ok(())

4
src/tools/miri/src/diagnostics.rs
View file

@ -362,6 +362,10 @@ pub fn report_result<'tcx>(
vec![
note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
],
ResourceExhaustion(ResourceExhaustionInfo::AddressSpaceFull) if ecx.machine.data_race.as_genmc_ref().is_some() =>
vec![
note!("in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused")
],
UndefinedBehavior(AlignmentCheckFailed { .. })
if ecx.machine.check_alignment == AlignmentCheck::Symbolic
=>

26
src/tools/miri/tests/genmc/fail/simple/alloc_large.multiple.stderr Normal file
View file

@ -0,0 +1,26 @@
Running GenMC Verification...
error: resource exhaustion: there are no more free addresses in the address space
--> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
|
LL | AllocInit::Uninitialized => alloc.allocate(layout),
| ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here
|
= help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused
= note: BACKTRACE:
= note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
= note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
= note: inside `alloc::raw_vec::RawVec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
= note: inside `std::vec::Vec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `std::vec::Vec::<u8>::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
note: inside `miri_start`
--> tests/genmc/fail/simple/alloc_large.rs:LL:CC
|
LL | let _v = Vec::<u8>::with_capacity(1024 * 1024 * 1024);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

24
src/tools/miri/tests/genmc/fail/simple/alloc_large.rs Normal file
View file

@ -0,0 +1,24 @@
//@revisions: single multiple
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
//@error-in-other-file: resource exhaustion
// Ensure that we emit a proper error if GenMC fails to fulfill an allocation.
// Two variants: one for a single large allocation, one for multiple ones
// that are individually below the limit, but together are too big.
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
if cfg!(multiple) {
for _i in 1..8 {
let _v = Vec::<u8>::with_capacity(1024 * 1024 * 1024);
}
} else {
let _v = Vec::<u8>::with_capacity(8 * 1024 * 1024 * 1024);
}
0
}

26
src/tools/miri/tests/genmc/fail/simple/alloc_large.single.stderr Normal file
View file

@ -0,0 +1,26 @@
Running GenMC Verification...
error: resource exhaustion: there are no more free addresses in the address space
--> RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
|
LL | AllocInit::Uninitialized => alloc.allocate(layout),
| ^^^^^^^^^^^^^^^^^^^^^^ resource exhaustion occurred here
|
= help: in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused
= note: BACKTRACE:
= note: inside `alloc::raw_vec::RawVecInner::try_allocate_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
= note: inside `alloc::raw_vec::RawVecInner::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
= note: inside `alloc::raw_vec::RawVec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/raw_vec/mod.rs:LL:CC
= note: inside `std::vec::Vec::<u8>::with_capacity_in` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `std::vec::Vec::<u8>::with_capacity` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
note: inside `miri_start`
--> tests/genmc/fail/simple/alloc_large.rs:LL:CC
|
LL | let _v = Vec::<u8>::with_capacity(8 * 1024 * 1024 * 1024);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

2
src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs
View file

@ -67,7 +67,7 @@ macro_rules! test_rmw_edge_cases {
x.store(10, ORD);
assert_eq(10, x.fetch_add(<$int>::MAX, ORD)); // definitely overflows, so new value of x is smaller than 10
assert_eq(<$int>::MAX.wrapping_add(10), x.fetch_max(10, ORD)); // new value of x should be 10
// assert_eq(10, x.load(ORD)); // FIXME(genmc,#4572): enable this check once GenMC correctly handles min/max truncation.
assert_eq(10, x.load(ORD));
}};
}