Skip to content

Conversation

@aslitaser
Copy link

overview

refactors the binopoffset implementation to use symbolic offset tracking instead of eagerly updating pointer metadata. follows the approach outlined in branch 709-binopoffset-again.

changes

data structures

  • introduced PtrEmulation sort to track pointer offsets symbolically
  • four variants: ptrEmulation (wraps metadata), ptrOffset (valid offset), ptrOrigSize (original allocation size), InvalidOffset (out-of-bounds)
  • modified PtrLocalValue in python to use PtrEmulation instead of raw Metadata

pointer operations

  • refactored binOpOffset to create offset nodes instead of immediately checking bounds
  • bounds checking now happens lazily at dereference time (matches rust's unsafe semantics)
  • simplified dereference rules from 4 separate cases down to 2 unified rules

type conversions

  • implemented #convertPtrEmul to handle array ↔ element pointer conversions
  • when casting array pointer to element pointer, creates ptrOrigSize to remember allocation size
  • when casting back, validates bounds and creates InvalidOffset if out of bounds

intrinsics

  • implemented std::intrinsics::offset (signed offset)
  • implemented ptr::add (unsigned, forward offset)
  • implemented ptr::sub (unsigned, backward offset)

tests

  • added 5 new prove-rs tests covering basic offset, bounds failures, negative offsets
  • added corresponding exec-smir tests with generated state files

current status

dereferencing logic needs refinement - the tests are failing because #applyPtrOffset currently uses PointerOffset projection for all cases. according to the notes in 709-binopoffset-again, when dereferencing ptrOffset(N, ptrOrigSize(_)) (pointer to single element), it should use ConstantIndex projection instead of PointerOffset which expects a Range value.

the current implementation works for array/slice pointers but gets stuck when dereferencing offset pointers to single elements.

related

- add helper functions for ptremulation (init, accessors, bounds checking)
- refactor binopoffset to use symbolic offset tracking
- simplify dereference rules from 4 to 2 using ptremulation
- implement convertptremul for array/element pointer conversions
- add bounds checking at dereference time instead of offset time
@aslitaser aslitaser marked this pull request as draft October 29, 2025 13:43
@dkcumming
Copy link
Collaborator

@aslitaser thank you, we will take a look at this!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Implement binOpOffset

2 participants