Skip to content

Commit 149df8a

Browse files
committed
genmc/api: Handle new GenMC error API
The new error-reporting mechanism of GenMC changed its public API. This commit adjusts the Miri interface accordingly (all driver calls need an extra argument that represents possible debugging information).
1 parent 4bb682c commit 149df8a

File tree

4 files changed

+19
-9
lines changed

4 files changed

+19
-9
lines changed

genmc-sys/cpp/include/MiriInterface.hpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,8 @@ struct MiriGenmcShim : private GenMCDriver {
220220
auto handle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
221221
-> HandleResult<SVal> {
222222
const auto pos = inc_pos(tid);
223-
const auto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
223+
const auto ret =
224+
GenMCDriver::handleLoad<k>(nullptr, pos, old_val, std::forward<Ts>(params)...);
224225
// If we didn't get a value, we have to reset the index of the current thread.
225226
if (!std::holds_alternative<SVal>(ret)) {
226227
dec_pos(tid);

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

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@
3434

3535
void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
3636
BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
37-
GenMCDriver::handleAssume(inc_pos(thread_id), assume_type);
37+
GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
3838
}
3939

4040
/**** Memory access handling ****/
@@ -76,6 +76,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
7676
) -> StoreResult {
7777
const auto pos = inc_pos(thread_id);
7878
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
79+
nullptr,
7980
pos,
8081
GenmcScalarExt::try_to_sval(old_val),
8182
ord,
@@ -100,7 +101,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
100101

101102
void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
102103
const auto pos = inc_pos(thread_id);
103-
GenMCDriver::handleFence(pos, ord, EventDeps());
104+
GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
104105
}
105106

106107
[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
@@ -143,6 +144,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
143144

144145
const auto storePos = inc_pos(thread_id);
145146
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
147+
nullptr,
146148
storePos,
147149
GenmcScalarExt::try_to_sval(old_val),
148150
ordering,
@@ -210,6 +212,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
210212

211213
const auto storePos = inc_pos(thread_id);
212214
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
215+
nullptr,
213216
storePos,
214217
GenmcScalarExt::try_to_sval(old_val),
215218
success_ordering,
@@ -242,6 +245,7 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al
242245
const auto address_space = AddressSpace::AS_User;
243246

244247
const SVal ret_val = GenMCDriver::handleMalloc(
248+
nullptr,
245249
pos,
246250
size,
247251
alignment,
@@ -255,7 +259,7 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al
255259

256260
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
257261
const auto pos = inc_pos(thread_id);
258-
GenMCDriver::handleFree(pos, SAddr(address), EventDeps());
262+
GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
259263
// FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
260264
return getResult().status.has_value();
261265
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
6060
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
6161
if (is_lock_acquired) {
6262
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
63+
nullptr,
6364
inc_pos(thread_id),
6465
old_val,
6566
address,
@@ -93,6 +94,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
9394
// a mutex to be "unlocked".
9495
const auto old_val = MUTEX_UNLOCKED;
9596
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
97+
nullptr,
9698
++currPos,
9799
old_val,
98100
SAddr(address),
@@ -115,6 +117,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
115117
}
116118

117119
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
120+
nullptr,
118121
++currPos,
119122
old_val,
120123
SAddr(address),
@@ -136,6 +139,7 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
136139
-> StoreResult {
137140
const auto pos = inc_pos(thread_id);
138141
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
142+
nullptr,
139143
pos,
140144
// As usual, we need to tell GenMC which value was stored at this location before this
141145
// atomic access, if there previously was a non-atomic initializing access. We set the

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

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,11 @@ void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id)
1919
// FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
2020
const unsigned fun_id = 0;
2121
const SVal arg = SVal(0);
22-
const ThreadInfo child_info = ThreadInfo { thread_id, parent_id, fun_id, arg };
22+
const ThreadInfo child_info =
23+
ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
2324

2425
// NOTE: Default memory ordering (`Release`) used here.
25-
const auto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
26+
const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
2627
// Sanity check the thread id, which is the index in the `threads_action_` array.
2728
BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
2829
threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
@@ -33,7 +34,7 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
3334
const auto pos = inc_pos(thread_id);
3435

3536
// NOTE: Default memory ordering (`Acquire`) used here.
36-
const auto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
37+
const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
3738
// If the join failed, decrease the event index again:
3839
if (!std::holds_alternative<SVal>(ret)) {
3940
dec_pos(thread_id);
@@ -46,10 +47,10 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
4647
void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
4748
const auto pos = inc_pos(thread_id);
4849
// NOTE: Default memory ordering (`Release`) used here.
49-
GenMCDriver::handleThreadFinish(pos, SVal(ret_val));
50+
GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
5051
}
5152

5253
void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
5354
const auto pos = inc_pos(thread_id);
54-
GenMCDriver::handleThreadKill(pos);
55+
GenMCDriver::handleThreadKill(nullptr, pos);
5556
}

0 commit comments

Comments
 (0)