Repository: bytecodealliance/wasmtime
Pull request #7393 (2023-10-27 21:28:23)

mpk: turn on `memory_protection_keys` during fuzzing
This also twists the `max_memory_protection_keys` knob.

<!--
Please make sure you include the following information:

- If this work has been discussed elsewhere, please include a link to that
  conversation. If it was discussed in an issue, just mention "issue #...".

- Explain why this change is needed. If the details are in an issue already,
  this can be brief.

Our development process is documented in the Wasmtime book:
https://docs.wasmtime.dev/contributing-development-process.html

Please ensure all communication follows the code of conduct:
https://github.com/bytecodealliance/wasmtime/blob/main/CODE_OF_CONDUCT.md
-->


abrown: I've been running some fuzzing locally with this and it seems OK:

- currently at `#227829` of `cargo +nighly fuzz run instantiate`
- currently at `#160974` of `cargo +nighly fuzz run spectests`
- I had trouble running the `differential` target, though: I ran into build issues with the `wasm-spec-interpreter` and, with that disabled, I observed a segfault from V8. Has anyone else run this target recently?

This PR never really force-enables the MPK feature: it is only ever set to `auto`, so if the machine doing the fuzzing does not have MPK enabled, this feature won't really get tested.

Patch:
diff --git a/cranelift/codegen/src/ir/memtype.rs b/cranelift/codegen/src/ir/memtype.rs
index 403661d89..9a6ca67d9 100644
--- a/cranelift/codegen/src/ir/memtype.rs
+++ b/cranelift/codegen/src/ir/memtype.rs
@@ -51,10 +51,6 @@
 //!
 //! Eventually we plan to also have:
 //!
-//! - A dynamic memory is an untyped blob of storage with a size given
-//!   by a global value (GV). This is otherwise just like the "static
-//!   memory" variant described above.
-//!
 //! - A dynamic array is a sequence of struct memory types, with a
 //!   length given by a global value (GV). This is useful to model,
 //!   e.g., tables.
@@ -67,7 +63,7 @@
 //!   field is not null (all zero bits).
 
 use crate::ir::pcc::Fact;
-use crate::ir::Type;
+use crate::ir::{GlobalValue, Type};
 use alloc::vec::Vec;
 
 #[cfg(feature = "enable-serde")]
@@ -99,6 +95,15 @@ pub enum MemoryTypeData {
         size: u64,
     },
 
+    /// A dynamically-sized untyped blob of memory, with bound given
+    /// by a global value plus some static amount.
+    DynamicMemory {
+        /// Static part of size.
+        size: u64,
+        /// Dynamic part of size.
+        gv: GlobalValue,
+    },
+
     /// A type with no size.
     Empty,
 }
@@ -135,6 +140,9 @@ impl std::fmt::Display for MemoryTypeData {
             Self::Memory { size } => {
                 write!(f, "memory {size:#x}")
             }
+            Self::DynamicMemory { size, gv } => {
+                write!(f, "dynamic_memory {}+{:#x}", gv, size)
+            }
             Self::Empty => {
                 write!(f, "empty")
             }
@@ -175,6 +183,7 @@ impl MemoryTypeData {
         match self {
             Self::Struct { size, .. } => Some(*size),
             Self::Memory { size } => Some(*size),
+            Self::DynamicMemory { .. } => None,
             Self::Empty => Some(0),
         }
     }
diff --git a/cranelift/codegen/src/ir/pcc.rs b/cranelift/codegen/src/ir/pcc.rs
index fe7f08c96..6910ee73e 100644
--- a/cranelift/codegen/src/ir/pcc.rs
+++ b/cranelift/codegen/src/ir/pcc.rs
@@ -47,12 +47,6 @@
 //!
 //! TODO:
 //!
-//! Completeness:
-//! - Propagate facts through optimization (egraph layer).
-//! - Generate facts in cranelift-wasm frontend when lowering memory ops.
-//! - Support bounds-checking-type operations for dynamic memories and
-//!   tables.
-//!
 //! More checks:
 //! - Check that facts on `vmctx` GVs are subsumed by the actual facts
 //!   on the vmctx arg in block0 (function arg).
@@ -65,11 +59,6 @@
 //! Nicer errors:
 //! - attach instruction index or some other identifier to errors
 //!
-//! Refactoring:
-//! - avoid the "default fact" infra everywhere we fetch facts,
-//!   instead doing it in the subsume check (and take the type with
-//!   subsume)?
-//!
 //! Text format cleanup:
 //! - make the bitwidth on `max` facts optional in the CLIF text
 //!   format?
@@ -155,6 +144,19 @@ pub enum Fact {
         max: u64,
     },
 
+    /// A value bounded by a global value.
+    ///
+    /// The range is in `(min_GV + min_offset)..(max_GV +
+    /// max_offset)`, inclusive on the lower and upper bound.
+    DynamicRange {
+        /// The bitwidth of bits we care about, from the LSB upward.
+        bit_width: u16,
+        /// The lower bound, inclusive.
+        min: Expr,
+        /// The upper bound, inclusive.
+        max: Expr,
+    },
+
     /// A pointer to a memory type.
     Mem {
         /// The memory type.
@@ -165,12 +167,215 @@ pub enum Fact {
         max_offset: u64,
     },
 
+    /// A pointer to a memory type, dynamically bounded. The pointer
+    /// is within `(GV_min+offset_min)..(GV_max+offset_max)`
+    /// (inclusive on both ends) in the memory type.
+    DynamicMem {
+        /// The memory type.
+        ty: ir::MemoryType,
+        /// The lower bound, inclusive.
+        min: Expr,
+        /// The upper bound, inclusive.
+        max: Expr,
+        /// This pointer can also be null.
+        nullable: bool,
+    },
+
+    /// A comparison result between two dynamic values with a
+    /// comparison of a certain kind.
+    Compare {
+        /// The kind of comparison.
+        kind: ir::condcodes::IntCC,
+        /// The left-hand side of the comparison.
+        lhs: BaseExpr,
+        /// The right-hand side of the comparison.
+        rhs: BaseExpr,
+    },
+
     /// A "conflict fact": this fact results from merging two other
     /// facts, and it can never be satisfied -- checking any value
     /// against this fact will fail.
     Conflict,
 }
 
+/// A bound expression.
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
+pub struct Expr {
+    /// The dynamic (base) part.
+    pub base: BaseExpr,
+    /// The static (offset) part.
+    pub offset: i64,
+}
+
+/// The base part of a bound expression.
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
+pub enum BaseExpr {
+    /// No dynamic part (i.e., zero).
+    None,
+    /// A global value.
+    GlobalValue(ir::GlobalValue),
+    /// An SSA Value as a symbolic value. This can be referenced in
+    /// facts even after we've lowered out of SSA: it becomes simply
+    /// some symbolic value.
+    Value(ir::Value),
+    /// Top of the address space. This is "saturating": the offset
+    /// doesn't matter.
+    Max,
+}
+
+impl BaseExpr {
+    /// Is one base less than or equal to another? (We can't always
+    /// know; in such cases, returns `false`.)
+    fn le(lhs: &BaseExpr, rhs: &BaseExpr) -> bool {
+        // (i) reflexivity; (ii) 0 <= x for all (unsigned) x; (iii) x <= max for all x.
+        lhs == rhs || *lhs == BaseExpr::None || *rhs == BaseExpr::Max
+    }
+
+    /// Compute some BaseExpr that will be less than or equal to both
+    /// inputs. This is a generalization of `min` (but looser).
+    fn min(lhs: &BaseExpr, rhs: &BaseExpr) -> BaseExpr {
+        if lhs == rhs {
+            lhs.clone()
+        } else if *lhs == BaseExpr::Max {
+            rhs.clone()
+        } else if *rhs == BaseExpr::Max {
+            lhs.clone()
+        } else {
+            BaseExpr::None // zero is <= x for all (unsigned) x.
+        }
+    }
+
+    /// Compute some BaseExpr that will be greater than or equal to
+    /// both inputs.
+    fn max(lhs: &BaseExpr, rhs: &BaseExpr) -> BaseExpr {
+        if lhs == rhs {
+            lhs.clone()
+        } else if *lhs == BaseExpr::None {
+            rhs.clone()
+        } else if *rhs == BaseExpr::None {
+            lhs.clone()
+        } else {
+            BaseExpr::Max
+        }
+    }
+}
+
+impl Expr {
+    /// Is one expression definitely less than or equal to another?
+    /// (We can't always know; in such cases, returns `false`.)
+    fn le(lhs: &Expr, rhs: &Expr) -> bool {
+        if rhs.base == BaseExpr::Max {
+            true
+        } else {
+            BaseExpr::le(&lhs.base, &rhs.base) && lhs.offset <= rhs.offset
+        }
+    }
+
+    /// Generalization of `min`: compute some Expr that is less than
+    /// or equal to both inputs.
+    fn min(lhs: &Expr, rhs: &Expr) -> Expr {
+        if lhs.base == BaseExpr::None && lhs.offset == 0 {
+            lhs.clone()
+        } else if rhs.base == BaseExpr::None && rhs.offset == 0 {
+            rhs.clone()
+        } else {
+            Expr {
+                base: BaseExpr::min(&lhs.base, &rhs.base),
+                offset: std::cmp::min(lhs.offset, rhs.offset),
+            }
+        }
+    }
+
+    /// Generalization of `max`: compute some Expr that is greater
+    /// than or equal to both inputs.
+    fn max(lhs: &Expr, rhs: &Expr) -> Expr {
+        if lhs.base == BaseExpr::None && lhs.offset == 0 {
+            rhs.clone()
+        } else if rhs.base == BaseExpr::None && rhs.offset == 0 {
+            lhs.clone()
+        } else {
+            Expr {
+                base: BaseExpr::max(&lhs.base, &rhs.base),
+                offset: std::cmp::max(lhs.offset, rhs.offset),
+            }
+        }
+    }
+
+    /// Add one expression to another.
+    fn add(lhs: &Expr, rhs: &Expr) -> Option<Expr> {
+        if lhs.base == rhs.base {
+            Some(Expr {
+                base: lhs.base.clone(),
+                offset: lhs.offset.checked_add(rhs.offset)?,
+            })
+        } else if lhs.base == BaseExpr::None {
+            Some(Expr {
+                base: rhs.base.clone(),
+                offset: lhs.offset.checked_add(rhs.offset)?,
+            })
+        } else if rhs.base == BaseExpr::None {
+            Some(Expr {
+                base: lhs.base.clone(),
+                offset: lhs.offset.checked_add(rhs.offset)?,
+            })
+        } else {
+            Some(Expr {
+                base: BaseExpr::Max,
+                offset: 0,
+            })
+        }
+    }
+
+    /// Add a static offset to an expression.
+    fn offset(lhs: &Expr, rhs: i64) -> Option<Expr> {
+        let offset = lhs.offset.checked_add(rhs)?;
+        Some(Expr {
+            base: lhs.base.clone(),
+            offset,
+        })
+    }
+}
+
+impl fmt::Display for BaseExpr {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self {
+            BaseExpr::None => Ok(()),
+            BaseExpr::Max => write!(f, "max"),
+            BaseExpr::GlobalValue(gv) => write!(f, "{gv}"),
+            BaseExpr::Value(value) => write!(f, "{value}"),
+        }
+    }
+}
+
+impl BaseExpr {
+    /// Does this dynamic_expression take an offset?
+    pub fn is_some(&self) -> bool {
+        match self {
+            BaseExpr::None => false,
+            _ => true,
+        }
+    }
+}
+
+impl fmt::Display for Expr {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "{}", self.base)?;
+        match self.offset {
+            offset if offset > 0 && self.base.is_some() => write!(f, "+{offset:#x}"),
+            offset if offset > 0 => write!(f, "{offset:#x}"),
+            offset if offset < 0 => {
+                let negative_offset = -i128::from(offset); // upcast to support i64::MIN.
+                write!(f, "-{negative_offset:#x}")
+            }
+            0 if self.base.is_some() => Ok(()),
+            0 => write!(f, "0"),
+            _ => unreachable!(),
+        }
+    }
+}
+
 impl fmt::Display for Fact {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
@@ -178,12 +383,31 @@ impl fmt::Display for Fact {
                 bit_width,
                 min,
                 max,
-            } => write!(f, "range({}, {:#x}, {:#x})", bit_width, min, max),
+            } => write!(f, "range({bit_width}, {min:#x}, {max:#x})"),
+            Fact::DynamicRange {
+                bit_width,
+                min,
+                max,
+            } => {
+                write!(f, "dynamic_range({bit_width}, {min}, {max})")
+            }
             Fact::Mem {
                 ty,
                 min_offset,
                 max_offset,
-            } => write!(f, "mem({}, {:#x}, {:#x})", ty, min_offset, max_offset),
+            } => write!(f, "mem({ty}, {min_offset:#x}, {max_offset:#x})"),
+            Fact::DynamicMem {
+                ty,
+                min,
+                max,
+                nullable,
+            } => {
+                let nullable_flag = if *nullable { ", nullable" } else { "" };
+                write!(f, "dynamic_mem({ty}, {min}, {max}{nullable_flag})")
+            }
+            Fact::Compare { kind, lhs, rhs } => {
+                write!(f, "compare({kind}, {lhs}, {rhs})")
+            }
             Fact::Conflict => write!(f, "conflict"),
         }
     }
