Auto merge of #3709 - RalfJung:docs-clarifications, r=saethlin

clarify the warning shown when optimizations are enabled, and the status of Tree Borrows

src/tools/miri/README.md

@@ -425,8 +425,12 @@ to Miri failing to detect cases of undefined behavior in a program.
   value from a load. This can help diagnose problems that disappear under
   `-Zmiri-disable-weak-memory-emulation`.
 * `-Zmiri-tree-borrows` replaces [Stacked Borrows] with the [Tree Borrows] rules.
-  The soundness rules are already experimental without this flag, but even more
-  so with this flag.
+  Tree Borrows is even more experimental than Stacked Borrows. While Tree Borrows
+  is still sound in the sense of catching all aliasing violations that current versions
+  of the compiler might exploit, it is likely that the eventual final aliasing model
+  of Rust will be stricter than Tree Borrows. In other words, if you use Tree Borrows,
+  even if your code is accepted today, it might be declared UB in the future.
+  This is much less likely with Stacked Borrows.
 * `-Zmiri-force-page-size=<num>` overrides the default page size for an architecture, in multiples of 1k.
   `4` is default for most targets. This value should always be a power of 2 and nonzero.
 * `-Zmiri-unique-is-unique` performs additional aliasing checks for `core::ptr::Unique` to ensure

src/tools/miri/src/bin/miri.rs

@@ -98,10 +98,9 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
             }
 
             if tcx.sess.opts.optimize != OptLevel::No {
-                tcx.dcx().warn("Miri does not support optimizations. If you have enabled optimizations \
-                    by selecting a Cargo profile (such as --release) which changes other profile settings \
-                    such as whether debug assertions and overflow checks are enabled, those settings are \
-                    still applied.");
+                tcx.dcx().warn("Miri does not support optimizations: the opt-level is ignored. The only effect \
+                    of selecting a Cargo profile that enables optimizations (such as --release) is to apply \
+                    its remaining settings, such as whether debug assertions and overflow checks are enabled.");
             }
             if tcx.sess.mir_opt_level() > 0 {
                 tcx.dcx().warn("You have explicitly enabled MIR optimizations, overriding Miri's default \