feat(LLVM): add poison tracking to pointers in interpreter

Test/Interpreter/LLVM/null_pointer_bitcast.mlir

@@ -0,0 +1,15 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// The operation `llvm.mlir.zero` yields the zero address (null-pointer). Bitcasting it gives that address
+// with no poison bits, both as an `llvm.byte` and as an integer.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> (!llvm.ptr, !llvm.byte<64>, i64)}> ({
+    %p = "llvm.mlir.zero"() : () -> !llvm.ptr
+    %byte = "llvm.bitcast"(%p) : (!llvm.ptr) -> !llvm.byte<64>
+    %int = "llvm.bitcast"(%p) : (!llvm.ptr) -> i64
+    "func.return"(%p, %byte, %int) : (!llvm.ptr, !llvm.byte<64>, i64) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Program output: #[ptr(0x0000000000000000), 0b0000000000000000000000000000000000000000000000000000000000000000#64, 0x0000000000000000#64]

Test/Interpreter/LLVM/poison_pointer_bitcast.mlir

@@ -0,0 +1,15 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// Bitcasting a poison pointer gives a value whose bits are all poison: every
+// bit of an `llvm.byte` is poison, and an integer is poison as a whole.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> (!llvm.byte<64>, i64)}> ({
+    %p = "llvm.mlir.poison"() : () -> !llvm.ptr
+    %byte = "llvm.bitcast"(%p) : (!llvm.ptr) -> !llvm.byte<64>
+    %int = "llvm.bitcast"(%p) : (!llvm.ptr) -> i64
+    "func.return"(%byte, %int) : (!llvm.byte<64>, i64) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Program output: #[0b????????????????????????????????????????????????????????????????#64, poison]

Test/Interpreter/LLVM/poison_pointer_freeze.mlir

@@ -0,0 +1,15 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// Freezing a poison pointer yields some pointer; the interpreter picks null.
+// In the future, we would like to use ctrees to enable a non-determistic choice,
+// at least in our model.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> !llvm.ptr}> ({
+    %p = "llvm.mlir.poison"() : () -> !llvm.ptr
+    %f = "llvm.freeze"(%p) : (!llvm.ptr) -> !llvm.ptr
+    "func.return"(%f) : (!llvm.ptr) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Program output: #[ptr(0x0000000000000000)]

Test/Interpreter/LLVM/poison_pointer_gep.mlir

@@ -0,0 +1,14 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// Offsetting a poison pointer gives a poison pointer.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> !llvm.ptr}> ({
+    %four = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %p = "llvm.mlir.poison"() : () -> !llvm.ptr
+    %q = "llvm.getelementptr"(%p, %four) <{elem_type = i8, rawConstantIndices = array<i32: -2147483648>}> : (!llvm.ptr, i64) -> !llvm.ptr
+    "func.return"(%q) : (!llvm.ptr) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Program output: #[poison]

Test/Interpreter/LLVM/poison_pointer_load.mlir

@@ -0,0 +1,13 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// Loading from a poison pointer is undefined behaviour.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> i64}> ({
+    %p = "llvm.mlir.poison"() : () -> !llvm.ptr
+    %v = "llvm.load"(%p) : (!llvm.ptr) -> i64
+    "func.return"(%v) : (i64) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Undefined behavior

Test/Interpreter/LLVM/poison_pointer_register.mlir

@@ -0,0 +1,13 @@
+// RUN: not veir-interpret %s 2>&1 | filecheck %s
+
+// Moving a poison pointer into a riscv register is not yet supported.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> !riscv.reg}> ({
+    %p = "llvm.mlir.poison"() : () -> !llvm.ptr
+    %r = "builtin.unrealized_conversion_cast"(%p) : (!llvm.ptr) -> !riscv.reg
+    "func.return"(%r) : (!riscv.reg) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Error while interpreting module

Test/Interpreter/LLVM/poison_pointer_store_reload.mlir

