Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
a9e56e4
fix empty stack in deadlock error message
RalfJung Dec 6, 2025
673b3b1
Merge pull request #4748 from RalfJung/deadlock-empty-stack
RalfJung Dec 6, 2025
ef33430
run ptr_int tests with Tree Borrows
RalfJung Dec 7, 2025
4ac95c1
Merge pull request #4750 from RalfJung/ptr-int-tb
RalfJung Dec 7, 2025
8a99d48
genmc: suppress compare_exchange warnings from dependencies
RalfJung Dec 7, 2025
eb01df9
Merge pull request #4751 from RalfJung/genmc-warnings
RalfJung Dec 7, 2025
3f48189
ftruncate: return proper error code for non-file-backed FDs
RalfJung Dec 8, 2025
001d2f7
Merge pull request #4754 from RalfJung/ftruncate-non-file-backed
RalfJung Dec 8, 2025
c033444
tree borrows: split perform_protector_end_access from perform_access
royAmmerschuber Dec 3, 2025
ed768d3
Merge pull request #4741 from royAmmerschuber/feature/refactor-protec…
RalfJung Dec 8, 2025
5516e54
Remove `[no-mentions]` handler in our triagebot config
Urgau Dec 8, 2025
442b868
Merge pull request #4755 from Urgau/triagebot-remove-no-mentions
RalfJung Dec 8, 2025
27590b0
fix manual_let_else
RalfJung Dec 9, 2025
8014987
Merge pull request #4756 from RalfJung/clippy-manual_let_else
RalfJung Dec 9, 2025
85e3acc
tree borrows: put accesses diagnostics data into single struct
royAmmerschuber Dec 3, 2025
0830b84
Merge pull request #4740 from royAmmerschuber/feature/refactor-diagno…
RalfJung Dec 9, 2025
0b11cdf
Prepare for merging from rust-lang/rust
Dec 11, 2025
a9f0a49
Merge ref 'f5209000832c' from rust-lang/rust
Dec 11, 2025
a4777e4
Merge pull request #4758 from rust-lang/rustup-2025-12-11
RalfJung Dec 11, 2025
82118ff
gitconfig is not a toml file
RalfJung Dec 11, 2025
d1afde2
Merge pull request #4759 from RalfJung/contrib
RalfJung Dec 11, 2025
395c6f5
README: add more papers to the paper list
RalfJung Dec 12, 2025
bc81d84
Merge pull request #4760 from RalfJung/papers
RalfJung Dec 12, 2025
3fd0fb6
Prepare for merging from rust-lang/rust
Dec 13, 2025
96f2d59
Merge ref 'dc47a69ed94b' from rust-lang/rust
Dec 13, 2025
05227a7
Merge pull request #4762 from rust-lang/rustup-2025-12-13
oli-obk Dec 13, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/tools/miri/CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -351,7 +351,7 @@ you need to pull rustc changes into Miri first, and then re-do the rustc push.
If this fails due to authentication problems, it can help to make josh push via ssh instead of
https. Add the following to your `.gitconfig`:

```toml
```text
[url "git@github.com:"]
pushInsteadOf = https://github.com/
```
Expand Down
5 changes: 5 additions & 0 deletions src/tools/miri/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -651,6 +651,11 @@ Violations of [Stacked Borrows] found that are likely bugs (but Stacked Borrows
* [Stacked Borrows: An Aliasing Model for Rust](https://plv.mpi-sws.org/rustbelt/stacked-borrows/)
* [Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3](https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3)
* [SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis](https://dl.acm.org/doi/10.1145/3453483.3454084)
* [Crabtree: Rust API Test Synthesis Guided by Coverage and Type](https://dl.acm.org/doi/10.1145/3689733)
* [Rustlantis: Randomized Differential Testing of the Rust Compiler](https://dl.acm.org/doi/10.1145/3689780)
* [A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries](https://arxiv.org/abs/2404.11671)
* [Tree Borrows](https://plf.inf.ethz.ch/research/pldi25-tree-borrows.html)
* [Miri: Practical Undefined Behavior Detection for Rust](https://plf.inf.ethz.ch/research/popl26-miri.html) **(this paper describes Miri itself)**

## License

Expand Down
47 changes: 21 additions & 26 deletions src/tools/miri/doc/genmc.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
# **(WIP)** Documentation for Miri-GenMC

**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).**

**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572) and [other limitations](#limitations). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).**

[GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program.
Miri-GenMC integrates that model checker into Miri.
Expand All @@ -12,11 +11,14 @@ This includes all possible thread interleavings and all allowed return values fo
It is hence still possible to have latent bugs in a test case even if they passed GenMC.)

GenMC requires the input program to be bounded, i.e., have finitely many possible executions, otherwise it will not terminate.
Any loops that may run infinitely must be replaced or bounded (see below).
Any loops that may run infinitely must be replaced or bounded (see [below](#eliminating-unbounded-loops)).

GenMC makes use of Dynamic Partial Order Reduction (DPOR) to reduce the number of executions that must be explored, but the runtime can still be super-exponential in the size of the input program (number of threads and amount of interaction between threads).
Large programs may not be verifiable in a reasonable amount of time.

GenMC currently only supports Linux hosts.
Both the host and the target must be 64-bit little-endian.

## Usage

For testing/developing Miri-GenMC:
Expand Down Expand Up @@ -50,16 +52,24 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
- `debug2`: Print the execution graph after every memory access.
- `debug3`: Print reads-from values considered by GenMC.
- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.

#### Regular Miri parameters useful for GenMC mode

- `-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled).

