@@ -104,8 +104,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
104104 return LoadResultExt::from_error (format_error (*err));
105105 const auto * ret_val = std::get_if<SVal>(&ret);
106106 // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
107- if (ret_val == nullptr )
108- ERROR (" Unimplemented: load returned unexpected result." );
107+ ERROR_ON (!ret_val, " Unimplemented: load returned unexpected result." );
109108 return LoadResultExt::from_value (*ret_val);
110109}
111110
@@ -133,13 +132,10 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
133132 if (const auto * err = std::get_if<VerificationError>(&ret))
134133 return StoreResultExt::from_error (format_error (*err));
135134
136- const bool * is_coherence_order_maximal_write = std::get_if<bool >(&ret);
135+ const auto * is_co_max = std::get_if<bool >(&ret);
137136 // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
138- ERROR_ON (
139- nullptr == is_coherence_order_maximal_write,
140- " Unimplemented: Store returned unexpected result."
141- );
142- return StoreResultExt::ok (*is_coherence_order_maximal_write);
137+ ERROR_ON (!is_co_max, " Unimplemented: Store returned unexpected result." );
138+ return StoreResultExt::ok (*is_co_max);
143139}
144140
145141void MiriGenmcShim::handle_fence (ThreadId thread_id, MemOrdering ord) {
@@ -178,9 +174,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
178174
179175 const auto * ret_val = std::get_if<SVal>(&load_ret);
180176 // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
181- if (nullptr == ret_val) {
182- ERROR (" Unimplemented: read-modify-write returned unexpected result." );
183- }
177+ ERROR_ON (!ret_val, " Unimplemented: read-modify-write returned unexpected result." );
184178 const auto read_old_val = *ret_val;
185179 const auto new_value =
186180 executeRMWBinOp (read_old_val, GenmcScalarExt::to_sval (rhs_value), size, rmw_op);
@@ -199,16 +193,13 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
199193 if (const auto * err = std::get_if<VerificationError>(&store_ret))
200194 return ReadModifyWriteResultExt::from_error (format_error (*err));
201195
202- const bool * is_coherence_order_maximal_write = std::get_if<bool >(&store_ret);
196+ const auto * is_co_max = std::get_if<bool >(&store_ret);
203197 // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
204- ERROR_ON (
205- nullptr == is_coherence_order_maximal_write,
206- " Unimplemented: RMW store returned unexpected result."
207- );
198+ ERROR_ON (!is_co_max, " Unimplemented: RMW store returned unexpected result." );
208199 return ReadModifyWriteResultExt::ok (
209200 /* old_value: */ read_old_val,
210201 new_value,
211- *is_coherence_order_maximal_write
202+ *is_co_max
212203 );
213204}
214205
@@ -266,13 +257,10 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
266257 );
267258 if (const auto * err = std::get_if<VerificationError>(&store_ret))
268259 return CompareExchangeResultExt::from_error (format_error (*err));
269- const bool * is_coherence_order_maximal_write = std::get_if<bool >(&store_ret);
260+ const auto * is_co_max = std::get_if<bool >(&store_ret);
270261 // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
271- ERROR_ON (
272- nullptr == is_coherence_order_maximal_write,
273- " Unimplemented: compare-exchange store returned unexpected result."
274- );
275- return CompareExchangeResultExt::success (read_old_val, *is_coherence_order_maximal_write);
262+ ERROR_ON (!is_co_max, " Unimplemented: compare-exchange store returned unexpected result." );
263+ return CompareExchangeResultExt::success (read_old_val, *is_co_max);
276264}
277265
278266/* *** Memory (de)allocation ****/
@@ -385,11 +373,8 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
385373 // We don't update Miri's memory for this operation so we don't need to know if the store
386374 // was the co-maximal store, but we still check that we at least get a boolean as the result
387375 // of the store.
388- const bool * is_coherence_order_maximal_write = std::get_if<bool >(&store_ret);
389- ERROR_ON (
390- nullptr == is_coherence_order_maximal_write,
391- " Unimplemented: store part of mutex try_lock returned unexpected result."
392- );
376+ const auto * is_co_max = std::get_if<bool >(&store_ret);
377+ ERROR_ON (!is_co_max, " Unimplemented: mutex_try_lock store returned unexpected result." );
393378 } else {
394379 // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
395380 // it. GenMC determines this based on the annotation we pass with the load further up in
@@ -416,18 +401,15 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
416401 if (const auto * err = std::get_if<VerificationError>(&load_ret))
417402 return MutexLockResultExt::from_error (format_error (*err));
418403 const auto * ret_val = std::get_if<SVal>(&load_ret);
419- if (nullptr == ret_val) {
420- ERROR (" Unimplemented: mutex trylock load returned unexpected result." );
421- }
404+ ERROR_ON (!ret_val, " Unimplemented: mutex trylock load returned unexpected result." );
422405
423406 ERROR_ON (
424407 *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
425408 " Mutex read value was neither 0 nor 1"
426409 );
427410 const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
428- if (!is_lock_acquired) {
411+ if (!is_lock_acquired)
429412 return MutexLockResultExt::ok (false ); /* Lock already held. */
430- }
431413
432414 const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
433415 nullptr ,
@@ -440,11 +422,8 @@ auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address,
440422 return MutexLockResultExt::from_error (format_error (*err));
441423 // We don't update Miri's memory for this operation so we don't need to know if the store was
442424 // co-maximal, but we still check that we get a boolean result.
443- const bool * is_coherence_order_maximal_write = std::get_if<bool >(&store_ret);
444- ERROR_ON (
445- nullptr == is_coherence_order_maximal_write,
446- " Unimplemented: store part of mutex try_lock returned unexpected result."
447- );
425+ const auto * is_co_max = std::get_if<bool >(&store_ret);
426+ ERROR_ON (!is_co_max, " Unimplemented: store part of mutex try_lock returned unexpected result." );
448427 return MutexLockResultExt::ok (true );
449428}
450429
@@ -467,12 +446,9 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
467446 );
468447 if (const auto * err = std::get_if<VerificationError>(&ret))
469448 return StoreResultExt::from_error (format_error (*err));
470- const bool * is_coherence_order_maximal_write = std::get_if<bool >(&ret);
471- ERROR_ON (
472- nullptr == is_coherence_order_maximal_write,
473- " Unimplemented: store part of mutex unlock returned unexpected result."
474- );
475- return StoreResultExt::ok (*is_coherence_order_maximal_write);
449+ const auto * is_co_max = std::get_if<bool >(&ret);
450+ ERROR_ON (!is_co_max, " Unimplemented: store part of mutex unlock returned unexpected result." );
451+ return StoreResultExt::ok (*is_co_max);
476452}
477453
478454/* * Thread creation/joining */
0 commit comments