Skip to content

Updates from master #865

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
jberthold merged 4 commits into from
Nov 24, 2025
Merged

Updates from master #865

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3363f4e
Solana 109: implement `sizeof`, refactor `alignOf` (#859)
jberthold Nov 21, 2025
d124b36
Union Value Sort (#861)
dkcumming Nov 21, 2025
3d763c0
Union fields and layout plumbing (#862)
dkcumming Nov 21, 2025
b4182cd
More byte simplification (#864)
jberthold Nov 24, 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
7 changes: 6 additions & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,7 @@ update-exec-smir:

# Update checked-in smir.json files (using stable-mir-json dependency and jq)
# file paths for spans in the the updated smir are truncated to known infixes
# Compiles run-smir-random files as libraries, others as binaries
.PHONY: update-smir-json
update-smir-json: TARGETS = $(shell git ls-files | grep -e ".*\.smir\.json$$" | grep -v -e pinocchio)
update-smir-json: SMIR = cargo -q -Z unstable-options -C deps/stable-mir-json run --
Expand All @@ -140,7 +141,11 @@ update-smir-json: stable-mir-json
dir=$$(realpath $$(dirname $$file)); \
rust=$$dir/$$(basename $${file%.smir.json}.rs); \
[ -f "$$rust" ] || (echo "Source file $$rust missing."; exit 1); \
${SMIR} -Zno-codegen --out-dir $$dir $$rust; \
if echo "$$file" | grep -q "run-smir-random"; then \
${SMIR} --crate-type=lib --out-dir $$dir $$rust; \
else \
${SMIR} -Zno-codegen --out-dir $$dir $$rust; \
fi; \
jq '.spans[].[1].[0] |= sub("/.*lib/rustlib"; "rustlib") | .spans[].[1].[0] |= sub("/.*/integration/data"; "data")' $$file > $$file.tmp; \
mv $$file.tmp $$file; \
done
Expand Down
16 changes: 15 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/kmir.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,11 +97,25 @@ will effectively be no-ops at this level).
```k

// all memory accesses relegated to another module (to be added)
rule [execStmt]: <k> #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN))
rule [execStmt]: <k> #execStmt(statement(statementKindAssign(place(local(I), _PROJ) #as PLACE, RVAL), _SPAN))
=>
#setLocalValue(PLACE, RVAL)
...
</k>
<locals> LOCALS </locals>
requires 0 <=Int I andBool I <Int size(LOCALS)
andBool notBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
[preserves-definedness]

rule [execStmt.union]: <k> #execStmt(statement(statementKindAssign(place(local(I), _PROJ) #as PLACE, RVAL), _SPAN))
=>
#setLocalValue(PLACE, #evalUnion(RVAL))
...
</k>
<locals> LOCALS </locals>
requires 0 <=Int I andBool I <Int size(LOCALS)
andBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
[preserves-definedness]

// RVAL evaluation is implemented in rt/data.md

Expand Down
23 changes: 21 additions & 2 deletions kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ This file contains basic lemmas required for symbolic execution of MIR programs

Lemmas are simpliciations of symbolic function application that aims to confirm conditions for rewrite rules to avoid spurious branching on symbolic program parts.

Some of the lemmas relate to the control flow implementation in `kmir.md` and will be needed in various proofs (for instance the simplification of list size for partially-symbolic lists of locals or stack frames).
Some of the lemmas relate to the control flow implementation in `kmir.md` and will be needed in various proofs (for instance the simplification of list size for partially-symbolic lists of locals or stack frames).
Others are related to helper functions used for integer arithmetic.

```k
Expand All @@ -20,7 +20,7 @@ module KMIR-LEMMAS
```
## Simplifications for lists to avoid spurious branching on error cases in control flow

Rewrite rules that look up locals or stack frames require that an index into the respective `List`s in the configuration be within the bounds of the locals list/stack. Therefore, the `size` function on lists needs to be computed. The following simplifications allow for locals and stacks to have concrete values in the beginning but a symbolic rest (of unknown size).
Rewrite rules that look up locals or stack frames require that an index into the respective `List`s in the configuration be within the bounds of the locals list/stack. Therefore, the `size` function on lists needs to be computed. The following simplifications allow for locals and stacks to have concrete values in the beginning but a symbolic rest (of unknown size).
The lists used in the semantics are cons-lists, so only rules with a head element match are required.

```k
Expand Down Expand Up @@ -208,6 +208,25 @@ This avoids building up large expressions related to overflow checks and vacuous
[simplification, preserves-definedness, symbolic]
```

Another more general simplification relates a `NUMBER` and the bytes from its representation.
If the number is initially masked at 64 bits (`&Int bitmask64`), it is guaranteed to be positive
and therefore the masked value equals its bytes taken individually and multiplied.
Terms like this have been observed as branching conditions in a proof that heavily uses `[u8;8] <--> u64` conversions.
The simplification eliminates the vacuous branches instantly.

```k
rule ((NUMBER &Int bitmask64) &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8))))))))
&Int bitmask64
=> NUMBER &Int bitmask64
[simplification, preserves-definedness, symbolic(NUMBER)]
```

For the case where the (symbolic) byte values are first converted to a number, the round-trip simplification requires different matching.
First, the bit-masking with `&Int 255` eliminates `Bytes2Int(Int2Bytes(1, ..) +Bytes ..)` enclosing a byte-valued variable:
Expand Down
65 changes: 61 additions & 4 deletions kmir/src/kmir/kdist/mir-semantics/rt/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,6 +312,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr

// retains information about the value that was deconstructed by a projection
syntax Context ::= CtxField( VariantIdx, List, Int , Ty )
| CtxFieldUnion( FieldIdx, Value, Ty )
| CtxIndex( List , Int ) // array index constant or has been read before
| CtxSubslice( List , Int , Int ) // start and end always counted from beginning
| CtxPointerOffset( List, Int, Int ) // pointer offset for accessing elements with an offset (Offset, Origin Length)
Expand All @@ -329,6 +330,10 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
=> #buildUpdate(Aggregate(IDX, ARGS[I <- VAL]), CTXS)
[preserves-definedness] // valid list indexing checked upon context construction

rule #buildUpdate(VAL, CtxFieldUnion(FIELD_IDX, _ARG, _TY) CTXS)
=> #buildUpdate(Union(FIELD_IDX, VAL), CTXS)
[preserves-definedness]

rule #buildUpdate(VAL, CtxIndex(ELEMS, I) CTXS)
=> #buildUpdate(Range(ELEMS[I <- VAL]), CTXS)
[preserves-definedness] // valid list indexing checked upon context construction
Expand Down Expand Up @@ -400,7 +405,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
rule originSize(dynamicSize(SIZE)) => SIZE
```

