Skip to content

Commit 7097633

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 d2f81cf commit 7097633

File tree

1 file changed

+18
-7
lines changed

1 file changed

+18
-7
lines changed

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

Lines changed: 18 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,24 @@ 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+
return SchedulingResult { ExecutionState::Finished, 0 };
40+
},
41+
result
42+
);
3243
}
3344

3445
/**** Execution start/end handling ****/

0 commit comments

Comments
 (0)