Skip to content

More cut point rules #790

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Oct 31, 2025
Merged

More cut point rules #790

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0c1b1b4
Added --break-on-thunk
dkcumming Oct 30, 2025
4e663c4
Added --break-every-statement
dkcumming Oct 30, 2025
9d44563
added many commands to break on terminator (and improved --break-on-c…
dkcumming Oct 30, 2025
584b377
Added --break-on-function-calls and --break-on-intrinsic-calls to add…
dkcumming Oct 30, 2025
9baba04
Added --break-every-step which breaks on MIR statements and terminators
dkcumming Oct 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 89 additions & 1 deletion kmir/src/kmir/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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(
Expand Down
22 changes: 11 additions & 11 deletions kmir/src/kmir/kdist/mir-semantics/kmir.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
...
Expand Down Expand Up @@ -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>
Expand All @@ -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>
Expand Down Expand Up @@ -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>
Expand All @@ -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>
Expand Down Expand Up @@ -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>
Expand Down Expand Up @@ -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
)
Expand Down Expand Up @@ -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>
Expand All @@ -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
...
Expand Down
2 changes: 1 addition & 1 deletion kmir/src/kmir/kdist/mir-semantics/rt/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
67 changes: 64 additions & 3 deletions kmir/src/kmir/kmir.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
65 changes: 65 additions & 0 deletions kmir/src/kmir/options.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down