Initial Ptr Offset semantics binOpOffset (#746)

Support for `binOpOffset`

- `binOpOffset` is applied to a `PtrLocal` but must come from a `Range`
of some kind (e.g. `[u8; 2]`, `&[u8]`) in which case the offset is
applied to a pointer to the element e.g. `*const u8`;
- Both `Reference` and `PtrLocal` has the same `Metadata` that tracks
and offset;
- In order to ensure that pointers are not out of range when the offset
is applied, `Metadata` has an `OriginSize` field for `PtrLocal` and
`Reference` for the necessary bounds checking in the external `Range`;
- After an offset is applied to a `PtrLocal` it can be turned back into
a `Reference`, which essentially is an index into the `Range` but it
does not return the element type but the `Range` type (with smaller
bounds);
- The bulk of the change is in `#traverseProjection` that now needs to
account for an offset when a `projectionDeref` occurs;
- When a non-zero offset is encountered a
`ProjectionElem::PointerOffset` is appended to the place projections,
later this will be turned into a `CtxPointerOffset` when the contexts
are being processed;
- `CtxPointerOffset` is essentially the same as a subslice as we must
have a `Range` to be offsetting through

Test cases for read and write are added

---------

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Author: dkcumming

kmir/src/kmir/decoding.py

@@ -43,7 +43,7 @@
     from pyk.kast import KInner
 
     from .ty import FieldsShape, IntegerLength, LayoutShape, MachineSize, Scalar, TagEncoding, Ty, TypeMetadata, UintTy
-    from .value import Metadata
+    from .value import MetadataSize
 
 
 @dataclass
@@ -145,7 +145,7 @@ def _pointee_ty(type_info: TypeMetadata) -> Ty | None:
             return None
 
 
-def _metadata(type_info: TypeMetadata) -> Metadata:
+def _metadata(type_info: TypeMetadata) -> MetadataSize:
     match type_info:
         case ArrayT(length=None):
             return DynamicSize(1)  # 1 is a placeholder, the actual size is inferred from the slice data

kmir/src/kmir/kast.py

@@ -23,7 +23,7 @@
 
     from .smir import SMIRInfo
     from .ty import TypeMetadata
-    from .value import Metadata, Value
+    from .value import MetadataSize, Value
 
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -312,6 +312,14 @@ 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
+
+        no_metadata = KApply(
+            'Metadata',
+            KApply('noMetadataSize', ()),
+            token(0),
+            KApply('noMetadataSize', ()),
+        )
+
         match self.types.get(ty):
             case IntT(info):
                 val, constraints = int_var(self._fresh_var('ARG_INT'), info.value, True)
@@ -359,7 +367,14 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                 return (
                     KApply('Value::Range', (elems,)),
                     [mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), l))],
-                    KApply('dynamicSize', (l,)),
+                    KApply(
+                        'Metadata',
+                        (
+                            KApply('dynamicSize', (l,)),
+                            token(0),
+                            KApply('dynamicSize', (l,)),
+                        ),
+                    ),
                 )
 
             case ArrayT(element_type, size) if size is not None:
@@ -372,7 +387,14 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                 return (
                     KApply('Value::Range', (list_of(elem_vars),)),
                     elem_constraints,
-                    KApply('staticSize', (token(size),)),
+                    KApply(
+                        'Metadata',
+                        (
+                            KApply('staticSize', (token(size),)),
+                            token(0),
+                            KApply('staticSize', (token(size),)),
+                        ),
+                    ),
                 )
 
             case TupleT(components):
@@ -397,10 +419,10 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                     KApply(
                         'Value::Reference',
                         (
-                            token(0),
+                            token(0),  # Stack OFFSET field
                             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 KApply('noMetadata', ()),
+                            metadata if metadata is not None else no_metadata,
                         ),
                     ),
                     pointee_constraints,
@@ -418,7 +440,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
                             token(0),
                             KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
                             KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
-                            KApply('PtrEmulation', (metadata if metadata is not None else KApply('noMetadata', ()),)),
+                            metadata if metadata is not None else no_metadata,
                         ),
                     ),
                     pointee_constraints,
@@ -479,7 +501,7 @@ class SimpleRes(NamedTuple):
 
 class ArrayRes(NamedTuple):
     value: TypedValue
-    metadata: Metadata
+    metadata: MetadataSize
 
 
 class PointerRes(NamedTuple):