Skip to content

Commit 2a4a8c8

Browse files
committed
Auto merge of #113974 - RalfJung:miri, r=RalfJung
update Miri r? `@ghost`
2 parents cec34a4 + 0c9d1a3 commit 2a4a8c8

24 files changed

+166
-100
lines changed

src/tools/miri/.github/workflows/ci.yml

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,12 @@ jobs:
115115
run: cargo install -f rustup-toolchain-install-master
116116

117117
- name: Install "master" toolchain
118-
run: ./miri toolchain
118+
run: |
119+
if [[ ${{ github.event_name }} == 'schedule' ]]; then
120+
echo "Building against latest rustc git version"
121+
git ls-remote https://github.com/rust-lang/rust/ HEAD | cut -f 1 > rust-version
122+
fi
123+
./miri toolchain
119124
120125
- name: Show Rust version
121126
run: |
@@ -203,7 +208,7 @@ jobs:
203208
./miri fmt --check || (./miri fmt && git commit -am "fmt")
204209
- name: Push changes to a branch
205210
run: |
206-
BRANCH="rustup$(date -u +%Y-%m-%d)"
211+
BRANCH="rustup-$(date -u +%Y-%m-%d)"
207212
git switch -c $BRANCH
208213
git push -u origin $BRANCH
209214
- name: Create Pull Request

src/tools/miri/README.md

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -74,12 +74,19 @@ behavior** in your program, and cannot run all programs:
7474
unobservable by compiled programs running on real hardware when `SeqCst` fences are used, and it
7575
cannot produce all behaviors possibly observable on real hardware.
7676

77+
Moreover, Miri fundamentally cannot tell you whether your code is *sound*. [Soundness] is the property
78+
of never causing undefined behavior when invoked from arbitrary safe code, even in combination with
79+
other sound code. In contrast, Miri can just tell you if *a particular way of interacting with your
80+
code* (e.g., a test suite) causes any undefined behavior. It is up to you to ensure sufficient
81+
coverage.
82+
7783
[rust]: https://www.rust-lang.org/
7884
[mir]: https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md
7985
[`unreachable_unchecked`]: https://doc.rust-lang.org/stable/std/hint/fn.unreachable_unchecked.html
8086
[`copy_nonoverlapping`]: https://doc.rust-lang.org/stable/std/ptr/fn.copy_nonoverlapping.html
8187
[Stacked Borrows]: https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md
8288
[Tree Borrows]: https://perso.crans.org/vanille/treebor/
89+
[Soundness]: https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#soundness-of-code--of-a-library
8390

8491

8592
## Using Miri
@@ -400,15 +407,11 @@ to Miri failing to detect cases of undefined behavior in a program.
400407
application instead of raising an error within the context of Miri (and halting
401408
execution). Note that code might not expect these operations to ever panic, so
402409
this flag can lead to strange (mis)behavior.
403-
* `-Zmiri-retag-fields` changes Stacked Borrows retagging to recurse into *all* fields.
404-
This means that references in fields of structs/enums/tuples/arrays/... are retagged,
405-
and in particular, they are protected when passed as function arguments.
406-
(The default is to recurse only in cases where rustc would actually emit a `noalias` attribute.)
407-
* `-Zmiri-retag-fields=<all|none|scalar>` controls when Stacked Borrows retagging recurses into
408-
fields. `all` means it always recurses (like `-Zmiri-retag-fields`), `none` means it never
409-
recurses, `scalar` (the default) means it only recurses for types where we would also emit
410-
`noalias` annotations in the generated LLVM IR (types passed as individual scalars or pairs of
411-
scalars). Setting this to `none` is **unsound**.
410+
* `-Zmiri-retag-fields[=<all|none|scalar>]` controls when Stacked Borrows retagging recurses into
411+
fields. `all` means it always recurses (the default, and equivalent to `-Zmiri-retag-fields`
412+
without an explicit value), `none` means it never recurses, `scalar` means it only recurses for
413+
types where we would also emit `noalias` annotations in the generated LLVM IR (types passed as
414+
individual scalars or pairs of scalars). Setting this to `none` is **unsound**.
412415
* `-Zmiri-tag-gc=<blocks>` configures how often the pointer tag garbage collector runs. The default
413416
is to search for and remove unreachable tags once every `10000` basic blocks. Setting this to
414417
`0` disables the garbage collector, which causes some programs to have explosive memory usage

