Skip to content

chore: update feature/p-token branch with master changes #774

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Oct 27, 2025
Merged

chore: update feature/p-token branch with master changes #774

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4fb9a32
Initial Ptr Offset semantics `binOpOffset` (#746)
dkcumming Oct 24, 2025
c8d9260
feat(decode): runtime support for structures (#769)
Stevengre Oct 27, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions kmir/src/kmir/decoding.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
36 changes: 29 additions & 7 deletions kmir/src/kmir/kast.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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__)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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:
Expand All @@ -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):
Expand All @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -479,7 +501,7 @@ class SimpleRes(NamedTuple):

class ArrayRes(NamedTuple):
value: TypedValue
metadata: Metadata
metadata: MetadataSize


class PointerRes(NamedTuple):
Expand Down
Loading