Skip to content

Commit

Permalink
Auto merge of #2275 - RalfJung:permissive-provenance-for-all, r=RalfJung
Browse files Browse the repository at this point in the history
Enable permissive provenance by default

This completes the plan laid out in #2133:
- We use permissive provenance with wildcard pointers by default.
- We print a warning on int2ptr casts. `-Zmiri-permissive-provenance` suppresses the warning; `-Zmiri-strict-provenance` turns it into a hard error.
- Raw pointer tagging is now always enabled, so we remove the `-Zmiri-tag-raw-pointers` flag and the code for untagged pointers. (Passing the flag still works, for compatibility -- but we just ignore it, with a warning.)

We also fix an intptrcast issue:
- Only live allocations are considered when computing the AllocId from an address.

So, finally, Miri has a good story for ptr2int2ptr roundtrips *and* no weird false negatives when doing raw pointer stuff with Stacked Borrows. :-) 🎉   Thanks a lot to everyone who helped with this, in particular `@carbotaniuman` who convinced me this is even possible.

Fixes #2133
Fixes #1866
Fixes #1993
  • Loading branch information
bors committed Jun 28, 2022
2 parents f5593de + c1eddbc commit 7fafbde
Show file tree
Hide file tree
Showing 78 changed files with 440 additions and 544 deletions.
47 changes: 17 additions & 30 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -289,6 +289,11 @@ environment variable. We first document the most relevant and most commonly used
`-Zmiri-disable-isolation` is set.
* `-Zmiri-ignore-leaks` disables the memory leak checker, and also allows some
remaining threads to exist when the main thread exits.
* `-Zmiri-permissive-provenance` disables the warning for integer-to-pointer casts and
[`ptr::from_exposed_addr`](https://doc.rust-lang.org/nightly/std/ptr/fn.from_exposed_addr.html).
This will necessarily miss some bugs as those operations are not efficiently and accurately
implementable in a sanitizer, but it will only miss bugs that concern memory/pointers which is
subject to these operations.
* `-Zmiri-preemption-rate` configures the probability that at the end of a basic block, the active
thread will be preempted. The default is `0.01` (i.e., 1%). Setting this to `0` disables
preemption.
Expand All @@ -306,7 +311,17 @@ environment variable. We first document the most relevant and most commonly used
* `-Zmiri-strict-provenance` enables [strict
provenance](https://github.com/rust-lang/rust/issues/95228) checking in Miri. This means that
casting an integer to a pointer yields a result with 'invalid' provenance, i.e., with provenance
that cannot be used for any memory access. Also implies `-Zmiri-tag-raw-pointers`.
that cannot be used for any memory access.
* `-Zmiri-symbolic-alignment-check` makes the alignment check more strict. By default, alignment is
checked by casting the pointer to an integer, and making sure that is a multiple of the alignment.
This can lead to cases where a program passes the alignment check by pure chance, because things
"happened to be" sufficiently aligned -- there is no UB in this execution but there would be UB in
others. To avoid such cases, the symbolic alignment check only takes into account the requested
alignment of the relevant allocation, and the offset into that allocation. This avoids missing
such bugs, but it also incurs some false positives when the code does manual integer arithmetic to
ensure alignment. (The standard library `align_to` method works fine in both modes; under
symbolic alignment it only fills the middle slice when the allocation guarantees sufficient
alignment.)

The remaining flags are for advanced use only, and more likely to change or be removed.
Some of these are **unsound**, which means they can lead
Expand All @@ -321,7 +336,7 @@ to Miri failing to detect cases of undefined behavior in a program.
integers via `mem::transmute` or union/pointer type punning. This has two effects: it disables the
check against integers storing a pointer (i.e., data with provenance), thus allowing
pointer-to-integer transmutation, and it treats integer-to-pointer transmutation as equivalent to
a cast. Using this flag is **unsound** and
a cast. Implies `-Zmiri-permissive-provenance`. Using this flag is **unsound** and
[deprecated](https://github.com/rust-lang/miri/issues/2188).
* `-Zmiri-disable-abi-check` disables checking [function ABI]. Using this flag
is **unsound**.
Expand Down Expand Up @@ -354,27 +369,6 @@ to Miri failing to detect cases of undefined behavior in a program.
application instead of raising an error within the context of Miri (and halting
execution). Note that code might not expect these operations to ever panic, so
this flag can lead to strange (mis)behavior.
* `-Zmiri-permissive-provenance` is **experimental**. This will make Miri do a
best-effort attempt to implement the semantics of
[`expose_addr`](https://doc.rust-lang.org/nightly/std/primitive.pointer.html#method.expose_addr)
and
[`ptr::from_exposed_addr`](https://doc.rust-lang.org/nightly/std/ptr/fn.from_exposed_addr.html)
for pointer-to-int and int-to-pointer casts, respectively. This will
necessarily miss some bugs as those semantics are not efficiently
implementable in a sanitizer, but it will only miss bugs that concerns
memory/pointers which is subject to these operations.
* `-Zmiri-symbolic-alignment-check` makes the alignment check more strict. By
default, alignment is checked by casting the pointer to an integer, and making
sure that is a multiple of the alignment. This can lead to cases where a
program passes the alignment check by pure chance, because things "happened to
be" sufficiently aligned -- there is no UB in this execution but there would
be UB in others. To avoid such cases, the symbolic alignment check only takes
into account the requested alignment of the relevant allocation, and the
offset into that allocation. This avoids missing such bugs, but it also
incurs some false positives when the code does manual integer arithmetic to
ensure alignment. (The standard library `align_to` method works fine in both
modes; under symbolic alignment it only fills the middle slice when the
allocation guarantees sufficient alignment.)
* `-Zmiri-track-alloc-id=<id1>,<id2>,...` shows a backtrace when the given allocations are
being allocated or freed. This helps in debugging memory leaks and
use after free bugs. Specifying this argument multiple times does not overwrite the previous
Expand All @@ -389,13 +383,6 @@ to Miri failing to detect cases of undefined behavior in a program.
happening and where in your code would be a good place to look for it.
Specifying this argument multiple times does not overwrite the previous
values, instead it appends its values to the list. Listing a tag multiple times has no effect.
* `-Zmiri-tag-raw-pointers` makes Stacked Borrows assign proper tags even for raw pointers. This can
make valid code using int-to-ptr casts fail to pass the checks, but also can help identify latent
aliasing issues in code that Miri accepts by default. You can recognize false positives by
`<untagged>` occurring in the message -- this indicates a pointer that was cast from an integer,
so Miri was unable to track this pointer. Note that it is not currently guaranteed that code that
works with `-Zmiri-tag-raw-pointers` also works without `-Zmiri-tag-raw-pointers`, but for the
vast majority of code, this will be the case.

[function ABI]: https://doc.rust-lang.org/reference/items/functions.html#extern-function-qualifier

Expand Down
11 changes: 5 additions & 6 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -340,6 +340,7 @@ fn main() {
Please let us know at <https://github.com/rust-lang/miri/issues/2188> if you rely on this flag."
);
miri_config.allow_ptr_int_transmute = true;
miri_config.provenance_mode = ProvenanceMode::Permissive;
} else if arg == "-Zmiri-disable-abi-check" {
miri_config.check_abi = false;
} else if arg == "-Zmiri-disable-isolation" {
Expand Down Expand Up @@ -374,20 +375,18 @@ fn main() {
} else if arg == "-Zmiri-panic-on-unsupported" {
miri_config.panic_on_unsupported = true;
} else if arg == "-Zmiri-tag-raw-pointers" {
miri_config.tag_raw = true;
eprintln!("WARNING: `-Zmiri-tag-raw-pointers` has no effect; it is enabled by default");
} else if arg == "-Zmiri-strict-provenance" {
miri_config.provenance_mode = ProvenanceMode::Strict;
miri_config.tag_raw = true;
miri_config.allow_ptr_int_transmute = false;
} else if arg == "-Zmiri-permissive-provenance" {
miri_config.provenance_mode = ProvenanceMode::Permissive;
miri_config.tag_raw = true;
} else if arg == "-Zmiri-mute-stdout-stderr" {
miri_config.mute_stdout_stderr = true;
} else if arg == "-Zmiri-track-raw-pointers" {
eprintln!(
"WARNING: -Zmiri-track-raw-pointers has been renamed to -Zmiri-tag-raw-pointers, the old name is deprecated."
"WARNING: `-Zmiri-track-raw-pointers` has no effect; it is enabled by default"
);
miri_config.tag_raw = true;
} else if let Some(param) = arg.strip_prefix("-Zmiri-seed=") {
if miri_config.seed.is_some() {
panic!("Cannot specify -Zmiri-seed multiple times!");
Expand All @@ -410,7 +409,7 @@ fn main() {
err
),
};
for id in ids.into_iter().map(miri::PtrId::new) {
for id in ids.into_iter().map(miri::SbTag::new) {
if let Some(id) = id {
miri_config.tracked_pointer_tags.insert(id);
} else {
Expand Down
45 changes: 25 additions & 20 deletions src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,9 @@ pub enum NonHaltingDiagnostic {
FreedAlloc(AllocId),
RejectedIsolatedOp(String),
ProgressReport,
Int2Ptr {
details: bool,
},
}

/// Level of Miri specific diagnostics
Expand Down Expand Up @@ -177,24 +180,6 @@ pub fn report_error<'tcx, 'mir>(
helps.push((Some(*protection_span), "this protector is live for this call".to_string()));
}
}
Some(TagHistory::Untagged{ recently_created, recently_invalidated, matching_created, protected }) => {
if let Some((range, span)) = recently_created {
let msg = format!("tag was most recently created at offsets {}", HexRange(*range));
helps.push((Some(*span), msg));
}
if let Some((range, span)) = recently_invalidated {
let msg = format!("tag was later invalidated at offsets {}", HexRange(*range));
helps.push((Some(*span), msg));
}
if let Some((range, span)) = matching_created {
let msg = format!("this tag was also created here at offsets {}", HexRange(*range));
helps.push((Some(*span), msg));
}
if let Some((protecting_tag, protecting_tag_span, protection_span)) = protected {
helps.push((Some(*protecting_tag_span), format!("{:?} was protected due to a tag which was created here", protecting_tag)));
helps.push((Some(*protection_span), "this protector is live for this call".to_string()));
}
}
None => {}
}
helps
Expand Down Expand Up @@ -468,15 +453,35 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
format!("{op} was made to return an error due to isolation"),
ProgressReport =>
format!("progress report: current operation being executed is here"),
Int2Ptr { .. } => format!("integer-to-pointer cast"),
};

let (title, diag_level) = match e {
RejectedIsolatedOp(_) =>
("operation rejected by isolation", DiagLevel::Warning),
_ => ("tracking was triggered", DiagLevel::Note),
Int2Ptr { .. } => ("integer-to-pointer cast", DiagLevel::Warning),
CreatedPointerTag(..)
| PoppedPointerTag(..)
| CreatedCallId(..)
| CreatedAlloc(..)
| FreedAlloc(..)
| ProgressReport => ("tracking was triggered", DiagLevel::Note),
};

let helps = match e {
Int2Ptr { details: true } =>
vec![
(None, format!("this program is using integer-to-pointer casts or (equivalently) `from_exposed_addr`,")),
(None, format!("which means that Miri might miss pointer bugs in this program")),
(None, format!("see https://doc.rust-lang.org/nightly/std/ptr/fn.from_exposed_addr.html for more details on that operation")),
(None, format!("to ensure that Miri does not miss bugs in your program, use `with_addr` (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance) instead")),
(None, format!("you can then pass the `-Zmiri-strict-provenance` flag to Miri, to ensure you are not relying on `from_exposed_addr` semantics")),
(None, format!("alternatively, the `-Zmiri-permissive-provenance` flag disables this warning")),
],
_ => vec![],
};

report_msg(this, diag_level, title, vec![msg], vec![], &stacktrace);
report_msg(this, diag_level, title, vec![msg], helps, &stacktrace);
}
});
}
Expand Down
7 changes: 2 additions & 5 deletions src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,13 +96,11 @@ pub struct MiriConfig {
/// The seed to use when non-determinism or randomness are required (e.g. ptr-to-int cast, `getrandom()`).
pub seed: Option<u64>,
/// The stacked borrows pointer ids to report about
pub tracked_pointer_tags: HashSet<PtrId>,
pub tracked_pointer_tags: HashSet<SbTag>,
/// The stacked borrows call IDs to report about
pub tracked_call_ids: HashSet<CallId>,
/// The allocation ids to report about.
pub tracked_alloc_ids: HashSet<AllocId>,
/// Whether to track raw pointers in stacked borrows.
pub tag_raw: bool,
/// Determine if data race detection should be enabled
pub data_race_detector: bool,
/// Determine if weak memory emulation should be enabled. Requires data race detection to be enabled
Expand Down Expand Up @@ -146,14 +144,13 @@ impl Default for MiriConfig {
tracked_pointer_tags: HashSet::default(),
tracked_call_ids: HashSet::default(),
tracked_alloc_ids: HashSet::default(),
tag_raw: false,
data_race_detector: true,
weak_memory_emulation: true,
cmpxchg_weak_failure_rate: 0.8, // 80%
measureme_out: None,
panic_on_unsupported: false,
backtrace_style: BacktraceStyle::Short,
provenance_mode: ProvenanceMode::Legacy,
provenance_mode: ProvenanceMode::Default,
mute_stdout_stderr: false,
preemption_rate: 0.01, // 1%
report_progress: None,
Expand Down
Loading

0 comments on commit 7fafbde

Please sign in to comment.