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 - 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/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/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected similarity index 94% rename from kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected index e5b630195..a02498ead 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-false-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (566 steps) +│ (8 steps) └─ 3 (stuck, leaf) #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h span: 32 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/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/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/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/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/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/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/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/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 82% 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 index c373bdd71..3fd2c5ad1 100644 --- 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 @@ -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/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/symbolic-args-fail.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected deleted file mode 100644 index e4e10b74c..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.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-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-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/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 94% 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 index e68710b66..314438917 100644 --- 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 @@ -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-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-unsupported.main.expected similarity index 94% 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 index 420e0659d..b2fe8891b 100644 --- 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 @@ -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/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/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_cli.py b/kmir/src/tests/integration/test_cli.py index ed40f516f..1d1b71e29 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-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-fail.rs'), - 'main', + (PROVE_DIR / 'symbolic-structs-fail.rs'), + 'eats_struct_args', False, - id='symbolic-args-fail.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-fail.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 diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a2d77d7bd..61494885b 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -28,12 +28,12 @@ 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'], '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'], @@ -41,37 +41,6 @@ 'iter-eq-copied-take-dereftruncate': ['repro'], 'spl-multisig-iter-eq-copied-next': ['repro'], } -PROVE_SHOW_SPECS = [ - 'local-raw-fail', - 'interior-mut-fail', - 'interior-mut3-fail', - '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', - 'niche-enum', - 'assume-cheatcode-conflict-fail', - 'raw-ptr-cast-fail', - 'transmute-u8-to-enum-fail', - 'assert-inhabited-fail', - 'iterator-simple', - 'unions-fail', - 'transmute-maybe-uninit-fail', - 'ptr-through-wrapper-fail', - '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', -] @pytest.mark.parametrize( @@ -81,23 +50,27 @@ ) def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: should_fail = rs_file.stem.endswith('fail') - should_show = rs_file.stem in PROVE_SHOW_SPECS + should_show = should_fail or rs_file.stem.endswith('unsupported') is_smir = rs_file.suffix == '.json' + 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_symbols = [start_symbol] apr_proof = kmir.prove_program(prove_opts) + expected_file = PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected' if should_show: display_opts = ShowOpts( @@ -105,13 +78,12 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: ) 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 - ) - - if not should_fail: - assert apr_proof.passed + 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