feat(LLVM): add poison tracking to pointers in interpreter by tobiasgrosser · Pull Request #1463 · opencompl/veir

tobiasgrosser · 2026-09-13T19:48:24Z

In LLVM, values of type ptr can be poison. This PR lifts our previously poison-free pointer runtime values to support element-level poison. We add the following interpreter semantics:

llvm.mlir.poison yields a poison value
llvm.mlir.zero yields a non-poison zero address
llvm.load and llvm.store trigger UB when accessing a poison address
llvm.getelementptr forwards poison on both operands
llvm.bitcast of a poison pointer yields (all) poison for llvm.int and llvm.byte

These semantics choices are worth taking a closer look:

unrealized_conversion_cast from llvm.ptr to riscv.reg where llvm.ptr is poison is fail for now.

As riscv.reg does not carry poison, the cast must either choose a concrete value or trigger UB. We will likely replace unrealized_conversion_cast in the future with zeroext, signext, anyext, and will also have ctrees, which will allow us to define meaningful semantics when casting to riscv.reg.
llvm.load into a llvm.ptr type yields poison if any bit loaded was labeled poison

Currently, LLVM models certain uninitialized memory as undef, but undef is due to be replaced. The paper Towards Removing Undef Values from LLVM IR proposes to set uninitialized memory to poison and use freezing loads to obtain unknown non-poisonous values. Without ctrees, a freeze is currently equal to picking a fixed concrete value, but eventually this will be a non-deterministic choice of any concrete bit pattern. As we neither want to introduce undef, we lack support for ctree, and also do not have freezing loads the current semantics means that in certain cases our semantics allow poison to propagate further than LLVM's. We document this.

For better readability of the test cases, we improve the toString method used for printing pointers.

regehr

this moves us in the right direction, I'd be happy to land this and work on the finer details as we move forward

Every other runtime value could be poison; a pointer could not, so the places that should have produced one returned an address of 0 instead. The pointer load even said so in a FIXME. An address of 0 is a value rather than a bottom element, so the substitute was observable. `Data.LLVM.Ptr` now wraps the address the way `Data.LLVM.Int` wraps its bit vector, and `RuntimeValue.addr` carries it. The memory interface stays indexed by a concrete address, because using a poison pointer for an access is undefined behaviour and that is decided by the operation before memory is reached. A pointer is poison when it is loaded from bytes with any poison in them, when it is bitcast from poisoned bits, or when it is offset from a poison pointer or by a poison index. Storing one writes eight poison bytes, which read back as poison both as a pointer and as an integer. Loading or storing through one, or casting one into a RISC-V register, is undefined behaviour: a register is a plain bit pattern with no poison to carry, which is the same reason Alive2's assembly mode drops poison entirely. `freeze` turns one into null. Refinement follows `Int`: poison is refined by every pointer, and a pointer only by itself.

luigirinaldi

From what I understand, it looks good. Some really minor nits in the new Ptr file.

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

nchappe

This looks good, thanks. Nit: the PR body is unclear, only unrealized casts from poison pointers to registers are fail.

tobiasgrosser · 2026-09-14T14:06:59Z

This looks good, thanks. Nit: the PR body is unclear, only unrealized casts from poison pointers to registers are fail.

Nice. I fixed the PR body wording.

math-fehr

Nice! I just had 1-2 style comments, but nothing major!
I think however we should change the semantics of unrealized_conversion_cast, otherwise currently our lowering would be unsound

math-fehr · 2026-09-14T21:43:30Z

+  cases q <;> simp_all
+
+/-- The pointer whose bits are `b`, poison if any bit is poison. -/
+def ofByte (b : Byte 64) : Ptr :=


Should we have the same for conversions with LLVM.Int, or is the conversion only with Byte?

math-fehr · 2026-09-14T21:45:29Z

+          if bw = 64 then
+            match val' with
+            | .val v => .ok (.int 64 (LLVM.Int.val v.toBitVec))
+            | .poison => .ok (.int 64 .poison)


For instance here, we should probably have a LLVM.Ptr.toInt?

math-fehr · 2026-09-14T22:31:49Z

    | .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)


This would be incorrect with

%p = "llvm.mlir.poison"() : () -> !llvm.ptr %b = "llvm.bitcast"(%p) : (!llvm.ptr) -> !llvm.byte<64>

Here, the current lowering might create this program:

%p = "llvm.mlir.poison"() : () -> !llvm.ptr %r = "builtin.unrealized_conversion_cast"(%p) : (!llvm.ptr) -> !riscv.reg %b = "builtin.unrealized_conversion_cast"(%r) : (!riscv.reg) -> !llvm.byte<64>

So returning fail here is making this transformation incorrect. I think the answer is to return non-deterministically any possible value of !riscv.reg, like we do with poison (and in that case here, only return 0 in the current interpreter).

math-fehr · 2026-09-14T22:58:35Z

+  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


tobiasgrosser changed the title ~~feat(interpreter): poison pointers~~ feat(LLVM): add poison tracking to pointers in interpreter Sep 13, 2026

tobiasgrosser force-pushed the tobias/poison_pointer branch 2 times, most recently from 78d457f to d963848 Compare September 13, 2026 22:47

regehr reviewed Sep 13, 2026

View reviewed changes

Comment thread Test/Interpreter/LLVM/poison_pointer_freeze.mlir Outdated

regehr reviewed Sep 13, 2026

View reviewed changes

Comment thread Veir/Data/LLVM/Ptr.lean Outdated

regehr approved these changes Sep 13, 2026

View reviewed changes

tobiasgrosser force-pushed the tobias/poison_pointer branch 7 times, most recently from 1e239b5 to 49b27bf Compare September 14, 2026 06:00

tobiasgrosser self-assigned this Sep 14, 2026

tobiasgrosser added the LLVM The LLVM Dialect label Sep 14, 2026

tobiasgrosser marked this pull request as ready for review September 14, 2026 07:32

tobiasgrosser force-pushed the tobias/poison_pointer branch from 0787d8a to 44d9650 Compare September 14, 2026 07:33

tobiasgrosser requested review from luigirinaldi, math-fehr and nchappe September 14, 2026 07:42

luigirinaldi approved these changes Sep 14, 2026

View reviewed changes

Comment thread Veir/Data/LLVM/Ptr.lean Outdated

Comment thread Veir/Data/LLVM/Ptr.lean Outdated

Comment thread Veir/Data/LLVM/Ptr.lean Outdated

Comment thread Veir/Data/LLVM/Ptr.lean

tobiasgrosser and others added 4 commits September 14, 2026 11:37

Update Veir/Data/LLVM/Ptr.lean

82d067a

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

Update Veir/Data/LLVM/Ptr.lean

c5dbac7

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

Update Veir/Data/LLVM/Ptr.lean

5be7b81

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

Add a comment about freeze

25ecfe2

tobiasgrosser commented Sep 14, 2026

View reviewed changes

Comment thread Test/Interpreter/LLVM/null_pointer_bitcast.mlir Outdated

Apply suggestion from @tobiasgrosser

86a8791

nchappe approved these changes Sep 14, 2026

View reviewed changes

math-fehr reviewed Sep 14, 2026

View reviewed changes

Uh oh!

Conversation

tobiasgrosser commented Sep 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

regehr left a comment

Choose a reason for hiding this comment

Uh oh!

luigirinaldi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

nchappe left a comment

Choose a reason for hiding this comment

Uh oh!

tobiasgrosser commented Sep 14, 2026

Uh oh!

math-fehr left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

math-fehr Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

math-fehr Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

math-fehr Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

math-fehr Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

tobiasgrosser commented Sep 13, 2026 •

edited

Loading