Skip to content

Commit d2176c3

Browse files
committed
genmc/api: Don't use macros for mutex state
Use scoped constexprs instead.
1 parent 286fac0 commit d2176c3

File tree

1 file changed

+18
-20
lines changed

1 file changed

+18
-20
lines changed

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

Lines changed: 18 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -309,8 +309,14 @@ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult {
309309

310310
/** Mutexes */
311311

312-
#define MUTEX_UNLOCKED SVal(0)
313-
#define MUTEX_LOCKED SVal(1)
312+
struct MutexState {
313+
static constexpr SVal UNLOCKED { 0 };
314+
static constexpr SVal LOCKED { 1 };
315+
316+
static constexpr bool isValid(SVal v) {
317+
return v == UNLOCKED || v == LOCKED;
318+
}
319+
};
314320

315321
auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
316322
-> MutexLockResult {
@@ -325,7 +331,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
325331
// The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
326332
// other variables from previous expressions that may be used here.
327333
RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
328-
ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED)
334+
ConcreteExpr<ModuleID::ID>::create(size_bits, MutexState::LOCKED)
329335
)
330336
.release()
331337
)
@@ -334,7 +340,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
334340
// As usual, we need to tell GenMC which value was stored at this location before this atomic
335341
// access, if there previously was a non-atomic initializing access. We set the initial state of
336342
// a mutex to be "unlocked".
337-
const auto old_val = MUTEX_UNLOCKED;
343+
const auto old_val = MutexState::UNLOCKED;
338344
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
339345
thread_id,
340346
old_val,
@@ -354,15 +360,11 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
354360

355361
const auto* ret_val = std::get_if<SVal>(&load_ret);
356362
ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
357-
ERROR_ON(
358-
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
359-
"Mutex read value was neither 0 nor 1"
360-
);
361-
auto is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
362-
if (!is_lock_acquired) {
363+
ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1");
364+
if (*ret_val == MutexState::LOCKED) {
363365
// We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
364366
// it. GenMC determines this based on the annotation we pass with the load further up in
365-
// this function, namely when that load will read a value other than `MUTEX_LOCKED`.
367+
// this function, namely when that load will read a value other than `MutexState::LOCKED`.
366368
this->handle_assume_block(thread_id, AssumeType::Spinloop);
367369
return MutexLockResultExt::ok(false);
368370
}
@@ -391,7 +393,7 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
391393
// As usual, we need to tell GenMC which value was stored at this location before this atomic
392394
// access, if there previously was a non-atomic initializing access. We set the initial state of
393395
// a mutex to be "unlocked".
394-
const auto old_val = MUTEX_UNLOCKED;
396+
const auto old_val = MutexState::UNLOCKED;
395397
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
396398
nullptr,
397399
++currPos,
@@ -404,12 +406,8 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
404406
const auto* ret_val = std::get_if<SVal>(&load_ret);
405407
ERROR_ON(!ret_val, "Unimplemented: mutex trylock load returned unexpected result.");
406408

407-
ERROR_ON(
408-
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
409-
"Mutex read value was neither 0 nor 1"
410-
);
411-
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
412-
if (!is_lock_acquired)
409+
ERROR_ON(!MutexState::isValid(*ret_val), "Mutex read value was neither 0 nor 1");
410+
if (*ret_val == MutexState::LOCKED)
413411
return MutexLockResultExt::ok(false); /* Lock already held. */
414412

415413
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
@@ -437,12 +435,12 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
437435
// As usual, we need to tell GenMC which value was stored at this location before this
438436
// atomic access, if there previously was a non-atomic initializing access. We set the
439437
// initial state of a mutex to be "unlocked".
440-
/* old_val */ MUTEX_UNLOCKED,
438+
/* old_val */ MutexState::UNLOCKED,
441439
MemOrdering::Release,
442440
SAddr(address),
443441
ASize(size),
444442
AType::Signed,
445-
/* store_value */ MUTEX_UNLOCKED,
443+
/* store_value */ MutexState::UNLOCKED,
446444
EventDeps()
447445
);
448446
if (const auto* err = std::get_if<VerificationError>(&ret))

0 commit comments

Comments
 (0)