Skip to content

Commit 6f3c37d

Browse files
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 31045a9 + 484bb61 commit 6f3c37d

32 files changed

+422
-110
lines changed

kmir/src/kmir/kast.py

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
from pyk.kast.prelude.ml import mlEqualsTrue
99
from pyk.kast.prelude.utils import token
1010

11-
from .smir import ArrayT, Bool, EnumT, Int, RefT, StructT, TupleT, Uint, UnionT
11+
from .smir import ArrayT, Bool, EnumT, Int, PtrT, RefT, StructT, TupleT, Uint, UnionT
1212

1313
if TYPE_CHECKING:
1414
from collections.abc import Iterable
@@ -219,5 +219,21 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
219219
),
220220
pointee_constraints,
221221
)
222+
case PtrT(pointee_ty):
223+
pointee_var, pointee_constraints = self._symbolic_value(pointee_ty, mutable)
224+
ref = self.ref_offset
225+
self.ref_offset += 1
226+
self.pointees.append(_typed_value(pointee_var, pointee_ty, mutable))
227+
return (
228+
KApply(
229+
'Value::PtrLocal',
230+
(
231+
token(0),
232+
KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))),
233+
KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()),
234+
),
235+
),
236+
pointee_constraints,
237+
)
222238
case _:
223239
return self._fresh_var('ARG'), []

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ Another type-related `Map` is required to associate an `AdtDef` ID with its corr
8484
// --------------------------------------------------------------
8585
rule #mkAdtMap(ACC, .TypeMappings) => ACC
8686
87-
rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoStructType(_, ADTDEF)) MORE:TypeMappings)
87+
rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoStructType(_, ADTDEF, _)) MORE:TypeMappings)
8888
=>
8989
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
9090
requires notBool TY in_keys(ACC)
@@ -94,6 +94,10 @@ Another type-related `Map` is required to associate an `AdtDef` ID with its corr
9494
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
9595
requires notBool TY in_keys(ACC)
9696
97+
rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoUnionType(_, ADTDEF)) MORE:TypeMappings)
98+
=>
99+
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
100+
requires notBool TY in_keys(ACC)
97101
rule #mkAdtMap(ACC, TypeMapping(_, _) MORE:TypeMappings)
98102
=>
99103
#mkAdtMap(ACC, MORE)

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

Lines changed: 166 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,9 @@ This module addresses all aspects of handling "values" i.e., data, at runtime du
44

55

66
```k
7-
requires "../ty.md"
87
requires "../body.md"
8+
requires "../ty.md"
9+
requires "./types.md"
910
requires "./value.md"
1011
requires "./numbers.md"
1112
@@ -23,6 +24,7 @@ module RT-DATA
2324
2425
imports RT-VALUE-SYNTAX
2526
imports RT-NUMBERS
27+
imports RT-TYPES
2628
imports KMIR-CONFIGURATION
2729
```
2830

@@ -215,7 +217,7 @@ A `Deref` projection in the projections list changes the target of the write ope
215217
These helpers mark down, as we traverse the projection, what `Place` we are currently looking up in the traversal.
216218
`#buildUpdate` helps to reconstruct the new value stored at that `Place` if we need to do a write (using the `Context` built during traversal).
217219