@@ -305,6 +529,25 @@ impl Fact {
                 max: std::cmp::min(*max_lhs, *max_rhs),
             },
 
+            (
+                Fact::DynamicRange {
+                    bit_width: bw_lhs,
+                    min: min_lhs,
+                    max: max_lhs,
+                },
+                Fact::DynamicRange {
+                    bit_width: bw_rhs,
+                    min: min_rhs,
+                    max: max_rhs,
+                },
+            ) if bw_lhs == bw_rhs && Expr::le(min_rhs, max_lhs) && Expr::le(min_lhs, max_rhs) => {
+                Fact::DynamicRange {
+                    bit_width: *bw_lhs,
+                    min: Expr::max(min_lhs, min_rhs),
+                    max: Expr::min(max_lhs, max_rhs),
+                }
+            }
+
             (
                 Fact::Mem {
                     ty: ty_lhs,
@@ -327,9 +570,68 @@ impl Fact {
                 }
             }
 
+            (
+                Fact::DynamicMem {
+                    ty: ty_lhs,
+                    min: min_lhs,
+                    max: max_lhs,
+                    nullable: null_lhs,
+                },
+                Fact::DynamicMem {
+                    ty: ty_rhs,
+                    min: min_rhs,
+                    max: max_rhs,
+                    nullable: null_rhs,
+                },
+            ) if ty_lhs == ty_rhs && Expr::le(min_rhs, max_lhs) && Expr::le(min_lhs, max_rhs) => {
+                Fact::DynamicMem {
+                    ty: *ty_lhs,
+                    min: Expr::max(min_lhs, min_rhs),
+                    max: Expr::min(max_lhs, max_rhs),
+                    nullable: *null_lhs && *null_rhs,
+                }
+            }
+
             _ => Fact::Conflict,
         }
     }
+
+    /// Compute the union of two facts, if possible.
+    pub fn union(lhs: &Fact, rhs: &Fact) -> Option<Fact> {
+        match (lhs, rhs) {
+            (lhs, rhs) if lhs == rhs => Some(lhs.clone()),
+
+            (
+                Fact::DynamicMem {
+                    ty: ty_lhs,
+                    min: min_lhs,
+                    max: max_lhs,
+                    nullable: nullable_lhs,
+                },
+                Fact::DynamicMem {
+                    ty: ty_rhs,
+                    min: min_rhs,
+                    max: max_rhs,
+                    nullable: nullable_rhs,
+                },
+            ) if ty_lhs == ty_rhs => Some(Fact::DynamicMem {
+                ty: *ty_lhs,
+                min: Expr::min(min_lhs, min_rhs),
+                max: Expr::max(max_lhs, max_rhs),
+                nullable: *nullable_lhs || *nullable_rhs,
+            }),
+
+            _ => None,
+        }
+    }
+
+    /// Is this fact a single-value range with a symbolic Expr?
+    fn as_symbol(&self) -> Option<&Expr> {
+        match self {
+            Fact::DynamicRange { min, max, .. } if min == max => Some(min),
+            _ => None,
+        }
+    }
 }
 
 macro_rules! ensure {
@@ -346,6 +648,16 @@ macro_rules! bail {
     }};
 }
 
