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 4 commits
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
175 changes: 96 additions & 79 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,11 +32,13 @@ struct GenmcScalar;
struct SchedulingResult;
struct EstimationResult;
struct LoadResult;
struct NonAtomicResult;
struct StoreResult;
struct ReadModifyWriteResult;
struct CompareExchangeResult;
struct MutexLockResult;
struct MallocResult;
struct FreeResult;

// GenMC uses `int` for its thread IDs.
using ThreadId = int;
Expand Down Expand Up @@ -94,7 +96,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 +126,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 All @@ -134,7 +136,7 @@ struct MiriGenmcShim : private GenMCDriver {
auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> MallocResult;

/** 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>;
auto handle_free(ThreadId thread_id, uint64_t address) -> FreeResult;

/**** Thread management ****/
void handle_thread_create(ThreadId thread_id, ThreadId parent_id);
Expand Down Expand Up @@ -277,154 +279,169 @@ 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(),
};
namespace MakeLoadResult {
inline LoadResult value(SVal read_value) {
return LoadResult { .status = OperationStatus::Ok,
.error = nullptr,
.read_value = GenmcScalarExt::from_sval(read_value) };
}

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

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

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

inline LoadResult from_invalid() {
return LoadResult { .invalid = true, .error = nullptr, .read_value = GenmcScalarExt::uninit() };
inline NonAtomicResult error(std::unique_ptr<std::string> err) {
return NonAtomicResult { .status = OperationStatus::Error, .error = std::move(err) };
}

} // namespace LoadResultExt
inline NonAtomicResult invalid() {
return NonAtomicResult { .status = OperationStatus::Invalid, .error = nullptr };
}
} // namespace MakeNonAtomicResult

namespace StoreResultExt {
namespace MakeStoreResult {
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,
.error = std::move(error),
inline StoreResult error(std::unique_ptr<std::string> err) {
return StoreResult { .status = OperationStatus::Error,
.error = std::move(err),
.is_coherence_order_maximal_write = false };
}

inline StoreResult from_invalid() {
return StoreResult { .invalid = true,
inline StoreResult invalid() {
return StoreResult { .status = OperationStatus::Invalid,
.error = nullptr,
.is_coherence_order_maximal_write = false };
}
} // namespace StoreResultExt
} // namespace MakeStoreResult

namespace ReadModifyWriteResultExt {
namespace MakeReadModifyWriteResult {
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,
.error = std::move(error),
inline ReadModifyWriteResult error(std::unique_ptr<std::string> err) {
return ReadModifyWriteResult { .status = OperationStatus::Error,
.error = std::move(err),
.old_value = GenmcScalarExt::uninit(),
.new_value = GenmcScalarExt::uninit(),
.is_coherence_order_maximal_write = false };
}

inline ReadModifyWriteResult from_invalid() {
return ReadModifyWriteResult { .invalid = true,
inline ReadModifyWriteResult invalid() {
return ReadModifyWriteResult { .status = OperationStatus::Invalid,
.error = nullptr,
.old_value = GenmcScalarExt::uninit(),
.new_value = GenmcScalarExt::uninit(),
.is_coherence_order_maximal_write = false };
}
} // namespace ReadModifyWriteResultExt
} // namespace MakeReadModifyWriteResult

namespace CompareExchangeResultExt {
inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) {
return CompareExchangeResult { .invalid = false,
namespace MakeCasResult {
inline CompareExchangeResult succeeded(SVal old_value, bool is_coherence_order_maximal_write) {
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,
inline CompareExchangeResult failed(SVal old_value) {
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,
.error = std::move(error),
inline CompareExchangeResult error(std::unique_ptr<std::string> err) {
return CompareExchangeResult { .status = CasStatus::Error,
.error = std::move(err),
.old_value = GenmcScalarExt::uninit(),
.is_success = false,
.is_coherence_order_maximal_write = false };
}

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

namespace MutexLockResultExt {
inline MutexLockResult ok(bool is_lock_acquired) {
return MutexLockResult { .invalid = false,
.error = nullptr,
.is_reset = false,
.is_lock_acquired = is_lock_acquired };
namespace MakeMutexLockResult {
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 };
inline MutexLockResult error(std::unique_ptr<std::string> err) {
return MutexLockResult { .status = MutexLockStatus::Error, .error = std::move(err) };
}

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

namespace MallocResultExt {
namespace MakeMallocResult {
inline MallocResult ok(SVal addr) {
return MallocResult { .error = nullptr, .address = addr.get() };
return MallocResult { .status = OperationStatus::Ok, .error = nullptr, .address = addr.get() };
}

inline MallocResult error(std::unique_ptr<std::string> err) {
return MallocResult { .status = OperationStatus::Error,
.error = std::move(err),
.address = 0UL };
}

inline MallocResult invalid() {
return MallocResult { .status = OperationStatus::Invalid, .error = nullptr, .address = 0UL };
}
} // namespace MakeMallocResult

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

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

inline MallocResult from_error(std::unique_ptr<std::string> error) {
return MallocResult { .error = std::move(error), .address = 0UL };
inline FreeResult invalid() {
return FreeResult { .status = OperationStatus::Invalid, .error = nullptr };
}
} // namespace MallocResultExt
} // namespace MakeFreeResult

#endif /* GENMC_MIRI_INTERFACE_HPP */
6 changes: 6 additions & 0 deletions genmc-sys/cpp/include/ResultHandling.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,10 @@ static auto format_error(VerificationError err) -> std::unique_ptr<std::string>
return std::make_unique<std::string>(s.str());
}

/** Standard overloaded-lambda helper for std::visit.
* See https://en.cppreference.com/w/cpp/utility/variant/visit2.html for usage. */
template <class... Ts> struct overloaded : Ts... {
using Ts::operator()...;
};

#endif /* GENMC_RESULT_HANDLING_HPP */
Loading