218-
```k
220+
```k
219221
// stores the target of the write operation, which may change when references are dereferenced.
220222
syntax WriteTo ::= toLocal ( Int )
221223
| toStack ( Int , Local )
@@ -271,6 +273,8 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
271273
272274
rule #adjustRef(typedValue(Reference(HEIGHT, PLACE, REFMUT), TY, MUT), OFFSET)
273275
=> typedValue(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT)
276+
rule #adjustRef(typedValue(PtrLocal(HEIGHT, PLACE, REFMUT), TY, MUT), OFFSET)
277+
=> typedValue(PtrLocal(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT)
274278
rule #adjustRef(TL, _) => TL [owise]
275279
276280
rule #incrementRef(TL) => #adjustRef(TL, 1)
@@ -438,6 +442,45 @@ In the simplest case, the reference refers to a local in the same stack frame (h
438442
requires OFFSET ==Int 0
439443
andBool 0 <=Int I andBool I <Int size(LOCALS)
440444
[preserves-definedness]
445+
446+
447+
rule <k> #traverseProjection(
448+
_DEST,
449+
typedValue(PtrLocal(OFFSET, place(LOCAL, PLACEPROJ), _MUT), _, _),
450+
projectionElemDeref PROJS,
451+
_CTXTS
452+
)
453+
=> #traverseProjection(
454+
toStack(OFFSET, LOCAL),
455+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET),
456+
appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest
457+
.Contexts // previous contexts obsolete
458+
)
459+
...
460+
</k>
461+
<stack> STACK </stack>
462+
requires 0 <Int OFFSET andBool OFFSET <=Int size(STACK)
463+
andBool isStackFrame(STACK[OFFSET -Int 1])
464+
[preserves-definedness]
465+
466+
rule <k> #traverseProjection(
467+
_DEST,
468+
typedValue(PtrLocal(OFFSET, place(local(I), PLACEPROJ), _MUT), _, _),
469+
projectionElemDeref PROJS,
470+
_CTXTS
471+
)
472+
=> #traverseProjection(
473+
toLocal(I),
474+
{LOCALS[I]}:>TypedLocal,
475+
appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest
476+
.Contexts // previous contexts obsolete
477+
)
478+
...
479+
</k>
480+
<locals> LOCALS </locals>
481+
requires OFFSET ==Int 0
482+
andBool 0 <=Int I andBool I <Int size(LOCALS)
483+
[preserves-definedness]
441484
```
442485

443486
## Evaluation of R-Values (`Rvalue` sort)
@@ -533,6 +576,8 @@ For tuples and `struct`s, this index is always 0.
533576
Tuples, `struct`s, and `enum`s are built as `Aggregate` values with a list of argument values.
534577
For `enums`, the `VariantIdx` is set, and for `struct`s and `enum`s, the type ID (`Ty`) is retrieved from a special mapping of `AdtDef` to `Ty`.
535578

579+
Literal arrays are also built using this RValue.
580+
536581
```k
537582
rule <k> rvalueAggregate(KIND, ARGS) => #readOperands(ARGS) ~> #mkAggregate(KIND) ... </k>
538583
@@ -547,12 +592,18 @@ For `enums`, the `VariantIdx` is set, and for `struct`s and `enum`s, the type ID
547592
<adt-to-ty> ADTMAPPING </adt-to-ty>
548593
requires isTy(ADTMAPPING[ADTDEF])
549594
550-
rule <k> ARGS:List ~> #mkAggregate(_OTHERKIND)
595+
rule <k> ARGS:List ~> #mkAggregate(aggregateKindArray(_TY))
596+
=>
597+
typedValue(Range(ARGS), TyUnknown, mutabilityNot)
598+
...
599+
</k>
600+
601+
602+
rule <k> ARGS:List ~> #mkAggregate(aggregateKindTuple)
551603
=>
552604
typedValue(Aggregate(variantIdx(0), ARGS), TyUnknown, mutabilityNot)
553605
...
554606
</k>
555-
[owise]
556607
557608
558609
// #readOperands accumulates a list of `TypedLocal` values from operands
@@ -640,23 +691,71 @@ A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`,
640691

641692
```k
642693
rule <k> rvalueCopyForDeref(PLACE) => rvalueUse(operandCopy(PLACE)) ... </k>
694+
```
695+
696+
The `RValue::AddressOf` operation is very similar to creating a reference, since it also
697+
refers to a given _place_. However, the raw pointer obtained by `AddressOf` can be subject
698+
to casts and pointer arithmetic using `BinOp::Offset`.
643699

644-
// AddressOf: not implemented yet
700+
```k
701+
rule <k> rvalueAddressOf(MUT, PLACE)
702+
=>
703+
typedValue(PtrLocal(0, PLACE, MUT), TyUnknown, MUT)
704+
// we should use #alignOf to emulate the address
705+
...
706+
</k>
707+
```
708+
709+
In practice, the `AddressOf` can often be found applied to references that get dereferenced first,
710+
turning a borrowed value into a raw pointer. To shorten out chains of Deref and AddressOf/Reference,
711+
a special rule for this case is applied with higher priority.
712+
713+
```k
714+
rule <k> rvalueAddressOf(MUT, place(local(I), projectionElemDeref .ProjectionElems))
715+
=>
716+
typedValue(refToPtrLocal({LOCALS[I]}:>TypedValue), TyUnknown, MUT)
717+
// we should use #alignOf to emulate the address
718+
...
719+
</k>
720+
<locals> LOCALS </locals>
721+
requires 0 <=Int I
722+
andBool I <Int size(LOCALS)
723+
andBool isTypedValue(LOCALS[I])
724+
andBool isRef({LOCALS[I]}:>TypedValue)
725+
[priority(40), preserves-definedness] // valid indexing checked, toPtrLocal can convert the reference
726+
727+
syntax Bool ::= isRef ( TypedValue ) [function, total]
728+
// -----------------------------------------------------
729+
rule isRef(typedValue(Reference(_, _, _), _, _)) => true
730+
rule isRef( _OTHER ) => false [owise]
731+
732+
syntax Value ::= refToPtrLocal ( TypedValue ) [function]
733+
734+
rule refToPtrLocal(typedValue(Reference(OFFSET, PLACE, MUT), _, _)) => PtrLocal(OFFSET, PLACE, MUT)
645735
```
646736

647737
## Type casts
648738

649739
Type casts between a number of different types exist in MIR.
650-
We implement a type cast from a `TypedLocal` to another when it is followed by a `#cast` item, rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`.
651740

