diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 776b51bff..b23bc1e8e 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 diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index e3304290b..3c7798e30 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)) @@ -1705,6 +1683,19 @@ The argument types must be the same for all comparison operations, however this rule #applyBinOp(OP, Integer(VAL1, WIDTH, SIGN), Integer(VAL2, WIDTH, SIGN), _) => 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) + rule #applyBinOp(OP, Integer(VAL1, 0, false), Integer(VAL2, _WIDTH, _SIGN), _) + => + BoolVal(cmpOpInt(OP, VAL1, VAL2)) + requires isComparison(OP) + [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 @@ -1712,7 +1703,7 @@ The argument types must be the same for all comparison operations, however this => 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 ) )