+/// The two kinds of inequalities: "strict" (`<`, `>`) and "loose"
+/// (`<=`, `>=`), the latter of which admit equality.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum InequalityKind {
+    /// Strict inequality: {less,greater}-than.
+    Strict,
+    /// Loose inequality: {less,greater}-than-or-equal.
+    Loose,
+}
+
 /// A "context" in which we can evaluate and derive facts. This
 /// context carries environment/global properties, such as the machine
 /// pointer width.
@@ -392,6 +704,27 @@ impl<'a> FactContext<'a> {
                 bw_lhs >= bw_rhs && max_lhs <= max_rhs && min_lhs >= min_rhs
             }
 
+            (
+                Fact::DynamicRange {
+                    bit_width: bw_lhs,
+                    min: min_lhs,
+                    max: max_lhs,
+                },
+                Fact::DynamicRange {
+                    bit_width: bw_rhs,
+                    min: min_rhs,
+                    max: max_rhs,
+                },
+            ) => {
+                // Nearly same as above, but with dynamic-expression
+                // comparisons. Note that we require equal bitwidths
+                // here: unlike in the static case, we don't have
+                // fixed values for min and max, so we can't lean on
+                // the well-formedness requirements of the static
+                // ranges fitting within the bit-width max.
+                bw_lhs == bw_rhs && Expr::le(max_lhs, max_rhs) && Expr::le(min_rhs, min_lhs)
+            }
+
             (
                 Fact::Mem {
                     ty: ty_lhs,
@@ -409,6 +742,36 @@ impl<'a> FactContext<'a> {
                     && min_offset_lhs >= min_offset_rhs
             }
 
+            (
+                Fact::DynamicMem {
+                    ty: ty_lhs,
+                    min: min_lhs,
+                    max: max_lhs,
+                    nullable: nullable_lhs,
+                },
+                Fact::DynamicMem {
+                    ty: ty_rhs,
+                    min: min_rhs,
+                    max: max_rhs,
+                    nullable: nullable_rhs,
+                },
+            ) => {
+                ty_lhs == ty_rhs
+                    && Expr::le(max_lhs, max_rhs)
+                    && Expr::le(min_rhs, min_lhs)
+                    && (*nullable_lhs || !*nullable_rhs)
+            }
+
+            // Constant zero subsumes nullable DynamicMem pointers.
+            (
+                Fact::Range {
+                    bit_width,
+                    min: 0,
+                    max: 0,
+                },
+                Fact::DynamicMem { nullable: true, .. },
+            ) if *bit_width == self.pointer_width => true,
+
             _ => false,
         }
     }
@@ -431,7 +794,7 @@ impl<'a> FactContext<'a> {
     /// pointer width: e.g., many 64-bit machines can still do 32-bit
     /// adds that wrap at 2^32.
     pub fn add(&self, lhs: &Fact, rhs: &Fact, add_width: u16) -> Option<Fact> {
-        match (lhs, rhs) {
+        let result = match (lhs, rhs) {
             (
                 Fact::Range {
                     bit_width: bw_lhs,
@@ -487,23 +850,125 @@ impl<'a> FactContext<'a> {
                 })
             }
 
+            (
+                Fact::Range {
+                    bit_width: bw_static,
+                    min: min_static,
+                    max: max_static,
+                },
+                Fact::DynamicRange {
+                    bit_width: bw_dynamic,
+                    min: ref min_dynamic,
+                    max: ref max_dynamic,
+                },
+            )
+            | (
+                Fact::DynamicRange {
+                    bit_width: bw_dynamic,
+                    min: ref min_dynamic,
+                    max: ref max_dynamic,
+                },
+                Fact::Range {
+                    bit_width: bw_static,
+                    min: min_static,
+                    max: max_static,
+                },
+            ) if bw_static == bw_dynamic => {
+                let min = Expr::offset(min_dynamic, i64::try_from(*min_static).ok()?)?;
+                let max = Expr::offset(max_dynamic, i64::try_from(*max_static).ok()?)?;
+                Some(Fact::DynamicRange {
+                    bit_width: *bw_dynamic,
+                    min,
+                    max,
+                })
+            }
+
+            (
+                Fact::DynamicMem {
+                    ty,
+                    min: min_mem,
+                    max: max_mem,
+                    nullable,
+                },
+                Fact::DynamicRange {
+                    bit_width,
+                    min: min_range,
+                    max: max_range,
+                },
+            )
+            | (
+                Fact::DynamicRange {
+                    bit_width,
+                    min: min_range,
+                    max: max_range,
+                },
+                Fact::DynamicMem {
+                    ty,
+                    min: min_mem,
+                    max: max_mem,
+                    nullable,
+                },
+            ) if *bit_width == self.pointer_width => {
+                let min = Expr::add(min_mem, min_range)?;
+                let max = Expr::add(max_mem, max_range)?;
+                Some(Fact::DynamicMem {
+                    ty: *ty,
+                    min,
+                    max,
+                    nullable: *nullable,
+                })
+            }
+
+            (
+                Fact::Range {
+                    bit_width: bw_static,
+                    min: min_static,
+                    max: max_static,
+                },
+                Fact::DynamicMem {
+                    ty,
+                    min: ref min_dynamic,
+                    max: ref max_dynamic,
+                    nullable,
+                },
+            )
+            | (
+                Fact::DynamicMem {
+                    ty,
+                    min: ref min_dynamic,
+                    max: ref max_dynamic,
+                    nullable,
+                },
+                Fact::Range {
+                    bit_width: bw_static,
+                    min: min_static,
+                    max: max_static,
+                },
+            ) if *bw_static == self.pointer_width => {
+                let min = Expr::offset(min_dynamic, i64::try_from(*min_static).ok()?)?;
+                let max = Expr::offset(max_dynamic, i64::try_from(*max_static).ok()?)?;
+                Some(Fact::DynamicMem {
+                    ty: *ty,
+                    min,
+                    max,
+                    nullable: *nullable,
+                })
+            }
+
             _ => None,
-        }
+        };
+
+        trace!("add: {lhs:?} + {rhs:?} -> {result:?}");
+        result
     }
 
     /// Computes the `uextend` of a value with the given facts.
     pub fn uextend(&self, fact: &Fact, from_width: u16, to_width: u16) -> Option<Fact> {
-        trace!(
-            "uextend: fact {:?} from {} to {}",
-            fact,
-            from_width,
-            to_width
-        );
         if from_width == to_width {
             return Some(fact.clone());
         }
 
-        match fact {
+        let result = match fact {
             // If the claim is already for a same-or-wider value and the min
             // and max are within range of the narrower value, we can
             // claim the same range.
@@ -521,12 +986,27 @@ impl<'a> FactContext<'a> {
                     max: *max,
                 })
             }
+
+            // If the claim is a dynamic range for the from-width, we
+            // can extend to the to-width.
+            Fact::DynamicRange {
+                bit_width,
+                min,
+                max,
+            } if *bit_width == from_width => Some(Fact::DynamicRange {
+                bit_width: to_width,
+                min: min.clone(),
+                max: max.clone(),
+            }),
+
             // Otherwise, we can at least claim that the value is
             // within the range of `from_width`.
             Fact::Range { .. } => Some(Fact::max_range_for_width_extended(from_width, to_width)),
 
             _ => None,
-        }
+        };
+        trace!("uextend: fact {fact:?} from {from_width} to {to_width} -> {result:?}");
+        result
     }
 
     /// Computes the `sextend` of a value with the given facts.
@@ -588,7 +1068,7 @@ impl<'a> FactContext<'a> {
 
     /// Scales a value with a fact by a known constant.
     pub fn scale(&self, fact: &Fact, width: u16, factor: u32) -> Option<Fact> {
-        match fact {
+        let result = match fact {
             Fact::Range {
                 bit_width,
                 min,
@@ -606,7 +1086,9 @@ impl<'a> FactContext<'a> {
                 })
             }
             _ => None,
-        }
+        };
+        trace!("scale: {fact:?} * {factor} at width {width} -> {result:?}");
+        result
     }
 
     /// Left-shifts a value with a fact by a known constant.