#### Aggregates
#### Aggregates (not Union)

A `Field` access projection operates on `struct`s and tuples, which are represented as `Aggregate` values.
The field is numbered from zero (in source order), and the field type is provided (not checked here).
Expand Down Expand Up @@ -445,6 +450,28 @@ This is done without consideration of the validity of the Downcast[^downcast].
</k>
```

#### Unions
```k
// Case: Union is in same state as field projection
rule <k> #traverseProjection(
DEST,
Union(FIELD_IDX, ARG),
projectionElemField(FIELD_IDX, TY) PROJS,
CTXTS
)
=> #traverseProjection(
DEST,
ARG,
PROJS,
CtxFieldUnion(FIELD_IDX, ARG, TY) CTXTS
)
...
</k>
[preserves-definedness]

// TODO: Case: Union is in different state as field projection
```

#### Ranges

An `Index` projection operates on an array or slice (`Range`) value, to access an element of the array.
Expand Down Expand Up @@ -934,6 +961,7 @@ Literal arrays are also built using this RValue.

// #mkAggregate produces an aggregate TypedLocal value of given kind from a preceeding list of values
syntax Value ::= #mkAggregate ( AggregateKind )
| #mkUnion ( FieldIdx )

rule <k> ARGS:List ~> #mkAggregate(aggregateKindAdt(_ADTDEF, VARIDX, _, _, _))
=>
Expand Down Expand Up @@ -977,6 +1005,26 @@ Literal arrays are also built using this RValue.
</k>
```