652741
```k
653742
syntax Evaluation ::= #cast( Evaluation, CastKind, Ty ) [strict(1)]
654743
```
655744

656-
### Integer Type Casts
745+
### Number Type Casts
746+
747+
The simplest case of a cast is conversion from one number type to another:
657748

658-
Casts between signed and unsigned integral numbers of different width exist, with a truncating semantics.
659-
These casts can only operate on the `Integer` variant of the `Value` type, adjusting bit width, signedness, and possibly truncating or 2s-complementing the value.
749+
| CastKind |
750+
|--------------|
751+
| IntToInt |
752+
| FloatToInt |
753+
| FloatToFloat |
754+
| IntToFloat |
755+
756+
`IntToInt` casts between signed and unsigned integral numbers of different width exist, with a
757+
truncating semantics. These casts can only operate on the `Integer` variant of the `Value` type, adjusting
758+
bit width, signedness, and possibly truncating or 2s-complementing the value.
660759

661760
```k
662761
// int casts
@@ -670,6 +769,63 @@ These casts can only operate on the `Integer` variant of the `Value` type, adjus
670769
[preserves-definedness] // ensures #numTypeOf is defined
671770
```
672771

772+
Casts involving `Float` values are currently not implemented.
773+
774+
### Casts between pointer types
775+
776+
777+
| CastKind | Description |
778+
|----------|------------------------------------------------------------|
779+
| PtrToPtr | Convert between references when representations compatible |
780+
781+
Pointers can be converted from one type to another (`PtrToPtr`) when the representations are compatible.
782+
The compatibility of types (defined in `rt/types.md`) considers their representations (recursively) in
783+
the `Value` sort.
784+
Conversion is especially possible for the case of _Slices_ (of dynamic length) and _Arrays_ (of static length),
785+
which have the same representation `Value::Range`.
786+
787+
```k
788+
rule <k> #cast(typedValue(VALUE, TY1, MUT), castKindPtrToPtr, TY2)
789+
=>
790+
typedValue(VALUE, TY2, MUT)
791+
...
792+
</k>
793+
<types> TYPEMAP </types>
794+
requires #typesCompatible({TYPEMAP[TY1]}:>TypeInfo, {TYPEMAP[TY2]}:>TypeInfo, TYPEMAP)
795+
```
796+
797+
`PointerCoercion` may achieve a simmilar effect, or deal with function and closure pointers, depending on the coercion type:
798+
799+
| CastKind | PointerCoercion | Description |
800+
|------------------------------------|--------------------------|----------------------- |
801+
| PointerCoercion(_, CoercionSource) | ArrayToPointer | from `*const [T; N]` to `*const T` |
802+
| | Unsize | drop size information |
803+
| | ReifyFnPointer | |
804+
| | UnsafeFnPointer | |
805+
| | ClosureFnPointer(Safety) | |
806+
| | DynStar | create a dyn* object |
807+
| | MutToConstPointer | make a mutable pointer immutable |
808+
809+
810+
```k
811+
// not checking whether types are actually compatible (trusting the compiler)
812+
rule <k> #cast(typedValue(VALUE, _TY, MUT), castKindPointerCoercion(pointerCoercionUnsize), TY)
813+
=>
814+
typedValue(VALUE, TY, MUT)
815+
...
816+
</k>
817+
```
818+
819+
### Other casts involving pointers
820+
821+
| CastKind | Description |
822+
|------------------------------|-------------|
823+
| PointerExposeProvenance | |
824+
| PointerWithExposedProvenance | |
825+
| FnPtrToPtr | |
826+
| Transmute | |
827+
828+
673829
## Decoding constants from their bytes representation to values
674830

