Skip to content

Miri-GenMC API refactor #4959

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
michaliskok wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Miri-GenMC API refactor #4959

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c279e09
genmc: Use per-operation status enums instead of unions with bools
michaliskok Apr 12, 2026
251b4fe
genmc: Rename *Ext factory namespaces to Make* and drop from_ prefix
michaliskok Apr 12, 2026
1b923f4
genmc: Use std::visit with overloaded{} for HandleResult dispatch
michaliskok Apr 12, 2026
be4509d
genmc: Add GenmcHandleResult<T> to collapse 3-field status checks
michaliskok Apr 12, 2026
b4d11e3
genmc/build,cpp: Flatten genmc-sys/cpp/src/ folder
michaliskok Apr 12, 2026
5f76116
genmc: Rename MiriGenmcShim to MiriGenMCInterface
michaliskok Apr 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 44 additions & 48 deletions genmc-sys/cpp/include/MiriInterface.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ struct GenmcScalar;
struct SchedulingResult;
struct EstimationResult;
struct LoadResult;
struct NonAtomicResult;
struct StoreResult;
struct ReadModifyWriteResult;
struct CompareExchangeResult;
Expand Down Expand Up @@ -94,7 +95,7 @@ struct MiriGenmcShim : private GenMCDriver {
MemOrdering ord,
GenmcScalar old_val
);
[[nodiscard]] LoadResult
[[nodiscard]] NonAtomicResult
handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size);
[[nodiscard]] ReadModifyWriteResult handle_read_modify_write(
ThreadId thread_id,
Expand Down Expand Up @@ -124,7 +125,7 @@ struct MiriGenmcShim : private GenMCDriver {
GenmcScalar old_val,
MemOrdering ord
);
[[nodiscard]] StoreResult
[[nodiscard]] NonAtomicResult
handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size);

void handle_fence(ThreadId thread_id, MemOrdering ord);
Expand Down Expand Up @@ -278,47 +279,54 @@ inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
} // namespace GenmcScalarExt