While Unions are Aggregate in the MIR, we distinguish between them because the semantics
are different. For example, field accesses to not access different data, but interpret
that data as a different type.
```k
syntax Rvalue ::= #evalUnion ( Rvalue )

rule <k> #evalUnion(rvalueAggregate(aggregateKindAdt( _, _, _, _, someFieldIdx ( FIELD )), ARGS))
=>
#readOperands(ARGS) ~> #mkUnion(FIELD)
...
</k>

rule <k> ListItem(ARG) .List ~> #mkUnion(FIELD)
=>
Union(FIELD, ARG)
...
</k>

```

The `AggregateKind::RawPtr`, somewhat as a special case of a `struct` aggregate, constructs a raw pointer
from a given data pointer and metadata[^rawPtrAgg]. In case of a _thin_ pointer, the metadata is a unit value,
for _fat_ pointers it is a `usize` value indicating the data length.
Expand Down Expand Up @@ -1063,6 +1111,7 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
rule #projectionsFor( CtxSubslice(_, I, J) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(I, J, false) PROJS)
// rule #projectionsFor(CtxPointerOffset(OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(OFFSET, ORIGIN_LENGTH, false) PROJS)
rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS)
rule #projectionsFor(CtxFieldUnion(F_IDX, _, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(F_IDX, TY) PROJS)

// Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule.
rule <k> rvalueRef(REGION, KIND, place(local(I), PROJS))
Expand Down Expand Up @@ -2075,12 +2124,18 @@ Since our arithmetic operations signal undefined behaviour on overflow independe

#### "Nullary" operations reifying type information

`nullOpSizeOf`
`nullOpAlignOf`
`nullOpOffsetOf(VariantAndFieldIndices)`
Operation `nullOpSizeOf` returns the size in bytes of a data structure or primitive type, as a `usize`.
Operation `nullOpAlignOf` returns the required alignment of a data structure or primitive type, as a `usize`.
This information is read from the layout in the `TypeInfo` if available, or a fixed constant for primitive types.

```k
// FIXME: 64 is hardcoded since usize not supported
rule <k> rvalueNullaryOp(nullOpSizeOf, TY)
=>
Integer(#sizeOf(lookupTy(TY)), 64, false)
...
</k>
requires lookupTy(TY) =/=K typeInfoVoidType
rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
=>
Integer(#alignOf(lookupTy(TY)), 64, false)
Expand All @@ -2089,6 +2144,8 @@ rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
requires lookupTy(TY) =/=K typeInfoVoidType
```

`nullOpOffsetOf(VariantAndFieldIndices)`

#### Other operations

The unary operation `unOpPtrMetadata`, when given a reference or pointer to a slice, will return the reference or pointer metadata.
Expand Down
25 changes: 0 additions & 25 deletions kmir/src/kmir/kdist/mir-semantics/rt/numbers.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,31 +147,6 @@ This truncation function is instrumental in the implementation of Integer arithm
[preserves-definedness]
```

## Alignment of Primitives

```k
// FIXME: Alignment is platform specific
syntax Int ::= #alignOf( TypeInfo ) [function]
rule #alignOf( typeInfoPrimitiveType(primTypeBool) ) => 1
rule #alignOf( typeInfoPrimitiveType(primTypeChar) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyIsize)) ) => 8 // FIXME: Hard coded since usize not implemented
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI8)) ) => 1
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI16)) ) => 2
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI32)) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI64)) ) => 8
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI128)) ) => 16
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyUsize)) ) => 8 // FIXME: Hard coded since usize not implemented
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU8)) ) => 1
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU16)) ) => 2
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU32)) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU64)) ) => 8
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU128)) ) => 16
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF16)) ) => 2
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF32)) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF64)) ) => 8
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF128)) ) => 16
```

```k
endmodule
```
75 changes: 75 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,15 @@ Pointers to structs with a single zero-offset field are compatible with pointers
rule #layoutOffsets(_) => .MachineSizes [owise]
```