<!-- FIXME(genmc): explain Miri-GenMC specific functions. -->

## Tips
## Limitations

There are several limitations which can make GenMC miss bugs:
- GenMC does not support re-using freed memory for new allocations, so any bugs related to that will be missed.
- GenMC does not support `compare_exchange_weak`, so the consequences of spurious failures are not explored.
A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies).
- GenMC does not support the separate failure ordering of `compare_exchange`. Miri will take the maximum of the success and failure ordering and use that for the access; outcomes that rely on the real ordering being weaker will not be explored.
A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies).
- GenMC is incompatible with borrow tracking (Stacked/Tree Borrows). You need to set `-Zmiri-disable-stacked-borrows` to use GenMC.
- Like all C++ memory model verification tools, GenMC has to solve the [out-of-thin-air problem](https://www.cl.cam.ac.uk/~pes20/cpp/notes42.html).
It takes the [usual approach](https://plv.mpi-sws.org/scfix/paper.pdf) of requiring the union of "program-order" and "reads-from" to be acyclic.
This means it excludes certain behaviors allowed by the C++ memory model, some of which can occur on hardware that performs load buffering.

<!-- FIXME(genmc): add tips for using Miri-GenMC more efficiently. -->
## Tips

### Eliminating unbounded loops

Expand Down Expand Up @@ -121,24 +131,11 @@ fn count_until_true_genmc(flag: &AtomicBool) -> u64 {
<!-- FIXME: update the code above once Miri supports a loop bounding features like GenMC's `--unroll=N`. -->
<!-- FIXME: update this section once Miri-GenMC supports automatic program transformations (like spinloop-assume replacement). -->

## Limitations

Some or all of these limitations might get removed in the future:

- Borrow tracking is currently incompatible (stacked/tree borrows).
- Only Linux is supported for now.
- No support for 32-bit or big-endian targets.
- No cross-target interpretation.

<!-- FIXME(genmc): document remaining limitations -->

## Development

GenMC is written in C++, which complicates development a bit.
The prerequisites for building Miri-GenMC are:
- A compiler with C++23 support.
- LLVM developments headers and clang.
<!-- FIXME(genmc,llvm): remove once LLVM dependency is no longer required. -->
- A compiler with sufficient C++20 support (we are testing GCC 13).

The actual code for GenMC is not contained in the Miri repo itself, but in a [separate GenMC repo](https://github.com/MPI-SWS/genmc) (with its own maintainers).
These sources need to be available to build Miri-GenMC.
Expand All @@ -149,6 +146,8 @@ The process for obtaining them is as follows:
If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
formatting the Rust files inside that folder.

<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->

### Formatting the C++ code

For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory.
Expand All @@ -157,7 +156,3 @@ With `clang-format` installed, run this command to format the c++ files (replace
find ./genmc-sys/cpp/ -name "*.cpp" -o -name "*.hpp" | xargs clang-format --style=file:"./genmc-sys/.clang-format" -i
```
NOTE: this is currently not done automatically on pull requests to Miri.

<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->

<!-- FIXME(genmc): explain development. -->
2 changes: 1 addition & 1 deletion src/tools/miri/rust-version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
36b2369c91d32c2659887ed6fe3d570640f44fd2
dc47a69ed94bc88b10b7d500cceacf29b87bcbbe
13 changes: 5 additions & 8 deletions src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -826,15 +826,12 @@ trait EvalContextPrivExt<'tcx, 'ecx>: crate::MiriInterpCxExt<'tcx> {
// FIXME: If we cannot determine the size (because the unsized tail is an `extern type`),
// bail out -- we cannot reasonably figure out which memory range to reborrow.
// See https://github.com/rust-lang/unsafe-code-guidelines/issues/276.
let size = match size {
Some(size) => size,
None => {
static DEDUP: AtomicBool = AtomicBool::new(false);
if !DEDUP.swap(true, std::sync::atomic::Ordering::Relaxed) {
this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow);
}
return interp_ok(place.clone());
let Some(size) = size else {
static DEDUP: AtomicBool = AtomicBool::new(false);
if !DEDUP.swap(true, std::sync::atomic::Ordering::Relaxed) {
this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow);
}
return interp_ok(place.clone());
};

// Compute new borrow.
Expand Down
66 changes: 44 additions & 22 deletions src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,32 @@ pub struct Event {
pub span: Span,
}

/// Diagnostics data about the current access and the location we are accessing.
/// Used to create history events and errors.
#[derive(Clone, Debug)]
pub struct DiagnosticInfo {
pub alloc_id: AllocId,
pub span: Span,
/// The range the diagnostic actually applies to.
/// This is always a subset of `access_range`.
pub transition_range: Range<u64>,
/// The range the access is happening to. Is `None` if this is the protector release access
pub access_range: Option<AllocRange>,
pub access_cause: AccessCause,
}
impl DiagnosticInfo {
/// Creates a history event.
pub fn create_event(&self, transition: PermTransition, is_foreign: bool) -> Event {
Event {
transition,
is_foreign,
access_cause: self.access_cause,
access_range: self.access_range,
transition_range: self.transition_range.clone(),
span: self.span,
}
}
}
/// List of all events that affected a tag.
/// NOTE: not all of these events are relevant for a particular location,
/// the events should be filtered before the generation of diagnostics.
Expand Down Expand Up @@ -280,32 +306,29 @@ impl History {
pub(super) struct TbError<'node> {
/// What failure occurred.
pub error_kind: TransitionError,
/// The allocation in which the error is happening.
pub alloc_id: AllocId,
/// The offset (into the allocation) at which the conflict occurred.
pub error_offset: u64,
/// Diagnostic data about the access that caused the error.
pub access_info: &'node DiagnosticInfo,
/// The tag on which the error was triggered.
/// On protector violations, this is the tag that was protected.
/// On accesses rejected due to insufficient permissions, this is the
/// tag that lacked those permissions.
pub conflicting_info: &'node NodeDebugInfo,
// What kind of access caused this error (read, write, reborrow, deallocation)
pub access_cause: AccessCause,
pub conflicting_node_info: &'node NodeDebugInfo,
/// Which tag, if any, the access that caused this error was made through, i.e.
/// which tag was used to read/write/deallocate.
/// Not set on wildcard accesses.
pub accessed_info: Option<&'node NodeDebugInfo>,
pub accessed_node_info: Option<&'node NodeDebugInfo>,
}

impl TbError<'_> {
/// Produce a UB error.
pub fn build<'tcx>(self) -> InterpErrorKind<'tcx> {
use TransitionError::*;
let cause = self.access_cause;
let accessed = self.accessed_info;
let cause = self.access_info.access_cause;
let error_offset = self.access_info.transition_range.start;
let accessed = self.accessed_node_info;
let accessed_str =
self.accessed_info.map(|v| format!("{v}")).unwrap_or_else(|| "<wildcard>".into());
let conflicting = self.conflicting_info;
self.accessed_node_info.map(|v| format!("{v}")).unwrap_or_else(|| "<wildcard>".into());
let conflicting = self.conflicting_node_info;
// An access is considered conflicting if it happened through a
// different tag than the one who caused UB.
// When doing a wildcard access (where `accessed` is `None`) we
Expand All @@ -316,9 +339,8 @@ impl TbError<'_> {
// all tags through which an access would cause UB.
let accessed_is_conflicting = accessed.map(|a| a.tag) == Some(conflicting.tag);
let title = format!(
"{cause} through {accessed_str} at {alloc_id:?}[{offset:#x}] is forbidden",
alloc_id = self.alloc_id,
offset = self.error_offset
"{cause} through {accessed_str} at {alloc_id:?}[{error_offset:#x}] is forbidden",
alloc_id = self.access_info.alloc_id
);
let (title, details, conflicting_tag_name) = match self.error_kind {
ChildAccessForbidden(perm) => {
Expand Down Expand Up @@ -362,13 +384,13 @@ impl TbError<'_> {
}
};
let mut history = HistoryData::default();
if let Some(accessed_info) = self.accessed_info
if let Some(accessed_info) = self.accessed_node_info
&& !accessed_is_conflicting
{
history.extend(accessed_info.history.forget(), "accessed", false);
}
history.extend(
self.conflicting_info.history.extract_relevant(self.error_offset, self.error_kind),
self.conflicting_node_info.history.extract_relevant(error_offset, self.error_kind),
conflicting_tag_name,
true,
);
Expand All @@ -379,12 +401,12 @@ impl TbError<'_> {
/// Cannot access this allocation with wildcard provenance, as there are no
/// valid exposed references for this access kind.
pub fn no_valid_exposed_references_error<'tcx>(
alloc_id: AllocId,
offset: u64,
access_cause: AccessCause,
DiagnosticInfo { alloc_id, transition_range, access_cause, .. }: &DiagnosticInfo,
) -> InterpErrorKind<'tcx> {
let title =
format!("{access_cause} through <wildcard> at {alloc_id:?}[{offset:#x}] is forbidden");
let title = format!(
"{access_cause} through <wildcard> at {alloc_id:?}[{offset:#x}] is forbidden",
offset = transition_range.start
);
let details = vec![format!("there are no exposed tags which may perform this access here")];
let history = HistoryData::default();
err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history })
Expand Down
51 changes: 25 additions & 26 deletions src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,9 @@ impl<'tcx> Tree {
let span = machine.current_user_relevant_span();
self.perform_access(
prov,
Some((range, access_kind, diagnostics::AccessCause::Explicit(access_kind))),
range,
access_kind,
diagnostics::AccessCause::Explicit(access_kind),
global,
alloc_id,
span,
Expand Down Expand Up @@ -94,8 +96,7 @@ impl<'tcx> Tree {
alloc_id: AllocId, // diagnostics
) -> InterpResult<'tcx> {
let span = machine.current_user_relevant_span();
// `None` makes it the magic on-protector-end operation
self.perform_access(ProvenanceExtra::Concrete(tag), None, global, alloc_id, span)?;
self.perform_protector_end_access(tag, global, alloc_id, span)?;

self.update_exposure_for_protector_release(tag);

Expand Down Expand Up @@ -219,26 +220,18 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
};

trace!("Reborrow of size {:?}", ptr_size);
let (alloc_id, base_offset, parent_prov) = match this.ptr_try_get_alloc_id(place.ptr(), 0) {
Ok(data) => {
// Unlike SB, we *do* a proper retag for size 0 if can identify the allocation.
// After all, the pointer may be lazily initialized outside this initial range.
data
}
Err(_) => {
assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here
// This pointer doesn't come with an AllocId, so there's no
// memory to do retagging in.
let new_prov = place.ptr().provenance;
trace!(
"reborrow of size 0: reusing {:?} (pointee {})",
place.ptr(),
place.layout.ty,
);
log_creation(this, None)?;
// Keep original provenance.
return interp_ok(new_prov);
}
// Unlike SB, we *do* a proper retag for size 0 if can identify the allocation.
// After all, the pointer may be lazily initialized outside this initial range.
let Ok((alloc_id, base_offset, parent_prov)) = this.ptr_try_get_alloc_id(place.ptr(), 0)
else {
assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here
// This pointer doesn't come with an AllocId, so there's no
// memory to do retagging in.
let new_prov = place.ptr().provenance;
trace!("reborrow of size 0: reusing {:?} (pointee {})", place.ptr(), place.layout.ty,);
log_creation(this, None)?;
// Keep original provenance.
return interp_ok(new_prov);
};
let new_prov = Provenance::Concrete { alloc_id, tag: new_tag };

Expand Down Expand Up @@ -344,7 +337,9 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {

tree_borrows.perform_access(
parent_prov,
Some((range_in_alloc, AccessKind::Read, diagnostics::AccessCause::Reborrow)),
range_in_alloc,
AccessKind::Read,
diagnostics::AccessCause::Reborrow,
this.machine.borrow_tracker.as_ref().unwrap(),
alloc_id,
this.machine.current_user_relevant_span(),
Expand Down Expand Up @@ -609,8 +604,12 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let this = self.eval_context_mut();
let (tag, alloc_id) = match ptr.provenance {
Some(Provenance::Concrete { tag, alloc_id }) => (tag, alloc_id),
_ => {
eprintln!("Can't give the name {name} to Wildcard pointer");
Some(Provenance::Wildcard) => {
eprintln!("Can't give the name {name} to wildcard pointer");
return interp_ok(());
}
None => {
eprintln!("Can't give the name {name} to pointer without provenance");
return interp_ok(());
}
};
Expand Down
Loading
Loading