From 995caf64e3f136a8a5a0e1da5975a002f7f59e37 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 30 Jan 2026 17:39:49 +1100 Subject: [PATCH 1/3] refactor discriminant lookup (use only one function): master --- .../kdist/mir-semantics/lemmas/kmir-lemmas.md | 8 ++---- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 28 +++++++++++++------ 2 files changed, 21 insertions(+), 15 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md index b00b557b0..15a524153 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -79,18 +79,14 @@ Definedness of the list and list elements is also guaranteed. For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored: ```k - syntax Int ::= size(Discriminants) [function, total] - rule size(.Discriminants) => 0 - rule size(discriminant(_) REST) => 1 +Int size(REST) - - rule #Ceil(#lookupDiscrAux(DISCRS:Discriminants, I:Int)) + rule #Ceil(#lookupDiscrAux(DISCRS:Discriminants, variantIdx(I))) => #Ceil(DISCRS) #And #Ceil(I) #And {true #Equals 0 <=Int I} #And {true #Equals I DISCR + rule #lookupDiscrAux(DISCRS, #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR requires isOneOf(DISCR, DISCRS) [simplification, preserves-definedness, symbolic(DISCR)] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 1ff99eeaf..c71c9ffe1 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1111,21 +1111,31 @@ The `getTyOf` helper applies the projections from the `Place` to determine the ` [preserves-definedness] // valid indexing and sort coercion syntax Evaluation ::= #discriminant ( Evaluation , MaybeTy ) [strict(1)] + | #discriminantFor ( VariantIdx , TypeInfo ) // ---------------------------------------------------------------- rule #discriminant(Aggregate(IDX, _), TY:Ty) - => Integer(#lookupDiscriminant(lookupTy(TY), IDX), 0, false) // HACK: bit width 0 means "flexible" + => #discriminantFor(IDX, lookupTy(TY)) + ... + + + rule #discriminantFor(variantIdx(I) #as IDX, typeInfoEnumType(_, _, DISCRIMINANTS:Discriminants, _, _)) + => Integer(#lookupDiscrAux(DISCRIMINANTS, IDX), 0, false) // HACK: bit width 0 means "flexible" ... + requires I <=Int size(DISCRIMINANTS) + [preserves-definedness] - syntax Int ::= #lookupDiscriminant ( TypeInfo , VariantIdx ) [function, total] - | #lookupDiscrAux ( Discriminants , Int ) [function] - // -------------------------------------------------------------------- - rule #lookupDiscriminant(typeInfoEnumType(_, _, DISCRIMINANTS, _, _), variantIdx(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. + syntax Int ::= size(Discriminants) [function, total] + rule size(.Discriminants) => 0 + rule size(discriminant(_) REST) => 1 +Int size(REST) + + // default 0 for non-enum types. May be undefined behaviour, though. + // rule #discriminant(_, _) => 0 [owise] + + syntax Int ::= #lookupDiscrAux ( Discriminants , VariantIdx ) [function] // -------------------------------------------------------------------- - rule #lookupDiscrAux( discriminant(RESULT) _ , IDX) => RESULT requires IDX ==Int 0 - rule #lookupDiscrAux( _:Discriminant MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX -Int 1) requires 0 RESULT requires I ==Int 0 + rule #lookupDiscrAux( _:Discriminant MORE:Discriminants, variantIdx(I)) => #lookupDiscrAux(MORE, variantIdx(I -Int 1)) requires 0 Date: Fri, 30 Jan 2026 20:00:27 +1100 Subject: [PATCH 2/3] adjust step counts in integration tests after refactoring --- deps/stable-mir-json | 2 +- .../data/crate-tests/two-crate-bin/crate2::main.expected | 2 +- .../two-crate-dylib/crate2::test_crate1_with.expected | 2 +- .../data/prove-rs/show/interior-mut-fail.main.expected | 2 +- .../data/prove-rs/show/iter_next_2-fail.main.expected | 2 +- .../integration/data/prove-rs/show/niche-enum.main.expected | 2 +- ...te-u8-to-enum-changed-discriminant-signed-fail.main.expected | 2 +- kmir/src/tests/integration/test_integration.py | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/deps/stable-mir-json b/deps/stable-mir-json index a5b714d89..e9395d9b7 160000 --- a/deps/stable-mir-json +++ b/deps/stable-mir-json @@ -1 +1 @@ -Subproject commit a5b714d89d0c12c7f4b00602a95ad2d3a34530f0 +Subproject commit e9395d9b763f1e78ed19ee106c6ab4f0128566a7 diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 9dbc45230..953882c36 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (736 steps) +│ (741 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected index bd3076868..bdade977c 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (216 steps) +│ (217 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected index 44581b4f2..c8c46f143 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (877 steps) +│ (879 steps) └─ 3 (stuck, leaf) #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected index 70f8119ac..9d18ac532 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (2000 steps) +│ (2003 steps) └─ 3 (stuck, leaf) #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio span: 146 diff --git a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected index 586c10ed1..1dee9274c 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (740 steps) +│ (750 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main 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 index ce7aaeddb..9eac44985 100644 --- 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 @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (102 steps) +│ (103 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo span: 153 diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index f3e172edd..93f575554 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -246,7 +246,7 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo EXEC_DATA_DIR / 'references' / 'weirdRefs.state', None, ), - ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 136), + ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 139), ( 'Array-indexing', EXEC_DATA_DIR / 'arrays' / 'array_indexing.smir.json', From b601b980a6a1e3db829bcf85fc4edbab69f2987d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 30 Jan 2026 20:19:49 +1100 Subject: [PATCH 3/3] revert submodule bump --- 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 e9395d9b7..a5b714d89 160000 --- a/deps/stable-mir-json +++ b/deps/stable-mir-json @@ -1 +1 @@ -Subproject commit e9395d9b763f1e78ed19ee106c6ab4f0128566a7 +Subproject commit a5b714d89d0c12c7f4b00602a95ad2d3a34530f0