Implement decoding for references with a single provenance entry (#728)

Author: tothtamas28

kmir/src/kmir/alloc.py

@@ -71,21 +71,21 @@ def from_dict(dct: dict[str, Any]) -> Allocation:
 
 @dataclass
 class ProvenanceMap:
-    ptrs: list[ProvenanceItem]
+    ptrs: list[ProvenanceEntry]
 
     @staticmethod
     def from_dict(dct: dict[str, Any]) -> ProvenanceMap:
         return ProvenanceMap(
             ptrs=[
-                ProvenanceItem(
-                    size=int(size),
+                ProvenanceEntry(
+                    offset=int(size),
                     prov=AllocId(prov),
                 )
                 for size, prov in dct['ptrs']
             ],
         )
 
 
-class ProvenanceItem(NamedTuple):
-    size: int
+class ProvenanceEntry(NamedTuple):
+    offset: int
     prov: AllocId

kmir/src/kmir/decoding.py

@@ -1,23 +1,33 @@
 from __future__ import annotations
 
 from dataclasses import dataclass
-from typing import TYPE_CHECKING, NamedTuple
+from typing import TYPE_CHECKING
 
 from pyk.kast.inner import KApply
 from pyk.kast.prelude.bytes import bytesToken
 from pyk.kast.prelude.kint import intToken
 
-from .alloc import Allocation, AllocInfo, Memory, ProvenanceMap
-from .ty import ArrayT, Bool, EnumT, Int, IntTy, Uint
-from .value import AggregateValue, BoolValue, IntValue, RangeValue, Value
+from .alloc import Allocation, AllocInfo, Memory, ProvenanceEntry, ProvenanceMap
+from .ty import ArrayT, Bool, EnumT, Int, IntTy, PtrT, RefT, Uint
+from .value import (
+    NO_METADATA,
+    AggregateValue,
+    AllocRefValue,
+    BoolValue,
+    DynamicSize,
+    IntValue,
+    RangeValue,
+    StaticSize,
+    Value,
+)
 
 if TYPE_CHECKING:
     from collections.abc import Mapping
 
     from pyk.kast import KInner
 
-    from .alloc import AllocId
     from .ty import Ty, TypeMetadata, UintTy
+    from .value import Metadata
 
 
 @dataclass
@@ -47,11 +57,6 @@ def to_kast(self) -> KInner:
         )
 
 
-class ProvenanceMapEntry(NamedTuple):
-    offset: int
-    alloc_id: AllocId
-
-
 def decode_alloc_or_unable(alloc_info: AllocInfo, types: Mapping[Ty, TypeMetadata]) -> Value:
     match alloc_info:
         case AllocInfo(
@@ -66,16 +71,52 @@ def decode_alloc_or_unable(alloc_info: AllocInfo, types: Mapping[Ty, TypeMetadat
             ),
         ):
             data = bytes(n or 0 for n in bytez)
+            type_info = types[ty]
+
+            match ptrs:
+                case []:
+                    return decode_value_or_unable(data=data, type_info=type_info, types=types)
+
+                case [ProvenanceEntry(0, alloc_id)]:
+                    if (pointee_ty := _pointee_ty(type_info)) is not None:  # ensures this is a reference type
+                        pointee_type_info = types[pointee_ty]
+                        metadata = _metadata(pointee_type_info)
 
-            if not ptrs:  # TODO generalize to lists with at most one entry
-                type_info = types[ty]
-                return decode_value_or_unable(data=data, type_info=type_info, types=types)
+                        if len(data) == 8:
+                            # single slim pointer (assumes usize == u64)
+                            return AllocRefValue(alloc_id=alloc_id, metadata=metadata)
+
+                        if len(data) == 16 and metadata == DynamicSize(1):
+                            # sufficient data to decode dynamic size (assumes usize == u64)
+                            # expect fat pointer
+                            return AllocRefValue(
+                                alloc_id=alloc_id,
+                                metadata=DynamicSize(int.from_bytes(data[8:16], byteorder='little', signed=False)),
+                            )
 
             return UnableToDecodeAlloc(data=data, ty=ty)
         case _:
             raise AssertionError('Unhandled case')
 
 
+def _pointee_ty(type_info: TypeMetadata) -> Ty | None:
+    match type_info:
+        case PtrT(ty) | RefT(ty):
+            return ty
+        case _:
+            return None
+
+
+def _metadata(type_info: TypeMetadata) -> Metadata:
+    match type_info:
+        case ArrayT(length=None):
+            return DynamicSize(1)  # 1 is a placeholder, the actual size is inferred from the slice data
+        case ArrayT(length=int() as length):
+            return StaticSize(length)
+        case _:
+            return NO_METADATA
+
+
 def decode_value_or_unable(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMetadata]) -> Value:
     try:
         return decode_value(data=data, type_info=type_info, types=types)

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

@@ -43,6 +43,7 @@ The special `Moved` value represents values that have been used and should not b
                    // pointer to a local TypedValue (on the stack)
                    // first 3 fields are the same as in Reference, plus pointee metadata
                  | AllocRef ( AllocId , ProjectionElems , Metadata )
+                                                          [symbol(Value::AllocRef)]
                    // reference to static allocation, by AllocId, possibly projected, carrying metadata if applicable
                  | "Moved"
                    // The value has been used and is gone now

kmir/src/kmir/value.py

@@ -5,12 +5,18 @@
 from typing import TYPE_CHECKING
 
 from pyk.kast.inner import KApply
+from pyk.kast.prelude.collections import list_of
+from pyk.kast.prelude.kbool import boolToken
+from pyk.kast.prelude.kint import intToken
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
+    from typing import Final
 
     from pyk.kast import KInner
 
+    from .alloc import AllocId
+
 
 class Value(ABC):
     @abstractmethod
@@ -22,8 +28,6 @@ class BoolValue(Value):
     value: bool
 
     def to_kast(self) -> KInner:
-        from pyk.kast.prelude.kbool import boolToken
-
         return KApply('Value::BoolVal', boolToken(self.value))
 
 
@@ -34,9 +38,6 @@ class IntValue(Value):
     signed: bool
 
     def to_kast(self) -> KInner:
-        from pyk.kast.prelude.kbool import boolToken
-        from pyk.kast.prelude.kint import intToken
-
         return KApply(
             'Value::Integer',
             intToken(self.value),
@@ -53,8 +54,6 @@ def __init__(self, elems: Iterable[Value]):
         self.elems = tuple(elems)
 
     def to_kast(self) -> KInner:
-        from pyk.kast.prelude.collections import list_of
-
         return KApply('Value::Range', list_of(elem.to_kast() for elem in self.elems))
 
 
@@ -68,11 +67,53 @@ def __init__(self, variant_idx: int, fields: Iterable[Value]):
         self.fields = tuple(fields)
 
     def to_kast(self) -> KInner:
-        from pyk.kast.prelude.collections import list_of
-        from pyk.kast.prelude.kint import intToken
-
         return KApply(
             'Value::Aggregate',
             KApply('variantIdx', intToken(self.variant_idx)),
             list_of(field.to_kast() for field in self.fields),
         )
+
+
+@dataclass
+class AllocRefValue(Value):
+    alloc_id: AllocId
+    # projection_elems: tuple[ProjectionElem, ...]
+    metadata: Metadata
+
+    def to_kast(self) -> KInner:
+        return KApply(
+            'Value::AllocRef',
+            KApply('allocId', intToken(self.alloc_id)),
+            KApply('ProjectionElems::empty'),  # TODO
+            self.metadata.to_kast(),
+        )
+
+
+class Metadata(ABC):
+    @abstractmethod
+    def to_kast(self) -> KInner: ...
+
+
+@dataclass
+class NoMetadata(Metadata):
+    def to_kast(self) -> KInner:
+        return KApply('noMetadata')
+
+
+NO_METADATA: Final = NoMetadata()
+
+
+@dataclass
+class StaticSize(Metadata):
+    size: int
+
+    def to_kast(self) -> KInner:
+        return KApply('staticSize', intToken(self.size))
+
+
+@dataclass
+class DynamicSize(Metadata):
+    size: int
+
+    def to_kast(self) -> KInner:
+        return KApply('dynamicSize', intToken(self.size))