refactor(tests): distinguish -fail from -unsupported, auto-detect show specs

.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
-

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:

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<span>', 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(

kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected → 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<hash>
     span: 32

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
+
+

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<hash>
+    span: 32
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected → 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: <span>
 │
 │  (35 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toAlloc ( allocId ( 0 ) ) , StringVal ( "123" ) , .Project
-    span: 48
+    span: <span>
 
 
 ┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K
-
-
+│   #EndProgram ~> .K

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<hash>
+┃  ┃      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 <k> CELLS
+---------------
+Node 2:
+  #EndProgram ~> .K
+
+Node 10:
+  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>E" ) , 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<hash>
+  >> call span: <REPO>/kmir/src/tests/integration/data/prove-rs/symbolic-structs-fail.rs:29:5

kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected → 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)

kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected → 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)

kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs → 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
 }