Skip to content

Commit b655ea3

Browse files
authored
Rollup merge of #149998 - RalfJung:miri, r=RalfJung
miri subtree update Subtree update of `miri` to rust-lang/miri@b796ced. Created using https://github.com/rust-lang/josh-sync. r? `@ghost`
2 parents 98f8736 + 05227a7 commit b655ea3

File tree

60 files changed

+397
-1135
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+397
-1135
lines changed

src/tools/miri/CONTRIBUTING.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -351,7 +351,7 @@ you need to pull rustc changes into Miri first, and then re-do the rustc push.
351351
If this fails due to authentication problems, it can help to make josh push via ssh instead of
352352
https. Add the following to your `.gitconfig`:
353353

354-
```toml
354+
```text
355355
[url "git@github.com:"]
356356
pushInsteadOf = https://github.com/
357357
```

src/tools/miri/README.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -651,6 +651,11 @@ Violations of [Stacked Borrows] found that are likely bugs (but Stacked Borrows
651651
* [Stacked Borrows: An Aliasing Model for Rust](https://plv.mpi-sws.org/rustbelt/stacked-borrows/)
652652
* [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)
653653
* [SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis](https://dl.acm.org/doi/10.1145/3453483.3454084)
654+
* [Crabtree: Rust API Test Synthesis Guided by Coverage and Type](https://dl.acm.org/doi/10.1145/3689733)
655+
* [Rustlantis: Randomized Differential Testing of the Rust Compiler](https://dl.acm.org/doi/10.1145/3689780)
656+
* [A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries](https://arxiv.org/abs/2404.11671)
657+
* [Tree Borrows](https://plf.inf.ethz.ch/research/pldi25-tree-borrows.html)
658+
* [Miri: Practical Undefined Behavior Detection for Rust](https://plf.inf.ethz.ch/research/popl26-miri.html) **(this paper describes Miri itself)**
654659

655660
## License
656661

src/tools/miri/doc/genmc.md

Lines changed: 21 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
# **(WIP)** Documentation for Miri-GenMC
22

3-
**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).**
4-
3+
**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).**
54

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

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

1716
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).
1817
Large programs may not be verifiable in a reasonable amount of time.
1918

19+
GenMC currently only supports Linux hosts.
20+
Both the host and the target must be 64-bit little-endian.
21+
2022
## Usage
2123

2224
For testing/developing Miri-GenMC:
@@ -50,16 +52,24 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
5052
- `debug2`: Print the execution graph after every memory access.
5153
- `debug3`: Print reads-from values considered by GenMC.
5254
- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.
53-
54-
#### Regular Miri parameters useful for GenMC mode
55-
5655
- `-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).
5756

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

60-
## Tips
59+
## Limitations
60+
61+
There are several limitations which can make GenMC miss bugs:
62+
- GenMC does not support re-using freed memory for new allocations, so any bugs related to that will be missed.
63+
- GenMC does not support `compare_exchange_weak`, so the consequences of spurious failures are not explored.
64+
A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies).
65+
- 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.
66+
A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies).
67+
- GenMC is incompatible with borrow tracking (Stacked/Tree Borrows). You need to set `-Zmiri-disable-stacked-borrows` to use GenMC.
68+
- 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).
69+
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.
70+
This means it excludes certain behaviors allowed by the C++ memory model, some of which can occur on hardware that performs load buffering.
6171

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

6474
### Eliminating unbounded loops
6575

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

124-
## Limitations
125-
126-
Some or all of these limitations might get removed in the future:
127-
128-
- Borrow tracking is currently incompatible (stacked/tree borrows).
129-
- Only Linux is supported for now.
130-
- No support for 32-bit or big-endian targets.
131-
- No cross-target interpretation.
132-
133-
<!-- FIXME(genmc): document remaining limitations -->
134-
135134
## Development
136135

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

