Miri-GenMC API refactor

genmc-sys/build.rs

@@ -178,7 +178,7 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     // 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/Exploration.cpp", "MiriInterface/Setup.cpp"]
+    let cpp_files = ["Exploration.cpp", "Setup.cpp"]
         .map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
 
     let mut bridge = cxx_build::bridge("src/lib.rs");

genmc-sys/cpp/include/MiriInterface.hpp

@@ -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;
@@ -52,26 +54,26 @@ using ThreadId = int;
 /// Never calling this function is safe, GenMC will fall back to its default log level.
 /* unsafe */ void set_log_level_raw(LogLevel log_level);
 
-struct MiriGenmcShim : private GenMCDriver {
+struct MiriGenMCInterface : private GenMCDriver {
 
   public:
-    MiriGenmcShim(std::shared_ptr<const Config> conf, Mode mode /* = VerificationMode{} */)
+    MiriGenMCInterface(std::shared_ptr<const Config> conf, Mode mode /* = VerificationMode{} */)
         : GenMCDriver(std::move(conf), nullptr, mode) {}
 
-    /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`.
+    /// Create a new `MiriGenMCInterface`, which wraps a `GenMCDriver`.
     ///
     /// # Safety
     ///
     /// This function is marked as unsafe since the `logLevel` global variable is non-atomic.
     /// This function should not be called in an unsynchronized way with `set_log_level_raw`,
-    /// since this function and any methods on the returned `MiriGenmcShim` may read the
+    /// since this function and any methods on the returned `MiriGenMCInterface` may read the
     /// `logLevel`, causing a data race. The safest way to use these functions is to call
     /// `set_log_level_raw` once, and only then start creating handles. There should not be any
-    /// other (safe) way to create a `MiriGenmcShim`.
+    /// other (safe) way to create a `MiriGenMCInterface`.
     /* unsafe */ static auto create_handle(const GenmcParams& params, bool estimation_mode)
-        -> std::unique_ptr<MiriGenmcShim>;
+        -> std::unique_ptr<MiriGenMCInterface>;
 
-    virtual ~MiriGenmcShim() {}
+    virtual ~MiriGenMCInterface() {}
 
     /**** Execution start/end handling ****/
 
@@ -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,
@@ -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);
@@ -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);
@@ -240,8 +242,8 @@ constexpr auto get_global_alloc_static_mask() -> uint64_t {
 }
 
 // CXX.rs generated headers:
-// NOTE: this must be included *after* `MiriGenmcShim` and all the other types we use are defined,
-// otherwise there will be compilation errors due to missing definitions.
+// NOTE: this must be included *after* `MiriGenMCInterface` and all the other types we use are
+// defined, otherwise there will be compilation errors due to missing definitions.
 #include "genmc-sys/src/lib.rs.h"
 
 /**** Result handling ****/
@@ -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 */

genmc-sys/cpp/include/ResultHandling.hpp

@@ -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 */