From 3e44a255a44395d648b759666d4b6b689193b23d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 20 Oct 2026 21:21:40 +0000
Subject: [PATCH] Disable MIR inlining so calls are always checked against
 callee specs

At -C opt-level=2/3 with incremental compilation off (e.g. cargo
--release), rustc's MIR Inline pass inlines small same-crate functions
into their callers, including ones with requires/ensures and
#[thrust::trusted] ones. An inlined call leaves no Call terminator, so
its arguments were never checked against the callee's precondition and
violations verified as safe.

Fixes #348

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YQVMLYpCUxi5PMD6MSDMqM
---
 src/main.rs                                 |  4 ++++
 tests/ui/fail/trusted_requires_opt_level.rs | 11 +++++++++++
 tests/ui/pass/trusted_requires_opt_level.rs | 11 +++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 tests/ui/fail/trusted_requires_opt_level.rs
 create mode 100644 tests/ui/pass/trusted_requires_opt_level.rs

diff --git a/src/main.rs b/src/main.rs
index a3489fe0c..235629380 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -40,6 +40,10 @@ impl Callbacks for CompilerCalls {
                 .push((pass.to_owned(), false));
         }
 
+        // A call inlined by the MIR inliner leaves no `Call` terminator behind, so the
+        // arguments are never checked against the callee's specification.
+        config.opts.unstable_opts.inline_mir = Some(false);
+
         config.override_queries = Some(|_sess, providers| {
             providers.mir_borrowck = thrust::mir_borrowck_skip_formula_fn;
         });
diff --git a/tests/ui/fail/trusted_requires_opt_level.rs b/tests/ui/fail/trusted_requires_opt_level.rs
new file mode 100644
index 000000000..97b5bc8df
--- /dev/null
+++ b/tests/ui/fail/trusted_requires_opt_level.rs
@@ -0,0 +1,11 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off -C opt-level=3
+
+#[thrust::trusted]
+#[thrust_macros::requires(x != 0)]
+#[thrust_macros::ensures(true)]
+fn assume_nonzero(x: i32) {}
+
+fn main() {
+    assume_nonzero(0);
+}
diff --git a/tests/ui/pass/trusted_requires_opt_level.rs b/tests/ui/pass/trusted_requires_opt_level.rs
new file mode 100644
index 000000000..dd197254f
--- /dev/null
+++ b/tests/ui/pass/trusted_requires_opt_level.rs
@@ -0,0 +1,11 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off -C opt-level=3
+
+#[thrust::trusted]
+#[thrust_macros::requires(x != 0)]
+#[thrust_macros::ensures(true)]
+fn assume_nonzero(x: i32) {}
+
+fn main() {
+    assume_nonzero(1);
+}