Helper function to identify an `union` type, this is needed so `#setLocalValue`
will not create an `Aggregate` instead of a `Union` `Value`.
```k
syntax Bool ::= #isUnionType ( TypeInfo ) [function, total]
// --------------------------------------------------------
rule #isUnionType(typeInfoUnionType(_NAME, _ADTDEF, _FIELDS, _LAYOUT) ) => true
rule #isUnionType(_) => false [owise]
```

## Determining types of places with projection

A helper function `getTyOf` traverses type metadata (using the type metadata map `Ty -> TypeInfo`) along the applied projections to determine the `Ty` of the projected place.
Expand Down Expand Up @@ -203,6 +212,72 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does
rule #zeroSizedType(_) => false [owise]
```

## Alignment and Size of Types as per `TypeInfo`

The `alignOf` and `sizeOf` nullary operations return the alignment / size in bytes as a `usize`.
This information is either hard-wired for primitive types (numbers, first and foremost), or read from the layout in `TypeInfo`.

```k
syntax Int ::= #sizeOf ( TypeInfo ) [function, total]
| #alignOf ( TypeInfo ) [function, total]

// primitive int types: use bit width (both for size and alignment)
rule #sizeOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
rule #alignOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
rule #alignOf(typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
rule #alignOf(typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
// bool and char
rule #sizeOf(typeInfoPrimitiveType(primTypeBool)) => 1
rule #alignOf(typeInfoPrimitiveType(primTypeBool)) => 1
rule #sizeOf(typeInfoPrimitiveType(primTypeChar)) => 4
rule #alignOf(typeInfoPrimitiveType(primTypeChar)) => 4
// The str primitive has alignment of a Char but size 0 (indicating dynamic size)
rule #sizeOf(typeInfoPrimitiveType(primTypeStr)) => 0
rule #alignOf(typeInfoPrimitiveType(primTypeStr)) => 4
// enums, structs , and tuples provide the values from their layout information
rule #sizeOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoEnumType(_, _, _, _, noLayoutShape)) => 0
rule #alignOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
rule #alignOf(typeInfoEnumType(_, _, _, _, noLayoutShape)) => 1
// struct
rule #sizeOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoStructType(_, _, _, noLayoutShape)) => 0
rule #alignOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
rule #alignOf(typeInfoStructType(_, _, _, noLayoutShape)) => 1
// tuple
rule #sizeOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoTupleType(_, noLayoutShape)) => 0
rule #alignOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
rule #alignOf(typeInfoTupleType(_, noLayoutShape)) => 1
// union
rule #sizeOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize( BITS ))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
rule #sizeOf(typeInfoUnionType(_, _, _, noLayoutShape)) => 0
rule #alignOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
rule #alignOf(typeInfoUnionType(_, _, _, noLayoutShape)) => 1
// arrays with known length have the alignment of the element type, and a size multiplying element count and element size
rule #sizeOf(typeInfoArrayType(ELEM_TY, someTyConst(tyConst(KIND, _)))) => #sizeOf(lookupTy(ELEM_TY)) *Int readTyConstInt(KIND)
rule #sizeOf(typeInfoArrayType( _ , noTyConst )) => 0
rule #alignOf(typeInfoArrayType(ELEM_TY, _)) => #alignOf(lookupTy(ELEM_TY))
// thin ptr and ref types have the size of `usize` and twice that for fat pointers/refs. Alignment is that of `usize`
rule #sizeOf(typeInfoPtrType(POINTEE_TY))
=> #sizeOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
*Int (#if #metadataSize(POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi)
rule #sizeOf(typeInfoRefType(POINTEE_TY))
=> #sizeOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
*Int (#if #metadataSize(POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi)
rule #alignOf(typeInfoPtrType(_)) => #alignOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
rule #alignOf(typeInfoRefType(_)) => #alignOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
// other types (fun and void types) have size and alignment 0
rule #sizeOf(_) => 0 [owise]
rule #alignOf(_) => 0 [owise]
```

```k
endmodule
```
Loading