Skip to content

Commit 5e6d9fa

Browse files
committed
genmc/api: Use returned value from handleFree()
GenMC's handleFree() does return an optional<Error>, so we may as well use that value.
1 parent fafd6de commit 5e6d9fa

File tree

4 files changed

+18
-12
lines changed

4 files changed

+18
-12
lines changed

src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,8 +125,11 @@ struct MiriGenmcShim : private GenMCDriver {
125125
void handle_fence(ThreadId thread_id, MemOrdering ord);
126126

127127
/**** Memory (de)allocation ****/
128+
128129
auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
129-
auto handle_free(ThreadId thread_id, uint64_t address) -> bool;
130+
131+
/** Returns null on success, or an error string if an error occurs. */
132+
auto handle_free(ThreadId thread_id, uint64_t address) -> std::unique_ptr<std::string>;
130133

131134
/**** Thread management ****/
132135
void handle_thread_create(ThreadId thread_id, ThreadId parent_id);

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -288,11 +288,11 @@ auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t al
288288
return ret_val.get();
289289
}
290290

291-
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
292-
const auto pos = inc_pos(thread_id);
293-
GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
294-
// FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
295-
return getResult().status.has_value();
291+
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address)
292+
-> std::unique_ptr<std::string> {
293+
auto pos = inc_pos(thread_id);
294+
auto ret = GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
295+
return ret.has_value() ? format_error(*ret) : nullptr;
296296
}
297297

298298
/**** Estimation mode result ****/

src/tools/miri/genmc-sys/src/lib.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -438,7 +438,11 @@ mod ffi {
438438
alignment: u64,
439439
) -> u64;
440440
/// Returns true if an error was found.
441-
fn handle_free(self: Pin<&mut MiriGenmcShim>, thread_id: i32, address: u64) -> bool;
441+
fn handle_free(
442+
self: Pin<&mut MiriGenmcShim>,
443+
thread_id: i32,
444+
address: u64,
445+
) -> UniquePtr<CxxString>;
442446

443447
/**** Thread management ****/
444448
fn handle_thread_create(self: Pin<&mut MiriGenmcShim>, thread_id: i32, parent_id: i32);

src/tools/miri/src/concurrency/genmc/mod.rs

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -622,15 +622,14 @@ impl GenmcCtx {
622622
!self.get_alloc_data_races(),
623623
"memory deallocation with data race checking disabled."
624624
);
625-
if self
625+
let free_result = self
626626
.handle
627627
.borrow_mut()
628628
.pin_mut()
629-
.handle_free(self.active_thread_genmc_tid(machine), address.bytes())
630-
{
629+
.handle_free(self.active_thread_genmc_tid(machine), address.bytes());
630+
if let Some(error) = free_result.as_ref() {
631631
// FIXME(genmc): improve error handling.
632-
// An error was detected, so we get the error string from GenMC.
633-
throw_ub_format!("{}", self.try_get_error().unwrap());
632+
throw_ub_format!("{}", error.to_string_lossy());
634633
}
635634

636635
interp_ok(())

0 commit comments

Comments
 (0)