Skip to content

499 enum support in mir-semantics #521

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 13 commits into from
Apr 10, 2025
Merged

499 enum support in mir-semantics #521

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8676c1e
add VariantIdx field ot Aggregate Value
jberthold Mar 31, 2025
47e8575
add AdtDef -> Ty mapping to config and compute it from type metadata
jberthold Apr 4, 2025
30bdfd8
create Aggregate values for struct/enum with type information
jberthold Apr 4, 2025
6d1f02b
implement Discriminant RValue using type metadata
jberthold Apr 4, 2025
3a2674c
add comment about the discriminant type being u128 by default
jberthold Apr 4, 2025
3671a0c
Set Version: 0.3.113
rv-auditor Apr 4, 2025
233f033
add enum test program, update all smir.json
jberthold Apr 4, 2025
d8f38c3
update test expectations (added adt_def information)
jberthold Apr 4, 2025
4e4b4d1
use 128 bit (it is bit width, not byte width)
jberthold Apr 4, 2025
aecc3b0
Merge branch 'master' into 499-enum-support-tmp
jberthold Apr 7, 2025
46b1c99
Set Version: 0.3.114
rv-auditor Apr 7, 2025
7ff823d
Merge branch 'master' into 499-enum-support-tmp
jberthold Apr 8, 2025
e6e78e0
Set Version: 0.3.115
rv-auditor Apr 8, 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
2 changes: 1 addition & 1 deletion deps/stable-mir-json
Open in desktop
Submodule stable-mir-json updated 4 files
+0 −1 panic_example.rs
+0 −1 panic_example.smir.json
+5 −2 src/printer.rs
+3 −0 tests/integration/normalise-filter.jq
2 changes: 1 addition & 1 deletion kmir/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kmir"
version = "0.3.114"
version = "0.3.115"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kmir/src/kmir/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
from typing import Final

VERSION: Final = '0.3.114'
VERSION: Final = '0.3.115'
25 changes: 24 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 @@ -51,10 +51,11 @@ function map and the initial memory have to be set up.
<functions> _ => #mkFunctionMap(FUNCTIONS, ITEMS) </functions>
<start-symbol> FUNCNAME </start-symbol>
<types> _ => #mkTypeMap(.Map, TYPES) </types>
<adt-to-ty> _ => #mkAdtMap(.Map, TYPES) </adt-to-ty>
```

The `Map` of types is static information used for decoding constants and allocated data into `Value`s.
It maps `Ty` IDs to `RigidTy` that can be supplied to decoding functions.
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).

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

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.

```k
syntax Map ::= #mkAdtMap ( Map , TypeMappings ) [function, total]
// --------------------------------------------------------------
rule #mkAdtMap(ACC, .TypeMappings) => ACC

rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoStructType(_, ADTDEF)) MORE:TypeMappings)
=>
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
requires notBool TY in_keys(ACC)

rule #mkAdtMap(ACC, TypeMapping(TY, typeInfoEnumType(_, ADTDEF, _)) MORE:TypeMappings)
=>
#mkAdtMap(ACC[ADTDEF <- TY], MORE)
requires notBool TY in_keys(ACC)

rule #mkAdtMap(ACC, TypeMapping(_, _) MORE:TypeMappings)
=>
#mkAdtMap(ACC, MORE)
[owise]
```

The `Map` of `functions` is constructed from the lookup table of `FunctionNames`,
composed with a secondary lookup of `Item`s via `symbolName`. This composed map will
Expand Down
1 change: 1 addition & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ module KMIR-CONFIGURATION
<start-symbol> symbol($STARTSYM:String) </start-symbol>
// static information about the base type interning in the MIR
<types> .Map </types>
<adt-to-ty> .Map </adt-to-ty>
</kmir>

endmodule
Expand Down
65 changes: 54 additions & 11 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 @@ -189,7 +189,7 @@ A `Field` access projection operates on `struct`s and tuples, which are represen

```k
rule <k> #readProjection(
typedValue(Aggregate(ARGS), _, _),
typedValue(Aggregate(_, ARGS), _, _),
projectionElemField(fieldIdx(I), _TY) PROJS
)
=>
Expand Down Expand Up @@ -421,7 +421,7 @@ The solution is to use rewrite operations in a downward pass through the project
| toStack ( Int , Local )

