Skip to content

Commit 8029cf1

Browse files
jbertholdrv-auditor
jberthold
and
rv-auditor
authored
499 enum support in mir-semantics (#521)
* Using the new type metadata to get the enum variant discriminator mapping and ADT Def ID * Enums are created as `Aggregate` values, which now carry the variant index * `Aggregate`s for `struct`s and `enum`s now have a correct `Ty` field (still `TyUnknown` for tuples, though) * `RValue::Discriminant` is implemented: - for an `enum`, it looks up the discriminant and returns it as a `u128` (discriminant type information unavailable) - for other `Aggregate`s, it will always return `0` (see related discussion in `rustc`: rust-lang/rust#91095) This is a first step. The data returned by `Discriminant` is actually not consistent (bit width and signedness do not match the indicated `Ty`), which will cause issues if the obtained discriminant is used in any way other than as a `SwitchInt` argument. Fixes #499 --------- Co-authored-by: devops <[email protected]>
1 parent f2c9a09 commit 8029cf1

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+2952
-147
lines changed

Diff for: ‎deps/stable-mir-json

Diff for: ‎kmir/pyproject.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kmir"
7-
version = "0.3.114"
7+
version = "0.3.115"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

Diff for: ‎kmir/src/kmir/__init__.py

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
from typing import Final
22

3-
VERSION: Final = '0.3.114'
3+
VERSION: Final = '0.3.115'

Diff for: ‎kmir/src/kmir/kdist/mir-semantics/kmir.md

+24-1
Original file line numberDiff line numberDiff line change
@@ -51,10 +51,11 @@ function map and the initial memory have to be set up.
5151
<functions> _ => #mkFunctionMap(FUNCTIONS, ITEMS) </functions>
5252
<start-symbol> FUNCNAME </start-symbol>
5353
<types> _ => #mkTypeMap(.Map, TYPES) </types>
54+
<adt-to-ty> _ => #mkAdtMap(.Map, TYPES) </adt-to-ty>
5455
```
5556

5657
The `Map` of types is static information used for decoding constants and allocated data into `Value`s.
57-
It maps `Ty` IDs to `RigidTy` that can be supplied to decoding functions.
58+
It maps `Ty` IDs to `TypeInfo` that can be supplied to decoding and casting functions as well as operations involving `Aggregate` values (related to `struct`s and `enum`s).
5859

5960
```k
6061
syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total]
@@ -75,6 +76,28 @@ It maps `Ty` IDs to `RigidTy` that can be supplied to decoding functions.
7576
[owise]
7677
```
7778

79+
Another type-related `Map` is required to associate an `AdtDef` ID with its corresponding `Ty` ID for `struct`s and `enum`s when creating or using `Aggregate` values.
80+
81+
```k
82+
syntax Map ::= #mkAdtMap ( Map , TypeMappings ) [function, total]
83+
// --------------------------------------------------------------
84+
rule #mkAdtMap(ACC, .TypeMappings) => ACC
85+
86+
rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoStructType(_, ADTDEF)) MORE:TypeMappings)
87+
=>
88+
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
89+
requires notBool TY in_keys(ACC)
90+
91+
rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoEnumType(_, ADTDEF, _)) MORE:TypeMappings)
92+
=>
93+
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
94+
requires notBool TY in_keys(ACC)
95+
96+
rule #mkAdtMap(ACC, TypeMapping(_, _) MORE:TypeMappings)
97+
=>
98+
#mkAdtMap(ACC, MORE)
99+
[owise]
100+
```
78101

79102
The `Map` of `functions` is constructed from the lookup table of `FunctionNames`,
80103
composed with a secondary lookup of `Item`s via `symbolName`. This composed map will

Diff for: ‎kmir/src/kmir/kdist/mir-semantics/rt/configuration.md

+1
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ module KMIR-CONFIGURATION
5454
<start-symbol> symbol($STARTSYM:String) </start-symbol>
5555
// static information about the base type interning in the MIR
5656
<types> .Map </types>
57+
<adt-to-ty> .Map </adt-to-ty>
5758
</kmir>
5859
5960
endmodule

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

+54-11
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,7 @@ A `Field` access projection operates on `struct`s and tuples, which are represen
189189

190190
```k
191191
rule <k> #readProjection(
192-
typedValue(Aggregate(ARGS), _, _),
192+
typedValue(Aggregate(_, ARGS), _, _),
193193
projectionElemField(fieldIdx(I), _TY) PROJS
194194
)
195195
=>
@@ -421,7 +421,7 @@ The solution is to use rewrite operations in a downward pass through the project
421421
| toStack ( Int , Local )
422422
423423
// retains information about the value that was deconstructed by a projection
424-
syntax Context ::= CtxField( Ty, List, Int )
424+
syntax Context ::= CtxField( Ty, VariantIdx, List, Int )
425425
// | array context will be added here
426426
427427
syntax Contexts ::= List{Context, ""}
@@ -431,19 +431,19 @@ The solution is to use rewrite operations in a downward pass through the project
431431
rule #buildUpdate(VAL, .Contexts) => VAL
432432
[preserves-definedness]
433433
434-
rule #buildUpdate(VAL, CtxField(TY, ARGS, I) CTXS)
435-
=> #buildUpdate(typedValue(Aggregate(ARGS[I <- VAL]), TY, mutabilityMut), CTXS)
434+
rule #buildUpdate(VAL, CtxField(TY, IDX, ARGS, I) CTXS)
435+
=> #buildUpdate(typedValue(Aggregate(IDX, ARGS[I <- VAL]), TY, mutabilityMut), CTXS)
436436
[preserves-definedness] // valid list indexing checked upon context construction
437437
438438
rule <k> #projectedUpdate(
439439
DEST,
440-
typedValue(Aggregate(ARGS), TY, MUT),
440+
typedValue(Aggregate(IDX, ARGS), TY, MUT),
441441
projectionElemField(fieldIdx(I), _) PROJS,
442442
UPDATE,
443443
CTXTS,
444444
FORCE
445445
) =>
446-
#projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, ARGS, I) CTXTS, FORCE)
446+
#projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE)
447447
...
448448
</k>
449449
requires 0 <=Int I
@@ -603,21 +603,31 @@ Other `RValue`s exist in order to construct or operate on arrays and slices, whi
603603
```
604604

605605
Likewise built into the language are aggregates (tuples and `struct`s) and variants (`enum`s).
606+
Besides their list of arguments, `enum`s also carry a `VariantIdx` indicating which variant was used. For tuples and `struct`s, this index is always 0.
606607

607-
Tuples and structs are built as `Aggregate` values with a list of argument values.
608+
Tuples, `struct`s, and `enum`s are built as `Aggregate` values with a list of argument values.
609+
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`.
608610

