Skip to content

Commit 128bbca

Browse files
authored
Rollup merge of #124896 - RalfJung:miri-intrinsic-fallback, r=oli-obk
miri: rename intrinsic_fallback_checks_ub to intrinsic_fallback_is_spec Checking UB is not the only concern, we also have to make sure we are not losing out on non-determinism. r? ``@oli-obk`` (not urgent, take your time)
2 parents 388606b + 193e6b0 commit 128bbca

File tree

4 files changed

+18
-18
lines changed

4 files changed

+18
-18
lines changed

src/intrinsics/mod.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,18 +43,18 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
4343
if this.tcx.intrinsic(instance.def_id()).unwrap().must_be_overridden {
4444
throw_unsup_format!("unimplemented intrinsic: `{intrinsic_name}`")
4545
}
46-
let intrinsic_fallback_checks_ub = Symbol::intern("intrinsic_fallback_checks_ub");
46+
let intrinsic_fallback_is_spec = Symbol::intern("intrinsic_fallback_is_spec");
4747
if this
4848
.tcx
4949
.get_attrs_by_path(
5050
instance.def_id(),
51-
&[sym::miri, intrinsic_fallback_checks_ub],
51+
&[sym::miri, intrinsic_fallback_is_spec],
5252
)
5353
.next()
5454
.is_none()
5555
{
5656
throw_unsup_format!(
57-
"miri can only use intrinsic fallback bodies that check UB. After verifying that `{intrinsic_name}` does so, add the `#[miri::intrinsic_fallback_checks_ub]` attribute to it; also ping @rust-lang/miri when you do that"
57+
"Miri can only use intrinsic fallback bodies that exactly reflect the specification: they fully check for UB and are as non-deterministic as possible. After verifying that `{intrinsic_name}` does so, add the `#[miri::intrinsic_fallback_is_spec]` attribute to it; also ping @rust-lang/miri when you do that"
5858
);
5959
}
6060
Ok(Some(ty::Instance {

tests/fail/intrinsic_fallback_checks_ub.stderr

Lines changed: 0 additions & 14 deletions
This file was deleted.

tests/fail/intrinsic_fallback_checks_ub.rs renamed to tests/fail/intrinsic_fallback_is_spec.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,5 @@ pub const fn ptr_guaranteed_cmp<T>(ptr: *const T, other: *const T) -> u8 {
1010

1111
fn main() {
1212
ptr_guaranteed_cmp::<()>(std::ptr::null(), std::ptr::null());
13-
//~^ ERROR: can only use intrinsic fallback bodies that check UB.
13+
//~^ ERROR: can only use intrinsic fallback bodies that exactly reflect the specification
1414
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
error: unsupported operation: Miri can only use intrinsic fallback bodies that exactly reflect the specification: they fully check for UB and are as non-deterministic as possible. After verifying that `ptr_guaranteed_cmp` does so, add the `#[miri::intrinsic_fallback_is_spec]` attribute to it; also ping @rust-lang/miri when you do that
2+
--> $DIR/intrinsic_fallback_is_spec.rs:LL:CC
3+
|
4+
LL | ptr_guaranteed_cmp::<()>(std::ptr::null(), std::ptr::null());
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Miri can only use intrinsic fallback bodies that exactly reflect the specification: they fully check for UB and are as non-deterministic as possible. After verifying that `ptr_guaranteed_cmp` does so, add the `#[miri::intrinsic_fallback_is_spec]` attribute to it; also ping @rust-lang/miri when you do that
6+
|
7+
= help: this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support
8+
= note: BACKTRACE:
9+
= note: inside `main` at $DIR/intrinsic_fallback_is_spec.rs:LL:CC
10+
11+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
12+
13+
error: aborting due to 1 previous error
14+

0 commit comments

Comments
 (0)