143140
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).
144141
These sources need to be available to build Miri-GenMC.
@@ -149,6 +146,8 @@ The process for obtaining them is as follows:
149146
If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
150147
formatting the Rust files inside that folder.
151148

149+
<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
150+
152151
### Formatting the C++ code
153152

154153
For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory.
@@ -157,7 +156,3 @@ With `clang-format` installed, run this command to format the c++ files (replace
157156
find ./genmc-sys/cpp/ -name "*.cpp" -o -name "*.hpp" | xargs clang-format --style=file:"./genmc-sys/.clang-format" -i
158157
```
159158
NOTE: this is currently not done automatically on pull requests to Miri.
160-
161-
<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
162-
163-
<!-- FIXME(genmc): explain development. -->

src/tools/miri/rust-version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
36b2369c91d32c2659887ed6fe3d570640f44fd2
1+
dc47a69ed94bc88b10b7d500cceacf29b87bcbbe

src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -826,15 +826,12 @@ trait EvalContextPrivExt<'tcx, 'ecx>: crate::MiriInterpCxExt<'tcx> {
826826
// FIXME: If we cannot determine the size (because the unsized tail is an `extern type`),
827827
// bail out -- we cannot reasonably figure out which memory range to reborrow.
828828
// See https://github.com/rust-lang/unsafe-code-guidelines/issues/276.
829-
let size = match size {
830-
Some(size) => size,
831-
None => {
832-
static DEDUP: AtomicBool = AtomicBool::new(false);
833-
if !DEDUP.swap(true, std::sync::atomic::Ordering::Relaxed) {
834-
this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow);
835-
}
836-
return interp_ok(place.clone());
829+
let Some(size) = size else {
830+
static DEDUP: AtomicBool = AtomicBool::new(false);
831+
if !DEDUP.swap(true, std::sync::atomic::Ordering::Relaxed) {
832+
this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow);
837833
}
834+
return interp_ok(place.clone());
838835
};
839836

840837
// Compute new borrow.

src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs

Lines changed: 44 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,32 @@ pub struct Event {
7777
pub span: Span,
7878
}
7979

80+
/// Diagnostics data about the current access and the location we are accessing.
81+
/// Used to create history events and errors.
82+
#[derive(Clone, Debug)]
83+
pub struct DiagnosticInfo {
84+
pub alloc_id: AllocId,
85+
pub span: Span,
86+
/// The range the diagnostic actually applies to.
87+
/// This is always a subset of `access_range`.
88+
pub transition_range: Range<u64>,
89+
/// The range the access is happening to. Is `None` if this is the protector release access
90+
pub access_range: Option<AllocRange>,
91+
pub access_cause: AccessCause,
92+
}
93+
impl DiagnosticInfo {
94+
/// Creates a history event.
95+
pub fn create_event(&self, transition: PermTransition, is_foreign: bool) -> Event {
96+
Event {
97+
transition,
98+
is_foreign,
99+
access_cause: self.access_cause,
100+
access_range: self.access_range,
101+
transition_range: self.transition_range.clone(),
102+
span: self.span,
103+
}
104+
}
105+
}
80106
/// List of all events that affected a tag.
81107
/// NOTE: not all of these events are relevant for a particular location,
82108
/// the events should be filtered before the generation of diagnostics.
@@ -280,32 +306,29 @@ impl History {
280306
pub(super) struct TbError<'node> {
281307
/// What failure occurred.
282308
pub error_kind: TransitionError,
283-
/// The allocation in which the error is happening.
284-
pub alloc_id: AllocId,
285-
/// The offset (into the allocation) at which the conflict occurred.
286-
pub error_offset: u64,
309+
/// Diagnostic data about the access that caused the error.
310+
pub access_info: &'node DiagnosticInfo,
287311
/// The tag on which the error was triggered.
288312
/// On protector violations, this is the tag that was protected.
289313
/// On accesses rejected due to insufficient permissions, this is the
290314
/// tag that lacked those permissions.
291-
pub conflicting_info: &'node NodeDebugInfo,
292-
// What kind of access caused this error (read, write, reborrow, deallocation)
293-
pub access_cause: AccessCause,
315+
pub conflicting_node_info: &'node NodeDebugInfo,
294316
/// Which tag, if any, the access that caused this error was made through, i.e.
295317
/// which tag was used to read/write/deallocate.
296318
/// Not set on wildcard accesses.
297-
pub accessed_info: Option<&'node NodeDebugInfo>,
319+
pub accessed_node_info: Option<&'node NodeDebugInfo>,
298320
}
299321

300322
impl TbError<'_> {
301323
/// Produce a UB error.
302324
pub fn build<'tcx>(self) -> InterpErrorKind<'tcx> {
303325
use TransitionError::*;
304-
let cause = self.access_cause;
305-
let accessed = self.accessed_info;
326+
let cause = self.access_info.access_cause;
327+
let error_offset = self.access_info.transition_range.start;
328+
let accessed = self.accessed_node_info;
306329
let accessed_str =
307-
self.accessed_info.map(|v| format!("{v}")).unwrap_or_else(|| "<wildcard>".into());
308-
let conflicting = self.conflicting_info;
330+
self.accessed_node_info.map(|v| format!("{v}")).unwrap_or_else(|| "<wildcard>".into());
331+
let conflicting = self.conflicting_node_info;
309332
// An access is considered conflicting if it happened through a
310333
// different tag than the one who caused UB.
311334
// When doing a wildcard access (where `accessed` is `None`) we
@@ -316,9 +339,8 @@ impl TbError<'_> {
316339
// all tags through which an access would cause UB.
317340
let accessed_is_conflicting = accessed.map(|a| a.tag) == Some(conflicting.tag);
318341
let title = format!(
319-
"{cause} through {accessed_str} at {alloc_id:?}[{offset:#x}] is forbidden",
320-
alloc_id = self.alloc_id,
321-
offset = self.error_offset
342+
"{cause} through {accessed_str} at {alloc_id:?}[{error_offset:#x}] is forbidden",
343+
alloc_id = self.access_info.alloc_id
322344
);
323345
let (title, details, conflicting_tag_name) = match self.error_kind {
324346
ChildAccessForbidden(perm) => {
@@ -362,13 +384,13 @@ impl TbError<'_> {
362384
}
363385
};
364386
let mut history = HistoryData::default();
365-
if let Some(accessed_info) = self.accessed_info
387+
if let Some(accessed_info) = self.accessed_node_info
366388
&& !accessed_is_conflicting
367389
{
368390
history.extend(accessed_info.history.forget(), "accessed", false);
369391
}
370392
history.extend(
371-
self.conflicting_info.history.extract_relevant(self.error_offset, self.error_kind),
393+
self.conflicting_node_info.history.extract_relevant(error_offset, self.error_kind),
372394
conflicting_tag_name,
373395
true,
374396
);
@@ -379,12 +401,12 @@ impl TbError<'_> {
379401
/// Cannot access this allocation with wildcard provenance, as there are no
380402
/// valid exposed references for this access kind.
381403
pub fn no_valid_exposed_references_error<'tcx>(
382-
alloc_id: AllocId,
383-
offset: u64,
384-
access_cause: AccessCause,
404+
DiagnosticInfo { alloc_id, transition_range, access_cause, .. }: &DiagnosticInfo,
385405
) -> InterpErrorKind<'tcx> {
386-
let title =
387-
format!("{access_cause} through <wildcard> at {alloc_id:?}[{offset:#x}] is forbidden");
406+
let title = format!(
407+
"{access_cause} through <wildcard> at {alloc_id:?}[{offset:#x}] is forbidden",
408+
offset = transition_range.start
409+
);
388410
let details = vec![format!("there are no exposed tags which may perform this access here")];
389411
let history = HistoryData::default();
390412
err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history })

src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

Lines changed: 25 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,9 @@ impl<'tcx> Tree {
6060
let span = machine.current_user_relevant_span();
6161
self.perform_access(
6262
prov,
63-
Some((range, access_kind, diagnostics::AccessCause::Explicit(access_kind))),
63+
range,
64+
access_kind,
65+
diagnostics::AccessCause::Explicit(access_kind),
6466
global,
6567
alloc_id,
6668
span,
@@ -94,8 +96,7 @@ impl<'tcx> Tree {
9496
alloc_id: AllocId, // diagnostics
9597
) -> InterpResult<'tcx> {
9698
let span = machine.current_user_relevant_span();
97-
// `None` makes it the magic on-protector-end operation
98-
self.perform_access(ProvenanceExtra::Concrete(tag), None, global, alloc_id, span)?;
99+
self.perform_protector_end_access(tag, global, alloc_id, span)?;
99100

100101
self.update_exposure_for_protector_release(tag);
101102

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

221222
trace!("Reborrow of size {:?}", ptr_size);
222-
let (alloc_id, base_offset, parent_prov) = match this.ptr_try_get_alloc_id(place.ptr(), 0) {
223-
Ok(data) => {
224-
// Unlike SB, we *do* a proper retag for size 0 if can identify the allocation.
225-
// After all, the pointer may be lazily initialized outside this initial range.
226-
data
227-
}
228-
Err(_) => {
229-
assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here
230-
// This pointer doesn't come with an AllocId, so there's no
231-
// memory to do retagging in.
232-
let new_prov = place.ptr().provenance;
233-
trace!(
234-
"reborrow of size 0: reusing {:?} (pointee {})",
235-
place.ptr(),
236-
place.layout.ty,
237-
);
238-
log_creation(this, None)?;
239-
// Keep original provenance.
240-
return interp_ok(new_prov);
241-
}
223+
// Unlike SB, we *do* a proper retag for size 0 if can identify the allocation.
224+
// After all, the pointer may be lazily initialized outside this initial range.
225+
let Ok((alloc_id, base_offset, parent_prov)) = this.ptr_try_get_alloc_id(place.ptr(), 0)
226+
else {
227+
assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here
228+
// This pointer doesn't come with an AllocId, so there's no
229+
// memory to do retagging in.
230+
let new_prov = place.ptr().provenance;
231+
trace!("reborrow of size 0: reusing {:?} (pointee {})", place.ptr(), place.layout.ty,);
232+
log_creation(this, None)?;
233+
// Keep original provenance.
234+
return interp_ok(new_prov);
242235
};
243236
let new_prov = Provenance::Concrete { alloc_id, tag: new_tag };
244237

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

345338
tree_borrows.perform_access(
346339
parent_prov,
347-
Some((range_in_alloc, AccessKind::Read, diagnostics::AccessCause::Reborrow)),
340+
range_in_alloc,
341+
AccessKind::Read,
342+
diagnostics::AccessCause::Reborrow,
348343
this.machine.borrow_tracker.as_ref().unwrap(),
349344
alloc_id,
350345
this.machine.current_user_relevant_span(),
@@ -609,8 +604,12 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
609604
let this = self.eval_context_mut();
610605
let (tag, alloc_id) = match ptr.provenance {
611606
Some(Provenance::Concrete { tag, alloc_id }) => (tag, alloc_id),
612-
_ => {
613-
eprintln!("Can't give the name {name} to Wildcard pointer");
607+
Some(Provenance::Wildcard) => {
608+
eprintln!("Can't give the name {name} to wildcard pointer");
609+
return interp_ok(());
610+
}
611+
None => {
612+
eprintln!("Can't give the name {name} to pointer without provenance");
614613
return interp_ok(());
615614
}
616615
};

0 commit comments

Comments
 (0)