namespace LoadResultExt {
inline LoadResult no_value() {
return LoadResult {
.invalid = false,
.error = std::unique_ptr<std::string>(nullptr),
.read_value = GenmcScalarExt::uninit(),
};
}

inline LoadResult from_value(SVal read_value) {
return LoadResult { .invalid = false,
.error = std::unique_ptr<std::string>(nullptr),
return LoadResult { .status = OperationStatus::Ok,
.error = nullptr,
.read_value = GenmcScalarExt::from_sval(read_value) };
}

inline LoadResult from_error(std::unique_ptr<std::string> error) {
return LoadResult { .invalid = false,
return LoadResult { .status = OperationStatus::Error,
.error = std::move(error),
.read_value = GenmcScalarExt::uninit() };
}

inline LoadResult from_invalid() {
return LoadResult { .invalid = true, .error = nullptr, .read_value = GenmcScalarExt::uninit() };
return LoadResult { .status = OperationStatus::Invalid,
.error = nullptr,
.read_value = GenmcScalarExt::uninit() };
}

} // namespace LoadResultExt

namespace NonAtomicResultExt {
inline NonAtomicResult ok() {
return NonAtomicResult { .status = OperationStatus::Ok, .error = nullptr };
}

inline NonAtomicResult from_error(std::unique_ptr<std::string> error) {
return NonAtomicResult { .status = OperationStatus::Error, .error = std::move(error) };
}

inline NonAtomicResult from_invalid() {
return NonAtomicResult { .status = OperationStatus::Invalid, .error = nullptr };
}
} // namespace NonAtomicResultExt

namespace StoreResultExt {
inline StoreResult ok(bool is_coherence_order_maximal_write) {
return StoreResult { .invalid = false,
.error = std::unique_ptr<std::string>(nullptr),
return StoreResult { .status = OperationStatus::Ok,
.error = nullptr,
.is_coherence_order_maximal_write = is_coherence_order_maximal_write };
}

inline StoreResult from_error(std::unique_ptr<std::string> error) {
return StoreResult { .invalid = false,
return StoreResult { .status = OperationStatus::Error,
.error = std::move(error),
.is_coherence_order_maximal_write = false };
}

inline StoreResult from_invalid() {
return StoreResult { .invalid = true,
return StoreResult { .status = OperationStatus::Invalid,
.error = nullptr,
.is_coherence_order_maximal_write = false };
}
Expand All @@ -327,24 +335,24 @@ inline StoreResult from_invalid() {
namespace ReadModifyWriteResultExt {
inline ReadModifyWriteResult
ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
return ReadModifyWriteResult { .invalid = false,
.error = std::unique_ptr<std::string>(nullptr),
return ReadModifyWriteResult { .status = OperationStatus::Ok,
.error = nullptr,
.old_value = GenmcScalarExt::from_sval(old_value),
.new_value = GenmcScalarExt::from_sval(new_value),
.is_coherence_order_maximal_write =
is_coherence_order_maximal_write };
}

inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
return ReadModifyWriteResult { .invalid = false,
return ReadModifyWriteResult { .status = OperationStatus::Error,
.error = std::move(error),
.old_value = GenmcScalarExt::uninit(),
.new_value = GenmcScalarExt::uninit(),
.is_coherence_order_maximal_write = false };
}

inline ReadModifyWriteResult from_invalid() {
return ReadModifyWriteResult { .invalid = true,
return ReadModifyWriteResult { .status = OperationStatus::Invalid,
.error = nullptr,
.old_value = GenmcScalarExt::uninit(),
.new_value = GenmcScalarExt::uninit(),
Expand All @@ -354,66 +362,54 @@ inline ReadModifyWriteResult from_invalid() {

namespace CompareExchangeResultExt {
inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) {
return CompareExchangeResult { .invalid = false,
return CompareExchangeResult { .status = CasStatus::Succeeded,
.error = nullptr,
.old_value = GenmcScalarExt::from_sval(old_value),
.is_success = true,
.is_coherence_order_maximal_write =
is_coherence_order_maximal_write };
}

inline CompareExchangeResult failure(SVal old_value) {
return CompareExchangeResult { .invalid = false,
return CompareExchangeResult { .status = CasStatus::Failed,
.error = nullptr,
.old_value = GenmcScalarExt::from_sval(old_value),
.is_success = false,
.is_coherence_order_maximal_write = false };
}

inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
return CompareExchangeResult { .invalid = false,
return CompareExchangeResult { .status = CasStatus::Error,
.error = std::move(error),
.old_value = GenmcScalarExt::uninit(),
.is_success = false,
.is_coherence_order_maximal_write = false };
}

inline CompareExchangeResult from_invalid() {
return CompareExchangeResult { .invalid = true,
return CompareExchangeResult { .status = CasStatus::Invalid,
.error = nullptr,
.old_value = GenmcScalarExt::uninit(),
.is_success = false,
.is_coherence_order_maximal_write = false };
}
} // namespace CompareExchangeResultExt

namespace MutexLockResultExt {
inline MutexLockResult ok(bool is_lock_acquired) {
return MutexLockResult { .invalid = false,
.error = nullptr,
.is_reset = false,
.is_lock_acquired = is_lock_acquired };
inline MutexLockResult acquired() {
return MutexLockResult { .status = MutexLockStatus::Acquired, .error = nullptr };
}

inline MutexLockResult not_acquired() {
return MutexLockResult { .status = MutexLockStatus::NotAcquired, .error = nullptr };
}

inline MutexLockResult reset() {
return MutexLockResult { .invalid = false,
.error = nullptr,
.is_reset = true,
.is_lock_acquired = false };
return MutexLockResult { .status = MutexLockStatus::Reset, .error = nullptr };
}

inline MutexLockResult from_error(std::unique_ptr<std::string> error) {
return MutexLockResult { .invalid = false,
.error = std::move(error),
.is_reset = false,
.is_lock_acquired = false };
return MutexLockResult { .status = MutexLockStatus::Error, .error = std::move(error) };
}

inline MutexLockResult from_invalid() {
return MutexLockResult { .invalid = true,
.error = nullptr,
.is_reset = false,
.is_lock_acquired = false };
return MutexLockResult { .status = MutexLockStatus::Invalid, .error = nullptr };
}
} // namespace MutexLockResultExt

Expand Down
26 changes: 13 additions & 13 deletions genmc-sys/cpp/src/MiriInterface/Exploration.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty

[[nodiscard]] auto
MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint64_t size)
-> LoadResult {
-> NonAtomicResult {
const auto ret = GenMCDriver::handleNALoad(
nullptr,
curr_pos(thread_id),
Expand All @@ -123,15 +123,15 @@ MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint
inc_pos(thread_id, ret.count);

if (const auto* err = std::get_if<VerificationError>(&ret.result))
return LoadResultExt::from_error(format_error(*err));
return NonAtomicResultExt::from_error(format_error(*err));
if (std::holds_alternative<Invalid>(ret.result))
return LoadResultExt::from_invalid();
return NonAtomicResultExt::from_invalid();
// FIXME(genmc): handle `HandleResult::Reset` return value.
ERROR_ON(
!std::holds_alternative<std::monostate>(ret.result),
"Unimplemented: non-atomic load returned unexpected result."
);
return LoadResultExt::no_value();
return NonAtomicResultExt::ok();
}

[[nodiscard]] auto MiriGenmcShim::handle_atomic_store(
Expand Down Expand Up @@ -168,7 +168,7 @@ MiriGenmcShim::handle_non_atomic_load(ThreadId thread_id, uint64_t address, uint

[[nodiscard]] auto
MiriGenmcShim::handle_non_atomic_store(ThreadId thread_id, uint64_t address, uint64_t size)
-> StoreResult {
-> NonAtomicResult {
const auto ret = GenMCDriver::handleNAStore(
nullptr,
curr_pos(thread_id),
Expand All @@ -179,15 +179,15 @@ MiriGenmcShim::handle_non_atomic_store(ThreadId thread_id, uint64_t address, uin
inc_pos(thread_id, ret.count);

if (const auto* err = std::get_if<VerificationError>(&ret.result))
return StoreResultExt::from_error(format_error(*err));
return NonAtomicResultExt::from_error(format_error(*err));
if (std::holds_alternative<Invalid>(ret.result))
return StoreResultExt::from_invalid();
return NonAtomicResultExt::from_invalid();
// FIXME(genmc): handle `HandleResult::Reset` return value.
ERROR_ON(
!std::holds_alternative<std::monostate>(ret.result),
"Unimplemented: non-atomic store returned unexpected result."
);
return StoreResultExt::ok(true);
return NonAtomicResultExt::ok();
}

void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
Expand Down Expand Up @@ -457,7 +457,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
// 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);
return MutexLockResultExt::not_acquired();
}

const auto store_ret =
Expand All @@ -471,8 +471,8 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
// 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.result);
ERROR_ON(!is_co_max, "Unimplemented: mutex_try_lock store returned unexpected result.");
return MutexLockResultExt::ok(true);
ERROR_ON(!is_co_max, "Unimplemented: mutex lock store returned unexpected result.");
return MutexLockResultExt::acquired();
}

auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
Expand Down Expand Up @@ -500,7 +500,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,

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. */
return MutexLockResultExt::not_acquired(); /* Lock already held. */

const auto store_ret = GenMCDriver::handleTrylockCasWrite(
nullptr,
Expand All @@ -518,7 +518,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
// co-maximal, but we still check that we get a boolean result.
const auto* is_co_max = std::get_if<bool>(&store_ret.result);
ERROR_ON(!is_co_max, "Unimplemented: store part of mutex try_lock returned unexpected result.");
return MutexLockResultExt::ok(true);
return MutexLockResultExt::acquired();
}

auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
Expand Down
Loading