From fd8be40e9cfc21df4607b365b9b1370d895465d8 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 4 Mar 2026 12:16:07 +0800 Subject: [PATCH 1/3] test(prove-rs): add direct-tag enum decode test showing stuck states Add comprehensive test for direct-tag enum decoding covering: - repr(u8) with discriminants 0/1 (1+1 fields, unlike Option's 0+1) - repr(u8) with discriminants 2/5 (non-zero start) - repr(u16) with discriminants 0/256 (wide tag) - repr(u8) with 3 variants The show output captures the current failure: UnableToDecode thunks and stuck proof nodes because the existing decoder only handles the Option-like 0+1 field pattern with discriminants exactly 0 and 1. --- .../data/prove-rs/enum-direct-tag-decode.rs | 72 +++++++++++++++++++ .../show/enum-direct-tag-decode.main.expected | 69 ++++++++++++++++++ .../src/tests/integration/test_integration.py | 1 + 3 files changed, 142 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs b/kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs new file mode 100644 index 000000000..30eef03d1 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs @@ -0,0 +1,72 @@ +/// Comprehensive test for direct-tag enum decoding. +/// +/// Covers: +/// - `#[repr(u8)]` with discriminants 0/1 (baseline, like Option) +/// - `#[repr(u8)]` with discriminants 2/5 (non-zero start) +/// - `#[repr(u16)]` with discriminants 0/256 (wide tag exceeding u8 range) +/// - `#[repr(u8)]` with 3 variants (beyond two-variant restriction) + +// --- Baseline: repr(u8), disc 0 / 1 ------------------------------------------- + +#[repr(u8)] +enum TwoU8 { + A(bool) = 0, + B(bool) = 1, +} + +const TWO_U8_A: TwoU8 = TwoU8::A(true); +const TWO_U8_B: TwoU8 = TwoU8::B(false); + +// --- Non-zero discriminants: repr(u8), disc 2 / 5 ----------------------------- + +#[repr(u8)] +enum NonZero { + X(bool) = 2, + Y(bool) = 5, +} + +const NZ_X: NonZero = NonZero::X(false); +const NZ_Y: NonZero = NonZero::Y(true); + +// --- Wide tag: repr(u16), disc 0 / 256 ---------------------------------------- + +#[repr(u16)] +enum WideTag { + Lo(bool) = 0, + Hi(bool) = 256, +} + +const WIDE_LO: WideTag = WideTag::Lo(true); +const WIDE_HI: WideTag = WideTag::Hi(false); + +// --- Three variants: repr(u8), disc 0 / 1 / 2 --------------------------------- + +#[repr(u8)] +enum Three { + First(bool) = 0, + Second(bool) = 1, + Third(bool) = 2, +} + +const THREE_A: Three = Three::First(true); +const THREE_B: Three = Three::Second(false); +const THREE_C: Three = Three::Third(true); + +fn main() { + // Baseline + assert!(matches!(TWO_U8_A, TwoU8::A(true))); + assert!(matches!(TWO_U8_B, TwoU8::B(false))); + + // Non-zero discriminants + assert!(matches!(NZ_X, NonZero::X(false))); + assert!(matches!(NZ_Y, NonZero::Y(true))); + + // Wide tag + assert!(matches!(WIDE_LO, WideTag::Lo(true))); + assert!(matches!(WIDE_HI, WideTag::Hi(false))); + + // Three variants + assert!(matches!(THREE_A, Three::First(true))); + assert!(matches!(THREE_B, Three::Second(false))); + assert!(matches!(THREE_C, Three::Third(true))); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected b/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected new file mode 100644 index 000000000..eae2f3bd1 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected @@ -0,0 +1,69 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (33 steps) +├─ 3 +│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) +│ function: main +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ #execBlockIdx ( basicBlockIdx ( 2 ) ) ~> .K +┃ │ function: main +┃ │ +┃ │ (9 steps) +┃ └─ 7 (stuck, leaf) +┃ #traverseProjection ( toLocal ( 2 ) , thunk ( UnableToDecode ( b"\x00\x01" , typ +┃ function: main +┃ span: 50 +┃ +┣━━┓ +┃ │ +┃ ├─ 5 +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 1 ) ) +┃ │ function: main +┃ ┃ +┃ ┃ (1 step) +┃ ┣━━┓ +┃ ┃ │ +┃ ┃ ├─ 8 +┃ ┃ │ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K +┃ ┃ │ function: main +┃ ┃ │ +┃ ┃ │ (28 steps) +┃ ┃ └─ 11 (stuck, leaf) +┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , +┃ ┃ span: 32 +┃ ┃ +┃ ┣━━┓ +┃ ┃ │ +┃ ┃ ├─ 9 +┃ ┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId +┃ ┃ │ function: main +┃ ┃ │ +┃ ┃ │ (6 steps) +┃ ┃ └─ 12 (stuck, leaf) +┃ ┃ #ProgramError ( ReachedUnreachable ) ~> .K +┃ ┃ function: main +┃ ┃ +┃ ┗━━┓ +┃ │ +┃ └─ 10 (stuck, leaf) +┃ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 1 ) ) +┃ function: main +┃ +┗━━┓ + │ + └─ 6 (stuck, leaf) + #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) + function: main + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 5f36b155d..2e0d79ef1 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -62,6 +62,7 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', + 'enum-direct-tag-decode', ] From 5ef51f41ef50f3169f07ba2b41c29fa9b834d53e Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 4 Mar 2026 14:41:24 +0800 Subject: [PATCH 2/3] fix(rt): generalize direct-tag enum decoding to any variant count and discriminant Replace the specialized #decodeOptionTag01 rule (only handles 0+1 field pattern with discriminants exactly 0/1) with a general #decodeEnumDirect decoder that handles: - Any number of variants (not just two) - Any discriminant values (not just 0 and 1) - Any unsigned integer tag width (u8, u16, etc.) - Any number of fields per variant New K helper functions (all total with owise fallbacks): - #decodeEnumDirect: decode tag, find variant index, dispatch - #decodeEnumDirectAt: look up variant fields/offsets, decode fields - #decodeEnumDirectTag: read tag bytes as unsigned LE integer - #nthTys: index into per-variant field type lists - #nthVariantOffsets: extract offsets from nth variant layout --- .../kmir/kdist/mir-semantics/rt/decoding.md | 84 +++++++++++++------ .../show/enum-direct-tag-decode.main.expected | 68 ++------------- 2 files changed, 68 insertions(+), 84 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index 0ac8cff08..98b522012 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -297,27 +297,26 @@ If there are no fields, the enum can be decoded by using their data as the discr requires TAG =/=Int DISCRIMINANT ``` -#### Enums with two variants +#### Enums with direct tag encoding and fields -Having two variants with possibly zero or one field each is a very common case, -it includes a number of standard library types such as `Option` and `Result`. - -The following rules are specialised to the case of encoding an `Option`. -An important distinction here is whether or not the tag is niche-encoded. -If the option holds data that has all-zero as a possible value, a separate tag is used, usually as the first field. -In both cases we expect the tag to be in the single shared field, and the discriminant to be just 0 and 1. +Decodes any enum with `tagEncodingDirect` and a `primitiveInt` tag, +with arbitrary variant counts, discriminant values, and field counts per variant. +The tag is read as an unsigned little-endian integer, matched against the discriminant +list to find the variant index, and then the variant's fields are decoded using the +per-variant layout offsets. ```k + // General entry rule: direct-tag enum with at least one field somewhere. rule #decodeValue( BYTES , typeInfoEnumType(... name: _ , adtDef: _ - , discriminants: discriminant(0) discriminant(1) .Discriminants - , fields: (.Tys : (FIELD_TYPE .Tys) : .Tyss) + , discriminants: DISCRIMINANTS + , fields: FIELD_TYPESS , layout: someLayoutShape(layoutShape(... - fields: fieldsShapeArbitrary(mk(... offsets: machineSize(0) .MachineSizes)) + fields: _FIELDS , variants: variantsShapeMultiple( mk(... @@ -329,7 +328,7 @@ In both cases we expect the tag to be in the single shared field, and the discri ) , tagEncoding: tagEncodingDirect , tagField: 0 - , variants: _VARIANTS + , variants: VARIANT_LAYOUTS ) ) , abi: _ABI @@ -338,22 +337,59 @@ In both cases we expect the tag to be in the single shared field, and the discri )) ) #as ENUM_TYPE ) - => #decodeOptionTag01(BYTES, TAG_WIDTH, FIELD_TYPE, ENUM_TYPE) - - syntax Evaluation ::= #decodeOptionTag01 ( Bytes , IntegerLength , Ty , TypeInfo ) [function, total] - // -------------------------------------------------------------------------------------- - rule #decodeOptionTag01(BYTES, _LEN, _TY, _ENUM_TYPE) - => Aggregate(variantIdx(0), .List) - requires 0 ==Int BYTES[0] // expect only 0 or 1 as tags, so higher bytes do not matter - [preserves-definedness] - rule #decodeOptionTag01(BYTES, LEN, TY, _ENUM_TYPE) - => Aggregate(variantIdx(1), ListItem(#decodeValue(substrBytes(BYTES, #byteLength(LEN), lengthBytes(BYTES)), lookupTy(TY)))) - requires 1 ==Int BYTES[0] // expect only 0 or 1 as tags, so higher bytes do not matter + => #decodeEnumDirectFields( + BYTES, + #findVariantIdx(#decodeEnumDirectTag(BYTES, TAG_WIDTH), DISCRIMINANTS), + FIELD_TYPESS, + VARIANT_LAYOUTS, + ENUM_TYPE + ) + requires notBool #noFields(FIELD_TYPESS) + + // --------------------------------------------------------------------------- + // #decodeEnumDirectFields: given the variant index, decode its fields + // --------------------------------------------------------------------------- + syntax Evaluation ::= #decodeEnumDirectFields ( Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total] + // -------------------------------------------------------------------------------------------------------------------------- + rule #decodeEnumDirectFields(BYTES, variantIdx(IDX), FIELD_TYPESS, VARIANT_LAYOUTS, _ENUM_TYPE) + => Aggregate( + variantIdx(IDX), + #decodeFieldsWithOffsets(BYTES, #nthTys(FIELD_TYPESS, IDX), #nthVariantOffsets(VARIANT_LAYOUTS, IDX)) + ) + requires 0 <=Int IDX [preserves-definedness] - rule #decodeOptionTag01(BYTES, _LEN, _TY, ENUM_TYPE) + + // Error cases: variant not found or other failure + rule #decodeEnumDirectFields(BYTES, _, _FIELD_TYPESS, _VARIANT_LAYOUTS, ENUM_TYPE) => UnableToDecode(BYTES, ENUM_TYPE) [owise] + // --------------------------------------------------------------------------- + // #decodeEnumDirectTag: read the tag bytes as an unsigned little-endian int + // --------------------------------------------------------------------------- + syntax Int ::= #decodeEnumDirectTag ( Bytes , IntegerLength ) [function, total] + rule #decodeEnumDirectTag(BYTES, TAG_WIDTH) + => Bytes2Int(substrBytes(BYTES, 0, #byteLength(TAG_WIDTH)), LE, Unsigned) + requires lengthBytes(BYTES) >=Int #byteLength(TAG_WIDTH) + [preserves-definedness] + rule #decodeEnumDirectTag(_, _) => -1 [owise] + + // --------------------------------------------------------------------------- + // List-indexing helpers + // --------------------------------------------------------------------------- + + // Index into a Tyss (list of per-variant field type lists) + syntax Tys ::= #nthTys ( Tyss , Int ) [function, total] + rule #nthTys(TYS : _REST, 0) => TYS + rule #nthTys(_TYS : REST, N) => #nthTys(REST, N -Int 1) requires N >Int 0 + rule #nthTys(_, _) => .Tys [owise] + + // Index into variant layouts and extract field offsets in one step (total) + syntax MachineSizes ::= #nthVariantOffsets ( LayoutShapes , Int ) [function, total] + rule #nthVariantOffsets(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _) _REST, 0) => OFFSETS + rule #nthVariantOffsets(_L REST, N) => #nthVariantOffsets(REST, N -Int 1) requires N >Int 0 + rule #nthVariantOffsets(_, _) => .MachineSizes [owise] + syntax Int ::= #byteLength ( IntegerLength ) [function, total] // ----------------------------------------------------------- rule #byteLength(integerLengthI8 ) => 1 diff --git a/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected b/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected index eae2f3bd1..be5648a4f 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected @@ -3,67 +3,15 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (33 steps) -├─ 3 -│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) +│ (631 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K │ function: main -┃ -┃ (1 step) -┣━━┓ -┃ │ -┃ ├─ 4 -┃ │ #execBlockIdx ( basicBlockIdx ( 2 ) ) ~> .K -┃ │ function: main -┃ │ -┃ │ (9 steps) -┃ └─ 7 (stuck, leaf) -┃ #traverseProjection ( toLocal ( 2 ) , thunk ( UnableToDecode ( b"\x00\x01" , typ -┃ function: main -┃ span: 50 -┃ -┣━━┓ -┃ │ -┃ ├─ 5 -┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 1 ) ) -┃ │ function: main -┃ ┃ -┃ ┃ (1 step) -┃ ┣━━┓ -┃ ┃ │ -┃ ┃ ├─ 8 -┃ ┃ │ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K -┃ ┃ │ function: main -┃ ┃ │ -┃ ┃ │ (28 steps) -┃ ┃ └─ 11 (stuck, leaf) -┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , -┃ ┃ span: 32 -┃ ┃ -┃ ┣━━┓ -┃ ┃ │ -┃ ┃ ├─ 9 -┃ ┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId -┃ ┃ │ function: main -┃ ┃ │ -┃ ┃ │ (6 steps) -┃ ┃ └─ 12 (stuck, leaf) -┃ ┃ #ProgramError ( ReachedUnreachable ) ~> .K -┃ ┃ function: main -┃ ┃ -┃ ┗━━┓ -┃ │ -┃ └─ 10 (stuck, leaf) -┃ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 1 ) ) -┃ function: main -┃ -┗━━┓ - │ - └─ 6 (stuck, leaf) - #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) - function: main - +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K From 77713ea3899aad7b5b861b458b1cc11a269fc8d5 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 4 Mar 2026 21:59:27 +0800 Subject: [PATCH 3/3] test(prove-rs): remove enum-direct-tag-decode from show list --- .../show/enum-direct-tag-decode.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 2 files changed, 18 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected b/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected deleted file mode 100644 index be5648a4f..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/enum-direct-tag-decode.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (631 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 2e0d79ef1..5f36b155d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -62,7 +62,6 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'enum-direct-tag-decode', ]