609611
```k
610612
rule <k> rvalueAggregate(KIND, ARGS) => #readOperands(ARGS) ~> #mkAggregate(KIND) ... </k>
611613
612614
// #mkAggregate produces an aggregate TypedLocal value of given kind from a preceeding list of values
613615
syntax KItem ::= #mkAggregate ( AggregateKind )
614616
615-
rule <k> ARGS:List ~> #mkAggregate(_)
617+
rule <k> ARGS:List ~> #mkAggregate(aggregateKindAdt(ADTDEF, VARIDX, _, _, _))
616618
=>
617-
typedValue(Aggregate(ARGS), TyUnknown, mutabilityNot)
618-
// NB ty not determined ^^^^^^^^^
619+
typedValue(Aggregate(VARIDX, ARGS), {ADTMAPPING[ADTDEF]}:>MaybeTy, mutabilityNot)
619620
...
620621
</k>
622+
<adt-to-ty> ADTMAPPING </adt-to-ty>
623+
requires isTy(ADTMAPPING[ADTDEF])
624+
625+
rule <k> ARGS:List ~> #mkAggregate(_OTHERKIND)
626+
=>
627+
typedValue(Aggregate(variantIdx(0), ARGS), TyUnknown, mutabilityNot)
628+
...
629+
</k>
630+
[owise]
621631
622632
623633
// #readOperands accumulates a list of `TypedLocal` values from operands
@@ -640,8 +650,39 @@ Tuples and structs are built as `Aggregate` values with a list of argument value
640650
#readOperandsAux(ACC ListItem(VAL), REST)
641651
...
642652
</k>
653+
```
643654

644-
// Discriminant, ShallowIntBox: not implemented yet
655+
The `Aggregate` type carries a `VariantIdx` to distinguish the different variants for an `enum`.
656+
This variant index is used to look up the _discriminant_ from a table in the type metadata during evaluation of the `Rvalue::Discriminant`. Note that the discriminant may be different from the variant index for user-defined discriminants and uninhabited variants.
657+
658+
```k
659+
syntax KItem ::= #discriminant ( Evaluation ) [strict(1)]
660+
661+
rule <k> rvalueDiscriminant(PLACE) => #discriminant(operandCopy(PLACE)) ... </k>
662+
663+
rule <k> #discriminant(typedValue(Aggregate(IDX, _), TY, _))
664+
=>
665+
typedValue(
666+
Integer(#lookupDiscriminant({TYPEMAP[TY]}:>TypeInfo, IDX), 128, false), // parameters for storead u128
667+
TyUnknown,
668+
mutabilityNot
669+
)
670+
...
671+
</k>
672+
<types> TYPEMAP </types>
673+
requires isTypeInfo(TYPEMAP[TY])
674+
675+
syntax Int ::= #lookupDiscriminant ( TypeInfo , VariantIdx ) [function, total]
676+
| #lookupDiscrAux ( Discriminants , VariantIdx ) [function]
677+
// --------------------------------------------------------------------
678+
rule #lookupDiscriminant(typeInfoEnumType(_, _, DISCRIMINANTS), IDX) => #lookupDiscrAux(DISCRIMINANTS, IDX)
679+
requires isInt(#lookupDiscrAux(DISCRIMINANTS, IDX)) [preserves-definedness]
680+
rule #lookupDiscriminant(_OTHER, _) => 0 [owise, preserves-definedness] // default 0. May be undefined behaviour, though.
681+
// --------------------------------------------------------------------
682+
rule #lookupDiscrAux( Discriminant(IDX, RESULT) _ , IDX) => RESULT
683+
rule #lookupDiscrAux( _OTHER:Discriminant MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX) [owise]
684+
685+
// ShallowIntBox: not implemented yet
645686
```
646687

