More cut point rules (#790)

Closes #789 

In particular adds:
- [x] `--break-on-instrinsic-calls` breaks on calling `Intrinsic`s
- [x] `--break-on-function-calls` breaks on calling `Function`s
- [x] `--break-on-thunks` breaks on `thunk`
- [x] `--break-every-statement` breaks every MIR `Statement`
- [x] `--break-every-terminator` breaks every MIR `Terminator`
- [x] `--break-on-terminator-goto` breaks on calling
`TerminatorKind::Goto`
- [x] `--break-on-terminator-switch-int` breaks on calling
`TerminatorKind::SwitchInt`
- [x] `--break-on-terminator-return` breaks on calling
`TerminatorKind::Return`
- [x] `--break-on-terminator-call` breaks on calling
`TerminatorKind::Call`
- [x] `--break-on-terminator-assert` breaks on calling
`TerminatorKind::Assert`
- [x] `--break-on-terminator-drop` breaks on calling
`TerminatorKind::Drop`
- [x] `--break-on-terminator-unreachable` breaks on calling
`TerminatorKind::Unreachable`
- [x] `--break-every-step` breaks every MIR `Statement` and `Terminator`

And `--break-on-calls` now breaks on instrinics and function calls at
the `Terminator` call since it dumps `#setUpCalleeData` node after you
can see the name of the intrinsic or function still

Author: dkcumming

kmir/src/kmir/__main__.py

@@ -246,7 +246,82 @@ def _arg_parser() -> ArgumentParser:
     )
     prove_args.add_argument('--reload', action='store_true', help='Force restarting proof')
     prove_args.add_argument(
-        '--break-on-calls', dest='break_on_calls', action='store_true', help='Break on function calls'
+        '--break-on-calls', dest='break_on_calls', action='store_true', help='Break on all function and intrinsic calls'
+    )
+    prove_args.add_argument(
+        '--break-on-function-calls',
+        dest='break_on_function_calls',
+        action='store_true',
+        help='Break on function calls (not intrinsics)',
+    )
+    prove_args.add_argument(
+        '--break-on-intrinsic-calls',
+        dest='break_on_intrinsic_calls',
+        action='store_true',
+        help='Break on intrinsic calls (not other functions)',
+    )
+    prove_args.add_argument(
+        '--break-on-thunk', dest='break_on_thunk', action='store_true', help='Break on thunk evaluation'
+    )
+    prove_args.add_argument(
+        '--break-every-statement',
+        dest='break_every_statement',
+        action='store_true',
+        help='Break on every MIR Statement execution',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-goto',
+        dest='break_on_terminator_goto',
+        action='store_true',
+        help='Break on Goto terminator',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-switch-int',
+        dest='break_on_terminator_switch_int',
+        action='store_true',
+        help='Break on SwitchInt terminator',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-return',
+        dest='break_on_terminator_return',
+        action='store_true',
+        help='Break on Return terminator',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-call',
+        dest='break_on_terminator_call',
+        action='store_true',
+        help='Break on Call terminator',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-assert',
+        dest='break_on_terminator_assert',
+        action='store_true',
+        help='Break on Assert terminator',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-drop',
+        dest='break_on_terminator_drop',
+        action='store_true',
+        help='Break on Drop terminator',
+    )
+    prove_args.add_argument(
+        '--break-on-terminator-unreachable',
+        dest='break_on_terminator_unreachable',
+        action='store_true',
+        help='Break on Unreachable terminator',
+    )
+    prove_args.add_argument(
+        '--break-every-terminator',
+        dest='break_every_terminator',
+        action='store_true',
+        help='Break on every MIR terminator execution',
+    )
+    prove_args.add_argument(
+        '--break-every-step',
+        dest='break_every_step',
+        action='store_true',
+        help='Break on every MIR step (statements and terminators)',
     )
 
     proof_args = ArgumentParser(add_help=False)
@@ -419,6 +494,19 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 smir=ns.smir,
                 start_symbol=ns.start_symbol,
                 break_on_calls=ns.break_on_calls,