// retains information about the value that was deconstructed by a projection
syntax Context ::= CtxField( Ty, List, Int )
syntax Context ::= CtxField( Ty, VariantIdx, List, Int )
// | array context will be added here

syntax Contexts ::= List{Context, ""}
Expand All @@ -431,19 +431,19 @@ The solution is to use rewrite operations in a downward pass through the project
rule #buildUpdate(VAL, .Contexts) => VAL
[preserves-definedness]

rule #buildUpdate(VAL, CtxField(TY, ARGS, I) CTXS)
=> #buildUpdate(typedValue(Aggregate(ARGS[I <- VAL]), TY, mutabilityMut), CTXS)
rule #buildUpdate(VAL, CtxField(TY, IDX, ARGS, I) CTXS)
=> #buildUpdate(typedValue(Aggregate(IDX, ARGS[I <- VAL]), TY, mutabilityMut), CTXS)
[preserves-definedness] // valid list indexing checked upon context construction

rule <k> #projectedUpdate(
DEST,
typedValue(Aggregate(ARGS), TY, MUT),
typedValue(Aggregate(IDX, ARGS), TY, MUT),
projectionElemField(fieldIdx(I), _) PROJS,
UPDATE,
CTXTS,
FORCE
) =>
#projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, ARGS, I) CTXTS, FORCE)
#projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE)
...
</k>
requires 0 <=Int I
Expand Down Expand Up @@ -603,21 +603,31 @@ Other `RValue`s exist in order to construct or operate on arrays and slices, whi
```

Likewise built into the language are aggregates (tuples and `struct`s) and variants (`enum`s).
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.

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

```k
rule <k> rvalueAggregate(KIND, ARGS) => #readOperands(ARGS) ~> #mkAggregate(KIND) ... </k>

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

rule <k> ARGS:List ~> #mkAggregate(_)
rule <k> ARGS:List ~> #mkAggregate(aggregateKindAdt(ADTDEF, VARIDX, _, _, _))
=>
typedValue(Aggregate(ARGS), TyUnknown, mutabilityNot)
// NB ty not determined ^^^^^^^^^
typedValue(Aggregate(VARIDX, ARGS), {ADTMAPPING[ADTDEF]}:>MaybeTy, mutabilityNot)
...
</k>
<adt-to-ty> ADTMAPPING </adt-to-ty>
requires isTy(ADTMAPPING[ADTDEF])

rule <k> ARGS:List ~> #mkAggregate(_OTHERKIND)
=>
typedValue(Aggregate(variantIdx(0), ARGS), TyUnknown, mutabilityNot)
...
</k>
[owise]


// #readOperands accumulates a list of `TypedLocal` values from operands
Expand All @@ -640,8 +650,39 @@ Tuples and structs are built as `Aggregate` values with a list of argument value
#readOperandsAux(ACC ListItem(VAL), REST)
...
</k>
```

// Discriminant, ShallowIntBox: not implemented yet
The `Aggregate` type carries a `VariantIdx` to distinguish the different variants for an `enum`.
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.

```k
syntax KItem ::= #discriminant ( Evaluation ) [strict(1)]

rule <k> rvalueDiscriminant(PLACE) => #discriminant(operandCopy(PLACE)) ... </k>

