From 3ae1286b6652807de8bf8c9cd915fd39fd0840f8 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 30 Oct 2025 13:25:57 +1100 Subject: [PATCH 1/4] Use bitwidth=0 for discriminant values, allow comparisons --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 39 ++++++++------------ 1 file changed, 15 insertions(+), 24 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index cd744b4a2..da8171bd9 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1015,10 +1015,9 @@ The `getTyOf` helper applies the projections from the `Place` to determine the ` syntax Evaluation ::= #discriminant ( Evaluation , MaybeTy ) [strict(1)] // ---------------------------------------------------------------- rule #discriminant(Aggregate(IDX, _), TY:Ty) - => Integer(#lookupDiscriminant(lookupTy(TY), IDX), #discriminantSize(lookupTy(TY)), false) + => Integer(#lookupDiscriminant(lookupTy(TY), IDX), 0, false) // HACK: bit width 0 means "flexible" ... - requires #discriminantSize(lookupTy(TY)) =/=Int 0 syntax Int ::= #lookupDiscriminant ( TypeInfo , VariantIdx ) [function, total] | #lookupDiscrAux ( Discriminants , Int ) [function] @@ -1029,27 +1028,6 @@ The `getTyOf` helper applies the projections from the `Place` to determine the ` // -------------------------------------------------------------------- rule #lookupDiscrAux( discriminant(RESULT) _ , IDX) => RESULT requires IDX ==Int 0 rule #lookupDiscrAux( _:Discriminant MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX -Int 1) requires 0 #discriminantSize(LAYOUT) - rule #discriminantSize(_OTHER_TYPE:TypeInfo) => 0 [owise] - - rule #discriminantSize(layoutShape(_, variantsShapeMultiple(mk(TAG, _, _, _)), _, _, _)) => #discriminantSize(TAG) - rule #discriminantSize(_OTHER:LayoutShape) => 0 [owise] - - rule #discriminantSize(scalarInitialized(mk(primitiveInt(mk(INTLENGTH, _SIGNED)), _VALIDRANGE))) => #intLength(INTLENGTH) - rule #discriminantSize(scalarInitialized(mk(primitivePointer(_) , _VALIDRANGE))) => 64 // pointer size assumed 64 bit - rule #discriminantSize(_OTHER:Scalar) => 0 [owise] - - rule #intLength(integerLengthI8) => 8 - rule #intLength(integerLengthI16) => 16 - rule #intLength(integerLengthI32) => 32 - rule #intLength(integerLengthI64) => 64 - rule #intLength(integerLengthI128) => 128 ``` ```k @@ -1422,7 +1400,7 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th rule #discriminant( thunk(#cast (Integer(DATA, _, false), castKindTransmute, _, TY)), TY - ) => Integer(DATA, #discriminantSize(lookupTy(TY)), false) + ) => Integer(DATA, 0, false) // HACK: bit width 0 means "flexible" ... requires #isEnumWithoutFields(lookupTy(TY)) @@ -1708,6 +1686,19 @@ The argument types must be the same for all comparison operations, however this requires isComparison(OP) [preserves-definedness] // OP known to be a comparison + // HACK: accept bit width 0 in comparisons (coming from discriminants) + rule #applyBinOp(OP, Integer(VAL1, 0, false), Integer(VAL2, _WIDTH, _SIGN), _) + => + BoolVal(cmpOpInt(OP, VAL1, VAL2)) + requires isComparison(OP) + [preserves-definedness] // OP known to be a comparison + rule #applyBinOp(OP, Integer(VAL1, _WIDTH, _SIGN_), Integer(VAL2, 0, false), _) + => + BoolVal(cmpOpInt(OP, VAL1, VAL2)) + requires isComparison(OP) + [preserves-definedness] // OP known to be a comparison + + rule #applyBinOp(OP, BoolVal(VAL1), BoolVal(VAL2), _) => BoolVal(cmpOpBool(OP, VAL1, VAL2)) From c23e36748713a10e5297a019408d8227e0991563 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 31 Oct 2025 10:43:49 +1100 Subject: [PATCH 2/4] fix up switchMatch equations to deal with discriminant ints --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 177cf8d94..37243c45b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -173,7 +173,8 @@ will be `129`. rule #switchMatch(0, BoolVal(B) ) => notBool B rule #switchMatch(1, BoolVal(B) ) => B - rule #switchMatch(I, Integer(I2, WIDTH, _)) => I ==Int truncate(I2, WIDTH, Unsigned) + rule #switchMatch(I, Integer(I2, WIDTH, _)) => I ==Int truncate(I2, WIDTH, Unsigned) requires 0 I ==Int I2 ``` `Return` simply returns from a function call, using the information From 0b8e7ba6bdcfc3c9bcda16050690b3ebbc3f8611 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 31 Oct 2025 15:37:37 +1100 Subject: [PATCH 3/4] disambiguate special rules for comparison to avoid branches, test expectation --- deps/stable-mir-json | 2 +- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 6 +++--- kmir/src/tests/integration/data/exec-smir/enum/enum.state | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/deps/stable-mir-json b/deps/stable-mir-json index cf0410fba..b54152a30 160000 --- a/deps/stable-mir-json +++ b/deps/stable-mir-json @@ -1 +1 @@ -Subproject commit cf0410fba16002276f6fcdc195b7003e145558e9 +Subproject commit b54152a3099c4756c31fea1a126c20167ae42798 diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index da8171bd9..14b9633ab 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1684,6 +1684,7 @@ The argument types must be the same for all comparison operations, however this => BoolVal(cmpOpInt(OP, VAL1, VAL2)) requires isComparison(OP) + andBool WIDTH =/=Int 0 [preserves-definedness] // OP known to be a comparison // HACK: accept bit width 0 in comparisons (coming from discriminants) @@ -1691,19 +1692,18 @@ The argument types must be the same for all comparison operations, however this => BoolVal(cmpOpInt(OP, VAL1, VAL2)) requires isComparison(OP) - [preserves-definedness] // OP known to be a comparison + [priority(55), preserves-definedness] // OP known to be a comparison rule #applyBinOp(OP, Integer(VAL1, _WIDTH, _SIGN_), Integer(VAL2, 0, false), _) => BoolVal(cmpOpInt(OP, VAL1, VAL2)) requires isComparison(OP) [preserves-definedness] // OP known to be a comparison - rule #applyBinOp(OP, BoolVal(VAL1), BoolVal(VAL2), _) => BoolVal(cmpOpBool(OP, VAL1, VAL2)) requires isComparison(OP) - [preserves-definedness] // OP known to be a comparison + [priority(60), preserves-definedness] // OP known to be a comparison ``` The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `std::cmp::Ordering as i8`), indicating `LE`, `EQ`, or `GT`. diff --git a/kmir/src/tests/integration/data/exec-smir/enum/enum.state b/kmir/src/tests/integration/data/exec-smir/enum/enum.state index beb8cd641..16e4c197d 100644 --- a/kmir/src/tests/integration/data/exec-smir/enum/enum.state +++ b/kmir/src/tests/integration/data/exec-smir/enum/enum.state @@ -47,7 +47,7 @@ ListItem ( newLocal ( ty ( 16 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) ) - ListItem ( typedValue ( Integer ( 9090 , 16 , false ) , ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Integer ( 9090 , 0 , false ) , ty ( 29 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 26 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) ) From 5f4344fda8328cbbcc4141e5b7a3588b6cdefd0b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 31 Oct 2025 15:51:41 +1100 Subject: [PATCH 4/4] revert bad stable-mir-json change --- deps/stable-mir-json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/stable-mir-json b/deps/stable-mir-json index b54152a30..cf0410fba 160000 --- a/deps/stable-mir-json +++ b/deps/stable-mir-json @@ -1 +1 @@ -Subproject commit b54152a3099c4756c31fea1a126c20167ae42798 +Subproject commit cf0410fba16002276f6fcdc195b7003e145558e9