@@ -620,13 +1102,6 @@ impl<'a> FactContext<'a> {
 
     /// Offsets a value with a fact by a known amount.
     pub fn offset(&self, fact: &Fact, width: u16, offset: i64) -> Option<Fact> {
-        trace!(
-            "FactContext::offset: {:?} + {} in width {}",
-            fact,
-            offset,
-            width
-        );
-
         let compute_offset = |base: u64| -> Option<u64> {
             if offset >= 0 {
                 base.checked_add(u64::try_from(offset).unwrap())
@@ -635,7 +1110,7 @@ impl<'a> FactContext<'a> {
             }
         };
 
-        match fact {
+        let result = match fact {
             Fact::Range {
                 bit_width,
                 min,
@@ -643,13 +1118,25 @@ impl<'a> FactContext<'a> {
             } if *bit_width == width => {
                 let min = compute_offset(*min)?;
                 let max = compute_offset(*max)?;
-
                 Some(Fact::Range {
                     bit_width: *bit_width,
                     min,
                     max,
                 })
             }
+            Fact::DynamicRange {
+                bit_width,
+                min,
+                max,
+            } if *bit_width == width => {
+                let min = Expr::offset(min, offset)?;
+                let max = Expr::offset(max, offset)?;
+                Some(Fact::DynamicRange {
+                    bit_width: *bit_width,
+                    min,
+                    max,
+                })
+            }
             Fact::Mem {
                 ty,
                 min_offset: mem_min_offset,
@@ -663,8 +1150,25 @@ impl<'a> FactContext<'a> {
                     max_offset,
                 })
             }
+            Fact::DynamicMem {
+                ty,
+                min,
+                max,
+                nullable,
+            } => {
+                let min = Expr::offset(min, offset)?;
+                let max = Expr::offset(max, offset)?;
+                Some(Fact::DynamicMem {
+                    ty: *ty,
+                    min,
+                    max,
+                    nullable: *nullable,
+                })
+            }
             _ => None,
-        }
+        };
+        trace!("offset: {fact:?} + {offset} in width {width} -> {result:?}");
+        result
     }
 
     /// Check that accessing memory via a pointer with this fact, with
@@ -689,6 +1193,7 @@ impl<'a> FactContext<'a> {
                     | ir::MemoryTypeData::Memory { size } => {
                         ensure!(end_offset <= *size, OutOfBounds)
                     }
+                    ir::MemoryTypeData::DynamicMemory { .. } => bail!(OutOfBounds),
                     ir::MemoryTypeData::Empty => bail!(OutOfBounds),
                 }
                 let specific_ty_and_offset = if min_offset == max_offset {
@@ -698,6 +1203,30 @@ impl<'a> FactContext<'a> {
                 };
                 Ok(specific_ty_and_offset)
             }
+            Fact::DynamicMem {
+                ty,
+                min: _,
+                max:
+                    Expr {
+                        base: BaseExpr::GlobalValue(max_gv),
+                        offset: max_offset,
+                    },
+                nullable: _,
+            } => match &self.function.memory_types[*ty] {
+                ir::MemoryTypeData::DynamicMemory {
+                    gv,
+                    size: mem_static_size,
+                } if gv == max_gv => {
+                    let end_offset = max_offset
+                        .checked_add(i64::from(size))
+                        .ok_or(PccError::Overflow)?;
+                    let mem_static_size =
+                        i64::try_from(*mem_static_size).map_err(|_| PccError::Overflow)?;
+                    ensure!(end_offset <= mem_static_size, OutOfBounds);
+                    Ok(None)
+                }
+                _ => bail!(OutOfBounds),
+            },
             _ => bail!(OutOfBounds),
         }
     }
@@ -755,6 +1284,57 @@ impl<'a> FactContext<'a> {
         }
         Ok(())
     }
