From 4d2b75aba2eac74a6cf8478957ffe44e2bcdb030 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 07:55:22 +0000 Subject: [PATCH 1/7] refactor(tests): distinguish -fail (program error) from -unsupported (missing semantics) Rename 19 prove-rs test files from `-fail` to `-unsupported` to clarify that they fail because the semantics doesn't support the feature yet, not because the program itself is expected to fail. Co-Authored-By: Claude Opus 4.6 (1M context) --- ...-fail.rs => box_heap_alloc-unsupported.rs} | 0 ...s-fail.rs => enum-two-refs-unsupported.rs} | 0 ...ut-fail.rs => interior-mut-unsupported.rs} | 0 ...3-fail.rs => interior-mut3-unsupported.rs} | 0 ...l-raw-fail.rs => local-raw-unsupported.rs} | 0 .../{loop-fail.rs => loop-unsupported.rs} | 0 ...et-u8-fail.rs => offset-u8-unsupported.rs} | 0 ...> pointer-cast-length-test-unsupported.rs} | 0 ...st-array-to-nested-wrapper-unsupported.rs} | 0 ...to-singleton-wrapped-array-unsupported.rs} | 0 ... ptr-cast-array-to-wrapper-unsupported.rs} | 0 ....rs => ptr-through-wrapper-unsupported.rs} | 0 ...st-fail.rs => raw-ptr-cast-unsupported.rs} | 0 ...> ref-ptr-cast-elem-offset-unsupported.rs} | 0 ...il.rs => ref-ptr-cast-elem-unsupported.rs} | 0 ... box_heap_alloc-unsupported.main.expected} | 0 ...=> interior-mut-unsupported.main.expected} | 0 ...> interior-mut3-unsupported.main.expected} | 0 ...ed => local-raw-unsupported.main.expected} | 0 ...ed => offset-u8-unsupported.main.expected} | 0 ...test-unsupported.array_cast_test.expected} | 0 ...-nested-wrapper-unsupported.main.expected} | 0 ...n-wrapped-array-unsupported.main.expected} | 0 ...rray-to-wrapper-unsupported.main.expected} | 0 ...through-wrapper-unsupported.main.expected} | 0 ...=> raw-ptr-cast-unsupported.main.expected} | 0 ...ast-elem-offset-unsupported.main.expected} | 0 ...f-ptr-cast-elem-unsupported.main.expected} | 0 ...te-maybe-uninit-unsupported.main.expected} | 0 ...ected => unions-unsupported.main.expected} | 0 ...ile_load_static-unsupported.main.expected} | 0 ...le_store_static-unsupported.main.expected} | 0 ... => transmute-maybe-uninit-unsupported.rs} | 0 .../{unions-fail.rs => unions-unsupported.rs} | 0 ...rs => volatile_load_static-unsupported.rs} | 0 ...s => volatile_store_static-unsupported.rs} | 0 .../src/tests/integration/test_integration.py | 38 +++++++++---------- 37 files changed, 19 insertions(+), 19 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{box_heap_alloc-fail.rs => box_heap_alloc-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{enum-two-refs-fail.rs => enum-two-refs-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{interior-mut-fail.rs => interior-mut-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{interior-mut3-fail.rs => interior-mut3-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{local-raw-fail.rs => local-raw-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{loop-fail.rs => loop-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{offset-u8-fail.rs => offset-u8-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{pointer-cast-length-test-fail.rs => pointer-cast-length-test-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{ptr-cast-array-to-nested-wrapper-fail.rs => ptr-cast-array-to-nested-wrapper-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{ptr-cast-array-to-singleton-wrapped-array-fail.rs => ptr-cast-array-to-singleton-wrapped-array-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{ptr-cast-array-to-wrapper-fail.rs => ptr-cast-array-to-wrapper-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{ptr-through-wrapper-fail.rs => ptr-through-wrapper-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{raw-ptr-cast-fail.rs => raw-ptr-cast-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{ref-ptr-cast-elem-offset-fail.rs => ref-ptr-cast-elem-offset-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{ref-ptr-cast-elem-fail.rs => ref-ptr-cast-elem-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{box_heap_alloc-fail.main.expected => box_heap_alloc-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{interior-mut-fail.main.expected => interior-mut-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{interior-mut3-fail.main.expected => interior-mut3-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{local-raw-fail.main.expected => local-raw-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{offset-u8-fail.main.expected => offset-u8-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{pointer-cast-length-test-fail.array_cast_test.expected => pointer-cast-length-test-unsupported.array_cast_test.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{ptr-cast-array-to-nested-wrapper-fail.main.expected => ptr-cast-array-to-nested-wrapper-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{ptr-cast-array-to-singleton-wrapped-array-fail.main.expected => ptr-cast-array-to-singleton-wrapped-array-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{ptr-cast-array-to-wrapper-fail.main.expected => ptr-cast-array-to-wrapper-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{ptr-through-wrapper-fail.main.expected => ptr-through-wrapper-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{raw-ptr-cast-fail.main.expected => raw-ptr-cast-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{ref-ptr-cast-elem-offset-fail.main.expected => ref-ptr-cast-elem-offset-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{ref-ptr-cast-elem-fail.main.expected => ref-ptr-cast-elem-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{transmute-maybe-uninit-fail.main.expected => transmute-maybe-uninit-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{unions-fail.main.expected => unions-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{volatile_load_static-fail.main.expected => volatile_load_static-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{volatile_store_static-fail.main.expected => volatile_store_static-unsupported.main.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/{transmute-maybe-uninit-fail.rs => transmute-maybe-uninit-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{unions-fail.rs => unions-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{volatile_load_static-fail.rs => volatile_load_static-unsupported.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{volatile_store_static-fail.rs => volatile_store_static-unsupported.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs b/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs rename to kmir/src/tests/integration/data/prove-rs/box_heap_alloc-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/enum-two-refs-fail.rs b/kmir/src/tests/integration/data/prove-rs/enum-two-refs-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/enum-two-refs-fail.rs rename to kmir/src/tests/integration/data/prove-rs/enum-two-refs-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut3-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut3-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/local-raw-fail.rs b/kmir/src/tests/integration/data/prove-rs/local-raw-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/local-raw-fail.rs rename to kmir/src/tests/integration/data/prove-rs/local-raw-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/loop-fail.rs b/kmir/src/tests/integration/data/prove-rs/loop-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/loop-fail.rs rename to kmir/src/tests/integration/data/prove-rs/loop-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/offset-u8-fail.rs b/kmir/src/tests/integration/data/prove-rs/offset-u8-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/offset-u8-fail.rs rename to kmir/src/tests/integration/data/prove-rs/offset-u8-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/pointer-cast-length-test-fail.rs b/kmir/src/tests/integration/data/prove-rs/pointer-cast-length-test-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/pointer-cast-length-test-fail.rs rename to kmir/src/tests/integration/data/prove-rs/pointer-cast-length-test-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs rename to kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-unsupported.main.expected 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-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/interior-mut-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/interior-mut3-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/local-raw-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/offset-u8-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-unsupported.array_cast_test.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected rename to kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-unsupported.array_cast_test.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/unions-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/unions-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute-maybe-uninit-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/unions-fail.rs b/kmir/src/tests/integration/data/prove-rs/unions-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/unions-fail.rs rename to kmir/src/tests/integration/data/prove-rs/unions-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_load_static-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs rename to kmir/src/tests/integration/data/prove-rs/volatile_load_static-unsupported.rs diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_store_static-unsupported.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs rename to kmir/src/tests/integration/data/prove-rs/volatile_store_static-unsupported.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d6e891398..e57d81609 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -33,7 +33,7 @@ 'unchecked_arithmetic': ['unchecked_add_i32', 'unchecked_sub_usize', 'unchecked_mul_isize'], 'checked_arithmetic-fail': ['checked_add_i32'], 'pointer-cast': ['main', 'test'], - 'pointer-cast-length-test-fail': ['array_cast_test'], + 'pointer-cast-length-test-unsupported': ['array_cast_test'], 'assume-cheatcode': ['check_assume'], 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], @@ -42,35 +42,35 @@ 'spl-multisig-iter-eq-copied-next': ['repro'], } PROVE_SHOW_SPECS = [ - 'local-raw-fail', - 'interior-mut-fail', - 'interior-mut3-fail', + 'local-raw-unsupported', + 'interior-mut-unsupported', + 'interior-mut3-unsupported', 'iter_next_3', 'assert_eq_exp', 'bitwise-not-shift', 'symbolic-args-fail', 'symbolic-structs-fail', 'checked_arithmetic-fail', - 'offset-u8-fail', - 'pointer-cast-length-test-fail', + 'offset-u8-unsupported', + 'pointer-cast-length-test-unsupported', 'niche-enum', 'assume-cheatcode-conflict-fail', - 'raw-ptr-cast-fail', + 'raw-ptr-cast-unsupported', 'transmute-u8-to-enum-fail', 'assert-inhabited-fail', 'iterator-simple', - 'unions-fail', - 'transmute-maybe-uninit-fail', - 'ptr-through-wrapper-fail', + 'unions-unsupported', + 'transmute-maybe-uninit-unsupported', + 'ptr-through-wrapper-unsupported', 'test_offset_from-fail', - 'ref-ptr-cast-elem-fail', - 'ref-ptr-cast-elem-offset-fail', - 'volatile_store_static-fail', - 'volatile_load_static-fail', - 'box_heap_alloc-fail', - 'ptr-cast-array-to-wrapper-fail', - 'ptr-cast-array-to-nested-wrapper-fail', - 'ptr-cast-array-to-singleton-wrapped-array-fail', + 'ref-ptr-cast-elem-unsupported', + 'ref-ptr-cast-elem-offset-unsupported', + 'volatile_store_static-unsupported', + 'volatile_load_static-unsupported', + 'box_heap_alloc-unsupported', + 'ptr-cast-array-to-wrapper-unsupported', + 'ptr-cast-array-to-nested-wrapper-unsupported', + 'ptr-cast-array-to-singleton-wrapped-array-unsupported', ] @@ -80,7 +80,7 @@ ids=[spec.stem for spec in PROVE_FILES], ) def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: - should_fail = rs_file.stem.endswith('fail') + should_fail = rs_file.stem.endswith('fail') or rs_file.stem.endswith('unsupported') should_show = rs_file.stem in PROVE_SHOW_SPECS is_smir = rs_file.suffix == '.json' From 784d826cfd51c5d112e1ffb1e6aa10a962e0a678 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 08:02:38 +0000 Subject: [PATCH 2/7] refactor(tests): auto-detect show specs from -fail/-unsupported suffix Remove the manually maintained PROVE_SHOW_SPECS list. All -fail and -unsupported tests now automatically verify show output; passing tests only assert proof success. Remove 5 show expected files for passing tests that no longer need show verification. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../prove-rs/show/assert_eq_exp.main.expected | 17 ------- .../show/bitwise-not-shift.main.expected | 17 ------- .../prove-rs/show/iter_next_3.main.expected | 17 ------- .../show/iterator-simple.main.expected | 17 ------- .../prove-rs/show/niche-enum.main.expected | 17 ------- .../src/tests/integration/test_integration.py | 44 ++----------------- 6 files changed, 4 insertions(+), 125 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected deleted file mode 100644 index 3fe017dcf..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (148 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/show/bitwise-not-shift.main.expected b/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected deleted file mode 100644 index 6cf403b84..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (837 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/show/iter_next_3.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected deleted file mode 100644 index a4c5bdc3d..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (2028 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/show/iterator-simple.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected deleted file mode 100644 index f1cd9a4d1..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (798 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/show/niche-enum.main.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected deleted file mode 100644 index 586c10ed1..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (740 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 e57d81609..fb91c4742 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -41,39 +41,6 @@ 'iter-eq-copied-take-dereftruncate': ['repro'], 'spl-multisig-iter-eq-copied-next': ['repro'], } -PROVE_SHOW_SPECS = [ - 'local-raw-unsupported', - 'interior-mut-unsupported', - 'interior-mut3-unsupported', - 'iter_next_3', - 'assert_eq_exp', - 'bitwise-not-shift', - 'symbolic-args-fail', - 'symbolic-structs-fail', - 'checked_arithmetic-fail', - 'offset-u8-unsupported', - 'pointer-cast-length-test-unsupported', - 'niche-enum', - 'assume-cheatcode-conflict-fail', - 'raw-ptr-cast-unsupported', - 'transmute-u8-to-enum-fail', - 'assert-inhabited-fail', - 'iterator-simple', - 'unions-unsupported', - 'transmute-maybe-uninit-unsupported', - 'ptr-through-wrapper-unsupported', - 'test_offset_from-fail', - 'ref-ptr-cast-elem-unsupported', - 'ref-ptr-cast-elem-offset-unsupported', - 'volatile_store_static-unsupported', - 'volatile_load_static-unsupported', - 'box_heap_alloc-unsupported', - 'ptr-cast-array-to-wrapper-unsupported', - 'ptr-cast-array-to-nested-wrapper-unsupported', - 'ptr-cast-array-to-singleton-wrapped-array-unsupported', -] - - @pytest.mark.parametrize( 'rs_file', PROVE_FILES, @@ -81,10 +48,9 @@ ) def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: should_fail = rs_file.stem.endswith('fail') or rs_file.stem.endswith('unsupported') - should_show = rs_file.stem in PROVE_SHOW_SPECS is_smir = rs_file.suffix == '.json' - if update_expected_output and not should_show: + if update_expected_output and not should_fail: pytest.skip() prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=True) @@ -99,7 +65,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: prove_opts.start_symbol = start_symbol apr_proof = kmir.prove_program(prove_opts) - if should_show: + if should_fail: + assert apr_proof.failed display_opts = ShowOpts( rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False ) @@ -108,11 +75,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: assert_or_update_show_output( show_res, PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected', update=update_expected_output ) - - if not should_fail: - assert apr_proof.passed else: - assert apr_proof.failed + assert apr_proof.passed VERIFY_RUST_STD_DIR = (Path(__file__).parent / 'data' / 'verify-rust-std').resolve(strict=True) From c94059705f69ec9d42502cd3117839127e50ab42 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 08:26:40 +0000 Subject: [PATCH 3/7] refactor(tests): rename symbolic-args-fail to symbolic-args-unsupported MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove artificial `assert!(false)` from main — it passes with concrete args. Keep only `eats_all_args` as proof entry (stuck on raw pointer deref and slice ops). Update test_cli.py references accordingly. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../show/symbolic-args-fail.main.expected | 15 --------------- ...bolic-args-unsupported.eats_all_args.expected} | 0 ...gs-unsupported.main.cli-stats-leaves.expected} | 0 ...-args-fail.rs => symbolic-args-unsupported.rs} | 2 -- kmir/src/tests/integration/test_cli.py | 8 ++++---- kmir/src/tests/integration/test_integration.py | 2 +- 6 files changed, 5 insertions(+), 22 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/show/{symbolic-args-fail.eats_all_args.expected => symbolic-args-unsupported.eats_all_args.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/show/{symbolic-args-fail.main.cli-stats-leaves.expected => symbolic-args-unsupported.main.cli-stats-leaves.expected} (100%) rename kmir/src/tests/integration/data/prove-rs/{symbolic-args-fail.rs => symbolic-args-unsupported.rs} (93%) diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected deleted file mode 100644 index e5b630195..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (566 steps) -└─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h - span: 32 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.eats_all_args.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected rename to kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.eats_all_args.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.main.cli-stats-leaves.expected similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected rename to kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.main.cli-stats-leaves.expected diff --git a/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs b/kmir/src/tests/integration/data/prove-rs/symbolic-args-unsupported.rs similarity index 93% rename from kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs rename to kmir/src/tests/integration/data/prove-rs/symbolic-args-unsupported.rs index eca505036..af235308e 100644 --- a/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs +++ b/kmir/src/tests/integration/data/prove-rs/symbolic-args-unsupported.rs @@ -49,6 +49,4 @@ fn main() { let mut a1 = [1, 2, 3]; let a2 = [1, 2, 3]; eats_all_args(1, &mut x2, true, my1, e4, &mut a1, &a2, &mut [my2, my3], &my4 as *const MyStruct<'_>); - - assert!(false); // makes the test with main fail, as the other one also fails } diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py index 9396e5fc5..60b314140 100644 --- a/kmir/src/tests/integration/test_cli.py +++ b/kmir/src/tests/integration/test_cli.py @@ -19,7 +19,7 @@ PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) MODULES_DIR = (Path(__file__).parent / 'data' / 'modules').resolve(strict=True) # Repo root: used to normalise absolute paths in expected-output snapshots so -# they don't differ between local checkouts and CI (e.g. symbolic-args-fail.main.cli-stats-leaves). +# they don't differ between local checkouts and CI (e.g. symbolic-args-unsupported.main.cli-stats-leaves). _REPO_ROOT = str(Path(__file__).resolve().parents[4]) _PATH_REPLACEMENTS: dict[str, str] = {_REPO_ROOT + '/': '/'} @@ -84,10 +84,10 @@ def test_cli_show_printers_snapshot( 'src,start_symbol,is_smir', [ pytest.param( - (PROVE_DIR / 'symbolic-args-fail.rs'), + (PROVE_DIR / 'symbolic-args-unsupported.rs'), 'main', False, - id='symbolic-args-fail.main', + id='symbolic-args-unsupported.main', ), pytest.param( (Path(__file__).parent / 'data' / 'exec-smir' / 'niche-enum' / 'niche-enum.smir.json').resolve(strict=True), @@ -242,7 +242,7 @@ def test_cli_show_to_module( def test_cli_show_minimize_proof(kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str]) -> None: """Test --minimize-proof option.""" - rs_file = PROVE_DIR / 'symbolic-args-fail.rs' + rs_file = PROVE_DIR / 'symbolic-args-unsupported.rs' start_symbol = 'main' # Use limited depth to create a partial proof with intermediate nodes that can be minimized apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False, max_depth=5) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index fb91c4742..5732098ee 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -28,7 +28,7 @@ PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) PROVE_FILES = list(PROVE_DIR.glob('*.*')) PROVE_START_SYMBOLS = { - 'symbolic-args-fail': ['main', 'eats_all_args'], + 'symbolic-args-unsupported': ['eats_all_args'], 'symbolic-structs-fail': ['eats_struct_args'], 'unchecked_arithmetic': ['unchecked_add_i32', 'unchecked_sub_usize', 'unchecked_mul_isize'], 'checked_arithmetic-fail': ['checked_add_i32'], From 63bead9e61c684a3055bd898fe89e1a467437baa Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 08:35:02 +0000 Subject: [PATCH 4/7] refactor(tests): use stable -fail fixture for CLI tests Switch test_cli_show_statistics_and_leaves and test_cli_show_minimize_proof to use symbolic-structs-fail with eats_struct_args entry. This provides a stable proof tree with symbolic branching (splits), unlike the previous symbolic-args fixture whose main entry now passes. Co-Authored-By: Claude Opus 4.6 (1M context) --- ...unsupported.main.cli-stats-leaves.expected | 38 ------- ...eats_struct_args.cli-stats-leaves.expected | 107 ++++++++++++++++++ kmir/src/tests/integration/test_cli.py | 14 +-- 3 files changed, 114 insertions(+), 45 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.main.cli-stats-leaves.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.cli-stats-leaves.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.main.cli-stats-leaves.expected deleted file mode 100644 index e4e10b74c..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-unsupported.main.cli-stats-leaves.expected +++ /dev/null @@ -1,38 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: src/rust/library/std/src/rt.rs:194 -│ -│ (566 steps) -└─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h - span: no-location:0 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - - -STATISTICS ------------ -Total nodes: 1 - -Node roles (exclusive): - failing : 1 ids: 3 - (root nodes omitted from totals: 1, 2) - -Leaf paths from init: - total leaves (non-root): 1 - reachable leaves : 1 - total steps : 566 - - leaf 3: steps 566, path 1 -> 3 - -LEAF CELLS ---------------- -Node 3: - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17hE" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) ) .Operands , span ( 117 ) ) ~> .K - >> function: core::panicking::panic::h - >> call span: /kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5 - >> message: 'assertion failed: false' \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.cli-stats-leaves.expected new file mode 100644 index 000000000..2201f44e4 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.cli-stats-leaves.expected @@ -0,0 +1,107 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: src/rust/library/std/src/rt.rs:194 +│ +│ (61 steps) +├─ 3 (split) +│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) +│ function: eats_struct_args +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ notBool ARG_INT2:Int ==Int ARG_INT5:Int +┃ │ +┃ ├─ 4 +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) +┃ │ function: eats_struct_args +┃ │ +┃ │ (96 steps) +┃ ├─ 6 (split) +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) ) +┃ │ function: eats_struct_args +┃ ┃ +┃ ┃ (branch) +┃ ┣━━┓ subst: .Subst +┃ ┃ ┃ constraint: +┃ ┃ ┃ ARG_UINT3:Int ==Int ARG_UINT6:Int +┃ ┃ │ +┃ ┃ ├─ 8 +┃ ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) ) +┃ ┃ │ function: eats_struct_args +┃ ┃ │ +┃ ┃ │ (6 steps) +┃ ┃ └─ 10 (stuck, leaf) +┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h +┃ ┃ span: no-location:0 +┃ ┃ +┃ ┗━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ notBool ARG_UINT3:Int ==Int ARG_UINT6:Int +┃ │ +┃ ├─ 9 +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) ) +┃ │ function: eats_struct_args +┃ │ +┃ │ (6 steps) +┃ ├─ 11 (terminal) +┃ │ #EndProgram ~> .K +┃ │ function: eats_struct_args +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ ARG_INT2:Int ==Int ARG_INT5:Int + │ + ├─ 5 + │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) + │ function: eats_struct_args + │ + │ (66 steps) + ├─ 7 (terminal) + │ #EndProgram ~> .K + │ function: eats_struct_args + │ + ┊ constraint: true + ┊ subst: ... + └─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + + +STATISTICS +----------- +Total nodes: 10 + +Node roles (exclusive): + target : 1 ids: 2 + terminal: 2 ids: 7, 11 + failing : 1 ids: 10 + split : 2 ids: 3, 6 + normal : 4 ids: 4, 5, 8, 9 + (root nodes omitted from totals: 1) + +Leaf paths from init: + total leaves (non-root): 2 + reachable leaves : 2 + total steps : 290 + + leaf 2 (path 1/2): steps 127, path 1 -> 3 -> 5 -> 7 -> 2 + leaf 2 (path 2/2): steps 163, path 1 -> 3 -> 4 -> 6 -> 9 -> 11 -> 2 + leaf 10: steps 163, path 1 -> 3 -> 4 -> 6 -> 8 -> 10 + +LEAF CELLS +--------------- +Node 2: + #EndProgram ~> .K + +Node 10: + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17hE" ) , id: defId ( 27 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x008\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 0 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) ) .Operands , span ( 65 ) ) ~> .K + >> function: core::panicking::panic::h + >> call span: /kmir/src/tests/integration/data/prove-rs/symbolic-structs-fail.rs:29:5 \ No newline at end of file diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py index 60b314140..6ef1e0efe 100644 --- a/kmir/src/tests/integration/test_cli.py +++ b/kmir/src/tests/integration/test_cli.py @@ -19,7 +19,7 @@ PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) MODULES_DIR = (Path(__file__).parent / 'data' / 'modules').resolve(strict=True) # Repo root: used to normalise absolute paths in expected-output snapshots so -# they don't differ between local checkouts and CI (e.g. symbolic-args-unsupported.main.cli-stats-leaves). +# they don't differ between local checkouts and CI (e.g. symbolic-structs-fail.eats_struct_args.cli-stats-leaves). _REPO_ROOT = str(Path(__file__).resolve().parents[4]) _PATH_REPLACEMENTS: dict[str, str] = {_REPO_ROOT + '/': '/'} @@ -84,10 +84,10 @@ def test_cli_show_printers_snapshot( 'src,start_symbol,is_smir', [ pytest.param( - (PROVE_DIR / 'symbolic-args-unsupported.rs'), - 'main', + (PROVE_DIR / 'symbolic-structs-fail.rs'), + 'eats_struct_args', False, - id='symbolic-args-unsupported.main', + id='symbolic-structs-fail.eats_struct_args', ), pytest.param( (Path(__file__).parent / 'data' / 'exec-smir' / 'niche-enum' / 'niche-enum.smir.json').resolve(strict=True), @@ -242,9 +242,9 @@ def test_cli_show_to_module( def test_cli_show_minimize_proof(kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str]) -> None: """Test --minimize-proof option.""" - rs_file = PROVE_DIR / 'symbolic-args-unsupported.rs' - start_symbol = 'main' - # Use limited depth to create a partial proof with intermediate nodes that can be minimized + rs_file = PROVE_DIR / 'symbolic-structs-fail.rs' + start_symbol = 'eats_struct_args' + # Use a stable -fail test with symbolic branching so max_depth=5 creates intermediate nodes with splits apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False, max_depth=5) # Get initial node count From 91fa4f34e0f757d85820ecddabd8714bd8ba064a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 08:41:20 +0000 Subject: [PATCH 5/7] style: fix black formatting in test_integration.py Co-Authored-By: Claude Opus 4.6 (1M context) --- kmir/src/tests/integration/test_integration.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 5732098ee..abadf292e 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -41,6 +41,8 @@ 'iter-eq-copied-take-dereftruncate': ['repro'], 'spl-multisig-iter-eq-copied-next': ['repro'], } + + @pytest.mark.parametrize( 'rs_file', PROVE_FILES, From 98c68be3c69dab9fc4d7002d31e82a6bbda75017 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 11:58:28 +0000 Subject: [PATCH 6/7] fix(tests): keep snapshots for -fail and -unsupported --- kmir/src/kmir/cargo.py | 3 ++ kmir/src/kmir/testing/fixtures.py | 12 ++++++-- .../show/assert-false-fail.main.expected | 15 ++++++++++ .../enum-two-refs-unsupported.main.expected | 22 +++++++++++++++ .../show/loop-unsupported.main.expected | 15 ++++++++++ .../show/offset-u8-unsupported.main.expected | 8 ++---- ...tile_load_static-unsupported.main.expected | 4 +-- ...ile_store_static-unsupported.main.expected | 4 +-- .../src/tests/integration/test_integration.py | 28 +++++++++++-------- 9 files changed, 88 insertions(+), 23 deletions(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/enum-two-refs-unsupported.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/loop-unsupported.main.expected diff --git a/kmir/src/kmir/cargo.py b/kmir/src/kmir/cargo.py index db3dc293b..0c8981a72 100644 --- a/kmir/src/kmir/cargo.py +++ b/kmir/src/kmir/cargo.py @@ -182,6 +182,9 @@ def cargo_get_smir_json( cwd = cwd or Path.cwd() smir_json_result = cwd / rs_file.with_suffix('.smir.json').name run_process_2(command, cwd=cwd) + resolved_smir_json_result = cwd / rs_file.resolve().with_suffix('.smir.json').name + if not smir_json_result.is_file() and resolved_smir_json_result.is_file(): + resolved_smir_json_result.rename(smir_json_result) json_smir = json.loads(smir_json_result.read_text()) _LOGGER.info(f'Loaded: {smir_json_result}') if save_smir: diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py index d42bf606d..999a231ad 100644 --- a/kmir/src/kmir/testing/fixtures.py +++ b/kmir/src/kmir/testing/fixtures.py @@ -31,20 +31,26 @@ def _normalize_symbol_hashes(text: str) -> str: return text +def _normalize_show_output(text: str) -> str: + text = _normalize_symbol_hashes(text) + text = re.sub(r'(?m)^(\s*(?:[│┃┊]\s*)?span: )\d+$', r'\1', text) + text = re.sub(r'(?m)^\s*>> message: .*\n?', '', text) + return text.rstrip('\r\n') + + def assert_or_update_show_output( actual_text: str, expected_file: Path, *, update: bool, path_replacements: dict[str, str] | None = None ) -> None: if path_replacements: for old, new in path_replacements.items(): actual_text = actual_text.replace(old, new) - # Normalize rustc symbol hash suffixes that can drift across builds/environments. - actual_text = _normalize_symbol_hashes(actual_text) + actual_text = _normalize_show_output(actual_text) if update: expected_file.write_text(actual_text) else: assert expected_file.is_file() expected_text = expected_file.read_text() - expected_text = _normalize_symbol_hashes(expected_text) + expected_text = _normalize_show_output(expected_text) if actual_text != expected_text: diff = '\n'.join( unified_diff( diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected new file mode 100644 index 000000000..a02498ead --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (8 steps) +└─ 3 (stuck, leaf) + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/enum-two-refs-unsupported.main.expected b/kmir/src/tests/integration/data/prove-rs/show/enum-two-refs-unsupported.main.expected new file mode 100644 index 000000000..5378b0d20 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/enum-two-refs-unsupported.main.expected @@ -0,0 +1,22 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (10 steps) +├─ 3 +│ #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00 +│ function: main +│ span: 118 +│ +│ (1 step) +└─ 4 (leaf, terminal) + thunk ( #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00 + function: main + span: 118 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/loop-unsupported.main.expected b/kmir/src/tests/integration/data/prove-rs/show/loop-unsupported.main.expected new file mode 100644 index 000000000..5140b2cbd --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/loop-unsupported.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (1450 steps) +└─ 3 (stuck, leaf) + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-unsupported.main.expected b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-unsupported.main.expected index c373bdd71..3fd2c5ad1 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-unsupported.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-unsupported.main.expected @@ -1,15 +1,13 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 +│ span: │ │ (35 steps) └─ 3 (stuck, leaf) #traverseProjection ( toAlloc ( allocId ( 0 ) ) , StringVal ( "123" ) , .Project - span: 48 + span: ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - +│ #EndProgram ~> .K \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-unsupported.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-unsupported.main.expected index e68710b66..314438917 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-unsupported.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-unsupported.main.expected @@ -7,13 +7,13 @@ ├─ 3 │ #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00 │ function: main -│ span: 56 +│ span: 53 │ │ (1 step) └─ 4 (leaf, terminal) thunk ( #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00 function: main - span: 56 + span: 53 ┌─ 2 (root, leaf, target, terminal) diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected index 420e0659d..b2fe8891b 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected @@ -7,13 +7,13 @@ ├─ 3 │ #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00 │ function: main -│ span: 57 +│ span: 54 │ │ (1 step) └─ 4 (leaf, terminal) thunk ( #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00 function: main - span: 57 + span: 54 ┌─ 2 (root, leaf, target, terminal) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index abadf292e..5e2c96104 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -49,37 +49,43 @@ ids=[spec.stem for spec in PROVE_FILES], ) def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: - should_fail = rs_file.stem.endswith('fail') or rs_file.stem.endswith('unsupported') + should_fail = rs_file.stem.endswith('fail') + should_show = should_fail or rs_file.stem.endswith('unsupported') is_smir = rs_file.suffix == '.json' - if update_expected_output and not should_fail: + start_symbols = ['main'] + if rs_file.stem in PROVE_START_SYMBOLS: + start_symbols = PROVE_START_SYMBOLS[rs_file.stem] + + if update_expected_output and not should_show: + for start_symbol in start_symbols: + expected_file = PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected' + assert not expected_file.is_file() pytest.skip() prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=True) printer = PrettyPrinter(kmir.definition) cterm_show = CTermShow(printer.print) - start_symbols = ['main'] - if rs_file.stem in PROVE_START_SYMBOLS: - start_symbols = PROVE_START_SYMBOLS[rs_file.stem] - for start_symbol in start_symbols: prove_opts.start_symbol = start_symbol apr_proof = kmir.prove_program(prove_opts) + expected_file = PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected' - if should_fail: - assert apr_proof.failed + if should_show: display_opts = ShowOpts( rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False ) shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts)) show_res = '\n'.join(shower.show(apr_proof)) - assert_or_update_show_output( - show_res, PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected', update=update_expected_output - ) + assert_or_update_show_output(show_res, expected_file, update=update_expected_output) else: + assert not expected_file.is_file() assert apr_proof.passed + if should_fail: + assert apr_proof.failed + VERIFY_RUST_STD_DIR = (Path(__file__).parent / 'data' / 'verify-rust-std').resolve(strict=True) VERIFY_RUST_STD_FILES = list(VERIFY_RUST_STD_DIR.glob('**/*.rs')) From 580ebe3375460de872f7e34c5e02e655a904f149 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 13 Apr 2026 15:42:37 +0000 Subject: [PATCH 7/7] ci: extend verify-rust-std timeout --- .github/workflows/test.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 5cd4fb0b4..2b9b92391 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -77,7 +77,7 @@ jobs: - name: 'Verify Rust Std' test-args: '-k test_verify_rust_std' parallel: 6 - timeout: 60 + timeout: 90 - name: 'Remainder' test-args: '-k "not llvm and not test_run_smir_random and not test_exec_smir and not test_prove_termination and not test_prove and not test_verify_rust_std"' parallel: 6 @@ -243,4 +243,3 @@ jobs: set -euxo pipefail nix --version nix flake check # build and run smoke test -