rule <k> #discriminant(typedValue(Aggregate(IDX, _), TY, _))
=>
typedValue(
Integer(#lookupDiscriminant({TYPEMAP[TY]}:>TypeInfo, IDX), 128, false), // parameters for storead u128
TyUnknown,
mutabilityNot
)
...
</k>
<types> TYPEMAP </types>
requires isTypeInfo(TYPEMAP[TY])

syntax Int ::= #lookupDiscriminant ( TypeInfo , VariantIdx ) [function, total]
| #lookupDiscrAux ( Discriminants , VariantIdx ) [function]
// --------------------------------------------------------------------
rule #lookupDiscriminant(typeInfoEnumType(_, _, DISCRIMINANTS), IDX) => #lookupDiscrAux(DISCRIMINANTS, IDX)
requires isInt(#lookupDiscrAux(DISCRIMINANTS, IDX)) [preserves-definedness]
rule #lookupDiscriminant(_OTHER, _) => 0 [owise, preserves-definedness] // default 0. May be undefined behaviour, though.
Comment on lines +675 to +680
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of this default returning 0 , we could signal undefined behaviour - if it was clear what exactly constitutes undefined behaviour here, the discussion on rust-lang/rust#91095 remains unresolved IIUC.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is consistent with miri which is probably good to start with. But I think signalling UB would be good for a future version

// --------------------------------------------------------------------
rule #lookupDiscrAux( Discriminant(IDX, RESULT) _ , IDX) => RESULT
rule #lookupDiscrAux( _OTHER:Discriminant MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX) [owise]

// ShallowIntBox: not implemented yet
```

### References and Dereferencing
Expand Down Expand Up @@ -891,6 +932,7 @@ The arithmetic operations require operands of the same numeric type.
=>
typedValue(
Aggregate(
variantIdx(0),
ListItem(typedValue(Integer(truncate(onInt(BOP, ARG1, ARG2), WIDTH, Signed), WIDTH, true), TY, mutabilityNot))
ListItem(
typedValue(
Expand Down Expand Up @@ -918,6 +960,7 @@ The arithmetic operations require operands of the same numeric type.
=>
typedValue(
Aggregate(
variantIdx(0),
ListItem(typedValue(Integer(truncate(onInt(BOP, ARG1, ARG2), WIDTH, Unsigned), WIDTH, false), TY, mutabilityNot))
ListItem(
typedValue(
Expand Down
2 changes: 1 addition & 1 deletion kmir/src/kmir/kdist/mir-semantics/rt/value.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ High-level values can be
// value, bit-width, signedness for un/signed int
| BoolVal( Bool )
// boolean
| Aggregate( List )
| Aggregate( VariantIdx , List )
// heterogenous value list for tuples and structs (standard, tuple, or anonymous)
| Float( Float, Int )
// value, bit-width for f16-f128
Expand Down
8 changes: 4 additions & 4 deletions kmir/src/kmir/kdist/mir-semantics/ty.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,12 +254,12 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
| "rigidTyUnimplemented" [group(mir-enum), symbol(RigidTy::Unimplemented), deprecated] // TODO: remove

// additional sort to provide type information in stable-mir-json
syntax TypeInfo ::= typeInfoPrimitiveType(PrimitiveType) [symbol(TypeInfo::PrimitiveType), group(mir-enum)]
| typeInfoEnumType(MIRString, Discriminants) [symbol(TypeInfo::EnumType) , group(mir-enum---name--discriminants)]
| typeInfoStructType(MIRString) [symbol(TypeInfo::StructType) , group(mir-enum---name)]
syntax TypeInfo ::= typeInfoPrimitiveType(PrimitiveType) [symbol(TypeInfo::PrimitiveType), group(mir-enum)]
| typeInfoEnumType(MIRString, AdtDef, Discriminants) [symbol(TypeInfo::EnumType) , group(mir-enum---name--adt-def--discriminants)]
| typeInfoStructType(MIRString, AdtDef) [symbol(TypeInfo::StructType) , group(mir-enum---name--adt-def)]

// discriminant information for enum types
syntax Discriminant ::= Discriminant ( Ty , MIRInt ) [group(mir)]
syntax Discriminant ::= Discriminant ( VariantIdx , MIRInt ) [group(mir)]

syntax Discriminants ::= List{Discriminant, ""} [group(mir-list), symbol(Discriminants::append), terminator-symbol(Discriminants::empty)]

Expand Down
25 changes: 14 additions & 11 deletions kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.smir.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@
100,
58,
32,
105,
117,
56,
58,
58,
Expand All @@ -54,9 +54,9 @@
101,
100,
95,
115,
117,
98,
97,
100,
100,
32,
99,
97,
Expand Down Expand Up @@ -120,7 +120,7 @@
100,
58,
32,
117,
105,
56,
58,
58,
Expand All @@ -134,9 +134,9 @@
101,
100,
95,
97,
100,
100,
115,
117,
98,
32,
99,
97,
Expand Down Expand Up @@ -237,7 +237,7 @@
}
],
[
38,
37,
{
"NoOpSym": ""
}
Expand Down Expand Up @@ -3630,6 +3630,7 @@
{
"EnumType": {
"name": "std::result::Result<T/#0, E/#1>",
"adt_def": 20,
"discriminants": [
[
0,
Expand All @@ -3647,7 +3648,8 @@
15,
{
"StructType": {
"name": "std::sys::pal::unix::process::process_common::ExitCode"
"name": "std::sys::pal::unix::process::process_common::ExitCode",
"adt_def": 13
}
}
],
Expand All @@ -3663,7 +3665,8 @@
17,
{
"StructType": {
"name": "std::process::ExitCode"
"name": "std::process::ExitCode",
"adt_def": 15
}
}
],
Expand Down
19 changes: 12 additions & 7 deletions kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,21 +33,21 @@
<locals>
ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( 254 , 8 , false ) , ty ( 9 ) , mutabilityNot ) )
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
ListItem ( Moved ) ) , ty ( 28 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( 255 , 8 , false ) , ty ( 9 ) , mutabilityNot ) )
ListItem ( typedValue ( Integer ( -100 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
ListItem ( Moved ) ) , ty ( 26 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( -128 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
ListItem ( typedValue ( Integer ( -32640 , 16 , true ) , ty ( 35 ) , mutabilityNot ) )
ListItem ( typedValue ( Integer ( 255 , 16 , true ) , ty ( 35 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( -128 , 16 , true ) , ty ( 35 ) , mutabilityMut ) )
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
ListItem ( Moved ) ) , ty ( 36 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( -32768 , 16 , true ) , ty ( 35 ) , mutabilityNot ) )
ListItem ( typedValue ( Integer ( -128 , 16 , true ) , ty ( 35 ) , mutabilityMut ) )
ListItem ( typedValue ( Aggregate ( ListItem ( Moved )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
ListItem ( Moved ) ) , ty ( 36 ) , mutabilityMut ) )
</locals>
</currentFrame>
Expand Down Expand Up @@ -76,11 +76,16 @@
ty ( 2 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI8 ) )
ty ( 6 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyIsize ) )
ty ( 9 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU8 ) )
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<T/#0, E/#1>" , Discriminant ( ty ( 0 ) , 0 ) Discriminant ( ty ( 1 ) , 1 ) .Discriminants )
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" )
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<T/#0, E/#1>" , adtDef ( 20 ) , Discriminant ( variantIdx ( 0 ) , 0 ) Discriminant ( variantIdx ( 1 ) , 1 ) .Discriminants )
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 13 ) )
ty ( 16 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI32 ) )
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" )
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 15 ) )
ty ( 21 ) |-> typeInfoPrimitiveType ( primTypeBool )
ty ( 35 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI16 ) )
</types>
<adt-to-ty>
adtDef ( 13 ) |-> ty ( 15 )
adtDef ( 15 ) |-> ty ( 17 )
adtDef ( 20 ) |-> ty ( 10 )
</adt-to-ty>
</kmir>
7 changes: 5 additions & 2 deletions kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.smir.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2745,6 +2745,7 @@
{
"EnumType": {
"name": "std::result::Result<T/#0, E/#1>",
"adt_def": 8,
"discriminants": [
[
0,
Expand All @@ -2762,7 +2763,8 @@
15,
{
"StructType": {
"name": "std::sys::pal::unix::process::process_common::ExitCode"
"name": "std::sys::pal::unix::process::process_common::ExitCode",
"adt_def": 14
}
}
],
Expand All @@ -2778,7 +2780,8 @@
17,
{
"StructType": {
"name": "std::process::ExitCode"
"name": "std::process::ExitCode",
"adt_def": 16
}
}
],
Expand Down
Loading
Loading