647688
### References and Dereferencing
@@ -891,6 +932,7 @@ The arithmetic operations require operands of the same numeric type.
891932
=>
892933
typedValue(
893934
Aggregate(
935+
variantIdx(0),
894936
ListItem(typedValue(Integer(truncate(onInt(BOP, ARG1, ARG2), WIDTH, Signed), WIDTH, true), TY, mutabilityNot))
895937
ListItem(
896938
typedValue(
@@ -918,6 +960,7 @@ The arithmetic operations require operands of the same numeric type.
918960
=>
919961
typedValue(
920962
Aggregate(
963+
variantIdx(0),
921964
ListItem(typedValue(Integer(truncate(onInt(BOP, ARG1, ARG2), WIDTH, Unsigned), WIDTH, false), TY, mutabilityNot))
922965
ListItem(
923966
typedValue(

Diff for: ‎kmir/src/kmir/kdist/mir-semantics/rt/value.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ High-level values can be
2626
// value, bit-width, signedness for un/signed int
2727
| BoolVal( Bool )
2828
// boolean
29-
| Aggregate( List )
29+
| Aggregate( VariantIdx , List )
3030
// heterogenous value list for tuples and structs (standard, tuple, or anonymous)
3131
| Float( Float, Int )
3232
// value, bit-width for f16-f128

Diff for: ‎kmir/src/kmir/kdist/mir-semantics/ty.md

+4-4
Original file line numberDiff line numberDiff line change
@@ -254,12 +254,12 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
254254
| "rigidTyUnimplemented" [group(mir-enum), symbol(RigidTy::Unimplemented), deprecated] // TODO: remove
255255
256256
// additional sort to provide type information in stable-mir-json
257-
syntax TypeInfo ::= typeInfoPrimitiveType(PrimitiveType) [symbol(TypeInfo::PrimitiveType), group(mir-enum)]
258-
| typeInfoEnumType(MIRString, Discriminants) [symbol(TypeInfo::EnumType) , group(mir-enum---name--discriminants)]
259-
| typeInfoStructType(MIRString) [symbol(TypeInfo::StructType) , group(mir-enum---name)]
257+
syntax TypeInfo ::= typeInfoPrimitiveType(PrimitiveType) [symbol(TypeInfo::PrimitiveType), group(mir-enum)]
258+
| typeInfoEnumType(MIRString, AdtDef, Discriminants) [symbol(TypeInfo::EnumType) , group(mir-enum---name--adt-def--discriminants)]
259+
| typeInfoStructType(MIRString, AdtDef) [symbol(TypeInfo::StructType) , group(mir-enum---name--adt-def)]
260260
261261
// discriminant information for enum types
262-
syntax Discriminant ::= Discriminant ( Ty , MIRInt ) [group(mir)]
262+
syntax Discriminant ::= Discriminant ( VariantIdx , MIRInt ) [group(mir)]
263263
264264
syntax Discriminants ::= List{Discriminant, ""} [group(mir-list), symbol(Discriminants::append), terminator-symbol(Discriminants::empty)]
265265

Diff for: ‎kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.smir.json

+14-11
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@
4040
100,
4141
58,
4242
32,
43-
105,
43+
117,
4444
56,
4545
58,
4646
58,
@@ -54,9 +54,9 @@
5454
101,
5555
100,
5656
95,
57-
115,
58-
117,
59-
98,
57+
97,
58+
100,
59+
100,
6060
32,
6161
99,
6262
97,
@@ -120,7 +120,7 @@
120120
100,
121121
58,
122122
32,
123-
117,
123+
105,
124124
56,
125125
58,
126126
58,
@@ -134,9 +134,9 @@
134134
101,
135135
100,
136136
95,
137-
97,
138-
100,
139-
100,
137+
115,
138+
117,
139+
98,
140140
32,
141141
99,
142142
97,
@@ -237,7 +237,7 @@
237237
}
238238
],
239239
[
240-
38,
240+
37,
241241
{
242242
"NoOpSym": ""
243243
}
@@ -3630,6 +3630,7 @@
36303630
{
36313631
"EnumType": {
36323632
"name": "std::result::Result<T/#0, E/#1>",
3633+
"adt_def": 20,
36333634
"discriminants": [
36343635
[
36353636
0,
@@ -3647,7 +3648,8 @@
36473648
15,
36483649
{
36493650
"StructType": {
3650-
"name": "std::sys::pal::unix::process::process_common::ExitCode"
3651+
"name": "std::sys::pal::unix::process::process_common::ExitCode",
3652+
"adt_def": 13
36513653
}
36523654
}
36533655
],
@@ -3663,7 +3665,8 @@
36633665
17,
36643666
{
36653667
"StructType": {
3666-
"name": "std::process::ExitCode"
3668+
"name": "std::process::ExitCode",
3669+
"adt_def": 15
36673670
}
36683671
}
36693672
],

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

+12-7
Original file line numberDiff line numberDiff line change
@@ -33,21 +33,21 @@
3333
<locals>
3434
ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
3535
ListItem ( typedValue ( Integer ( 254 , 8 , false ) , ty ( 9 ) , mutabilityNot ) )
36-
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
36+
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
3737
ListItem ( Moved ) ) , ty ( 28 ) , mutabilityMut ) )
3838
ListItem ( typedValue ( Integer ( 255 , 8 , false ) , ty ( 9 ) , mutabilityNot ) )
3939
ListItem ( typedValue ( Integer ( -100 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
40-
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
40+
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
4141
ListItem ( Moved ) ) , ty ( 26 ) , mutabilityMut ) )
4242
ListItem ( typedValue ( Integer ( -128 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
4343
ListItem ( typedValue ( Integer ( -32640 , 16 , true ) , ty ( 35 ) , mutabilityNot ) )
4444
ListItem ( typedValue ( Integer ( 255 , 16 , true ) , ty ( 35 ) , mutabilityMut ) )
4545
ListItem ( typedValue ( Integer ( -128 , 16 , true ) , ty ( 35 ) , mutabilityMut ) )
46-
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
46+
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
4747
ListItem ( Moved ) ) , ty ( 36 ) , mutabilityMut ) )
4848
ListItem ( typedValue ( Integer ( -32768 , 16 , true ) , ty ( 35 ) , mutabilityNot ) )
4949
ListItem ( typedValue ( Integer ( -128 , 16 , true ) , ty ( 35 ) , mutabilityMut ) )
50-
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
50+
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
5151
ListItem ( Moved ) ) , ty ( 36 ) , mutabilityMut ) )
5252
</locals>
5353
</currentFrame>
@@ -76,11 +76,16 @@
7676
ty ( 2 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI8 ) )
7777
ty ( 6 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyIsize ) )
7878
ty ( 9 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU8 ) )
79-
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<T/#0, E/#1>" , Discriminant ( ty ( 0 ) , 0 ) Discriminant ( ty ( 1 ) , 1 ) .Discriminants )
80-
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" )
79+
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<T/#0, E/#1>" , adtDef ( 20 ) , Discriminant ( variantIdx ( 0 ) , 0 ) Discriminant ( variantIdx ( 1 ) , 1 ) .Discriminants )
80+
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 13 ) )
8181
ty ( 16 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI32 ) )
82-
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" )
82+
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 15 ) )
8383
ty ( 21 ) |-> typeInfoPrimitiveType ( primTypeBool )
8484
ty ( 35 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI16 ) )
8585
</types>
86+
<adt-to-ty>
87+
adtDef ( 13 ) |-> ty ( 15 )
88+
adtDef ( 15 ) |-> ty ( 17 )
89+
adtDef ( 20 ) |-> ty ( 10 )
90+
</adt-to-ty>
8691
</kmir>

Diff for: ‎kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.smir.json

+5-2
Original file line numberDiff line numberDiff line change
@@ -2745,6 +2745,7 @@
27452745
{
27462746
"EnumType": {
27472747
"name": "std::result::Result<T/#0, E/#1>",
2748+
"adt_def": 8,
27482749
"discriminants": [
27492750
[
27502751
0,
@@ -2762,7 +2763,8 @@
27622763
15,
27632764
{
27642765
"StructType": {
2765-
"name": "std::sys::pal::unix::process::process_common::ExitCode"
2766+
"name": "std::sys::pal::unix::process::process_common::ExitCode",
2767+
"adt_def": 14
27662768
}
27672769
}
27682770
],
@@ -2778,7 +2780,8 @@
27782780
17,
27792781
{
27802782
"StructType": {
2781-
"name": "std::process::ExitCode"
2783+
"name": "std::process::ExitCode",
2784+
"adt_def": 16
27822785
}
27832786
}
27842787
],

0 commit comments

Comments
 (0)