Skip to content

Commit 3822fd2

Browse files
committed
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").
1 parent 149df8a commit 3822fd2

File tree

1 file changed

+17
-7
lines changed

1 file changed

+17
-7
lines changed

genmc-sys/cpp/src/MiriInterface/Exploration.cpp

Lines changed: 17 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,23 @@ auto MiriGenmcShim::schedule_next(
2222
// a scheduling decision.
2323
threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind;
2424

25-
if (const auto result = GenMCDriver::scheduleNext(threads_action_))
26-
return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(result.value()) };
27-
if (getExec().getGraph().isBlocked())
28-
return SchedulingResult { ExecutionState::Blocked, 0 };
29-
if (getResult().status.has_value()) // the "value" here is a `VerificationError`
30-
return SchedulingResult { ExecutionState::Error, 0 };
31-
return SchedulingResult { ExecutionState::Finished, 0 };
25+
auto result = GenMCDriver::scheduleNext(threads_action_);
26+
return std::visit(
27+
[](auto&& arg) {
28+
using T = std::decay_t<decltype(arg)>;
29+
if constexpr (std::is_same_v<T, int>)
30+
return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
31+
else if constexpr (std::is_same_v<T, Blocked>)
32+
return SchedulingResult { ExecutionState::Blocked, 0 };
33+
else if constexpr (std::is_same_v<T, Error>)
34+
return SchedulingResult { ExecutionState::Error, 0 };
35+
else if constexpr (std::is_same_v<T, Finished>)
36+
return SchedulingResult { ExecutionState::Finished, 0 };
37+
else
38+
static_assert(false, "non-exhaustive visitor!");
39+
},
40+
result
41+
);
3242
}
3343

3444
/**** Execution start/end handling ****/

0 commit comments

Comments
 (0)