+                break_on_function_calls=ns.break_on_function_calls,
+                break_on_intrinsic_calls=ns.break_on_intrinsic_calls,
+                break_on_thunk=ns.break_on_thunk,
+                break_every_statement=ns.break_every_statement,
+                break_on_terminator_goto=ns.break_on_terminator_goto,
+                break_on_terminator_switch_int=ns.break_on_terminator_switch_int,
+                break_on_terminator_return=ns.break_on_terminator_return,
+                break_on_terminator_call=ns.break_on_terminator_call,
+                break_on_terminator_assert=ns.break_on_terminator_assert,
+                break_on_terminator_drop=ns.break_on_terminator_drop,
+                break_on_terminator_unreachable=ns.break_on_terminator_unreachable,
+                break_every_terminator=ns.break_every_terminator,
+                break_every_step=ns.break_every_step,
             )
         case 'link':
             return LinkOpts(

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

@@ -96,7 +96,7 @@ will effectively be no-ops at this level).
 ```k
 
   // all memory accesses relegated to another module (to be added)
-  rule <k> #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN))
+  rule [execStmt]: <k> #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN))
          =>
             #setLocalValue(PLACE, RVAL)
          ...
@@ -139,7 +139,7 @@ function call, pushing a new stack frame and returning to a different
 block after the call returns.
 
 ```k
-  rule <k> #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT
+  rule [termGoto]: <k> #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT
          =>
            #execBlockIdx(I)
        </k>
@@ -154,7 +154,7 @@ will be `129`.
 ```k
   syntax KItem ::= #selectBlock ( SwitchTargets , Evaluation ) [strict(2)]
 
-  rule <k> #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT
+  rule [termSwitchInt]: <k> #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT
          =>
            #selectBlock(TARGETS, DISCR)
        </k>
@@ -188,7 +188,7 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l
 If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped.
 
 ```k
-  rule <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
+  rule [termReturnSome]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
          =>
            #setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET)
        </k>
@@ -205,7 +205,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
 
   // no value to return, skip writing
-  rule <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
+  rule [termReturnNone]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
          =>
            #execBlockIdx(TARGET)
        </k>
@@ -279,14 +279,14 @@ where the returned result should go.
 
 ```k
   // Intrinsic function call - execute directly without state switching
-  rule <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _
+  rule [termCallIntrinsic]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _
          =>
            #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET)
        </k>
     requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
 
   // Regular function call - full state switching and stack setup
-  rule <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _
+  rule [termCallFunction]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _
          =>
            #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
        </k>
@@ -324,7 +324,7 @@ An operand may be a `Reference` (the only way a function could access another fu
   syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands)
 
   // reserve space for local variables and copy/move arguments from old locals into their place
-  rule [call]: <k> #setUpCalleeData(
+  rule [setupCalleeData]: <k> #setUpCalleeData(
               monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
               ARGS
               )
@@ -403,7 +403,7 @@ Otherwise the provided message is passed to a `panic!` call, ending the program
 ```k
   syntax MIRError ::= AssertError ( AssertMessage )
 
-  rule <k> #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT
+  rule [termAssert]: <k> #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT
          =>
            #expect(COND, EXPECTED, MSG) ~> #execBlockIdx(TARGET)
        </k>
@@ -430,15 +430,15 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach
 Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error.
 
 ```k
-  rule <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
+  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
          =>
            #execBlockIdx(TARGET)
         ...
        </k>
 
   syntax MIRError ::= "ReachedUnreachable"
 
-  rule <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))
+  rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))
          =>
            ReachedUnreachable
         ...

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

@@ -102,7 +102,7 @@ It is also useful to capture unimplemented semantic constructs so that we can ha
 ```k
   syntax Value ::= thunk ( Evaluation )
 
