Skip to content

Commit 85460f4

Browse files
committed
Add comments detailing unhandled result values.
1 parent 2489dde commit 85460f4

File tree

2 files changed

+7
-0
lines changed

2 files changed

+7
-0
lines changed

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
6060
if (const auto* err = std::get_if<VerificationError>(&ret))
6161
return LoadResultExt::from_error(format_error(*err));
6262
const auto* ret_val = std::get_if<SVal>(&ret);
63+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
6364
if (ret_val == nullptr)
6465
ERROR("Unimplemented: load returned unexpected result.");
6566
return LoadResultExt::from_value(*ret_val);
@@ -89,6 +90,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_ty
8990
return StoreResultExt::from_error(format_error(*err));
9091

9192
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
93+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
9294
ERROR_ON(
9395
nullptr == is_coherence_order_maximal_write,
9496
"Unimplemented: Store returned unexpected result."
@@ -131,6 +133,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
131133
return ReadModifyWriteResultExt::from_error(format_error(*err));
132134

133135
const auto* ret_val = std::get_if<SVal>(&load_ret);
136+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
134137
if (nullptr == ret_val) {
135138
ERROR("Unimplemented: read-modify-write returned unexpected result.");
136139
}
@@ -152,6 +155,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
152155
return ReadModifyWriteResultExt::from_error(format_error(*err));
153156

154157
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
158+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
155159
ERROR_ON(
156160
nullptr == is_coherence_order_maximal_write,
157161
"Unimplemented: RMW store returned unexpected result."
@@ -196,6 +200,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
196200
if (const auto* err = std::get_if<VerificationError>(&load_ret))
197201
return CompareExchangeResultExt::from_error(format_error(*err));
198202
const auto* ret_val = std::get_if<SVal>(&load_ret);
203+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
199204
ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
200205
const auto read_old_val = *ret_val;
201206
if (read_old_val != expectedVal)
@@ -216,6 +221,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
216221
if (const auto* err = std::get_if<VerificationError>(&store_ret))
217222
return CompareExchangeResultExt::from_error(format_error(*err));
218223
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
224+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
219225
ERROR_ON(
220226
nullptr == is_coherence_order_maximal_write,
221227
"Unimplemented: compare-exchange store returned unexpected result."

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
3838
if (!std::holds_alternative<SVal>(ret)) {
3939
dec_pos(thread_id);
4040
}
41+
// FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
4142

4243
// NOTE: Thread return value is ignored, since Miri doesn't need it.
4344
}

0 commit comments

Comments
 (0)