src/tools/miri/miri

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,9 @@ toolchain)
9797
CUR_COMMIT=$(rustc +miri --version -v 2>/dev/null | grep "^commit-hash: " | cut -d " " -f 2)
9898
if [[ "$CUR_COMMIT" == "$NEW_COMMIT" ]]; then
9999
echo "miri toolchain is already at commit $CUR_COMMIT."
100-
rustup override set miri
100+
if [[ "$TOOLCHAIN" != "miri" ]]; then
101+
rustup override set miri
102+
fi
101103
exit 0
102104
fi
103105
# Install and setup new toolchain.

src/tools/miri/rust-version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
33a2c2487ac5d9927830ea4c1844335c6b9f77db
1+
cec34a43b1b14f4e39363f3b283d7ac4f593ee81

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -413,7 +413,7 @@ impl AllocState {
413413
alloc_id: AllocId,
414414
prov_extra: ProvenanceExtra,
415415
range: AllocRange,
416-
machine: &mut MiriMachine<'_, 'tcx>,
416+
machine: &MiriMachine<'_, 'tcx>,
417417
) -> InterpResult<'tcx> {
418418
match self {
419419
AllocState::StackedBorrows(sb) =>
@@ -434,7 +434,7 @@ impl AllocState {
434434
alloc_id: AllocId,
435435
prov_extra: ProvenanceExtra,
436436
range: AllocRange,
437-
machine: &mut MiriMachine<'_, 'tcx>,
437+
machine: &MiriMachine<'_, 'tcx>,
438438
) -> InterpResult<'tcx> {
439439
match self {
440440
AllocState::StackedBorrows(sb) =>

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

Lines changed: 45 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,19 @@ use rustc_span::{Span, SpanData};
66
use rustc_target::abi::Size;
77

88
use crate::borrow_tracker::{
9-
stacked_borrows::{err_sb_ub, Permission},
10-
AccessKind, GlobalStateInner, ProtectorKind,
9+
stacked_borrows::Permission, AccessKind, GlobalStateInner, ProtectorKind,
1110
};
1211
use crate::*;
1312

13+
/// Error reporting
14+
fn err_sb_ub<'tcx>(
15+
msg: String,
16+
help: Vec<String>,
17+
history: Option<TagHistory>,
18+
) -> InterpError<'tcx> {
19+
err_machine_stop!(TerminationInfo::StackedBorrowsUb { msg, help, history })
20+
}
21+
1422
#[derive(Clone, Debug)]
1523
pub struct AllocHistory {
1624
id: AllocId,
@@ -61,12 +69,15 @@ struct Invalidation {
6169
#[derive(Clone, Debug)]
6270
enum InvalidationCause {
6371
Access(AccessKind),
64-
Retag(Permission, RetagCause),
72+
Retag(Permission, RetagInfo),
6573
}
6674

6775
impl Invalidation {
6876
fn generate_diagnostic(&self) -> (String, SpanData) {
69-
let message = if let InvalidationCause::Retag(_, RetagCause::FnEntry) = self.cause {
77+
let message = if matches!(
78+
self.cause,
79+
InvalidationCause::Retag(_, RetagInfo { cause: RetagCause::FnEntry, .. })
80+
) {
7081
// For a FnEntry retag, our Span points at the caller.
7182
// See `DiagnosticCx::log_invalidation`.
7283
format!(
@@ -87,8 +98,8 @@ impl fmt::Display for InvalidationCause {
8798
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
8899
match self {
89100
InvalidationCause::Access(kind) => write!(f, "{kind}"),
90-
InvalidationCause::Retag(perm, kind) =>
91-
write!(f, "{perm:?} {retag}", retag = kind.summary()),
101+
InvalidationCause::Retag(perm, info) =>
102+
write!(f, "{perm:?} {retag}", retag = info.summary()),
92103
}
93104
}
94105
}
@@ -129,13 +140,13 @@ impl<'ecx, 'mir, 'tcx> DiagnosticCxBuilder<'ecx, 'mir, 'tcx> {
129140

130141
pub fn retag(
131142
machine: &'ecx MiriMachine<'mir, 'tcx>,
132-
cause: RetagCause,
143+
info: RetagInfo,
133144
new_tag: BorTag,
134145
orig_tag: ProvenanceExtra,
135146
range: AllocRange,
136147
) -> Self {
137148
let operation =
138-
Operation::Retag(RetagOp { cause, new_tag, orig_tag, range, permission: None });
149+
Operation::Retag(RetagOp { info, new_tag, orig_tag, range, permission: None });
139150

140151
DiagnosticCxBuilder { machine, operation }
141152
}
@@ -179,13 +190,19 @@ enum Operation {
179190

180191
#[derive(Debug, Clone)]
181192
struct RetagOp {
182-
cause: RetagCause,
193+
info: RetagInfo,
183194
new_tag: BorTag,
184195
orig_tag: ProvenanceExtra,
185196
range: AllocRange,
186197
permission: Option<Permission>,
187198
}
188199

200+
#[derive(Debug, Clone, Copy, PartialEq)]
201+
pub struct RetagInfo {
202+
pub cause: RetagCause,
203+
pub in_field: bool,
204+
}
205+
189206
#[derive(Debug, Clone, Copy, PartialEq)]
190207
pub enum RetagCause {
191208
Normal,
@@ -258,11 +275,11 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
258275
pub fn log_invalidation(&mut self, tag: BorTag) {
259276
let mut span = self.machine.current_span();
260277
let (range, cause) = match &self.operation {
261-
Operation::Retag(RetagOp { cause, range, permission, .. }) => {
262-
if *cause == RetagCause::FnEntry {
278+
Operation::Retag(RetagOp { info, range, permission, .. }) => {
279+
if info.cause == RetagCause::FnEntry {
263280
span = self.machine.caller_span();
264281
}
265-
(*range, InvalidationCause::Retag(permission.unwrap(), *cause))
282+
(*range, InvalidationCause::Retag(permission.unwrap(), *info))
266283
}
267284
Operation::Access(AccessOp { kind, range, .. }) =>
268285
(*range, InvalidationCause::Access(*kind)),
@@ -372,9 +389,13 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
372389
self.history.id,
373390
self.offset.bytes(),
374391
);
392+
let mut helps = vec![operation_summary(&op.info.summary(), self.history.id, op.range)];
393+
if op.info.in_field {
394+
helps.push(format!("errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling"));
395+
}
375396
err_sb_ub(
376397
format!("{action}{}", error_cause(stack, op.orig_tag)),
377-
Some(operation_summary(&op.cause.summary(), self.history.id, op.range)),
398+
helps,
378399
op.orig_tag.and_then(|orig_tag| self.get_logs_relevant_to(orig_tag, None)),
379400
)
380401
}
@@ -397,7 +418,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
397418
);
398419
err_sb_ub(
399420
format!("{action}{}", error_cause(stack, op.tag)),
400-
Some(operation_summary("an access", self.history.id, op.range)),
421+
vec![operation_summary("an access", self.history.id, op.range)],
401422
op.tag.and_then(|tag| self.get_logs_relevant_to(tag, None)),
402423
)
403424
}
@@ -423,7 +444,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
423444
Operation::Dealloc(_) =>
424445
err_sb_ub(
425446
format!("deallocating while item {item:?} is {protected} by call {call_id:?}",),
426-
None,
447+
vec![],
427448
None,
428449
),
429450
Operation::Retag(RetagOp { orig_tag: tag, .. })
@@ -432,7 +453,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
432453
format!(
433454
"not granting access to tag {tag:?} because that would remove {item:?} which is {protected} because it is an argument of call {call_id:?}",
434455
),
435-
None,
456+
vec![],
436457
tag.and_then(|tag| self.get_logs_relevant_to(tag, Some(item.tag()))),
437458
),
438459
}
@@ -450,7 +471,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
450471
alloc_id = self.history.id,
451472
cause = error_cause(stack, op.tag),
452473
),
453-
None,
474+
vec![],
454475
op.tag.and_then(|tag| self.get_logs_relevant_to(tag, None)),
455476
)
456477
}
@@ -496,14 +517,18 @@ fn error_cause(stack: &Stack, prov_extra: ProvenanceExtra) -> &'static str {
496517
}
497518
}
498519

499-
impl RetagCause {
520+
impl RetagInfo {
500521
fn summary(&self) -> String {
501-
match self {
522+
let mut s = match self.cause {
502523
RetagCause::Normal => "retag",
503524
RetagCause::FnEntry => "function-entry retag",
504525
RetagCause::InPlaceFnPassing => "in-place function argument/return passing protection",
505526
RetagCause::TwoPhase => "two-phase retag",
506527
}
507-
.to_string()
528+
.to_string();
529+
if self.in_field {
530+
s.push_str(" (of a reference/box inside this compound value)");
531+
}
532+
s
508533
}
509534
}

0 commit comments

Comments
 (0)