Dedupe function selector rules (#1074)

We currently have duplicated rules for function selector check, which
makes maintaining them a bit more fragile/brittle. This deduplicates
them by sequentializing the check.

In particular:

- Introduce extra step `#checkFunctionFilter(...)` for creating
cut-rules where we have function calls we want to inspect.
- Update tests that now need to take extra steps to get to the same
state.
- Update test expected output where relevant.

In addition, this makes a minor update to the `CLAUDE.md` with more
fine-grained information about how to run tests and update expected
output autonomously.

---------

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: ehildenb

CLAUDE.md

@@ -32,12 +32,22 @@ make test-unit
 make test-integration
 
 # Run a single test
-uv --directory kmir run pytest kmir/src/tests/integration/test_prove.py::test_prove -k "test_name"
+make test-integration TEST_ARGS='-k "test_name"'
 
 # Generate and parse SMIR for test files
 make smir-parse-tests
 ```
 
+You can pass `PARALLEL=N` to increase parallelism for a given test-run.
+You can add `TEST_ARGS=--update-expected-output` to update golden output files.
+Tests take up to 30 minutes to run, so set your timeout accordingly.
+
+When updating the expected output, make sure to inspect the updated test output and check that it's explained by the changes made to the code.
+If not, please provide a brief explanation of could have happend with the test, or what adjustments are needed.
+
+To run individual tests, add `TEST_ARGS='-k "test_id1 or test_id2"'` to the `make` invocation.
+For very specific queries, skip make and run the `uv --directory kmir run pytest path/to/test/file.py::test_name[test_selector]` directly with appropriate arguments.
+
 ### Code Quality
 ```bash
 # Format code
@@ -162,4 +172,4 @@ uv --directory kmir run kmir show proof_id --full-printer --no-omit-static-info
 ### Common Issues
 - `Function not found` errors: Check if function is in `FUNCTIONS_CELL` (may be intrinsic)
 - K compilation errors: Rules must be properly formatted, check syntax
-- SMIR generation fails: Ensure using correct Rust nightly version (2024-11-29)
+- SMIR generation fails: Ensure using correct Rust nightly version (2024-11-29)

kmir/src/kmir/_prove.py

@@ -357,8 +357,7 @@ def _cut_point_rules(
     ):
         cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunction')
     if break_on_function:
-        cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunctionFilter')
-        cut_point_rules.append('KMIR-CONTROL-FLOW.termCallIntrinsicFilter')
+        cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunctionFilterMatch')
     if break_on_terminator_assert or break_every_terminator or break_every_step:
         cut_point_rules.append('KMIR-CONTROL-FLOW.termAssert')
     if break_on_terminator_drop or break_every_terminator or break_every_step:

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -309,6 +309,7 @@ where the returned result should go.
 
 ```k
   syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction, Span)
+  syntax KItem ::= #checkFunctionFilter(MonoItemKind)
 
   rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), SPAN))
         => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
@@ -336,23 +337,14 @@ where the returned result should go.
   // Intrinsic function call - execute directly without state switching
   rule [termCallIntrinsic]:
         <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, SPAN) ~> _
-         => #execIntrinsic(FUNC, ARGS, DEST, SPAN) ~> #continueAt(TARGET)
+         => #checkFunctionFilter(FUNC) ~> #execIntrinsic(FUNC, ARGS, DEST, SPAN) ~> #continueAt(TARGET)
         </k>
     requires isIntrinsicFunction(FUNC)
-     andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC))
-
-  // Intrinsic function call to a function in the break-on set - same as termCallIntrinsic but separate rule id for cut-point
-  rule [termCallIntrinsicFilter]:
-        <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, SPAN) ~> _
-         => #execIntrinsic(FUNC, ARGS, DEST, SPAN) ~> #continueAt(TARGET)
-        </k>
-    requires isIntrinsicFunction(FUNC)
-     andBool #functionNameMatchesEnv(getFunctionName(FUNC))
 
   // Regular function call - full state switching and stack setup
   rule [termCallFunction]:
        <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _
-        => #setUpCalleeData(FUNC, ARGS, SPAN)
+        => #checkFunctionFilter(FUNC) ~> #setUpCalleeData(FUNC, ARGS, SPAN)
        </k>
        <currentFunc> CALLER => FTY </currentFunc>
        <currentFrame>
@@ -365,25 +357,15 @@ where the returned result should go.
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
     requires notBool isIntrinsicFunction(FUNC)
-     andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC))
 
-  // Function call to a function in the break-on set - same as termCallFunction but separate rule id for cut-point
-  rule [termCallFunctionFilter]:
-       <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _
-        => #setUpCalleeData(FUNC, ARGS, SPAN)
-       </k>
-       <currentFunc> CALLER => FTY </currentFunc>
-       <currentFrame>
-         <currentBody> _ </currentBody>
-         <caller> OLDCALLER => CALLER </caller>
-         <dest> OLDDEST => DEST </dest>
-         <target> OLDTARGET => TARGET </target>
-         <unwind> OLDUNWIND => UNWIND </unwind>
-         <locals> LOCALS </locals>
-       </currentFrame>
-       <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
-    requires notBool isIntrinsicFunction(FUNC)
-     andBool #functionNameMatchesEnv(getFunctionName(FUNC))
+  // Filter check injected after every call: fires as a cut-point only when the function matches the break-on list
+  rule [termCallFunctionFilterMatch]:
+       <k> #checkFunctionFilter(FUNC) => .K ... </k>
+    requires #functionNameMatchesEnv(getFunctionName(FUNC))
+
+  rule [termCallFunctionFilterNoMatch]:
+       <k> #checkFunctionFilter(FUNC) => .K ... </k>
+    requires notBool #functionNameMatchesEnv(getFunctionName(FUNC))
 
   syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function]
   rule isIntrinsicFunction(IntrinsicFunction(_)) => true

kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (44 steps)
+│  (46 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709
 ┃

kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (228 steps)
+│  (231 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (35 steps)
+│  (36 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709
 ┃

kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (114 steps)
+│  (116 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃
@@ -14,7 +14,7 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃  │
-┃  │  (6 steps)
+┃  │  (7 steps)
 ┃  └─ 6 (stuck, leaf)
 ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN3std7process4exit17h<hash>
 ┃
@@ -25,7 +25,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
    │
-   │  (182 steps)
+   │  (183 steps)
    ├─ 7 (terminal)
    │   #EndProgram ~> .K
    │

kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (737 steps)
+│  (746 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (216 steps)
+│  (220 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (10 steps)
+│  (12 steps)
 └─ 3 (stuck, leaf)
     #ProgramError ( AssertInhabitedFailure ) ~> .K
     function: main