From e60ca3ff1d97fe7995b25e8f64eb7d4e910b2f46 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sat, 28 Feb 2026 10:13:49 +0800 Subject: [PATCH 1/4] fix(decode): accept signed enum tag scalars in _extract_tag Some enums (e.g. 3-variant enums) use signed tag metadata in SMIR. Stable MIR discriminants represent raw tag bits, so unsigned decoding is always correct regardless of the signed flag. Change the pattern match from signed=False to signed=_ to accept both. Test: enum-3-variants-0-fields-signed-tag decode fixture. --- kmir/src/kmir/decoding.py | 4 +- ...um-3-variants-0-fields-signed-tag.expected | 1 + .../enum-3-variants-0-fields-signed-tag.json | 138 ++++++++++++++++++ 3 files changed, 142 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected create mode 100644 kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py index 4d0dc95fb..27a2dc019 100644 --- a/kmir/src/kmir/decoding.py +++ b/kmir/src/kmir/decoding.py @@ -445,10 +445,12 @@ def _extract_tag(*, data: bytes, tag_offset: MachineSize, tag: Scalar) -> tuple[ case Initialized( value=PrimitiveInt( length=length, - signed=False, + signed=_, ), valid_range=_, ): + # Stable MIR enum discriminants are represented against the raw tag bits. + # Use unsigned decoding even when the scalar metadata marks the tag as signed. tag_data = data[tag_offset.in_bytes : tag_offset.in_bytes + length.value] tag_value = int.from_bytes(tag_data, byteorder='little', signed=False) return tag_value, length diff --git a/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected new file mode 100644 index 000000000..8916e2b4d --- /dev/null +++ b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected @@ -0,0 +1 @@ +Aggregate ( variantIdx ( 1 ) , .List ) diff --git a/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json new file mode 100644 index 000000000..3696e0d04 --- /dev/null +++ b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json @@ -0,0 +1,138 @@ +{ + "bytes": [ + 0 + ], + "types": [], + "typeInfo": { + "EnumType": { + "name": "OrderingLike", + "adt_def": 72, + "discriminants": [ + 255, + 0, + 1 + ], + "fields": [ + [], + [], + [] + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Multiple": { + "tag": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": true + } + }, + "valid_range": { + "start": 255, + "end": 1 + } + } + }, + "tag_encoding": "Direct", + "tag_field": 0, + "variants": [ + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + }, + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 1 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + }, + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 2 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + ] + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": true + } + }, + "valid_range": { + "start": 255, + "end": 1 + } + } + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + } + } +} From 1e130dfc4ebe71887565190ae31282f3d6ecad09 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sat, 28 Feb 2026 21:02:56 +0800 Subject: [PATCH 2/4] Align signed discriminant transmute test with passing semantics --- ...anged-discriminant-signed-fail.main.expected | 15 --------------- ...um-changed-discriminant-signed.main.expected | 17 +++++++++++++++++ ...e-u8-to-enum-changed-discriminant-signed.rs} | 0 kmir/src/tests/integration/test_integration.py | 2 +- 4 files changed, 18 insertions(+), 16 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected rename kmir/src/tests/integration/data/prove-rs/{transmute-u8-to-enum-changed-discriminant-signed-fail.rs => transmute-u8-to-enum-changed-discriminant-signed.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected deleted file mode 100644 index ce7aaeddb..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (102 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo - span: 153 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected new file mode 100644 index 000000000..a46a576eb --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected @@ -0,0 +1,17 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (823 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index f4975bd29..0423216ad 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -54,7 +54,7 @@ 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', - 'transmute-u8-to-enum-changed-discriminant-signed-fail', + 'transmute-u8-to-enum-changed-discriminant-signed', 'assert-inhabited-fail', 'iterator-simple', 'unions-fail', From 6167019e9718be0ccba72b7f7e31e3647c71d843 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 10:55:23 +0800 Subject: [PATCH 3/4] test(integration): drop signed discriminant case from show specs --- kmir/src/tests/integration/test_integration.py | 1 - 1 file changed, 1 deletion(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 0423216ad..5f36b155d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -54,7 +54,6 @@ 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', - 'transmute-u8-to-enum-changed-discriminant-signed', 'assert-inhabited-fail', 'iterator-simple', 'unions-fail', From efc7edf58ccad9518618aced6a62ddda1d12fc51 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 10:58:51 +0800 Subject: [PATCH 4/4] test(integration): remove stale signed-discriminant show snapshot --- ...um-changed-discriminant-signed.main.expected | 17 ----------------- 1 file changed, 17 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected deleted file mode 100644 index a46a576eb..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (823 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - -