Update bin op offset from master (#772)

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

Author: jberthold

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