@@ -0,0 +1,16 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// A poison pointer written to memory and read back gives poison again.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> !llvm.ptr}> ({
+    %one = "llvm.mlir.constant"() <{value = 1 : i64}> : () -> i64
+    %p = "llvm.mlir.poison"() : () -> !llvm.ptr
+    %dst = "llvm.alloca"(%one) <{elem_type = !llvm.ptr}> : (i64) -> !llvm.ptr
+    "llvm.store"(%p, %dst) : (!llvm.ptr, !llvm.ptr) -> ()
+    %back = "llvm.load"(%dst) : (!llvm.ptr) -> !llvm.ptr
+    "func.return"(%back) : (!llvm.ptr) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Program output: #[poison]

Test/Interpreter/LLVM/poison_pointer_uninit_load.mlir

@@ -0,0 +1,15 @@
+// RUN: veir-interpret %s | filecheck %s
+
+// A ptr value loaded from a stack-allocated pointer that was never written to
+// is poison.
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> !llvm.ptr}> ({
+    %one = "llvm.mlir.constant"() <{value = 1 : i64}> : () -> i64
+    %slot = "llvm.alloca"(%one) <{elem_type = !llvm.ptr}> : (i64) -> !llvm.ptr
+    %p = "llvm.load"(%slot) : (!llvm.ptr) -> !llvm.ptr
+    "func.return"(%p) : (!llvm.ptr) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: Program output: #[poison]

Veir/Data/LLVM.lean

@@ -2,6 +2,7 @@ module
 
 public import Veir.Data.LLVM.Int
 public import Veir.Data.LLVM.Byte
+public import Veir.Data.LLVM.Ptr
 public import Veir.Data.LLVM.FloatPred
 public import Veir.Data.LLVM.AtomicOrdering
 public import Veir.Data.LLVM.ComdatKind

Veir/Data/LLVM/Ptr.lean

@@ -0,0 +1,73 @@
+module
+
+public import Veir.Data.LLVM.Byte.Basic
+
+import all Veir.Data.LLVM.Byte.Basic
+
+namespace Veir.Data.LLVM
+
+public section
+
+/--
+  A pointer-typed value: an address, or poison.
+-/
+inductive Ptr where
+  /-- An address. -/
+  | val (p : UInt64)
+  /-- A poison value indicating deferred undefined behavior. -/
+  | poison
+deriving Inhabited, Repr, DecidableEq
+
+namespace Ptr
+
+def null : Ptr := .val 0
+
+@[expose, simp, grind .]
+def isRefinedBy : Ptr → Ptr → Prop
+  | .poison, _ => True
+  | .val p, .val p' => p = p'
+  | .val _, .poison => False
+
+@[inherit_doc] infix:50 " ⊒ " => LLVM.Ptr.isRefinedBy
+
+@[simp, grind .]
+theorem isRefinedBy_refl (p : Ptr) : p ⊒ p := by
+  cases p <;> simp
+
+@[grind .]
+theorem isRefinedBy_trans {p₁ p₂ p₃ : Ptr}
+    (h12 : p₁ ⊒ p₂) (h23 : p₂ ⊒ p₃) : p₁ ⊒ p₃ := by
+  cases p₁ <;> cases p₂ <;> cases p₃ <;> simp_all
+
+/-- Only the same pointer refines a pointer that is not poison. -/
+@[grind .]
+theorem eq_of_val_isRefinedBy {p : UInt64} {q : Ptr}
+    (h : Ptr.val p ⊒ q) : q = .val p := by
+  cases q <;> simp_all
+
+/-- The pointer whose bits are `b`, poison if any bit is poison. -/
+def ofByte (b : Byte 64) : Ptr :=
+  if b.poison = 0 then .val b.toUInt64 else .poison
+
+/-- The bits of a pointer: all poison for a poison pointer. -/
+def toByte : Ptr → Byte 64
+  | .val p => Byte.fromUInt64 p
+  | .poison => Byte.allPoison
+
+@[simp, grind =]
+theorem ofByte_toByte (p : Ptr) : ofByte p.toByte = p := by
+  cases p <;> simp [ofByte, toByte, Byte.toUInt64, Byte.allPoison]
+
+/-- Prints as `ptr(0x…)`, so a pointer is told apart from an integer in program output. -/
+instance : ToString Ptr where
+  toString
+    | .val p =>
+      let digits := String.ofList (Nat.toDigits 16 p.toNat)
+      s!"ptr(0x{"".pushn '0' (16 - digits.length) ++ digits})"
+    | .poison => "poison"
+
+end Ptr
+
+end
+
+end Veir.Data.LLVM

Veir/Interpreter/Basic.lean

@@ -358,14 +358,16 @@ def Llvm.interpretOp' (opType : Veir.Llvm) (properties : propertiesOf opType)
       none
   | .mlir__poison => do
     let some resType := resultTypes[0]? | none
-    let .integerType bw := resType.val | none
-    return (#[.int bw.bitwidth (LLVM.Int.mlir_poison bw.bitwidth)], mem, none)
+    match resType.val with
+    | .integerType bw => return (#[.int bw.bitwidth (LLVM.Int.mlir_poison bw.bitwidth)], mem, none)
+    | .llvmPointerType _ => return (#[.addr .poison], mem, none)
+    | _ => none
   | .mlir__zero => do
     let some resType := resultTypes[0]? | none
     match resType.val with
     | .integerType bw =>
       return (#[.int bw.bitwidth (LLVM.Int.val (BitVec.ofNat bw.bitwidth 0))], mem, none)
-    | .llvmPointerType _ => return (#[.addr 0], mem, none)
+    | .llvmPointerType _ => return (#[.addr LLVM.Ptr.null], mem, none)
     | _ => none
   | .add => do
     let [.int bw lhs, .int bw' rhs] := operands.toList | none
@@ -616,14 +618,16 @@ def Llvm.interpretOp' (opType : Veir.Llvm) (properties : propertiesOf opType)
     let size ← layout.getTypeAllocSize properties.elem_type.val
     let totalSize := (size * count.toNat).toUInt64
     let (mem, addr) := mem.alloc totalSize
-    return (#[.addr addr], mem, none)
+    return (#[.addr (.val addr)], mem, none)
   | .load => do
     let [.addr addr] := operands.toList | none
+    let .val addr := addr | Interp.ub
     let [type] := resultTypes.toList | none
     let val ← mem.llvmLoad addr type
     return (#[val], mem, none)
   | .store => do
     let [val, .addr addr] := operands.toList | none
+    let .val addr := addr | Interp.ub
     let mem ← mem.llvmStore addr val
     return (#[], mem, none)
   | .getelementptr => do
@@ -632,16 +636,18 @@ def Llvm.interpretOp' (opType : Veir.Llvm) (properties : propertiesOf opType)
     /- The index scales by the element's stride, matching the `getTypeAllocSize`
        that `isel-riscv64` uses to lower this operation. -/
     let size ← layout.getTypeAllocSize properties.elem_type.val
-    match idx with
-    | .val idx => return (#[.addr (ptr.toNat + idx.toNat * size).toUInt64], mem, none)
-    | .poison => Interp.ub
+    match ptr, idx with
+    | .val ptr, .val idx => return (#[.addr (.val (ptr.toNat + idx.toNat * size).toUInt64)], mem, none)
+    | _, _ => return (#[.addr .poison], mem, none)
   | .freeze => do
     let [val] := operands.toList | none
     match val with
     | .int w val =>
         return (#[.int w val.freeze], mem, none)
     | .byte w val =>
         return (#[.byte w val.freeze], mem, none)
+    | .addr .poison => return (#[.addr LLVM.Ptr.null], mem, none)
+    | .addr (.val p) => return (#[.addr (.val p)], mem, none)
     | _ => none
   | .bitcast => do
     let [val] := operands.toList | none
@@ -656,10 +662,16 @@ def Llvm.interpretOp' (opType : Veir.Llvm) (properties : propertiesOf opType)
       | .byte bw1 val', .integerType ⟨bw2⟩ =>
           if bw1 ≠ bw2 then .fail else .ok ((.int bw1 $ val'.toInt))
       | .byte bw val', .llvmPointerType _ =>
-          if h : bw = 64 then .ok ((.addr (val'.cast h).toUInt64)) else .fail
+          if h : bw = 64 then .ok (.addr (LLVM.Ptr.ofByte (val'.cast h))) else .fail
       | .addr val', .llvmPointerType _ => .ok (val)
       | .addr val', .byteType ⟨bw⟩ =>
-          if h : bw = 64 then .ok ((.byte 64 $ LLVM.Byte.fromUInt64 val')) else .fail
+          if bw = 64 then .ok (.byte 64 val'.toByte) else .fail
+      | .addr val', .integerType ⟨bw⟩ =>
+          if bw = 64 then
+            match val' with
+            | .val v => .ok (.int 64 (LLVM.Int.val v.toBitVec))
+            | .poison => .ok (.int 64 .poison)
+          else .fail
       | _, _ => none
     return (#[result], mem, none)
   | _ => none
@@ -1284,6 +1296,8 @@ def interpretOp' (opType : OpCode) (properties : propertiesOf opType)
     | .registerType _, [.byte _bw val] =>
       return (#[.reg (LLVM.Byte.toReg val)], mem, none)
     | .registerType _, [.addr val] =>
+      /- A register has no poison to carry, so a poison pointer cannot be cast into one. -/
+      let .val val := val | Interp.fail
       return (#[.reg ⟨val.toNat⟩], mem, none)
     | .integerType _bw, [.reg val] =>
       let .integerType resBw := resType.val | none
@@ -1292,7 +1306,7 @@ def interpretOp' (opType : OpCode) (properties : propertiesOf opType)
       let .byteType resBw := resType.val | none
       return (#[.byte resBw.bitwidth (RISCV.Reg.toByte val resBw.bitwidth)], mem, none)
     | .llvmPointerType _, [.reg val] =>
-      return (#[.addr ⟨val.val⟩], mem, none)
+      return (#[.addr (.val ⟨val.val⟩)], mem, none)
     | _ , _ => none
   | _ => none
 

Veir/Interpreter/Memory.lean

@@ -80,6 +80,11 @@ def MemoryState.empoison (state : MemoryState) (addr : UInt64) (n : Nat)
   else
     Interp.ub
 
+/-- Store the 64 bits of `v`, poison bits included, at `addr`. -/
+def MemoryState.storeByte64 (state : MemoryState) (addr : UInt64) (v : Data.LLVM.Byte 64)
+    : Interp MemoryState :=
+  state.store addr (UInt64.ofBitVec v.val).toByteArrayLE (UInt64.ofBitVec v.poison).toByteArrayLE (by simp)
+
 /--
   Store an LLVM value to memory.
   Yields UB if the access is out of bounds or the address is 0.
@@ -92,9 +97,9 @@ def MemoryState.llvmStore (state : MemoryState) (addr : UInt64) (val : RuntimeVa
   | .int 16 (.val v) => state.store addr (UInt16.ofBitVec v).toByteArrayLE
   | .int 32 (.val v) => state.store addr (UInt32.ofBitVec v).toByteArrayLE
   | .int 64 (.val v) => state.store addr (UInt64.ofBitVec v).toByteArrayLE
-  | .byte 64 v => state.store addr (UInt64.ofBitVec v.val).toByteArrayLE (UInt64.ofBitVec v.poison).toByteArrayLE (by simp)
+  | .byte 64 v => state.storeByte64 addr v
   | .int n .poison => state.empoison addr (n / 8)
-  | .addr v => state.store addr v.toByteArrayLE
+  | .addr p => state.storeByte64 addr p.toByte
   | _ => none
 
 /--
@@ -133,9 +138,27 @@ def MemoryState.hasPoison (state : MemoryState) (addr size : UInt64)
       break
   return poison
 
+/-- Load the 64 bits at `addr`, poison bits included. Yields UB if the access is out of bounds. -/
+def MemoryState.loadByte64 (state : MemoryState) (addr : UInt64) : Interp (Data.LLVM.Byte 64) := do
+  let ba ← state.load addr 8
+  let baPoison ← state.loadPoison addr 8
+  let poison := baPoison.toUInt64LE!.toBitVec
+  return ⟨ba.toUInt64LE!.toBitVec &&& ~~~poison, poison, by bv_decide⟩
+
 /--
   Load an LLVM value from the given memory address.
   Yields UB if access is out of bounds or the address is 0.
+
+  An integer or pointer load with any poison bit is poison as a whole, and a
+  `byte` load keeps poison per bit.
+
+  Together with fresh memory being poison, this is the semantics proposed in
+  "Towards Removing Undef Values from LLVM IR" (Lobo et al., PLDI 2026), not
+  LangRef's, where uninitialized memory reads as `undef`.
+  As Clang on still on poison, e.g., for a bitfield or an integer copy of a
+  struct with uninitialized padding, we sometimes introduce UB where we should
+  not. The solution is to introduce a freezing load to LLVM and VeIR and ensure
+  that all frontends are using them.
 -/
 def MemoryState.llvmLoad (state : MemoryState) (addr : UInt64) (type : TypeAttr)
     : Interp RuntimeValue := do
@@ -158,15 +181,9 @@ def MemoryState.llvmLoad (state : MemoryState) (addr : UInt64) (type : TypeAttr)
       if ← state.hasPoison addr 8 then return .int 64 .poison
       return .int 64 (.val (BitVec.ofNat 64 ba.toUInt64LE!.toNat))
   | Attribute.byteType { bitwidth := 64 } =>
-      let ba ← state.load addr 8
-      let baPoison ← state.loadPoison addr 8
-      let poison := baPoison.toUInt64LE!.toBitVec
-      return .byte 64 ⟨ba.toUInt64LE!.toBitVec &&& ~~~poison, poison, by bv_decide⟩
+      return .byte 64 (← state.loadByte64 addr)
   | Attribute.llvmPointerType _ =>
-      let ba ← state.load addr 8
-      -- FIXME poison address
-      if ← state.hasPoison addr 8 then return .addr 0
-      return .addr ba.toUInt64LE!
+      return .addr (Data.LLVM.Ptr.ofByte (← state.loadByte64 addr))
   | _ => none
 
 end Veir

Veir/Interpreter/Refinement/Basic.lean

@@ -35,7 +35,7 @@ def RuntimeValue.isRefinedBy (source target : RuntimeValue) : Prop :=
   match source, target with
   | .int bw s, .int bw' t => ∃ h : bw = bw', s.cast h ⊒ t
   | .byte bw s, .byte bw' t => ∃ h : bw = bw', s.cast h ⊒ t
-  | .addr s, .addr t => s = t
+  | .addr s, .addr t => s ⊒ t
   | .reg s, .reg t => s = t
   | .felt fieldType s, .felt fieldType' t => fieldType = fieldType' ∧ s = t
   | .float ty s, .float ty' t =>

Veir/Interpreter/Refinement/Lemmas.lean

@@ -160,12 +160,6 @@ theorem RuntimeValue.float_of_isRefinedBy {ty : FloatType} {v : Data.Float.Float
     tv = RuntimeValue.float ty v := by
   cases tv <;> grind [RuntimeValue.isRefinedBy]
 
-/-- A runtime value `tv` that refines an address runtime value `v` is equal to it. -/
-theorem RuntimeValue.addr_of_isRefinedBy {v : UInt64} {tv : RuntimeValue}
-    (h : RuntimeValue.addr v ⊒ tv) :
-    tv = RuntimeValue.addr v := by
-  cases tv <;> grind [RuntimeValue.isRefinedBy]
-
 /-- A runtime value `tv` that refines a register runtime value `v` is equal to it. -/
 theorem RuntimeValue.reg_of_isRefinedBy {v : Data.RISCV.Reg} {tv : RuntimeValue}
     (h : RuntimeValue.reg v ⊒ tv) :