Repository: bytecodealliance/wasmtime
Pull request #7219 (2023-10-11 18:17:49)

PCC: add basic "memory types".
This PR adds a notion of "memory types" to the PCC (proof-carrying code) framework. To borrow a doc-comment:

A memory type is a struct-like definition -- fields with offsets, each field having a type and possibly an attached fact -- that we can use in proof-carrying code to validate accesses to structs and propagate facts onto the loaded values as well.

Memory types are meant to be rich enough to describe the *layout* of values in memory, but do not necessarily need to embody higher-level features such as subtyping directly. Rather, they should encode an implementation of a type or object system.

Note also that it is a non-goal for now for this type system to be "complete" or fully orthogonal: we have some restrictions now (e.g., struct fields are only primitives) because this is all we need for existing PCC applications, and it keeps the implementation simpler.

While developing this, we originally sketched out a more complete type-system that had arrays, allowed struct fields to be memory types themselves, and was in general more flexible. However, the possibility of cycles, non-statically-sized types, etc., was getting overly complex and I decided to YAGNI-simplify a bit for now. The Doc-comment on the module does sketch out what other types will be needed, and I think those plus a GV-bounded `max` fact will be enough to express PCC facts for all static and dynamic memories and table accesses in Wasmtime. (A partial further development of the more complete system, with some more validator checks for cycles, etc., is on [this WIP branch](https://github.com/cfallin/wasmtime/tree/pcc-memcap-wip).)

Part of this change was

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>


Patch:
diff --git a/cranelift/codegen/src/ir/dfg.rs b/cranelift/codegen/src/ir/dfg.rs
index ca02aee99..c903b18f4 100644
--- a/cranelift/codegen/src/ir/dfg.rs
+++ b/cranelift/codegen/src/ir/dfg.rs
@@ -188,6 +188,7 @@ impl DataFlowGraph {
         self.constants.clear();
         self.immediates.clear();
         self.jump_tables.clear();
+        self.facts.clear();
     }
 
     /// Get the total number of instructions created in this function, whether they are currently
diff --git a/cranelift/codegen/src/ir/entities.rs b/cranelift/codegen/src/ir/entities.rs
index f33e198c0..af2b0efc9 100644
--- a/cranelift/codegen/src/ir/entities.rs
+++ b/cranelift/codegen/src/ir/entities.rs
@@ -209,6 +209,29 @@ impl GlobalValue {
     }
 }
 
+/// An opaque reference to a memory type.
+///
+/// A `MemoryType` is a descriptor of a struct layout in memory, with
+/// types and proof-carrying-code facts optionally attached to the
+/// fields.
+#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
+pub struct MemoryType(u32);
+entity_impl!(MemoryType, "mt");
+
+impl MemoryType {
+    /// Create a new memory type reference from its number.
+    ///
+    /// This method is for use by the parser.
+    pub fn with_number(n: u32) -> Option<Self> {
+        if n < u32::MAX {
+            Some(Self(n))
+        } else {
+            None
+        }
+    }
+}
+
 /// An opaque reference to a constant.
 ///
 /// You can store [`ConstantData`](super::ConstantData) in a
@@ -412,6 +435,8 @@ pub enum AnyEntity {
     DynamicType(DynamicType),
     /// A Global value.
     GlobalValue(GlobalValue),
+    /// A memory type.
+    MemoryType(MemoryType),
     /// A jump table.
     JumpTable(JumpTable),
     /// A constant.
@@ -437,6 +462,7 @@ impl fmt::Display for AnyEntity {
             Self::DynamicStackSlot(r) => r.fmt(f),
             Self::DynamicType(r) => r.fmt(f),
             Self::GlobalValue(r) => r.fmt(f),
+            Self::MemoryType(r) => r.fmt(f),
             Self::JumpTable(r) => r.fmt(f),
             Self::Constant(r) => r.fmt(f),
             Self::FuncRef(r) => r.fmt(f),
@@ -495,6 +521,12 @@ impl From<GlobalValue> for AnyEntity {
     }
 }
 
+impl From<MemoryType> for AnyEntity {
+    fn from(r: MemoryType) -> Self {
+        Self::MemoryType(r)
+    }
+}
+
 impl From<JumpTable> for AnyEntity {
     fn from(r: JumpTable) -> Self {
         Self::JumpTable(r)
diff --git a/cranelift/codegen/src/ir/function.rs b/cranelift/codegen/src/ir/function.rs
index db91464d9..081ef15b2 100644
--- a/cranelift/codegen/src/ir/function.rs
+++ b/cranelift/codegen/src/ir/function.rs
@@ -7,8 +7,8 @@ use crate::entity::{PrimaryMap, SecondaryMap};
 use crate::ir::{
     self, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData, DynamicStackSlots,
     DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst, JumpTable,
-    JumpTableData, Layout, Opcode, SigRef, Signature, SourceLocs, StackSlot, StackSlotData,
-    StackSlots, Table, TableData, Type,
+    JumpTableData, Layout, MemoryType, MemoryTypeData, Opcode, SigRef, Signature, SourceLocs,
+    StackSlot, StackSlotData, StackSlots, Table, TableData, Type,
 };
 use crate::isa::CallConv;
 use crate::write::write_function;
@@ -172,6 +172,9 @@ pub struct FunctionStencil {
     /// Global values referenced.
     pub global_values: PrimaryMap<ir::GlobalValue, ir::GlobalValueData>,
 
+    /// Memory types for proof-carrying code.
+    pub memory_types: PrimaryMap<ir::MemoryType, ir::MemoryTypeData>,
+
     /// Tables referenced.
     pub tables: PrimaryMap<ir::Table, ir::TableData>,
 
@@ -201,6 +204,7 @@ impl FunctionStencil {
         self.sized_stack_slots.clear();
         self.dynamic_stack_slots.clear();
         self.global_values.clear();
+        self.memory_types.clear();
         self.tables.clear();
         self.dfg.clear();
         self.layout.clear();
@@ -235,6 +239,11 @@ impl FunctionStencil {
         self.global_values.push(data)
     }
 
+    /// Declares a memory type for use by the function.
+    pub fn create_memory_type(&mut self, data: MemoryTypeData) -> MemoryType {
+        self.memory_types.push(data)
+    }
+
     /// Find the global dyn_scale value associated with given DynamicType.
     pub fn get_dyn_scale(&self, ty: DynamicType) -> GlobalValue {
         self.dfg.dynamic_types.get(ty).unwrap().dynamic_scale
@@ -408,6 +417,7 @@ impl Function {
                 sized_stack_slots: StackSlots::new(),
                 dynamic_stack_slots: DynamicStackSlots::new(),
                 global_values: PrimaryMap::new(),
+                memory_types: PrimaryMap::new(),
                 tables: PrimaryMap::new(),
                 dfg: DataFlowGraph::new(),
                 layout: Layout::new(),
diff --git a/cranelift/codegen/src/ir/memtype.rs b/cranelift/codegen/src/ir/memtype.rs
new file mode 100644
index 000000000..04def7cf7
--- /dev/null
+++ b/cranelift/codegen/src/ir/memtype.rs
@@ -0,0 +1,174 @@
+//! Definitions for "memory types" in CLIF.
+//!
+//! A memory type is a struct-like definition -- fields with offsets,
+//! each field having a type and possibly an attached fact -- that we
+//! can use in proof-carrying code to validate accesses to structs and
+//! propagate facts onto the loaded values as well.
+//!
+//! Memory types are meant to be rich enough to describe the *layout*
+//! of values in memory, but do not necessarily need to embody
+//! higher-level features such as subtyping directly. Rather, they
+//! should encode an implementation of a type or object system.
+//!
+//! Note also that it is a non-goal for now for this type system to be
+//! "complete" or fully orthogonal: we have some restrictions now
+//! (e.g., struct fields are only primitives) because this is all we
+//! need for existing PCC applications, and it keeps the
+//! implementation simpler.
+//!
+//! There are a few basic kinds of types:
+//!
+//! - A struct is an aggregate of fields and an overall size. Each
+//!   field has a *primitive Cranelift type*. This is for simplicity's
+//!   sake: we do not allow nested memory types because to do so
+//!   invites cycles, requires recursive computation of sizes, creates
+//!   complicated questions when field types are dynamically-sized,
+//!   and in general is more complexity than we need.
+//!
+//!   The expectation (validated by PCC) is that when a checked load
+//!   or store accesses memory typed by a memory type, accesses will
+//!   only be to fields at offsets named in the type, and will be via
+//!   the given Cranelift type -- i.e., no type-punning occurs in
+//!   memory.
+//!
+//!   The overall size of the struct may be larger than that implied
+//!   by the fields because (i) we may not want or need to name all
+//!   the actually-existing fields in the memory type, and (ii) there
+//!   may be alignment padding that we also don't want or need to
+//!   represent explicitly.
+//!
+//! - A static memory is an untyped blob of storage with a static
+//!   size. This is memory that can be accessed with any type of load
+//!   or store at any valid offset.
+//!
+//!   Note that this is *distinct* from an "array of u8" kind of
+//!   representation of memory, if/when we can represent such a thing,
+//!   because the expectation with memory types' fields (including
+//!   array elements) is that they are strongly typed, only accessed
+//!   via that type, and not type-punned. We don't want to imply any
+//!   restriction on load/store size, or any actual structure, with
+//!   untyped memory; it's just a blob.
+//!
+//! 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.
+//!
+//! - A discriminated union is a union of several memory types
+//!   together with a tag field. This will be useful to model and
+//!   verify subtyping/downcasting for Wasm GC, among other uses.
+//!
+//! - Nullability on pointer fields: the fact will hold only if the
+//!   field is not null (all zero bits).
+
+use crate::ir::pcc::Fact;
+use crate::ir::Type;
+use alloc::vec::Vec;
+
+#[cfg(feature = "enable-serde")]
+use serde_derive::{Deserialize, Serialize};
+
+/// Data defining a memory type.
+///
+/// A memory type corresponds to a layout of data in memory. It may
+/// have a statically-known or dynamically-known size.
+#[derive(Clone, PartialEq, Hash)]
+#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
+pub enum MemoryTypeData {
+    /// An aggregate consisting of certain fields at certain offsets.
+    ///
+    /// Fields must be sorted by offset, must be within the struct's
+    /// overall size, and must not overlap. These conditions are
+    /// checked by the CLIF verifier.
+    Struct {
+        /// Size of this type.
+        size: u64,
+
+        /// Fields in this type. Sorted by offset.
+        fields: Vec<MemoryTypeField>,
+    },
+
+    /// A statically-sized untyped blob of memory.
+    Memory {
+        /// Accessible size.
+        size: u64,
+    },
+
+    /// A type with no size.
+    Empty,
+}
+
+impl std::default::Default for MemoryTypeData {
+    fn default() -> Self {
+        Self::Empty
+    }
+}
+
+impl std::fmt::Display for MemoryTypeData {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        match self {
+            Self::Struct { size, fields } => {
+                write!(f, "struct {size} {{")?;
+                let mut first = true;
+                for field in fields {
+                    if first {
+                        first = false;
+                    } else {
+                        write!(f, ",")?;
+                    }
+                    write!(f, " {}: {}", field.offset, field.ty)?;
+                    if field.readonly {
+                        write!(f, " readonly")?;
+                    }
+                    if let Some(fact) = &field.fact {
+                        write!(f, " ! {}", fact)?;
+                    }
+                }
+                write!(f, " }}")?;
+                Ok(())
+            }
+            Self::Memory { size } => {
+                write!(f, "memory {size:#x}")
+            }
+            Self::Empty => {
+                write!(f, "empty")
+            }
+        }
+    }
+}
+
+/// One field in a memory type.
+#[derive(Clone, PartialEq, Hash)]
+#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
+pub struct MemoryTypeField {
+    /// The offset of this field in the memory type.
+    pub offset: u64,
+    /// The primitive type of the value in this field. Accesses to the
+    /// field must use this type (i.e., cannot bitcast/type-pun in
+    /// memory).
+    pub ty: Type,
+    /// A proof-carrying-code fact about this value, if any.
+    pub fact: Option<Fact>,
+    /// Whether this field is read-only, i.e., stores should be
+    /// disallowed.
+    pub readonly: bool,
+}
+
+impl MemoryTypeData {
+    /// Provide the static size of this type, if known.
+    ///
+    /// (The size may not be known for dynamically-sized arrays or
+    /// memories, when those memtype kinds are added.)
+    pub fn static_size(&self) -> Option<u64> {
+        match self {
+            Self::Struct { size, .. } => Some(*size),
+            Self::Memory { size } => Some(*size),
+            Self::Empty => Some(0),
+        }
+    }
+}
diff --git a/cranelift/codegen/src/ir/mod.rs b/cranelift/codegen/src/ir/mod.rs
index c5cd50220..e2ec87d67 100644
--- a/cranelift/codegen/src/ir/mod.rs
+++ b/cranelift/codegen/src/ir/mod.rs
@@ -18,6 +18,7 @@ pub(crate) mod known_symbol;
 pub mod layout;
 pub(crate) mod libcall;
 mod memflags;
+mod memtype;
 pub mod pcc;
 mod progpoint;
 mod sourceloc;
@@ -38,7 +39,7 @@ pub use crate::ir::dfg::{BlockData, DataFlowGraph, ValueDef};
 pub use crate::ir::dynamic_type::{dynamic_to_fixed, DynamicTypeData, DynamicTypes};
 pub use crate::ir::entities::{
     Block, Constant, DynamicStackSlot, DynamicType, FuncRef, GlobalValue, Immediate, Inst,
-    JumpTable, SigRef, StackSlot, Table, UserExternalNameRef, Value,
+    JumpTable, MemoryType, SigRef, StackSlot, Table, UserExternalNameRef, Value,
 };
 pub use crate::ir::extfunc::{
     AbiParam, ArgumentExtension, ArgumentPurpose, ExtFuncData, Signature,
@@ -54,6 +55,7 @@ pub use crate::ir::known_symbol::KnownSymbol;
 pub use crate::ir::layout::Layout;
 pub use crate::ir::libcall::{get_probestack_funcref, LibCall};
 pub use crate::ir::memflags::{Endianness, MemFlags};
+pub use crate::ir::memtype::{MemoryTypeData, MemoryTypeField};
 pub use crate::ir::progpoint::ProgramPoint;
 pub use crate::ir::sourceloc::RelSourceLoc;
 pub use crate::ir::sourceloc::SourceLoc;
diff --git a/cranelift/codegen/src/ir/pcc.rs b/cranelift/codegen/src/ir/pcc.rs
index 08f2133cf..fc98bab18 100644
--- a/cranelift/codegen/src/ir/pcc.rs
+++ b/cranelift/codegen/src/ir/pcc.rs
@@ -46,6 +46,7 @@
 //! `FactContext::add()` and friends to forward-propagate facts.
 //!
 //! TODO:
+//! - Check blockparams' preds against blockparams' facts.
 //! - Propagate facts through optimization (egraph layer).
 //! - Generate facts in cranelift-wasm frontend when lowering memory ops.
 //! - Implement richer "points-to" facts that describe the pointed-to
@@ -58,6 +59,7 @@
 use crate::ir;
 use crate::isa::TargetIsa;
 use crate::machinst::{InsnIndex, LowerBackend, MachInst, VCode};
+use cranelift_entity::PrimaryMap;
 use std::fmt;
 
 #[cfg(feature = "enable-serde")]
@@ -110,32 +112,20 @@ pub enum Fact {
         max: u64,
     },
 
-    /// A pointer value to a memory region that can be accessed.
-    PointsTo {
-        /// A description of the memory region this pointer is allowed
-        /// to access (size, etc).
-        region: MemoryRegion,
+    /// A pointer to a memory type.
+    Mem {
+        /// The memory type.
+        ty: ir::MemoryType,
+        /// The offset into the memory type.
+        offset: i64,
     },
 }
 
-/// A memory region that can be accessed. This description is attached
-/// to a particular base pointer.
-#[derive(Clone, Debug, Hash, PartialEq, Eq)]
-#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
-pub struct MemoryRegion {
-    /// Includes both the actual memory bound as well as any guard
-    /// pages. Inclusive, so we can represent the full range of a
-    /// `u64`. The range is unsigned.
-    pub max: u64,
-}
-
 impl fmt::Display for Fact {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
-            Fact::ValueMax { bit_width, max } => write!(f, "max({}, 0x{:x})", bit_width, max),
-            Fact::PointsTo {
-                region: MemoryRegion { max },
-            } => write!(f, "points_to(0x{:x})", max),
+            Fact::ValueMax { bit_width, max } => write!(f, "max({}, {:#x})", bit_width, max),
+            Fact::Mem { ty, offset } => write!(f, "mem({}, {:#x})", ty, offset),
         }
     }
 }
@@ -157,20 +147,29 @@ macro_rules! bail {
 /// A "context" in which we can evaluate and derive facts. This
 /// context carries environment/global properties, such as the machine
 /// pointer width.
-#[derive(Debug)]
-pub struct FactContext {
+pub struct FactContext<'a> {
+    memory_types: &'a PrimaryMap<ir::MemoryType, ir::MemoryTypeData>,
     pointer_width: u16,
 }
 
-impl FactContext {
+impl<'a> FactContext<'a> {
     /// Create a new "fact context" in which to evaluate facts.
-    pub fn new(pointer_width: u16) -> Self {
-        FactContext { pointer_width }
+    pub fn new(
+        memory_types: &'a PrimaryMap<ir::MemoryType, ir::MemoryTypeData>,
+        pointer_width: u16,
+    ) -> Self {
+        FactContext {
+            memory_types,
+            pointer_width,
+        }
     }
 
     /// Computes whether `lhs` "subsumes" (implies) `rhs`.
     pub fn subsumes(&self, lhs: &Fact, rhs: &Fact) -> bool {
         match (lhs, rhs) {
+            // Reflexivity.
+            (l, r) if l == r => true,
+
             (
                 Fact::ValueMax {
                     bit_width: bw_lhs,
@@ -191,22 +190,7 @@ impl FactContext {
                 // possible value range.
                 bw_lhs == bw_rhs && max_lhs <= max_rhs
             }
-            (
-                Fact::PointsTo {
-                    region: MemoryRegion { max: max_lhs },
-                },
-                Fact::PointsTo {
-                    region: MemoryRegion { max: max_rhs },
-                },
-            ) => {
-                // If the pointer is valid up to `max_lhs`, and
-                // `max_rhs` is less than or equal to `max_lhs`, then
-                // it is certainly valid up to `max_rhs`.
-                //
-                // In other words, we can always shrink the valid
-                // addressable region.
-                max_rhs <= max_lhs
-            }
+
             _ => false,
         }
     }
@@ -240,19 +224,17 @@ impl FactContext {
                     bit_width: bw_max,
                     max,
                 },
-                Fact::PointsTo { region },
+                Fact::Mem { ty, offset },
             )
             | (
-                Fact::PointsTo { region },
+                Fact::Mem { ty, offset },
                 Fact::ValueMax {
                     bit_width: bw_max,
                     max,
                 },
             ) if *bw_max >= self.pointer_width && add_width >= *bw_max => {
-                let region = MemoryRegion {
-                    max: region.max.checked_sub(*max)?,
-                };
-                Some(Fact::PointsTo { region })
+                let offset = offset.checked_add(i64::try_from(*max).ok()?)?;
+                Some(Fact::Mem { ty: *ty, offset })
             }
 
             _ => None,
@@ -333,15 +315,15 @@ impl FactContext {
 
     /// Offsets a value with a fact by a known amount.
     pub fn offset(&self, fact: &Fact, width: u16, offset: i64) -> Option<Fact> {
-        // If we eventually support two-sided ranges, we can
-        // represent (0..n) + m -> ((0+m)..(n+m)). However,
-        // right now, all ranges start with zero, so any
-        // negative offset could underflow, and removes all
-        // claims of constrained range.
-        let offset = u64::try_from(offset).ok()?;
-
         match fact {
             Fact::ValueMax { bit_width, max } if *bit_width == width => {
+                // If we eventually support two-sided ranges, we can
+                // represent (0..n) + m -> ((0+m)..(n+m)). However,
+                // right now, all ranges start with zero, so any
+                // negative offset could underflow, and removes all
+                // claims of constrained range.
+                let offset = u64::try_from(offset).ok()?;
+
                 let max = match max.checked_add(offset) {
                     Some(max) => max,
                     None => {
@@ -357,13 +339,12 @@ impl FactContext {
                     max,
                 })
             }
-            Fact::PointsTo {
-                region: MemoryRegion { max },
+            Fact::Mem {
+                ty,
+                offset: mem_offset,
             } => {
-                let max = max.checked_sub(offset)?;
-                Some(Fact::PointsTo {
-                    region: MemoryRegion { max },
-                })
+                let offset = mem_offset.checked_sub(offset)?;
+                Some(Fact::Mem { ty: *ty, offset })
             }
             _ => None,
         }
@@ -373,9 +354,20 @@ impl FactContext {
     /// a memory access of the given size, is valid.
     pub fn check_address(&self, fact: &Fact, size: u32) -> PccResult<()> {
         match fact {
-            Fact::PointsTo {
-                region: MemoryRegion { max },
-            } => ensure!(u64::from(size) <= *max, OutOfBounds),
+            Fact::Mem { ty, offset } => {
+                let end_offset: i64 = offset
+                    .checked_add(i64::from(size))
+                    .ok_or(PccError::Overflow)?;
+                let end_offset: u64 =
+                    u64::try_from(end_offset).map_err(|_| PccError::OutOfBounds)?;
+                match &self.memory_types[*ty] {
+                    ir::MemoryTypeData::Struct { size, .. }
+                    | ir::MemoryTypeData::Memory { size } => {
+                        ensure!(end_offset <= *size, OutOfBounds)
+                    }
+                    ir::MemoryTypeData::Empty => bail!(OutOfBounds),
+                }
+            }
             _ => bail!(OutOfBounds),
         }
 
@@ -395,7 +387,7 @@ fn max_value_for_width(bits: u16) -> u64 {
 /// Top-level entry point after compilation: this checks the facts in
 /// VCode.
 pub fn check_vcode_facts<B: LowerBackend + TargetIsa>(
-    _f: &ir::Function,
+    f: &ir::Function,
     vcode: &VCode<B::MInst>,
     backend: &B,
 ) -> PccResult<()> {
@@ -407,7 +399,7 @@ pub fn check_vcode_facts<B: LowerBackend + TargetIsa>(
             // verify. We'll call into the backend to validate this
             // fact with respect to the instruction and the input
             // facts.
-            backend.check_fact(&vcode[inst], vcode)?;
+            backend.check_fact(&vcode[inst], f, vcode)?;
         }
     }
     Ok(())
diff --git a/cranelift/codegen/src/isa/aarch64/lower.rs b/cranelift/codegen/src/isa/aarch64/lower.rs
index 0ab57ec66..f3bbfd1e1 100644
--- a/cranelift/codegen/src/isa/aarch64/lower.rs
+++ b/cranelift/codegen/src/isa/aarch64/lower.rs
@@ -10,7 +10,7 @@
 use crate::ir::condcodes::{FloatCC, IntCC};
 use crate::ir::pcc::PccResult;
 use crate::ir::Inst as IRInst;
-use crate::ir::{Opcode, Value};
+use crate::ir::{Function, Opcode, Value};
 use crate::isa::aarch64::inst::*;
 use crate::isa::aarch64::pcc;
 use crate::isa::aarch64::AArch64Backend;
@@ -131,7 +131,12 @@ impl LowerBackend for AArch64Backend {
         Some(regs::pinned_reg())
     }
 
-    fn check_fact(&self, inst: &Self::MInst, vcode: &VCode<Self::MInst>) -> PccResult<()> {
-        pcc::check(inst, vcode)
+    fn check_fact(
+        &self,
+        inst: &Self::MInst,
+        function: &Function,
+        vcode: &VCode<Self::MInst>,
+    ) -> PccResult<()> {
+        pcc::check(inst, function, vcode)
     }
 }
diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index 50c3acfbe..81d330884 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -1,7 +1,7 @@
 //! Proof-carrying code checking for AArch64 VCode.
 
 use crate::ir::pcc::*;
-use crate::ir::MemFlags;
+use crate::ir::{Function, MemFlags};
 use crate::isa::aarch64::inst::args::{PairAMode, ShiftOp};
 use crate::isa::aarch64::inst::ALUOp;
 use crate::isa::aarch64::inst::Inst;
@@ -28,6 +28,12 @@ fn check_subsumes(ctx: &FactContext, subsumer: &Fact, subsumee: &Fact) -> PccRes
         subsumer,
         subsumee
     );
+
+    // For now, allow all `mem` facts to validate.
+    if matches!(subsumee, Fact::Mem { .. }) {
+        return Ok(());
+    }
+
     if ctx.subsumes(subsumer, subsumee) {
         Ok(())
     } else {
@@ -62,9 +68,9 @@ fn check_output<F: Fn() -> PccResult<Fact>>(
     }
 }
 
-pub(crate) fn check(inst: &Inst, vcode: &VCode<Inst>) -> PccResult<()> {
+pub(crate) fn check(inst: &Inst, function: &Function, vcode: &VCode<Inst>) -> PccResult<()> {
     // Create a new fact context with the machine's pointer width.
-    let ctx = FactContext::new(64);
+    let ctx = FactContext::new(&function.memory_types, 64);
 
     trace!("Checking facts on inst: {:?}", inst);
 
diff --git a/cranelift/codegen/src/machinst/lower.rs b/cranelift/codegen/src/machinst/lower.rs
index 0df5e7e73..4b360fd96 100644
--- a/cranelift/codegen/src/machinst/lower.rs
+++ b/cranelift/codegen/src/machinst/lower.rs
@@ -149,7 +149,12 @@ pub trait LowerBackend {
 
     /// Check any facts about an instruction, given VCode with facts
     /// on VRegs.
-    fn check_fact(&self, _inst: &Self::MInst, _vcode: &VCode<Self::MInst>) -> PccResult<()> {
+    fn check_fact(
+        &self,
+        _inst: &Self::MInst,
+        _function: &Function,
+        _vcode: &VCode<Self::MInst>,
+    ) -> PccResult<()> {
         Err(PccError::UnimplementedBackend)
     }
 }
diff --git a/cranelift/codegen/src/verifier/mod.rs b/cranelift/codegen/src/verifier/mod.rs
index 5eaecaa19..608d0ac05 100644
--- a/cranelift/codegen/src/verifier/mod.rs
+++ b/cranelift/codegen/src/verifier/mod.rs
@@ -47,6 +47,12 @@
 //! - Detect cycles in global values.
 //! - Detect use of 'vmctx' global value when no corresponding parameter is defined.
 //!
+//! Memory types
+//!
+//! - Ensure that struct fields are in offset order.
+//! - Ensure that struct fields are completely within the overall
+//!   struct size, and do not overlap.
+//!
 //! TODO:
 //! Ad hoc checking
 //!
@@ -66,7 +72,8 @@ use crate::ir::instructions::{CallInfo, InstructionFormat, ResolvedConstraint};
 use crate::ir::{self, ArgumentExtension};
 use crate::ir::{
     types, ArgumentPurpose, Block, Constant, DynamicStackSlot, FuncRef, Function, GlobalValue,
-    Inst, JumpTable, MemFlags, Opcode, SigRef, StackSlot, Type, Value, ValueDef, ValueList,
+    Inst, JumpTable, MemFlags, MemoryTypeData, Opcode, SigRef, StackSlot, Type, Value, ValueDef,
+    ValueList,
 };
 use crate::isa::TargetIsa;
 use crate::iterators::IteratorExtras;
@@ -403,6 +410,53 @@ impl<'a> Verifier<'a> {
         Ok(())
     }
 
+    fn verify_memory_types(&self, errors: &mut VerifierErrors) -> VerifierStepResult<()> {
+        // Verify that all fields are statically-sized and lie within
+        // the struct, do not overlap, and are in offset order
+        for (mt, mt_data) in &self.func.memory_types {
+            match mt_data {
+                MemoryTypeData::Struct { size, fields } => {
+                    let mut last_offset = 0;
+                    for field in fields {
+                        if field.offset < last_offset {
+                            errors.report((
+                                mt,
+                                format!(
+                                    "memory type {} has a field at offset {}, which is out-of-order",
+                                    mt, field.offset
+                                ),
+                            ));
+                        }
+                        last_offset = match field.offset.checked_add(u64::from(field.ty.bytes())) {
+                            Some(o) => o,
+                            None => {
+                                errors.report((
+                                        mt,
+                                        format!(
+                                            "memory type {} has a field at offset {} of size {}; offset plus size overflows a u64",
+                                            mt, field.offset, field.ty.bytes()),
+                                ));
+                                break;
+                            }
+                        };
+
+                        if last_offset > *size {
+                            errors.report((
+                                        mt,
+                                        format!(
+                                            "memory type {} has a field at offset {} of size {} that overflows the struct size {}",
+                                            mt, field.offset, field.ty.bytes(), *size),
+                                          ));
+                        }
+                    }
+                }
+                _ => {}
+            }
+        }
+
+        Ok(())
+    }
+
     fn verify_tables(&self, errors: &mut VerifierErrors) -> VerifierStepResult<()> {
         if let Some(isa) = self.isa {
             for (table, table_data) in &self.func.tables {
@@ -1754,6 +1808,7 @@ impl<'a> Verifier<'a> {
 
     pub fn run(&self, errors: &mut VerifierErrors) -> VerifierStepResult<()> {
         self.verify_global_values(errors)?;
+        self.verify_memory_types(errors)?;
         self.verify_tables(errors)?;
         self.typecheck_entry_block_params(errors)?;
         self.check_entry_not_cold(errors)?;
diff --git a/cranelift/codegen/src/write.rs b/cranelift/codegen/src/write.rs
index 20239d135..a550af4f3 100644
--- a/cranelift/codegen/src/write.rs
+++ b/cranelift/codegen/src/write.rs
@@ -56,6 +56,11 @@ pub trait FuncWriter {
             self.write_entity_definition(w, func, gv.into(), gv_data)?;
         }
 
+        for (mt, mt_data) in &func.memory_types {
+            any = true;
+            self.write_entity_definition(w, func, mt.into(), mt_data)?;
+        }
+
         for (table, table_data) in &func.tables {
             if !table_data.index_type.is_invalid() {
                 any = true;
diff --git a/cranelift/reader/src/lexer.rs b/cranelift/reader/src/lexer.rs
index 0367f4b7b..a738096af 100644
--- a/cranelift/reader/src/lexer.rs
+++ b/cranelift/reader/src/lexer.rs
@@ -40,6 +40,7 @@ pub enum Token<'a> {
     StackSlot(u32),        // ss3
     DynamicStackSlot(u32), // dss4
     GlobalValue(u32),      // gv3
+    MemoryType(u32),       // mt0
     Table(u32),            // table2
     Constant(u32),         // const2
     FuncRef(u32),          // fn2
@@ -344,6 +345,7 @@ impl<'a> Lexer<'a> {
             "dss" => Some(Token::DynamicStackSlot(number)),
             "dt" => Some(Token::DynamicType(number)),
             "gv" => Some(Token::GlobalValue(number)),
+            "mt" => Some(Token::MemoryType(number)),
             "table" => Some(Token::Table(number)),
             "const" => Some(Token::Constant(number)),
             "fn" => Some(Token::FuncRef(number)),
diff --git a/cranelift/reader/src/parser.rs b/cranelift/reader/src/parser.rs
index 100ef20ec..eabb7dff4 100644
--- a/cranelift/reader/src/parser.rs
+++ b/cranelift/reader/src/parser.rs
@@ -9,10 +9,10 @@ use crate::testcommand::TestCommand;
 use crate::testfile::{Comment, Details, Feature, TestFile};
 use cranelift_codegen::data_value::DataValue;
 use cranelift_codegen::entity::{EntityRef, PrimaryMap};
-use cranelift_codegen::ir::entities::{AnyEntity, DynamicType};
+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, MemoryRegion};
+use cranelift_codegen::ir::pcc::Fact;
 use cranelift_codegen::ir::types;
 use cranelift_codegen::ir::types::INVALID;
 use cranelift_codegen::ir::types::*;
@@ -20,8 +20,9 @@ use cranelift_codegen::ir::{self, UserExternalNameRef};
 use cranelift_codegen::ir::{
     AbiParam, ArgumentExtension, ArgumentPurpose, Block, Constant, ConstantData, DynamicStackSlot,
     DynamicStackSlotData, DynamicTypeData, ExtFuncData, ExternalName, FuncRef, Function,
-    GlobalValue, GlobalValueData, JumpTableData, MemFlags, Opcode, SigRef, Signature, StackSlot,
-    StackSlotData, StackSlotKind, Table, TableData, Type, UserFuncName, Value,
+    GlobalValue, GlobalValueData, JumpTableData, MemFlags, MemoryTypeData, MemoryTypeField, Opcode,
+    SigRef, Signature, StackSlot, StackSlotData, StackSlotKind, Table, TableData, Type,
+    UserFuncName, Value,
 };
 use cranelift_codegen::isa::{self, CallConv};
 use cranelift_codegen::packed_option::ReservedValue;
@@ -318,6 +319,16 @@ impl Context {
         Ok(())
     }
 
+    // Allocate a memory-type slot.
+    fn add_mt(&mut self, mt: MemoryType, data: MemoryTypeData, loc: Location) -> ParseResult<()> {
+        self.map.def_mt(mt, loc)?;
+        while self.function.memory_types.next_key().index() <= mt.index() {
+            self.function.create_memory_type(MemoryTypeData::default());
+        }
+        self.function.memory_types[mt] = data;
+        Ok(())
+    }
+
     // Resolve a reference to a global value.
     fn check_gv(&self, gv: GlobalValue, loc: Location) -> ParseResult<()> {
         if !self.map.contains_gv(gv) {
@@ -656,6 +667,17 @@ impl<'a> Parser<'a> {
         err!(self.loc, err_msg)
     }
 
+    // Match and consume a memory-type reference.
+    fn match_mt(&mut self, err_msg: &str) -> ParseResult<MemoryType> {
+        if let Some(Token::MemoryType(mt)) = self.token() {
+            self.consume();
+            if let Some(mt) = MemoryType::with_number(mt) {
+                return Ok(mt);
+            }
+        }
+        err!(self.loc, err_msg)
+    }
+
     // Match and consume a constant reference.
     fn match_constant(&mut self) -> ParseResult<Constant> {
         if let Some(Token::Constant(c)) = self.token() {
@@ -1448,6 +1470,11 @@ impl<'a> Parser<'a> {
                     self.parse_global_value_decl()
                         .and_then(|(gv, dat)| ctx.add_gv(gv, dat, self.loc))
                 }
+                Some(Token::MemoryType(..)) => {
+                    self.start_gathering_comments();
+                    self.parse_memory_type_decl()
+                        .and_then(|(mt, dat)| ctx.add_mt(mt, dat, self.loc))
+                }
                 Some(Token::Table(..)) => {
                     self.start_gathering_comments();
                     self.parse_table_decl()
@@ -1630,6 +1657,99 @@ impl<'a> Parser<'a> {
         Ok((gv, data))
     }
 
+    // Parse one field definition in a memory-type struct decl.
+    //
+    // memory-type-field ::=  offset ":" type ["readonly"] [ "!" fact ]
+    // offset ::= uimm64
+    fn parse_memory_type_field(&mut self) -> ParseResult<MemoryTypeField> {
+        let offset: u64 = self
+            .match_uimm64(
+                "expected u64 constant value for field offset in struct memory-type declaration",
+            )?
+            .into();
+        self.match_token(
+            Token::Colon,
+            "expected colon after field offset in struct memory-type declaration",
+        )?;
+        let ty = self.match_type("expected type for field in struct memory-type declaration")?;
+        let readonly = if self.token() == Some(Token::Identifier("readonly")) {
+            self.consume();
+            true
+        } else {
+            false
+        };
+        let fact = if self.token() == Some(Token::Bang) {
+            self.consume();
+            let fact = self.parse_fact()?;
+            Some(fact)
+        } else {
+            None
+        };
+        Ok(MemoryTypeField {
+            offset,
+            ty,
+            readonly,
+            fact,
+        })
+    }
+
+    // Parse a memory-type decl.
+    //
+    // memory-type-decl ::= MemoryType(mt) "=" memory-type-desc
+    // memory-type-desc ::= "struct" size "{" memory-type-field,* "}"
+    //                    | "memory" size
+    //                    | "empty"
+    // size ::= 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")?;
+
+        let data = match self.token() {
+            Some(Token::Identifier("struct")) => {
+                self.consume();
+                let size: u64 = self.match_uimm64("expected u64 constant value for struct size in struct memory-type declaration")?.into();
+                self.match_token(Token::LBrace, "expected opening brace to start struct fields in struct memory-type declaration")?;
+                let mut fields = vec![];
+                while self.token() != Some(Token::RBrace) {
+                    let field = self.parse_memory_type_field()?;
+                    fields.push(field);
+                    if self.token() == Some(Token::Comma) {
+                        self.consume();
+                    } else {
+                        break;
+                    }
+                }
+                self.match_token(
+                    Token::RBrace,
+                    "expected closing brace after struct fields in struct memory-type declaration",
+                )?;
+                MemoryTypeData::Struct { size, fields }
+            }
+            Some(Token::Identifier("memory")) => {
+                self.consume();
+                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("empty")) => {
+                self.consume();
+                MemoryTypeData::Empty
+            }
+            other => {
+                return err!(
+                    self.loc,
+                    "Unknown memory type declaration kind '{:?}'",
+                    other
+                )
+            }
+        };
+
+        // Collect any trailing comments.
+        self.token();
+        self.claim_gathered_comments(mt);
+
+        Ok((mt, data))
+    }
+
     // Parse a table decl.
     //
     // table-decl ::= * Table(table) "=" table-desc
@@ -2028,10 +2148,11 @@ impl<'a> Parser<'a> {
     // Parse a "fact" for proof-carrying code, attached to a value.
     //
     // fact ::= "max" "(" bit-width "," max-value ")"
-    //        | "points_to" "(" valid-range ")"
+    //        | "mem" "(" memory-type "," mt-offset ")"
     // bit-width ::= uimm64
     // max-value ::= uimm64
     // valid-range ::= uimm64
+    // mt-offset ::= imm64
     fn parse_fact(&mut self) -> ParseResult<Fact> {
         match self.token() {
             Some(Token::Identifier("max")) => {
@@ -2062,16 +2183,21 @@ impl<'a> Parser<'a> {
                     max: max.into(),
                 })
             }
-            Some(Token::Identifier("points_to")) => {
+            Some(Token::Identifier("mem")) => {
                 self.consume();
                 self.match_token(Token::LPar, "expected a `(`")?;
-                let max = self.match_uimm64("expected a max offset for `points_to` fact")?;
+                let ty = self.match_mt("expected a memory type for `mem` fact")?;
+                self.match_token(
+                    Token::Comma,
+                    "expected a comma after memory type in `mem` fact",
+                )?;
+                let offset: i64 = self
+                    .match_imm64("expected an imm64 pointer offset for `mem` fact")?
+                    .into();
                 self.match_token(Token::RPar, "expected a `)`")?;
-                Ok(Fact::PointsTo {
-                    region: MemoryRegion { max: max.into() },
-                })
+                Ok(Fact::Mem { ty, offset })
             }
-            _ => Err(self.error("expected a `max` or `points_to` fact")),
+            _ => Err(self.error("expected a `max` or `mem` fact")),
         }
     }
 
diff --git a/cranelift/reader/src/sourcemap.rs b/cranelift/reader/src/sourcemap.rs
index d8c21ebb1..99b55b9cb 100644
--- a/cranelift/reader/src/sourcemap.rs
+++ b/cranelift/reader/src/sourcemap.rs
@@ -10,8 +10,8 @@ use crate::error::{Location, ParseResult};
 use crate::lexer::split_entity_name;
 use cranelift_codegen::ir::entities::{AnyEntity, DynamicType};
 use cranelift_codegen::ir::{
-    Block, Constant, DynamicStackSlot, FuncRef, GlobalValue, JumpTable, SigRef, StackSlot, Table,
-    Value,
+    Block, Constant, DynamicStackSlot, FuncRef, GlobalValue, JumpTable, MemoryType, SigRef,
+    StackSlot, Table, Value,
 };
 use std::collections::HashMap;
 
@@ -182,6 +182,11 @@ impl SourceMap {
         self.def_entity(entity.into(), loc)
     }
 
+    /// Define the memory type `entity`.
+    pub fn def_mt(&mut self, entity: MemoryType, loc: Location) -> ParseResult<()> {
+        self.def_entity(entity.into(), loc)
+    }
+
     /// Define the table `entity`.
     pub fn def_table(&mut self, entity: Table, loc: Location) -> ParseResult<()> {
         self.def_entity(entity.into(), loc)
diff --git a/crates/runtime/src/memory.rs b/crates/runtime/src/memory.rs
index 84d568859..59cac8cab 100644
--- a/crates/runtime/src/memory.rs
+++ b/crates/runtime/src/memory.rs
@@ -565,6 +565,7 @@ impl SharedMemory {
     /// Implementation of `memory.atomic.notify` for this shared memory.
     pub fn atomic_notify(&self, addr_index: u64, count: u32) -> Result<u32, Trap> {
         validate_atomic_addr(&self.0.def.0, addr_index, 4, 4)?;
+        log::trace!("memory.atomic.notify(addr={addr_index}, count={count})");
         Ok(self.0.spot.unpark(addr_index, count))
     }
 
@@ -576,13 +577,18 @@ impl SharedMemory {
         timeout: Option<Instant>,
     ) -> Result<WaitResult, Trap> {
         let addr = validate_atomic_addr(&self.0.def.0, addr_index, 4, 4)?;
+        log::trace!(
+            "memory.atomic.wait32(addr={addr_index}, expected={expected}, timeout={timeout:?})"
+        );
+
         // SAFETY: `addr_index` was validated by `validate_atomic_addr` above.
         assert!(std::mem::size_of::<AtomicU32>() == 4);
         assert!(std::mem::align_of::<AtomicU32>() <= 4);
         let atomic = unsafe { &*(addr as *const AtomicU32) };
 
-        // We want the sequential consistency of `SeqCst` to ensure that the `load` sees the value that the `notify` will/would see.
-        // All WASM atomic operations are also `SeqCst`.
+        // We want the sequential consistency of `SeqCst` to ensure that the
+        // `load` sees the value that the `notify` will/would see. All WASM
+        // atomic operations are also `SeqCst`.
         let validate = || atomic.load(Ordering::SeqCst) == expected;
 
         Ok(self.0.spot.park(addr_index, validate, timeout))
@@ -596,6 +602,10 @@ impl SharedMemory {
         timeout: Option<Instant>,
     ) -> Result<WaitResult, Trap> {
         let addr = validate_atomic_addr(&self.0.def.0, addr_index, 8, 8)?;
+        log::trace!(
+            "memory.atomic.wait64(addr={addr_index}, expected={expected}, timeout={timeout:?})"
+        );
+
         // SAFETY: `addr_index` was validated by `validate_atomic_addr` above.
         assert!(std::mem::size_of::<AtomicU64>() == 8);
         assert!(std::mem::align_of::<AtomicU64>() <= 8);


Test patch:
diff --git a/cranelift/filetests/filetests/pcc/fail/load.clif b/cranelift/filetests/filetests/pcc/fail/load.clif
index 17a189fa0..a7b916add 100644
--- a/cranelift/filetests/filetests/pcc/fail/load.clif
+++ b/cranelift/filetests/filetests/pcc/fail/load.clif
@@ -3,57 +3,62 @@ set enable_pcc=true
 target aarch64
 
 function %f0(i64, i32) -> i64 {
-block0(v0 ! points_to(0x1000): i64, v1 ! max(32, 0x1000): i32):
+    mt0 = memory 0x1000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0x1000): i32):
     v2 ! max(64, 0x100) = uextend.i64 v1
-    v3 ! points_to(0x8) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0x100) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
 
 ;; Insufficient guard region: the 8-byte load could go off the end.
 function %f1(i64, i32) -> i64 {
-block0(v0 ! points_to(0x1_0000_0000): i64, v1 ! max(32, 0xffff_ffff): i32):
+    mt0 = memory 0x1_0000_0000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xffff_ffff): i32):
     v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
-    ;; 8 bytes of valid range is all we actually need, so let's only claim that.
-    v3 ! points_to(0x8) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
 
 ;; RegRegExtend mode on aarch64.
 function %f2(i64, i32) -> i8 {
-block0(v0 ! points_to(0x1000): i64, v1 ! max(32, 0x1000): i32):
+    mt0 = memory 0x1000
+block0(v0 ! mem(mt0, 0x1000): i64, v1 ! max(32, 0x1000): i32):
     v2 ! max(64, 0x100) = uextend.i64 v1
-    v3 ! points_to(0x1) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0x100) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
     return v4
 }
 
 ;; RegReg mode on aarch64.
 function %f3(i64, i64) -> i8 {
-block0(v0 ! points_to(0x100): i64, v1 ! max(64, 0xfff): i64):
-    v2 ! points_to(0x1) = iadd.i64 v0, v1
+    mt0 = memory 0x100
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(64, 0xfff): i64):
+    v2 ! mem(mt0, 0xfff) = iadd.i64 v0, v1
     v3 = load.i8 checked v2
     return v3
 }
 
 ;; RegScaledExtended mode on aarch64.
 function %f4(i64, i32) -> i64 {
-block0(v0 ! points_to(0x7000): i64, v1 ! max(32, 0xfff): i32):
+    mt0 = memory 0x7000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xfff): i32):
     v2 ! max(64, 0xfff) = uextend.i64 v1
     v3 = iconst.i32 3
     v4 ! max(64, 0x7ff8) = ishl.i64 v2, v3
-    v5 ! points_to(0x8) = iadd.i64 v0, v4
+    v5 ! mem(mt0, 0x7ff8) = iadd.i64 v0, v4
     v6 = load.i64 checked v5
     return v6
 }
 
 ;; RegScaled mode on aarch64.
 function %f5(i64, i64) -> i64 {
-block0(v0 ! points_to(0x7000): i64, v1 ! max(64, 0xfff): i64):
+    mt0 = memory 0x7000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(64, 0xfff): i64):
     v2 = iconst.i32 3
     v3 ! max(64, 0x7ff8) = ishl.i64 v1, v2
-    v4 ! points_to(0x8) = iadd.i64 v0, v3
+    v4 ! mem(mt0, 0x7ff8) = iadd.i64 v0, v3
     v5 = load.i64 checked v4
     return v5
 }
diff --git a/cranelift/filetests/filetests/pcc/fail/memtypes.clif b/cranelift/filetests/filetests/pcc/fail/memtypes.clif
new file mode 100644
index 000000000..2a9c87f1b
--- /dev/null
+++ b/cranelift/filetests/filetests/pcc/fail/memtypes.clif
@@ -0,0 +1,29 @@
+test verifier
+set enable_pcc=true
+target aarch64
+
+function %f0(i64) -> i32 {
+    mt0 = struct 8 { 4: i32, 0: i32 } ; error: out-of-order
+
+block0(v0 ! mem(mt0, 0): i64):
+    v1 = load.i32 v0+0
+    return v1
+}
+
+function %f0(i64) -> i32 {
+    ;; out-of-bounds field:
+    mt0 = struct 8 { 0: i32, 6: i32 } ; error: field at offset 6 of size 4 that overflows
+
+block0(v0 ! mem(mt0, 0): i64):
+    v1 = load.i32 v0+0
+    return v1
+}
+
+function %f0(i64) -> i32 {
+    ;; overflowing offset + field size:
+    mt0 = struct 8 { 0: i32, 0xffff_ffff_ffff_ffff: i32 } ; error: field at offset 18446744073709551615 of size 4; offset plus size overflows a u64
+
+block0(v0 ! mem(mt0, 0): i64):
+    v1 = load.i32 v0+0
+    return v1
+}
diff --git a/cranelift/filetests/filetests/pcc/fail/simple.clif b/cranelift/filetests/filetests/pcc/fail/simple.clif
index 5aac4f860..6196e4e31 100644
--- a/cranelift/filetests/filetests/pcc/fail/simple.clif
+++ b/cranelift/filetests/filetests/pcc/fail/simple.clif
@@ -2,14 +2,25 @@ test compile expect-fail
 set enable_pcc=true
 target aarch64
 
-;; The `points_to` annotation is not large enough here -- the
-;; 4GiB-range 32-bit offset could go out of range. PCC should catch
-;; this.
+;; The `memory` memtype is not large enough here -- the 4GiB-range
+;; 32-bit offset could go out of range. PCC should catch this.
 
 function %simple1(i64 vmctx, i32) -> i8 {
-block0(v0 ! points_to(0x8000_0000): i64, v1 ! max(32, 0xffff_ffff): i32):
+    mt0 = memory 0x8000_0000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xffff_ffff): i32):
     v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
-    v3 ! points_to(0x1) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0xffff_ffff) = iadd.i64 v0, v2
+    v4 = load.i8 checked v3
+    return v4
+}
+
+;; Check that the offset in the `mem` is validated too.
+
+function %simple2(i64 vmctx, i32) -> i8 {
+    mt0 = memory 0x8000_0000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xffff_ffff): i32):
+    v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
+    v3 ! mem(mt0, 0) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
     return v4
 }
diff --git a/cranelift/filetests/filetests/pcc/succeed/load.clif b/cranelift/filetests/filetests/pcc/succeed/load.clif
index e863cb059..6766c7a28 100644
--- a/cranelift/filetests/filetests/pcc/succeed/load.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/load.clif
@@ -3,58 +3,62 @@ set enable_pcc=true
 target aarch64
 
 function %f0(i64, i32) -> i64 {
-block0(v0 ! points_to(0x1_0000_0000): i64, v1 ! max(32, 0x100): i32):
+    mt0 = memory 0x1_0000_0000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0x100): i32):
     v2 ! max(64, 0x100) = uextend.i64 v1
-    ;; 8 bytes of valid range is all we actually need, so let's only claim that.
-    v3 ! points_to(0x8) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 8) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
 
-;; Note the guard region of 8 bytes -- just enough for the below!
 function %f1(i64, i32) -> i64 {
-block0(v0 ! points_to(0x1_0000_0008): i64, v1 ! max(32, 0xffff_ffff): i32):
+    ;; Note the guard region of 8 bytes -- just enough for the below!
+    mt0 = memory 0x1_0000_0008
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xffff_ffff): i32):
     v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
-    ;; 8 bytes of valid range is all we actually need, so let's only claim that.
-    v3 ! points_to(0x8) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i64 checked v3
     return v4
 }
 
 ;; RegRegExtend mode on aarch64.
 function %f2(i64, i32) -> i8 {
-block0(v0 ! points_to(0x1000): i64, v1 ! max(32, 0xfff): i32):
+    mt0 = memory 0x1000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xfff): i32):
     v2 ! max(64, 0x100) = uextend.i64 v1
-    v3 ! points_to(0x1) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0x100) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
     return v4
 }
 
 ;; RegReg mode on aarch64.
 function %f3(i64, i64) -> i8 {
-block0(v0 ! points_to(0x1000): i64, v1 ! max(64, 0xfff): i64):
-    v2 ! points_to(0x1) = iadd.i64 v0, v1
+    mt0 = memory 0x1000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(64, 0xfff): i64):
+    v2 ! mem(mt0, 0xfff) = iadd.i64 v0, v1
     v3 = load.i8 checked v2
     return v3
 }
 
 ;; RegScaledExtended mode on aarch64.
 function %f4(i64, i32) -> i64 {
-block0(v0 ! points_to(0x8000): i64, v1 ! max(32, 0xfff): i32):
+    mt0 = memory 0x8000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xfff): i32):
     v2 ! max(64, 0xfff) = uextend.i64 v1
     v3 = iconst.i32 3
     v4 ! max(64, 0x7ff8) = ishl.i64 v2, v3
-    v5 ! points_to(0x8) = iadd.i64 v0, v4
+    v5 ! mem(mt0, 0x7ff8) = iadd.i64 v0, v4
     v6 = load.i64 checked v5
     return v6
 }
 
 ;; RegScaled mode on aarch64.
 function %f5(i64, i64) -> i64 {
-block0(v0 ! points_to(0x8000): i64, v1 ! max(64, 0xfff): i64):
+    mt0 = memory 0x8000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(64, 0xfff): i64):
     v2 = iconst.i32 3
     v3 ! max(64, 0x7ff8) = ishl.i64 v1, v2
-    v4 ! points_to(0x8) = iadd.i64 v0, v3
+    v4 ! mem(mt0, 0x7ff8) = iadd.i64 v0, v3
     v5 = load.i64 checked v4
     return v5
 }
diff --git a/cranelift/filetests/filetests/pcc/succeed/memtypes.clif b/cranelift/filetests/filetests/pcc/succeed/memtypes.clif
new file mode 100644
index 000000000..9849ea00e
--- /dev/null
+++ b/cranelift/filetests/filetests/pcc/succeed/memtypes.clif
@@ -0,0 +1,23 @@
+test compile
+set enable_pcc=true
+target aarch64
+
+function %f0(i64) -> i32 {
+    mt0 = struct 8 { 0: i32, 4: i32 readonly }
+
+block0(v0 ! mem(mt0, 0): i64):  ;; v0 points to an instance of mt0, at offset 0
+    v1 = load.i32 v0+0
+    v2 = load.i32 v0+4
+    v3 = iadd.i32 v1, v2
+    return v3
+}
+
+function %f1(i64) -> i32 {
+    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0) }
+    mt1 = memory 0x1_0000_0000
+
+block0(v0 ! mem(mt0, 0): i64):
+    v1 ! mem(mt1, 0) = load.i64 v0
+    v2 = load.i32 v1+0x1000
+    return v2
+}
diff --git a/cranelift/filetests/filetests/pcc/succeed/simple.clif b/cranelift/filetests/filetests/pcc/succeed/simple.clif
index cf1793e5a..241124e67 100644
--- a/cranelift/filetests/filetests/pcc/succeed/simple.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/simple.clif
@@ -3,9 +3,10 @@ set enable_pcc=true
 target aarch64
 
 function %simple1(i64 vmctx, i32) -> i8 {
-block0(v0 ! points_to(0x1_0000_0000): i64, v1 ! max(32, 0xffff_ffff): i32):
+    mt0 = memory 0x1_0000_0000
+block0(v0 ! mem(mt0, 0): i64, v1 ! max(32, 0xffff_ffff): i32):
     v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
-    v3 ! points_to(0x1) = iadd.i64 v0, v2
+    v3 ! mem(mt0, 0xffff_ffff) = iadd.i64 v0, v2
     v4 = load.i8 checked v3
     return v4
 }