+
+    /// Apply a known inequality to rewrite dynamic bounds using transitivity, if possible.
+    ///
+    /// Given that `lhs >= rhs` (if not `strict`) or `lhs > rhs` (if
+    /// `strict`), update `fact`.
+    pub fn apply_inequality(
+        &self,
+        fact: &Fact,
+        lhs: &Fact,
+        rhs: &Fact,
+        kind: InequalityKind,
+    ) -> Fact {
+        match (lhs.as_symbol(), rhs.as_symbol(), fact) {
+            (
+                Some(lhs),
+                Some(rhs),
+                Fact::DynamicMem {
+                    ty,
+                    min,
+                    max,
+                    nullable,
+                },
+            ) if rhs.base == max.base => {
+                let strict_offset = match kind {
+                    InequalityKind::Strict => 1,
+                    InequalityKind::Loose => 0,
+                };
+                if let Some(offset) = max
+                    .offset
+                    .checked_add(lhs.offset)
+                    .and_then(|x| x.checked_sub(rhs.offset))
+                    .and_then(|x| x.checked_sub(strict_offset))
+                {
+                    let new_max = Expr {
+                        base: lhs.base.clone(),
+                        offset,
+                    };
+                    Fact::DynamicMem {
+                        ty: *ty,
+                        min: min.clone(),
+                        max: new_max,
+                        nullable: *nullable,
+                    }
+                } else {
+                    fact.clone()
+                }
+            }
+
+            _ => fact.clone(),
+        }
+    }
 }
 
 fn max_value_for_width(bits: u16) -> u64 {
@@ -779,9 +1359,10 @@ pub fn check_vcode_facts<B: LowerBackend + TargetIsa>(
     // facts, and support the stated output facts.
     for block in 0..vcode.num_blocks() {
         let block = BlockIndex::new(block);
+        let mut flow_state = B::FactFlowState::default();
         for inst in vcode.block_insns(block).iter() {
             // Check any output facts on this inst.
-            if let Err(e) = backend.check_fact(&ctx, vcode, inst) {
+            if let Err(e) = backend.check_fact(&ctx, vcode, inst, &mut flow_state) {
                 log::error!("Error checking instruction: {:?}", vcode[inst]);
                 return Err(e);
             }
diff --git a/cranelift/codegen/src/isa/aarch64/lower.rs b/cranelift/codegen/src/isa/aarch64/lower.rs
index de428e0c4..5ed10a490 100644
--- a/cranelift/codegen/src/isa/aarch64/lower.rs
+++ b/cranelift/codegen/src/isa/aarch64/lower.rs
@@ -136,7 +136,10 @@ impl LowerBackend for AArch64Backend {
         ctx: &FactContext<'_>,
         vcode: &mut VCode<Self::MInst>,
         inst: InsnIndex,
+        state: &mut pcc::FactFlowState,
     ) -> PccResult<()> {
-        pcc::check(ctx, vcode, inst)
+        pcc::check(ctx, vcode, inst, state)
     }
+
+    type FactFlowState = pcc::FactFlowState;
 }
diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index a84604aa0..6a0bbd98d 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -4,7 +4,8 @@ use crate::ir::pcc::*;
 use crate::ir::types::*;
 use crate::ir::MemFlags;
 use crate::ir::Type;
-use crate::isa::aarch64::inst::args::{PairAMode, ShiftOp};
+use crate::isa::aarch64::inst::args::{Cond, PairAMode, ShiftOp};
+use crate::isa::aarch64::inst::regs::zero_reg;
 use crate::isa::aarch64::inst::Inst;
 use crate::isa::aarch64::inst::{ALUOp, MoveWideOp};
 use crate::isa::aarch64::inst::{AMode, ExtendOp};
@@ -26,13 +27,26 @@ fn extend_fact(ctx: &FactContext, value: &Fact, mode: ExtendOp) -> Option<Fact>
     }
 }
 
+/// Flow-state between facts.
+#[derive(Clone, Debug, Default)]
+pub struct FactFlowState {
+    cmp_flags: Option<(Fact, Fact)>,
+}
+
 pub(crate) fn check(
     ctx: &FactContext,
     vcode: &mut VCode<Inst>,
     inst_idx: InsnIndex,
+    state: &mut FactFlowState,
 ) -> PccResult<()> {
     trace!("Checking facts on inst: {:?}", vcode[inst_idx]);
 
+    // We only persist flag state for one instruction, because we
+    // can't exhaustively enumerate all flags-effecting ops; so take
+    // the `cmp_state` here and perhaps use it below but don't let it
+    // remain.
+    let cmp_flags = state.cmp_flags.take();
+
     match vcode[inst_idx] {
         Inst::Args { .. } => {
             // Defs on the args have "axiomatic facts": we trust the
@@ -200,6 +214,20 @@ pub(crate) fn check(
             )
         }),
 
+        Inst::AluRRR {
+            alu_op: ALUOp::SubS,
+            size,
+            rd,
+            rn,
+            rm,
+        } if rd.to_reg() == zero_reg() => {
+            // Compare.
+            let rn = get_fact_or_default(vcode, rn, size.bits().into());
+            let rm = get_fact_or_default(vcode, rm, size.bits().into());
+            state.cmp_flags = Some((rn, rm));
+            Ok(())
+        }
+
         Inst::AluRRR { rd, size, .. }
         | Inst::AluRRImm12 { rd, size, .. }
         | Inst::AluRRRShift { rd, size, .. }
@@ -240,12 +268,9 @@ pub(crate) fn check(
 
         Inst::MovK { rd, rn, imm, .. } => {
             let input = get_fact_or_default(vcode, rn, 64);
-            trace!("MovK: input = {:?}", input);
             if let Some(input_constant) = input.as_const(64) {
-                trace!(" -> input_constant: {}", input_constant);
                 let constant = u64::from(imm.bits) << (imm.shift * 16);
                 let constant = input_constant | constant;
-                trace!(" -> merged constant: {}", constant);
                 check_constant(ctx, vcode, rd, 64, constant)
             } else {
                 check_output(ctx, vcode, rd, &[], |_vcode| {
@@ -254,6 +279,37 @@ pub(crate) fn check(
             }
         }
 
+        Inst::CSel { rd, cond, rn, rm } if cond == Cond::Hs && cmp_flags.is_some() => {
+            let (cmp_lhs, cmp_rhs) = cmp_flags.unwrap();
+            trace!("CSel: cmp {cond:?} ({cmp_lhs:?}, {cmp_rhs:?})");
+
+            check_output(ctx, vcode, rd, &[], |vcode| {
+                // We support transitivity-based reasoning. If the
+                // comparison establishes that
+                //
+                //   (x+K1) <= (y+K2)
+                //
+                // then on the true-side of the select we can edit the maximum
+                // in a DynamicMem or DynamicRange by replacing x's with y's
+                // with appropriate offsets -- this widens the range.
+                //
+                // Likewise, on the false-side of the select we can
+                // replace y's with x's -- this also widens the range. On
+                // the false side we know the inequality is strict, so we
+                // can offset by one.
+
+                // True side: lhs <= rhs, not strict.
+                let rn = get_fact_or_default(vcode, rn, 64);
+                let rn = ctx.apply_inequality(&rn, &cmp_lhs, &cmp_rhs, InequalityKind::Loose);
+                // false side: rhs < lhs, strict.
+                let rm = get_fact_or_default(vcode, rm, 64);
+                let rm = ctx.apply_inequality(&rm, &cmp_rhs, &cmp_lhs, InequalityKind::Strict);
+                let union = Fact::union(&rn, &rm);
+                // Union the two facts.
+                clamp_range(ctx, 64, 64, union)
+            })
+        }
+
         _ if vcode.inst_defines_facts(inst_idx) => Err(PccError::UnsupportedFact),
 
         _ => Ok(()),
diff --git a/cranelift/codegen/src/isa/riscv64/lower.rs b/cranelift/codegen/src/isa/riscv64/lower.rs
index 1477509f3..41b114441 100644
--- a/cranelift/codegen/src/isa/riscv64/lower.rs
+++ b/cranelift/codegen/src/isa/riscv64/lower.rs
@@ -30,4 +30,6 @@ impl LowerBackend for Riscv64Backend {
         // right now riscv64 not support this feature.
         None
     }
+
+    type FactFlowState = ();
 }
diff --git a/cranelift/codegen/src/isa/s390x/lower.rs b/cranelift/codegen/src/isa/s390x/lower.rs
index f4db0a459..eea3c1fdc 100644
--- a/cranelift/codegen/src/isa/s390x/lower.rs
+++ b/cranelift/codegen/src/isa/s390x/lower.rs
@@ -25,4 +25,6 @@ impl LowerBackend for S390xBackend {
     ) -> Option<()> {
         isle::lower_branch(ctx, self, ir_inst, targets)
     }
+
+    type FactFlowState = ();
 }
diff --git a/cranelift/codegen/src/isa/x64/inst/args.rs b/cranelift/codegen/src/isa/x64/inst/args.rs
index d88f3a2ac..1c6c2877d 100644
--- a/cranelift/codegen/src/isa/x64/inst/args.rs
+++ b/cranelift/codegen/src/isa/x64/inst/args.rs
@@ -2007,7 +2007,7 @@ impl fmt::Display for ShiftKind {
 
 /// These indicate condition code tests.  Not all are represented since not all are useful in
 /// compiler-generated code.
-#[derive(Copy, Clone)]
+#[derive(Copy, Clone, PartialEq, Eq)]
 #[repr(u8)]
 pub enum CC {
     ///  overflow
diff --git a/cranelift/codegen/src/isa/x64/lower.rs b/cranelift/codegen/src/isa/x64/lower.rs
index 6b071c48c..ac4f803b5 100644
--- a/cranelift/codegen/src/isa/x64/lower.rs
+++ b/cranelift/codegen/src/isa/x64/lower.rs
@@ -345,7 +345,10 @@ impl LowerBackend for X64Backend {
         ctx: &FactContext<'_>,
         vcode: &mut VCode<Self::MInst>,
         inst: InsnIndex,
+        state: &mut pcc::FactFlowState,
     ) -> PccResult<()> {
-        pcc::check(ctx, vcode, inst)
+        pcc::check(ctx, vcode, inst, state)
     }
+
+    type FactFlowState = pcc::FactFlowState;
 }
diff --git a/cranelift/codegen/src/isa/x64/pcc.rs b/cranelift/codegen/src/isa/x64/pcc.rs
index 3991186c5..16a953325 100644
--- a/cranelift/codegen/src/isa/x64/pcc.rs
+++ b/cranelift/codegen/src/isa/x64/pcc.rs
@@ -4,7 +4,8 @@ use crate::ir::pcc::*;
 use crate::ir::types::*;
 use crate::ir::Type;
 use crate::isa::x64::inst::args::{
-    AluRmiROpcode, Amode, Gpr, Imm8Reg, RegMem, RegMemImm, ShiftKind, SyntheticAmode, ToWritableReg,
+    AluRmiROpcode, Amode, Gpr, Imm8Reg, RegMem, RegMemImm, ShiftKind, SyntheticAmode,
+    ToWritableReg, CC,
 };
 use crate::isa::x64::inst::Inst;
 use crate::machinst::pcc::*;
@@ -32,13 +33,26 @@ fn ensure_no_fact(vcode: &VCode<Inst>, reg: Reg) -> PccResult<()> {
     }
 }
 
+/// Flow-state between facts.
+#[derive(Clone, Debug, Default)]
+pub(crate) struct FactFlowState {
+    cmp_flags: Option<(Fact, Fact)>,
+}
+
 pub(crate) fn check(
     ctx: &FactContext,
     vcode: &mut VCode<Inst>,
     inst_idx: InsnIndex,
+    state: &mut FactFlowState,
 ) -> PccResult<()> {
     trace!("Checking facts on inst: {:?}", vcode[inst_idx]);
 
+    // We only persist flag state for one instruction, because we
+    // can't exhaustively enumerate all flags-effecting ops; so take
+    // the `cmp_state` here and perhaps use it below but don't let it
+    // remain.
+    let cmp_flags = state.cmp_flags.take();
+
     match vcode[inst_idx] {
         Inst::Nop { .. } => Ok(()),
 
@@ -302,8 +316,7 @@ pub(crate) fn check(
             match <&RegMem>::from(src) {
                 RegMem::Reg { reg } => {
                     check_unop(ctx, vcode, 64, dst.to_writable_reg(), *reg, |src| {
-                        let extended = ctx.uextend(src, from_bytes * 8, to_bytes * 8);
-                        clamp_range(ctx, 64, from_bytes * 8, extended)
+                        clamp_range(ctx, 64, from_bytes * 8, Some(src.clone()))
                     })
                 }
                 RegMem::Mem { ref addr } => {
@@ -378,7 +391,7 @@ pub(crate) fn check(
                     )
                 })
             }
-            Imm8Reg::Reg { .. } => undefined_result(ctx, vcode, dst, 64, 64),
+            Imm8Reg::Reg { .. } => undefined_result(ctx, vcode, dst, 64, size.to_bits().into()),
         },
 
         Inst::ShiftR { size, dst, .. } => {
@@ -395,12 +408,23 @@ pub(crate) fn check(
             ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
         }
 
-        Inst::CmpRmiR { size, ref src, .. } => match <&RegMemImm>::from(src) {
+        Inst::CmpRmiR {
+            size, dst, ref src, ..
+        } => match <&RegMemImm>::from(src) {
             RegMemImm::Mem { ref addr } => {
-                check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
+                if let Some(rhs) = check_load(ctx, None, addr, vcode, size.to_type(), 64)? {
+                    let lhs = get_fact_or_default(vcode, dst.to_reg(), 64);
+                    state.cmp_flags = Some((lhs, rhs));
+                }
                 Ok(())
             }
-            RegMemImm::Reg { .. } | RegMemImm::Imm { .. } => Ok(()),
+            RegMemImm::Reg { reg } => {
+                let rhs = get_fact_or_default(vcode, *reg, 64);
+                let lhs = get_fact_or_default(vcode, dst.to_reg(), 64);
+                state.cmp_flags = Some((lhs, rhs));
+                Ok(())
+            }
+            RegMemImm::Imm { .. } => Ok(()),
         },
 
         Inst::Setcc { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
@@ -411,16 +435,32 @@ pub(crate) fn check(
             size,
             dst,
             ref consequent,
+            alternative,
+            cc,
             ..
-        } => {
-            match <&RegMem>::from(consequent) {
-                RegMem::Mem { ref addr } => {
-                    check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
-                }
-                RegMem::Reg { .. } => {}
+        } => match <&RegMem>::from(consequent) {
+            RegMem::Mem { ref addr } => {
+                check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
+                Ok(())
             }
-            undefined_result(ctx, vcode, dst, 64, 64)
-        }
+            RegMem::Reg { reg } if cc == CC::NB && cmp_flags.is_some() => {
+                let (cmp_lhs, cmp_rhs) = cmp_flags.unwrap();
+                trace!("lhs = {:?} rhs = {:?}", cmp_lhs, cmp_rhs);
+                let reg = *reg;
+                check_output(ctx, vcode, dst.to_writable_reg(), &[], |vcode| {
+                    // See comments in aarch64::pcc CSel for more details on this.
+                    let in_true = get_fact_or_default(vcode, reg, 64);
+                    let in_true =
+                        ctx.apply_inequality(&in_true, &cmp_lhs, &cmp_rhs, InequalityKind::Loose);
+                    let in_false = get_fact_or_default(vcode, alternative.to_reg(), 64);
+                    let in_false =
+                        ctx.apply_inequality(&in_false, &cmp_rhs, &cmp_lhs, InequalityKind::Strict);
+                    let union = Fact::union(&in_true, &in_false);
+                    clamp_range(ctx, 64, 64, union)
+                })
+            }
+            _ => undefined_result(ctx, vcode, dst, 64, 64),
+        },
 
         Inst::XmmCmove {
             dst,
diff --git a/cranelift/codegen/src/machinst/lower.rs b/cranelift/codegen/src/machinst/lower.rs
index bed1a3989..32d841ebb 100644
--- a/cranelift/codegen/src/machinst/lower.rs
+++ b/cranelift/codegen/src/machinst/lower.rs
@@ -148,6 +148,9 @@ pub trait LowerBackend {
         None
     }
 
+    /// The type of state carried between `check_fact` invocations.
+    type FactFlowState: Default + Clone + Debug;
+
     /// Check any facts about an instruction, given VCode with facts
     /// on VRegs. Takes mutable `VCode` so that it can propagate some
     /// kinds of facts automatically.
@@ -156,6 +159,7 @@ pub trait LowerBackend {
         _ctx: &FactContext<'_>,
         _vcode: &mut VCode<Self::MInst>,
         _inst: InsnIndex,
+        _state: &mut Self::FactFlowState,
     ) -> PccResult<()> {
         Err(PccError::UnimplementedBackend)
     }
diff --git a/cranelift/reader/src/parser.rs b/cranelift/reader/src/parser.rs
index dbd84d857..a3f0ec29a 100644
--- a/cranelift/reader/src/parser.rs
+++ b/cranelift/reader/src/parser.rs
@@ -12,7 +12,7 @@ use cranelift_codegen::entity::{EntityRef, PrimaryMap};
 use cranelift_codegen::ir::entities::{AnyEntity, DynamicType, MemoryType};
 use cranelift_codegen::ir::immediates::{Ieee32, Ieee64, Imm64, Offset32, Uimm32, Uimm64};
 use cranelift_codegen::ir::instructions::{InstructionData, InstructionFormat, VariableArgs};
-use cranelift_codegen::ir::pcc::Fact;
+use cranelift_codegen::ir::pcc::{BaseExpr, Expr, Fact};
 use cranelift_codegen::ir::types;
 use cranelift_codegen::ir::types::INVALID;
 use cranelift_codegen::ir::types::*;
@@ -1716,8 +1716,10 @@ impl<'a> Parser<'a> {
     // memory-type-decl ::= MemoryType(mt) "=" memory-type-desc
     // memory-type-desc ::= "struct" size "{" memory-type-field,* "}"
     //                    | "memory" size
+    //                    | "dynamic_memory" GlobalValue "+" offset
     //                    | "empty"
     // size ::= uimm64
+    // offset ::= uimm64
     fn parse_memory_type_decl(&mut self) -> ParseResult<(MemoryType, MemoryTypeData)> {
         let mt = self.match_mt("expected memory type number: mt«n»")?;
         self.match_token(Token::Equal, "expected '=' in memory type declaration")?;
@@ -1748,6 +1750,18 @@ impl<'a> Parser<'a> {
                 let size: u64 = self.match_uimm64("expected u64 constant value for size in static-memory memory-type declaration")?.into();
                 MemoryTypeData::Memory { size }
             }
+            Some(Token::Identifier("dynamic_memory")) => {
+                self.consume();
+                let gv = self.match_gv(
+                    "expected a global value for `dynamic_memory` memory-type declaration",
+                )?;
+                self.match_token(
+                    Token::Plus,
+                    "expected `+` after global value in `dynamic_memory` memory-type declaration",
+                )?;
+                let size: u64 = self.match_uimm64("expected u64 constant value for size offset in `dynamic_memory` memory-type declaration")?.into();
+                MemoryTypeData::DynamicMemory { gv, size }
+            }
             Some(Token::Identifier("empty")) => {
                 self.consume();
                 MemoryTypeData::Empty
@@ -2166,7 +2180,9 @@ impl<'a> Parser<'a> {
     // Parse a "fact" for proof-carrying code, attached to a value.
     //
     // fact ::= "range" "(" bit-width "," min-value "," max-value ")"
+    //        | "dynamic_range" "(" bit-width "," expr "," expr ")"
     //        | "mem" "(" memory-type "," mt-offset "," mt-offset ")"
+    //        | "dynamic_mem" "(" memory-type "," expr "," expr [ "," "nullable" ] ")"
     //        | "conflict"
     // bit-width ::= uimm64
     // min-value ::= uimm64
@@ -2213,6 +2229,23 @@ impl<'a> Parser<'a> {
                     max: max.into(),
                 })
             }
+            Some(Token::Identifier("dynamic_range")) => {
+                self.consume();
+                self.match_token(Token::LPar, "`dynamic_range` fact needs an opening `(`")?;
+                let bit_width: u64 = self
+                    .match_uimm64("expected a bit-width value for `dynamic_range` fact")?
+                    .into();
+                self.match_token(Token::Comma, "expected a comma")?;
+                let min = self.parse_expr()?;
+                self.match_token(Token::Comma, "expected a comma")?;
+                let max = self.parse_expr()?;
+                self.match_token(Token::RPar, "`dynamic_range` fact needs a closing `)`")?;
+                Ok(Fact::DynamicRange {
+                    bit_width: u16::try_from(bit_width).unwrap(),
+                    min,
+                    max,
+                })
+            }
             Some(Token::Identifier("mem")) => {
                 self.consume();
                 self.match_token(Token::LPar, "expected a `(`")?;
@@ -2224,10 +2257,7 @@ impl<'a> Parser<'a> {
                 let min_offset: u64 = self
                     .match_uimm64("expected a uimm64 minimum pointer offset for `mem` fact")?
                     .into();
-                self.match_token(
-                    Token::Comma,
-                    "expected a comma after memory type in `mem` fact",
-                )?;
+                self.match_token(Token::Comma, "expected a comma after offset in `mem` fact")?;
                 let max_offset: u64 = self
                     .match_uimm64("expected a uimm64 maximum pointer offset for `mem` fact")?
                     .into();
@@ -2238,11 +2268,124 @@ impl<'a> Parser<'a> {
                     max_offset,
                 })
             }
+            Some(Token::Identifier("dynamic_mem")) => {
+                self.consume();
+                self.match_token(Token::LPar, "expected a `(`")?;
+                let ty = self.match_mt("expected a memory type for `dynamic_mem` fact")?;
+                self.match_token(
+                    Token::Comma,
+                    "expected a comma after memory type in `dynamic_mem` fact",
+                )?;
+                let min = self.parse_expr()?;
+                self.match_token(
+                    Token::Comma,
+                    "expected a comma after offset in `dynamic_mem` fact",
+                )?;
+                let max = self.parse_expr()?;
+                let nullable = if self.token() == Some(Token::Comma) {
+                    self.consume();
+                    self.match_token(
+                        Token::Identifier("nullable"),
+                        "expected `nullable` in last optional field of `dynamic_mem`",
+                    )?;
+                    true
+                } else {
+                    false
+                };
+                self.match_token(Token::RPar, "expected a `)`")?;
+                Ok(Fact::DynamicMem {
+                    ty,
+                    min,
+                    max,
+                    nullable,
+                })
+            }
+            Some(Token::Identifier("compare")) => {
+                self.consume();
+                self.match_token(Token::LPar, "expected a `(`")?;
+                let kind = self.match_enum("expected intcc condition code in `compare` fact")?;
+                self.match_token(
+                    Token::Comma,
+                    "expected comma in `compare` fact after condition code",
+                )?;
+                let lhs = self.parse_base_expr()?;
+                self.match_token(Token::Comma, "expected comma in `compare` fact after LHS")?;
+                let rhs = self.parse_base_expr()?;
+                self.match_token(Token::RPar, "expected a `)`")?;
+                Ok(Fact::Compare { kind, lhs, rhs })
+            }
             Some(Token::Identifier("conflict")) => {
                 self.consume();
                 Ok(Fact::Conflict)
             }
-            _ => Err(self.error("expected a `range`, `mem` or `conflict` fact")),
+            _ => Err(self.error(
+                "expected a `range`, 'dynamic_range', `mem`, `dynamic_mem` or `conflict` fact",
+            )),
+        }
+    }
+
+    // Parse a dynamic expression used in some kinds of PCC facts.
+    //
+    // expr ::= base-expr
+    //        | base-expr + uimm64  // but in-range for imm64
+    //        | base-expr - uimm64  // but in-range for imm64
+    //        | imm64
+    fn parse_expr(&mut self) -> ParseResult<Expr> {
+        if let Some(Token::Integer(_)) = self.token() {
+            let offset: i64 = self
+                .match_imm64("expected imm64 for dynamic expression")?
+                .into();
+            Ok(Expr {
+                base: BaseExpr::None,
+                offset,
+            })
+        } else {
+            let base = self.parse_base_expr()?;
+            match self.token() {
+                Some(Token::Plus) => {
+                    self.consume();
+                    let offset: u64 = self
+                        .match_uimm64(
+                            "expected uimm64 in imm64 range for offset in dynamic expression",
+                        )?
+                        .into();
+                    let offset: i64 = i64::try_from(offset).map_err(|_| {
+                        self.error("integer offset in dynamic expression is out of range")
+                    })?;
+                    Ok(Expr { base, offset })
+                }
+                Some(Token::Integer(x)) if x.starts_with("-") => {
+                    let offset: i64 = self
+                        .match_imm64("expected an imm64 range for offset in dynamic expression")?
+                        .into();
+                    Ok(Expr { base, offset })
+                }
+                _ => Ok(Expr { base, offset: 0 }),
+            }
+        }
+    }
+
+    // Parse the base part of a dynamic expression, used in some PCC facts.
+    //
+    // base-expr ::= GlobalValue(base)
+    //             | Value(base)
+    //             | "max"
+    //             | (epsilon)
+    fn parse_base_expr(&mut self) -> ParseResult<BaseExpr> {
+        match self.token() {
+            Some(Token::Identifier("max")) => {
+                self.consume();
+                Ok(BaseExpr::Max)
+            }
+            Some(Token::GlobalValue(..)) => {
+                let gv = self.match_gv("expected global value")?;
+                Ok(BaseExpr::GlobalValue(gv))
+            }
+            Some(Token::Value(..)) => {
+                let value = self.match_value("expected value")?;
+                Ok(BaseExpr::Value(value))
+            }
+            _ => Ok(BaseExpr::None),
         }
     }
 
diff --git a/crates/fuzzing/src/generators/pooling_config.rs b/crates/fuzzing/src/generators/pooling_config.rs
index 9cdbd1d13..0997597f0 100644
--- a/crates/fuzzing/src/generators/pooling_config.rs
+++ b/crates/fuzzing/src/generators/pooling_config.rs
@@ -1,6 +1,7 @@
 //! Generate instance limits for the pooling allocation strategy.
 
 use arbitrary::{Arbitrary, Unstructured};
+use wasmtime::MpkEnabled;
 
 /// Configuration for `wasmtime::PoolingAllocationStrategy`.
 #[derive(Debug, Clone, Eq, PartialEq, Hash)]
@@ -30,6 +31,9 @@ pub struct PoolingAllocationConfig {
 
     pub async_stack_zeroing: bool,
     pub async_stack_keep_resident: usize,
+
+    pub memory_protection_keys: MpkEnabled,
+    pub max_memory_protection_keys: usize,
 }
 
 impl PoolingAllocationConfig {
@@ -62,6 +66,8 @@ impl PoolingAllocationConfig {
         cfg.async_stack_zeroing(self.async_stack_zeroing);
         cfg.async_stack_keep_resident(self.async_stack_keep_resident);
 
+        cfg.memory_protection_keys(self.memory_protection_keys);
+
         cfg
     }
 }
@@ -104,6 +110,9 @@ impl<'a> Arbitrary<'a> for PoolingAllocationConfig {
 
             async_stack_zeroing: u.arbitrary()?,
             async_stack_keep_resident: u.int_in_range(0..=1 << 20)?,
+
+            memory_protection_keys: u.choose(&[MpkEnabled::Auto, MpkEnabled::Disable])?.clone(),
+            max_memory_protection_keys: u.int_in_range(0..=20)?,
         })
     }
 }
diff --git a/crates/runtime/src/mpk/mod.rs b/crates/runtime/src/mpk/mod.rs
index bfffe2411..f60b3880b 100644
--- a/crates/runtime/src/mpk/mod.rs
+++ b/crates/runtime/src/mpk/mod.rs
@@ -42,7 +42,7 @@ cfg_if::cfg_if! {
 }
 
 /// Describe the tri-state configuration of memory protection keys (MPK).
-#[derive(Clone, Copy, Debug)]
+#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
 pub enum MpkEnabled {
     /// Use MPK if supported by the current system; fall back to guard regions
     /// otherwise.
diff --git a/crates/wasi/src/preview2/preview1.rs b/crates/wasi/src/preview2/preview1.rs
index 282f50ae7..ab5a9cbd5 100644
--- a/crates/wasi/src/preview2/preview1.rs
+++ b/crates/wasi/src/preview2/preview1.rs
@@ -9,7 +9,7 @@ use crate::preview2::bindings::{
     io::{poll, streams},
 };
 use crate::preview2::{FsError, IsATTY, StreamError, StreamResult, TableError, WasiView};
-use anyhow::{anyhow, bail, Context};
+use anyhow::{bail, Context};
 use std::borrow::Borrow;
 use std::collections::{BTreeMap, HashSet};
 use std::mem::{self, size_of, size_of_val};
@@ -1131,6 +1131,9 @@ impl<
             .map_err(types::Error::trap)?;
         let mut fs_flags = types::Fdflags::empty();
         let mut fs_rights_base = types::Rights::all();
+        if let types::Filetype::Directory = fs_filetype {
+            fs_rights_base &= !types::Rights::FD_SEEK;
+        }
         if !flags.contains(filesystem::DescriptorFlags::READ) {
             fs_rights_base &= !types::Rights::FD_READ;
         }
@@ -2258,14 +2261,11 @@ impl<
 
     #[instrument(skip(self))]
     fn proc_exit(&mut self, status: types::Exitcode) -> anyhow::Error {
-        let status = match status {
-            0 => Ok(()),
-            _ => Err(()),
-        };
-        match self.exit(status) {
-            Err(e) => e,
-            Ok(()) => anyhow!("`exit` did not return an error"),
+        // Check that the status is within WASI's range.
+        if status >= 126 {
+            return anyhow::Error::msg("exit with invalid exit status outside of [0..126)");
         }
+        crate::preview2::I32Exit(status as i32).into()
     }
 
     #[instrument(skip(self))]
diff --git a/src/commands/run.rs b/src/commands/run.rs
index df2fd673d..944c9434e 100644
--- a/src/commands/run.rs
+++ b/src/commands/run.rs
@@ -584,14 +584,22 @@ impl RunCommand {
         if self.run.common.wasi.common != Some(false) {
             match linker {
                 CliLinker::Core(linker) => {
-                    if self.run.common.wasi.preview2 == Some(true) {
-                        preview2::preview1::add_to_linker_sync(linker)?;
-                        self.set_preview2_ctx(store)?;
-                    } else {
-                        wasmtime_wasi::add_to_linker(linker, |host| {
-                            host.preview1_ctx.as_mut().unwrap()
-                        })?;
-                        self.set_preview1_ctx(store)?;
+                    match (self.run.common.wasi.preview2, self.run.common.wasi.threads) {
+                        // If preview2 is explicitly disabled, or if threads
+                        // are enabled, then use the historical preview1
+                        // implementation.
+                        (Some(false), _) | (None, Some(true)) => {
+                            wasmtime_wasi::add_to_linker(linker, |host| {
+                                host.preview1_ctx.as_mut().unwrap()
+                            })?;
+                            self.set_preview1_ctx(store)?;
+                        }
+                        // If preview2 was explicitly requested, always use it.
+                        // Otherwise use it so long as threads are disabled.
+                        (Some(true), _) | (None, Some(false) | None) => {
+                            preview2::preview1::add_to_linker_sync(linker)?;
+                            self.set_preview2_ctx(store)?;
+                        }
                     }
                 }
                 #[cfg(feature = "component-model")]


Test patch:
diff --git a/cranelift/filetests/filetests/pcc/succeed/dynamic.clif b/cranelift/filetests/filetests/pcc/succeed/dynamic.clif
new file mode 100644
index 000000000..13f96bc8b
--- /dev/null
+++ b/cranelift/filetests/filetests/pcc/succeed/dynamic.clif
@@ -0,0 +1,42 @@
+test compile
+set enable_pcc=true
+target aarch64
+target x86_64
+
+;; Equivalent to a Wasm `i64.load` from a dynamic memory.
+function %f0(i64 vmctx, i32) -> i64 {
+    gv0 = vmctx
+    gv1 = load.i64 notrap aligned checked gv0+0 ;; base
+    gv2 = load.i64 notrap aligned checked gv0+8 ;; size
+    
+    ;; mock vmctx struct:
+    mt0 = struct 16 {
+        0: i64 readonly ! dynamic_mem(mt1, 0, 0),
+        8: i64 readonly ! dynamic_range(64, gv2, gv2),
+    }
+    ;; mock dynamic memory: dynamic range, plus 2GiB guard
+    mt1 = dynamic_memory gv2 + 0x8000_0000
+
+block0(v0 ! mem(mt0, 0, 0): i64, v1 ! dynamic_range(32, v1, v1): i32):
+    v2 ! dynamic_range(64, v1, v1)            = uextend.i64 v1       ;; extended Wasm offset
+    v3 ! dynamic_mem(mt1, 0, 0)               = global_value.i64 gv1 ;; base
+    v4 ! dynamic_range(64, gv2, gv2)          = global_value.i64 gv2 ;; size
+    v5 ! compare(uge, v1, gv2)                = icmp.i64 uge v2, v4  ;; bounds-check compare of extended Wasm offset to size
+    v6 ! dynamic_mem(mt1, v1, v1)             = iadd.i64 v3, v2      ;; compute access address: memory base plus extended Wasm offset
+    v7 ! dynamic_mem(mt1, 0, 0, nullable)     = iconst.i64 0         ;; null pointer for speculative path
+    v8 ! dynamic_mem(mt1, 0, gv2-1, nullable) = select_spectre_guard v5, v7, v6  ;; if OOB, pick null, otherwise the real address
+    v9                                        = load.i64 checked v8
+    return v9
+}
+
+;; select sees:
+;;  v5 ! compare(uge, v1, gv2)
+;;  v6 ! dynamic_mem(mt1, v1, v1)
+;;  v7 ! dynamic_mem(mt0, 0, 0, nullable)
+;;
+;; preprocess:
+;; v6' (assuming compare is false) = dynamic_mem(mt1, 0, gv2-1)
+;; v7' (assuming compare is true)  = dynamic_mem(mt1, 0, 0, nullable)
+;;
+;; take the union of range and nullability:
+;; dynamic_mem(mt1, 0, gv2-1, nullable)
diff --git a/tests/all/cli_tests.rs b/tests/all/cli_tests.rs
index 2c8aa8122..39d435d9d 100644
--- a/tests/all/cli_tests.rs
+++ b/tests/all/cli_tests.rs
@@ -184,7 +184,7 @@ fn run_wasmtime_unreachable_wat() -> Result<()> {
 #[test]
 fn hello_wasi_snapshot0() -> Result<()> {
     let wasm = build_wasm("tests/all/cli_tests/hello_wasi_snapshot0.wat")?;
-    let stdout = run_wasmtime(&["-Ccache=n", wasm.path().to_str().unwrap()])?;
+    let stdout = run_wasmtime(&["-Ccache=n", "-Spreview2=n", wasm.path().to_str().unwrap()])?;
     assert_eq!(stdout, "Hello, world!\n");
     Ok(())
 }
@@ -248,7 +248,10 @@ fn timeout_in_invoke() -> Result<()> {
 #[test]
 fn exit2_wasi_snapshot0() -> Result<()> {
     let wasm = build_wasm("tests/all/cli_tests/exit2_wasi_snapshot0.wat")?;
-    let output = run_wasmtime_for_output(&["-Ccache=n", wasm.path().to_str().unwrap()], None)?;
+    let output = run_wasmtime_for_output(
+        &["-Ccache=n", "-Spreview2=n", wasm.path().to_str().unwrap()],
+        None,
+    )?;
     assert_eq!(output.status.code().unwrap(), 2);
     Ok(())
 }
@@ -266,7 +269,10 @@ fn exit2_wasi_snapshot1() -> Result<()> {
 #[test]
 fn exit125_wasi_snapshot0() -> Result<()> {
     let wasm = build_wasm("tests/all/cli_tests/exit125_wasi_snapshot0.wat")?;
-    let output = run_wasmtime_for_output(&["-Ccache=n", wasm.path().to_str().unwrap()], None)?;
+    let output = run_wasmtime_for_output(
+        &["-Ccache=n", "-Spreview2=n", wasm.path().to_str().unwrap()],
+        None,
+    )?;
     if cfg!(windows) {
         assert_eq!(output.status.code().unwrap(), 1);
     } else {
@@ -292,7 +298,10 @@ fn exit125_wasi_snapshot1() -> Result<()> {
 #[test]
 fn exit126_wasi_snapshot0() -> Result<()> {
     let wasm = build_wasm("tests/all/cli_tests/exit126_wasi_snapshot0.wat")?;
-    let output = run_wasmtime_for_output(&["-Ccache=n", wasm.path().to_str().unwrap()], None)?;
+    let output = run_wasmtime_for_output(
+        &["-Ccache=n", "-Spreview2=n", wasm.path().to_str().unwrap()],
+        None,
+    )?;
     assert_eq!(output.status.code().unwrap(), 1);
     assert!(output.stdout.is_empty());
     assert!(String::from_utf8_lossy(&output.stderr).contains("invalid exit status"));
@@ -439,7 +448,7 @@ fn hello_wasi_snapshot0_from_stdin() -> Result<()> {
     let wasm = build_wasm("tests/all/cli_tests/hello_wasi_snapshot0.wat")?;
     let stdout = {
         let path = wasm.path();
-        let args: &[&str] = &["-Ccache=n", "-"];
+        let args: &[&str] = &["-Ccache=n", "-Spreview2=n", "-"];
         let output = run_wasmtime_for_output(args, Some(path))?;
         if !output.status.success() {
             bail!(