-  rule <k> EV:Evaluation => thunk(EV) ... </k> requires notBool isValue(EV) andBool notBool isTypedValue(EV) [owise]
+  rule [thunk]: <k> EV:Evaluation => thunk(EV) ... </k> requires notBool isValue(EV) andBool notBool isTypedValue(EV) [owise]
 ```
 
 ### Errors Related to Accessing Local Variables

kmir/src/kmir/kmir.py

@@ -56,14 +56,60 @@ def __init__(
     @staticmethod
     def cut_point_rules(
         break_on_calls: bool,
+        break_on_function_calls: bool,
+        break_on_intrinsic_calls: bool,
+        break_on_thunk: bool,
+        break_every_statement: bool,
+        break_on_terminator_goto: bool,
+        break_on_terminator_switch_int: bool,
+        break_on_terminator_return: bool,
+        break_on_terminator_call: bool,
+        break_on_terminator_assert: bool,
+        break_on_terminator_drop: bool,
+        break_on_terminator_unreachable: bool,
+        break_every_terminator: bool,
+        break_every_step: bool,
     ) -> list[str]:
         cut_point_rules = []
-        if break_on_calls:
+        if break_on_thunk:
+            cut_point_rules.append('RT-DATA.thunk')
+        if break_every_statement or break_every_step:
+            cut_point_rules.append('KMIR-CONTROL-FLOW.execStmt')
+        if break_on_terminator_goto or break_every_terminator or break_every_step:
+            cut_point_rules.append('KMIR-CONTROL-FLOW.termGoto')
+        if break_on_terminator_switch_int or break_every_terminator or break_every_step:
+            cut_point_rules.append('KMIR-CONTROL-FLOW.termSwitchInt')
+        if break_on_terminator_return or break_every_terminator or break_every_step:
             cut_point_rules.extend(
                 [
-                    'KMIR-CONTROL-FLOW.call',
+                    'KMIR-CONTROL-FLOW.termReturnSome',
+                    'KMIR-CONTROL-FLOW.termReturnNone',
+                    'KMIR-CONTROL-FLOW.endprogram-return',
+                    'KMIR-CONTROL-FLOW.endprogram-no-return',
                 ]
             )
+        if (
+            break_on_intrinsic_calls
+            or break_on_calls
+            or break_on_terminator_call
+            or break_every_terminator
+            or break_every_step
+        ):
+            cut_point_rules.append('KMIR-CONTROL-FLOW.termCallIntrinsic')
+        if (
+            break_on_function_calls
+            or break_on_calls
+            or break_on_terminator_call
+            or break_every_terminator
+            or break_every_step
+        ):
+            cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunction')
+        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:
+            cut_point_rules.append('KMIR-CONTROL-FLOW.termDrop')
+        if break_on_terminator_unreachable or break_every_terminator or break_every_step:
+            cut_point_rules.append('KMIR-CONTROL-FLOW.termUnreachable')
         return cut_point_rules
 
     @staticmethod
@@ -197,7 +243,22 @@ def prove_rs(opts: ProveRSOpts) -> APRProof:
             if apr_proof.passed:
                 return apr_proof
 
-            cut_point_rules = KMIR.cut_point_rules(break_on_calls=opts.break_on_calls)
+            cut_point_rules = KMIR.cut_point_rules(
+                break_on_calls=opts.break_on_calls,
+                break_on_function_calls=opts.break_on_function_calls,
+                break_on_intrinsic_calls=opts.break_on_intrinsic_calls,
+                break_on_thunk=opts.break_on_thunk,
+                break_every_statement=opts.break_every_statement,
+                break_on_terminator_goto=opts.break_on_terminator_goto,
+                break_on_terminator_switch_int=opts.break_on_terminator_switch_int,
+                break_on_terminator_return=opts.break_on_terminator_return,
+                break_on_terminator_call=opts.break_on_terminator_call,
+                break_on_terminator_assert=opts.break_on_terminator_assert,
+                break_on_terminator_drop=opts.break_on_terminator_drop,
+                break_on_terminator_unreachable=opts.break_on_terminator_unreachable,
+                break_every_terminator=opts.break_every_terminator,
+                break_every_step=opts.break_every_step,
+            )
 
             with kmir.kcfg_explore(label) as kcfg_explore:
                 prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules)

kmir/src/kmir/options.py

@@ -42,6 +42,19 @@ class ProveOpts(KMirOpts):
     max_iterations: int | None
     reload: bool
     break_on_calls: bool
+    break_on_function_calls: bool
+    break_on_intrinsic_calls: bool
+    break_on_thunk: bool
+    break_every_statement: bool
+    break_on_terminator_goto: bool
+    break_on_terminator_switch_int: bool
+    break_on_terminator_return: bool
+    break_on_terminator_call: bool
+    break_on_terminator_assert: bool
+    break_on_terminator_drop: bool
+    break_on_terminator_unreachable: bool
+    break_every_terminator: bool
+    break_every_step: bool
 
     def __init__(
         self,
@@ -51,13 +64,39 @@ def __init__(
         max_iterations: int | None = None,
         reload: bool = False,
         break_on_calls: bool = False,
+        break_on_function_calls: bool = False,
+        break_on_intrinsic_calls: bool = False,
+        break_on_thunk: bool = False,
+        break_every_statement: bool = False,
+        break_on_terminator_goto: bool = False,
+        break_on_terminator_switch_int: bool = False,
+        break_on_terminator_return: bool = False,
+        break_on_terminator_call: bool = False,
+        break_on_terminator_assert: bool = False,
+        break_on_terminator_drop: bool = False,
+        break_on_terminator_unreachable: bool = False,
+        break_every_terminator: bool = False,
+        break_every_step: bool = False,
     ) -> None:
         self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
         self.bug_report = bug_report
         self.max_depth = max_depth
         self.max_iterations = max_iterations
         self.reload = reload
         self.break_on_calls = break_on_calls
+        self.break_on_function_calls = break_on_function_calls
+        self.break_on_intrinsic_calls = break_on_intrinsic_calls
+        self.break_on_thunk = break_on_thunk
+        self.break_every_statement = break_every_statement
+        self.break_on_terminator_goto = break_on_terminator_goto
+        self.break_on_terminator_switch_int = break_on_terminator_switch_int
+        self.break_on_terminator_return = break_on_terminator_return
+        self.break_on_terminator_call = break_on_terminator_call
+        self.break_on_terminator_assert = break_on_terminator_assert
+        self.break_on_terminator_drop = break_on_terminator_drop
+        self.break_on_terminator_unreachable = break_on_terminator_unreachable
+        self.break_every_terminator = break_every_terminator
+        self.break_every_step = break_every_step
 
 
 @dataclass
@@ -79,6 +118,19 @@ def __init__(
         smir: bool = False,
         start_symbol: str = 'main',
         break_on_calls: bool = False,
+        break_on_function_calls: bool = False,
+        break_on_intrinsic_calls: bool = False,
+        break_on_thunk: bool = False,
+        break_every_statement: bool = False,
+        break_on_terminator_goto: bool = False,
+        break_on_terminator_switch_int: bool = False,
+        break_on_terminator_return: bool = False,
+        break_on_terminator_call: bool = False,
+        break_on_terminator_assert: bool = False,
+        break_on_terminator_drop: bool = False,
+        break_on_terminator_unreachable: bool = False,
+        break_every_terminator: bool = False,
+        break_every_step: bool = False,
     ) -> None:
         self.rs_file = rs_file
         self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
@@ -90,6 +142,19 @@ def __init__(
         self.smir = smir
         self.start_symbol = start_symbol
         self.break_on_calls = break_on_calls
+        self.break_on_function_calls = break_on_function_calls
+        self.break_on_intrinsic_calls = break_on_intrinsic_calls
+        self.break_on_thunk = break_on_thunk
+        self.break_every_statement = break_every_statement
+        self.break_on_terminator_goto = break_on_terminator_goto
+        self.break_on_terminator_switch_int = break_on_terminator_switch_int
+        self.break_on_terminator_return = break_on_terminator_return
+        self.break_on_terminator_call = break_on_terminator_call
+        self.break_on_terminator_assert = break_on_terminator_assert
+        self.break_on_terminator_drop = break_on_terminator_drop
+        self.break_on_terminator_unreachable = break_on_terminator_unreachable
+        self.break_every_terminator = break_every_terminator
+        self.break_every_step = break_every_step
 
 
 @dataclass