refactor binopoffset with symbolic pointer offset tracking

kmir/src/kmir/kast.py

@@ -21,6 +21,7 @@
     Local,
     Metadata,
     Place,
+    PtrEmulationFromMetadata,
     PtrLocalValue,
     RangeValue,
     RefValue,
@@ -330,6 +331,8 @@ def _fresh_var(self, prefix: str) -> KVariable:
     def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInner], KInner | None]:
         # returns: symbolic value of given type, related constraints, related pointer metadata
 
+        ptr_emulation_label = 'ptrEmulation(_)_RT-VALUE-SYNTAX_PtrEmulation_Metadata'
+
         no_metadata = KApply(
             'Metadata',
             KApply('noMetadataSize', ()),
@@ -450,14 +453,15 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                 ref = self.ref_offset
                 self.ref_offset += 1
                 self.pointees.append(_typed_value(pointee_var, pointee_ty, mutable))
+                ptr_meta = metadata if metadata is not None else no_metadata
                 return (
                     KApply(
                         'Value::PtrLocal',
                         (
                             token(0),
                             KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
                             KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
-                            metadata if metadata is not None else no_metadata,
+                            KApply(ptr_emulation_label, (ptr_meta,)),
                         ),
                     ),
                     pointee_constraints,
@@ -632,6 +636,7 @@ def _random_ptr_value(self, mut: bool, type_info: PtrT | RefT) -> PtrLocalValue
                 metadata_size = NO_SIZE
 
         metadata = Metadata(size=metadata_size, pointer_offset=0, origin_size=metadata_size)
+        emulation = PtrEmulationFromMetadata(metadata)
 
         ref = next(self._ref)
 
@@ -641,7 +646,7 @@ def _random_ptr_value(self, mut: bool, type_info: PtrT | RefT) -> PtrLocalValue
                     stack_depth=0,
                     place=Place(local=Local(ref)),
                     mut=mut,
-                    metadata=metadata,
+                    emulation=emulation,
                 )
             case RefT():
                 return RefValue(

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -514,6 +514,75 @@ Execution gets stuck (no matching rule) when operands have different types or un
   rule #extractOperandType(_, _) => TyUnknown [owise]
 ```
 
+#### Pointer Offset (`std::intrinsics::offset`)
+
+The `offset` intrinsic performs pointer arithmetic, adding a signed offset to a pointer.
+It requires that the resulting pointer remain within bounds of the original allocation.
+This implementation delegates to the existing `binOpOffset` operation which handles bounds checking.
+
+```k
+  // Offset intrinsic: evaluate operands and apply offset operation
+  syntax KItem ::= #execOffsetTyped(Place, Evaluation, Evaluation, Evaluation) [seqstrict(2,3,4)]
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("offset")), PTR_OP:Operand OFFSET_OP:Operand .Operands, DEST)
+        => #execOffsetTyped(DEST, PTR_OP, OFFSET_OP, #applyBinOp(binOpOffset, PTR_OP, OFFSET_OP, false))
+       ... </k>
+
+  rule <k> #execOffsetTyped(DEST, _PTR:Value, _OFFSET:Value, RESULT:Value)
+        => #setLocalValue(DEST, RESULT)
+       ... </k>
+    [preserves-definedness]
+```
+
+#### Pointer Add (`core::ptr::const_ptr::add` / `core::ptr::mut_ptr::add`)
+
+The `ptr::add` intrinsic adds an unsigned count to a pointer, equivalent to `offset` with the count
+converted to a signed isize. This is a safe wrapper that only accepts non-negative offsets.
+
+```k
+  // ptr::add intrinsic: convert count to signed offset and delegate to offset
+  syntax KItem ::= #execPtrAddTyped(Place, Evaluation, Evaluation, Evaluation) [seqstrict(2,3,4)]
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_const_ptr_add")), PTR_OP:Operand COUNT_OP:Operand .Operands, DEST)
+        => #execPtrAddTyped(DEST, PTR_OP, COUNT_OP, #applyBinOp(binOpOffset, PTR_OP, COUNT_OP, false))
+       ... </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_mut_ptr_add")), PTR_OP:Operand COUNT_OP:Operand .Operands, DEST)
+        => #execPtrAddTyped(DEST, PTR_OP, COUNT_OP, #applyBinOp(binOpOffset, PTR_OP, COUNT_OP, false))
+       ... </k>
+
+  rule <k> #execPtrAddTyped(DEST, _PTR:Value, Integer(_COUNT, _WIDTH, false), RESULT:Value)
+        => #setLocalValue(DEST, RESULT)
+       ... </k>
+    [preserves-definedness]
+```
+
+#### Pointer Sub (`core::ptr::const_ptr::sub` / `core::ptr::mut_ptr::sub`)
+
+The `ptr::sub` intrinsic subtracts an unsigned count from a pointer, equivalent to `offset` with
+the negated count. This moves the pointer backwards in memory.
+
+```k
+  // ptr::sub intrinsic: negate count and delegate to offset
+  syntax KItem ::= #execPtrSubTyped(Place, Evaluation, Evaluation, Evaluation) [seqstrict(2,3,4)]
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_const_ptr_sub")), PTR_OP:Operand COUNT_OP:Operand .Operands, DEST)
+        => #execPtrSubTyped(DEST, PTR_OP, COUNT_OP, #computeSubOffset(PTR_OP, COUNT_OP))
+       ... </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_mut_ptr_sub")), PTR_OP:Operand COUNT_OP:Operand .Operands, DEST)
+        => #execPtrSubTyped(DEST, PTR_OP, COUNT_OP, #computeSubOffset(PTR_OP, COUNT_OP))
+       ... </k>
+
+  syntax Evaluation ::= #computeSubOffset(Evaluation, Evaluation) [seqstrict]
+  rule #computeSubOffset(PTR:Value, Integer(COUNT, _WIDTH, false))
+        => #applyBinOp(binOpOffset, PTR, Integer(0 -Int COUNT, 64, true), false)
+
+  rule <k> #execPtrSubTyped(DEST, _PTR:Value, Integer(_COUNT, _WIDTH, false), RESULT:Value)
+        => #setLocalValue(DEST, RESULT)
+       ... </k>
+    [preserves-definedness]
+```
+
 ### Stopping on Program Errors
 
 The semantics has a dedicated error sort to stop execution when flawed input or undefined behaviour is detected.