675831
The `Value` sort above operates at a higher level than the bytes representation found in the MIR syntax for constant values.
@@ -699,7 +855,7 @@ This is currently only defined for `PrimitiveType`s (primitive types in MIR).
699855
[preserves-definedness]
700856
701857
// zero-sized struct types
702-
rule <k> #decodeConstant(constantKindZeroSized, TY, typeInfoStructType(_, _))
858+
rule <k> #decodeConstant(constantKindZeroSized, TY, typeInfoStructType(_, _, _))
703859
=> typedValue(Aggregate(variantIdx(0), .List), TY, mutabilityNot) ... </k>
704860
705861
// TODO Char type
Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
# Helpers for type metadata (`TypeInfo`)
2+
3+
```k
4+
requires "../ty.md"
5+
6+
module RT-TYPES
7+
imports BOOL
8+
imports MAP
9+
imports K-EQUAL
10+
11+
imports TYPES
12+
13+
```
14+
15+
Type metadata from Stable MIR JSON is present in a type lookup table `Ty -> TypeInfo` at runtime.
16+
17+
This module contains helper functions to operate on this type information.
18+
19+
## Compatibility of types (high-level representation)
20+
21+
When two types use the same representation for their values, these
22+
values, and pointers to them, can be converted from one type to the other.
23+
The `#typesCompatible` function determines this compatibility, and is by default `false`.
24+
25+
```k
26+
syntax Bool ::= #typesCompatible ( TypeInfo , TypeInfo , Map ) [function, total]
27+
28+
// by default, only identical types are compatible
29+
rule #typesCompatible ( T , T , _ ) => true [priority(60)]
30+
rule #typesCompatible ( _ , _ , _ ) => false [owise]
31+
```
32+
33+
Arrays and slices are compatible if their element type is (ignoring length)
34+
```k
35+
rule #typesCompatible ( typeInfoArrayType(TY1, _), typeInfoArrayType(TY2, _), TYPEMAP) => #typesCompatible({TYPEMAP[TY1]}:>TypeInfo, {TYPEMAP[TY2]}:>TypeInfo, TYPEMAP)
36+
requires isTypeInfo(TYPEMAP[TY1])
37+
andBool isTypeInfo(TYPEMAP[TY2])
38+
```
39+
40+
Pointers are compatible if their pointee types are
41+
```k
42+
rule #typesCompatible ( typeInfoPtrType(TY1) , typeInfoPtrType(TY2) , TYPEMAP) => true
43+
requires isTypeInfo(TYPEMAP[TY1])
44+
andBool isTypeInfo(TYPEMAP[TY2])
45+
andBool #typesCompatible({TYPEMAP[TY1]}:>TypeInfo, {TYPEMAP[TY2]}:>TypeInfo, TYPEMAP)
46+
[priority(59)]
47+
```
48+
49+
Pointers to arrays/slices are compatible with pointers to the element type
50+
```k
51+
rule #typesCompatible ( typeInfoPtrType(TY1) , typeInfoPtrType(TY2) , TYPEMAP) => true
52+
requires isTypeInfo(TYPEMAP[TY1])
53+
andBool #isArrayOf({TYPEMAP[TY1]}:>TypeInfo, TY2)
54+
55+
rule #typesCompatible ( typeInfoPtrType(TY1) , typeInfoPtrType(TY2) , TYPEMAP) => true
56+
requires isTypeInfo(TYPEMAP[TY2])
57+
andBool #isArrayOf({TYPEMAP[TY2]}:>TypeInfo, TY1)
58+
59+
syntax Bool ::= #isArrayOf ( TypeInfo , Ty ) [function, total]
60+
61+
rule #isArrayOf(typeInfoArrayType(TY, _), TY) => true
62+
rule #isArrayOf( _ , _ ) => false [owise]
63+
```
64+
65+
66+
67+
```k
68+
endmodule
69+
```

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,10 @@ High-level values can be
3434
// stack depth (initially 0), place, borrow kind
3535
| Range( List ) [symbol(Value::Range)]
3636
// homogenous values for array/slice
37-
// | Ptr( Address, MaybeValue )
38-
// address, metadata for ref/ptr
37+
| PtrLocal( Int , Place , Mutability ) [symbol(Value::PtrLocal)]
38+
// pointer to a local TypedValue (on the stack)
39+
// first 3 fields are the same as in Reference, plus emulating pointer arithmetics (future work)
40+
3941
```
4042

4143
## Local variables

0 commit comments

Comments
 (0)