@@ -60,16 +60,15 @@ auto MiriGenMCShim::createHandle(const GenmcParams &config, bool estimation_mode
60
60
// Miri needs all threads to be replayed, even fully completed ones.
61
61
conf->replayCompletedThreads = true ;
62
62
63
- // TODO GENMC: make sure this doesn't affect any tests, and maybe make it changeable from
64
- // Miri:
63
+ // FIXME(genmc): make sure this doesn't affect any tests, and maybe make it changeable from Miri:
65
64
constexpr unsigned int DEFAULT_WARN_ON_GRAPH_SIZE = 16 * 1024 ;
66
65
conf->warnOnGraphSize = DEFAULT_WARN_ON_GRAPH_SIZE;
67
66
68
67
// We only support the RC11 memory model for Rust.
69
68
conf->model = ModelType::RC11;
70
69
71
- conf-> randomScheduleSeed =
72
- " 42" ; // TODO GENMC: only for random exploration/scheduling mode in GenMC
70
+ // FIXME(genmc): expose this setting to Miri
71
+ conf-> randomScheduleSeed = " 42" ;
73
72
conf->printRandomScheduleSeed = config.print_random_schedule_seed ;
74
73
if (config.quiet ) {
75
74
// logLevel = VerbosityLevel::Quiet;
@@ -82,19 +81,19 @@ auto MiriGenMCShim::createHandle(const GenmcParams &config, bool estimation_mode
82
81
logLevel = VerbosityLevel::Tip;
83
82
}
84
83
85
- // TODO GENMC (EXTRA ): check if we can enable IPR:
84
+ // FIXME(genmc ): check if we can enable IPR:
86
85
conf->ipr = false ;
87
- // TODO GENMC (EXTRA ): check if we can enable BAM:
86
+ // FIXME(genmc ): check if we can enable BAM:
88
87
conf->disableBAM = true ;
89
- // TODO GENMC (EXTRA ): check if we can do instruction caching (probably not)
88
+ // FIXME(genmc ): check if we can do instruction caching (probably not)
90
89
conf->instructionCaching = false ;
91
90
92
- // TODO GENMC (EXTRA ): check if we can enable Symmetry Reduction:
91
+ // FIXME(genmc ): implement symmetry reduction.
93
92
ERROR_ON (config.do_symmetry_reduction ,
94
93
" Symmetry reduction is currently unsupported in GenMC mode." );
95
94
conf->symmetryReduction = config.do_symmetry_reduction ;
96
95
97
- // TODO GENMC: Should there be a way to change this option from Miri?
96
+ // FIXME(genmc): expose this setting to Miri (useful for testing Miri-GenMC).
98
97
conf->schedulePolicy = SchedulePolicy::WF;
99
98
100
99
conf->estimate = estimation_mode;
@@ -236,7 +235,7 @@ void MiriGenMCShim::handleUserBlock(ThreadId thread_id)
236
235
237
236
auto loc = SAddr (address);
238
237
auto aSize = ASize (size);
239
- auto type = AType::Unsigned; // TODO GENMC : get correct type from Miri
238
+ auto type = AType::Unsigned; // FIXME(genmc) : get correct type from Miri(?)
240
239
241
240
auto newLab = std::make_unique<ReadLabel>(pos, ord, loc, aSize, type);
242
241
@@ -339,9 +338,9 @@ void MiriGenMCShim::handleUserBlock(ThreadId thread_id)
339
338
340
339
auto pos = incPos (thread_id);
341
340
342
- auto loc = SAddr (address); // TODO GENMC: called addr for write, loc for read?
341
+ auto loc = SAddr (address);
343
342
auto aSize = ASize (size);
344
- auto type = AType::Unsigned; // TODO GENMC : get from Miri
343
+ auto type = AType::Unsigned; // FIXME(genmc) : get correct type from Miri(?)
345
344
346
345
// TODO GENMC: u128 support
347
346
auto val = value.toSVal ();
@@ -388,14 +387,12 @@ auto MiriGenMCShim::handleMalloc(ThreadId thread_id, uint64_t size, uint64_t ali
388
387
{
389
388
auto pos = incPos (thread_id);
390
389
391
- auto sd = StorageDuration::SD_Heap; // TODO GENMC: get from Miri
392
- auto stype = StorageType::ST_Durable; // TODO GENMC
393
- auto spc = AddressSpace::AS_User; // TODO GENMC
394
-
395
- auto deps = EventDeps (); // TODO GENMC: without this, constructor is ambiguous
390
+ // FIXME(genmc): get correct values from Miri
391
+ auto sd = StorageDuration::SD_Heap;
392
+ auto stype = StorageType::ST_Durable;
393
+ auto spc = AddressSpace::AS_User;
396
394
397
- // TODO GENMC (types): size_t vs unsigned int
398
- auto aLab = std::make_unique<MallocLabel>(pos, size, alignment, sd, stype, spc, deps);
395
+ auto aLab = std::make_unique<MallocLabel>(pos, size, alignment, sd, stype, spc, EventDeps ());
399
396
400
397
SAddr retVal = GenMCDriver::handleMalloc (std::move (aLab));
401
398
0 commit comments