Skip to content

Commit 2a8f615

Browse files
jbertholdjberthold
authored
Adjust reference and pointer offsets within aggregate types and arrays (#636)
Fixes a bug where references and pointers contained within container types would become invalid when passed between functions as arguments or read through other references. Also included: Renaming of `VoidType` to `typeInfoVoidType`
1 parent 84bea09 commit 2a8f615

25 files changed

+57
-37
lines changed

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,12 @@ If nothing is removed, the list remains the same. If all elements are removed, n
5151
rule #Ceil(range(L, A, B)) => #Ceil(L) #And #Ceil(A) #And #Ceil(B) #And {true #Equals A +Int B <=Int size(L)} [simplification]
5252
```
5353

54+
The `#mapOffset` function maps `#adjustRef` over a lists of `Value`s, leaving the list length unchanged.
55+
56+
```k
57+
rule size(#mapOffset(L, _)) => size(L) [simplification, preserves-definedness]
58+
```
59+
5460
## Simplifications for Int
5561

5662
These are trivial simplifications driven by syntactic equality, which should be present upstream.

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

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -315,16 +315,30 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
315315
andBool isTypedValue(LOCALS[I])
316316
[preserves-definedness] // valid list indexing checked
317317
318-
syntax Value ::= #incrementRef ( Value ) [function, total]
319-
| #decrementRef ( Value ) [function, total]
320-
| #adjustRef (Value, Int ) [function, total]
321-
318+
syntax Value ::= #adjustRef (Value, Int ) [function, total]
319+
// --------------------------------------------------------
322320
rule #adjustRef(Reference(HEIGHT, PLACE, REFMUT, META), OFFSET)
323321
=> Reference(HEIGHT +Int OFFSET, PLACE, REFMUT, META)
324322
rule #adjustRef(PtrLocal(HEIGHT, PLACE, REFMUT, EMULATION), OFFSET)
325323
=> PtrLocal(HEIGHT +Int OFFSET, PLACE, REFMUT, EMULATION)
324+
rule #adjustRef(Aggregate(IDX, ARGS), OFFSET)
325+
=> Aggregate(IDX, #mapOffset(ARGS, OFFSET))
326+
rule #adjustRef(Range(ELEMS), OFFSET)
327+
=> Range(#mapOffset(ELEMS, OFFSET))
326328
rule #adjustRef(TL, _) => TL [owise]
327329
330+
syntax List ::= #mapOffset ( List, Int ) [function, total]
331+
// -------------------------------------------------------
332+
rule #mapOffset(.List, _)
333+
=> .List
334+
rule #mapOffset(ListItem(ELEM:Value) REST, OFFSET)
335+
=> ListItem(#adjustRef(ELEM, OFFSET)) #mapOffset(REST, OFFSET)
336+
rule #mapOffset(OTHER, _)
337+
=> OTHER [owise] // should not happen
338+
339+
syntax Value ::= #incrementRef ( Value ) [function, total]
340+
| #decrementRef ( Value ) [function, total]
341+
// --------------------------------------------------------
328342
rule #incrementRef(TL) => #adjustRef(TL, 1)
329343
rule #decrementRef(TL) => #adjustRef(TL, -1)
330344
```

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -265,7 +265,7 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
265265
| typeInfoRefType(Ty) [symbol(TypeInfo::RefType) , group(mir-enum---pointee-type)]
266266
| typeInfoTupleType(Tys) [symbol(TypeInfo::TupleType) , group(mir-enum---types)]
267267
| typeInfoFunType(MIRString) [symbol(TypeInfo::FunType) , group(mir-enum)]
268-
| "VoidType" [symbol(TypeInfo::VoidType) , group(mir-enum)]
268+
| "typeInfoVoidType" [symbol(TypeInfo::VoidType) , group(mir-enum)]
269269
270270
271271
// discriminant information for enum types

‎kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@
8282
ty ( 18 ) |-> typeInfoRefType ( ty ( 15 ) )
8383
ty ( 21 ) |-> typeInfoPrimitiveType ( primTypeBool )
8484
ty ( 24 ) |-> typeInfoRefType ( ty ( 37 ) )
85-
ty ( 25 ) |-> VoidType
85+
ty ( 25 ) |-> typeInfoVoidType
8686
ty ( 26 ) |-> typeInfoTupleType ( ty ( 2 ) ty ( 21 ) .Tys )
8787
ty ( 28 ) |-> typeInfoTupleType ( ty ( 9 ) ty ( 21 ) .Tys )
8888
ty ( 30 ) |-> typeInfoPtrType ( ty ( 12 ) )

‎kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@
9797
ty ( 28 ) |-> typeInfoTupleType ( ty ( 2 ) ty ( 25 ) .Tys )
9898
ty ( 29 ) |-> typeInfoTupleType ( ty ( 26 ) ty ( 25 ) .Tys )
9999
ty ( 32 ) |-> typeInfoPtrType ( ty ( 9 ) )
100-
ty ( 33 ) |-> VoidType
100+
ty ( 33 ) |-> typeInfoVoidType
101101
</types>
102102
<adt-to-ty>
103103
adtDef ( 9 ) |-> ty ( 17 )

‎kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@
6868
ty ( 25 ) |-> typeInfoPrimitiveType ( primTypeBool )
6969
ty ( 26 ) |-> typeInfoTupleType ( ty ( 9 ) ty ( 25 ) .Tys )
7070
ty ( 28 ) |-> typeInfoPtrType ( ty ( 9 ) )
71-
ty ( 29 ) |-> VoidType
71+
ty ( 29 ) |-> typeInfoVoidType
7272
</types>
7373
<adt-to-ty>
7474
adtDef ( 9 ) |-> ty ( 17 )

‎kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@
7777
ty ( 28 ) |-> typeInfoRefType ( ty ( 33 ) )
7878
ty ( 29 ) |-> typeInfoArrayType ( ty ( 26 ) , someTyConst ( tyConst (... kind: tyConstKindValue ( ty ( 25 ) , allocation (... bytes: b"\x04\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , id: tyConstId ( 0 ) ) ) )
7979
ty ( 30 ) |-> typeInfoPrimitiveType ( primTypeBool )
80-
ty ( 31 ) |-> VoidType
80+
ty ( 31 ) |-> typeInfoVoidType
8181
ty ( 32 ) |-> typeInfoRefType ( ty ( 34 ) )
8282
ty ( 33 ) |-> typeInfoPrimitiveType ( primTypeStr )
8383
ty ( 34 ) |-> typeInfoStructType ( "std::panic::Location<'_>" , adtDef ( 8 ) , ty ( 28 ) ty ( 35 ) ty ( 35 ) .Tys )

‎kmir/src/tests/integration/data/exec-smir/arrays/array_write.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@
8787
ty ( 29 ) |-> typeInfoArrayType ( ty ( 26 ) , someTyConst ( tyConst (... kind: tyConstKindValue ( ty ( 25 ) , allocation (... bytes: b"\x04\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , id: tyConstId ( 0 ) ) ) )
8888
ty ( 30 ) |-> typeInfoPrimitiveType ( primTypeBool )
8989
ty ( 31 ) |-> typeInfoRefType ( ty ( 26 ) )
90-
ty ( 32 ) |-> VoidType
90+
ty ( 32 ) |-> typeInfoVoidType
9191
ty ( 34 ) |-> typeInfoPtrType ( ty ( 9 ) )
9292
ty ( 35 ) |-> typeInfoRefType ( ty ( 37 ) )
9393
ty ( 36 ) |-> typeInfoPrimitiveType ( primTypeStr )

‎kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@
7676
ty ( 28 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU32 ) )
7777
ty ( 29 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU64 ) )
7878
ty ( 31 ) |-> typeInfoPtrType ( ty ( 9 ) )
79-
ty ( 32 ) |-> VoidType
79+
ty ( 32 ) |-> typeInfoVoidType
8080
</types>
8181
<adt-to-ty>
8282
adtDef ( 13 ) |-> ty ( 10 )

‎kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@
6464
ty ( 26 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyUsize ) )
6565
ty ( 28 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI16 ) )
6666
ty ( 30 ) |-> typeInfoPtrType ( ty ( 9 ) )
67-
ty ( 31 ) |-> VoidType
67+
ty ( 31 ) |-> typeInfoVoidType
6868
</types>
6969
<adt-to-ty>
7070
adtDef ( 14 ) |-> ty ( 10 )

0 commit comments

Comments
 (0)