From 689358ab36d7f0f2b1ef4043fef2bae340eaffb6 Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sat, 15 Nov 2025 17:10:11 +0100 Subject: [PATCH] genmc/schedule: Handle new GenMC scheduling API When GenMC says that an execution should not be explored further, Miri needs to know why (e.g., so that it returns an appropriate exit value). Until now, some (erroneous) heuristics were used for that. This commit changes the Miri/GenMC API to check the scheduling result of GenMC (that now reflects the "stop type"). --- .../cpp/src/MiriInterface/Exploration.cpp | 24 +++++++++++++------ 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 0f64083ddda6..7722c4bfab69 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -22,13 +22,23 @@ auto MiriGenmcShim::schedule_next( // a scheduling decision. threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind; - if (const auto result = GenMCDriver::scheduleNext(threads_action_)) - return SchedulingResult { ExecutionState::Ok, static_cast(result.value()) }; - if (getExec().getGraph().isBlocked()) - return SchedulingResult { ExecutionState::Blocked, 0 }; - if (getResult().status.has_value()) // the "value" here is a `VerificationError` - return SchedulingResult { ExecutionState::Error, 0 }; - return SchedulingResult { ExecutionState::Finished, 0 }; + auto result = GenMCDriver::scheduleNext(threads_action_); + return std::visit( + [](auto&& arg) { + using T = std::decay_t; + if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Ok, static_cast(arg) }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Blocked, 0 }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Error, 0 }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Finished, 0 }; + else + static_assert(false, "non-exhaustive visitor!"); + }, + result + ); } /**** Execution start/end handling ****/