-
Notifications
You must be signed in to change notification settings - Fork 391
Closed
Labels
A-aliasingArea: This affects the aliasing model (Stacked/Tree Borrows)Area: This affects the aliasing model (Stacked/Tree Borrows)A-data-raceArea: data race detectorArea: data race detectorC-bugCategory: This is a bug.Category: This is a bug.I-misses-UBImpact: makes Miri miss UB, i.e., a false negative (with default settings)Impact: makes Miri miss UB, i.e., a false negative (with default settings)
Description
Currently, many Stacked Borrows retags are effectively read/write accesses for the aliasing model:
miri/src/stacked_borrows/mod.rs
Lines 508 to 511 in 9568d7e
// A "safe" reborrow for a pointer that actually expects some aliasing guarantees. | |
// Here, creating a reference actually counts as an access. | |
// This ensures F2b for `Unique`, by removing offending `SharedReadOnly`. | |
self.access(access, derived_from, global, dcx, exposed_tags)?; |
However, the data race model never hears about them, which as @JakobDegen points out leads us to accept some code that we probably should not accept.
Metadata
Metadata
Assignees
Labels
A-aliasingArea: This affects the aliasing model (Stacked/Tree Borrows)Area: This affects the aliasing model (Stacked/Tree Borrows)A-data-raceArea: data race detectorArea: data race detectorC-bugCategory: This is a bug.Category: This is a bug.I-misses-UBImpact: makes Miri miss UB, i.e., a false negative (with default settings)Impact: makes Miri miss UB, i.e., a false negative (with default settings)