From 0c1b1b444eb6d07e01c5f2aaea707522452bee89 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 31 Oct 2025 02:33:03 +1000 Subject: [PATCH 1/5] Added --break-on-thunk --- kmir/src/kmir/__main__.py | 4 ++++ kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 +- kmir/src/kmir/kmir.py | 13 +++++++------ kmir/src/kmir/options.py | 5 +++++ 4 files changed, 17 insertions(+), 7 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 060ae0487..07160a916 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -248,6 +248,9 @@ def _arg_parser() -> ArgumentParser: prove_args.add_argument( '--break-on-calls', dest='break_on_calls', action='store_true', help='Break on function calls' ) + prove_args.add_argument( + '--break-on-thunk', dest='break_on_thunk', action='store_true', help='Break on thunk evaluation' + ) proof_args = ArgumentParser(add_help=False) proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') @@ -419,6 +422,7 @@ def _parse_args(ns: Namespace) -> KMirOpts: smir=ns.smir, start_symbol=ns.start_symbol, break_on_calls=ns.break_on_calls, + break_on_thunk=ns.break_on_thunk, ) case 'link': return LinkOpts( diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index cd744b4a2..e3304290b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/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 EV:Evaluation => thunk(EV) ... requires notBool isValue(EV) andBool notBool isTypedValue(EV) [owise] + rule [thunk]: EV:Evaluation => thunk(EV) ... requires notBool isValue(EV) andBool notBool isTypedValue(EV) [owise] ``` ### Errors Related to Accessing Local Variables diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index f4c7a8599..413726915 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -56,14 +56,13 @@ def __init__( @staticmethod def cut_point_rules( break_on_calls: bool, + break_on_thunk: bool, ) -> list[str]: cut_point_rules = [] if break_on_calls: - cut_point_rules.extend( - [ - 'KMIR-CONTROL-FLOW.call', - ] - ) + cut_point_rules.append('KMIR-CONTROL-FLOW.call') + if break_on_thunk: + cut_point_rules.append('RT-DATA.thunk') return cut_point_rules @staticmethod @@ -197,7 +196,9 @@ 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_thunk=opts.break_on_thunk + ) with kmir.kcfg_explore(label) as kcfg_explore: prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules) diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 8e05906a9..7f68acbfd 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -42,6 +42,7 @@ class ProveOpts(KMirOpts): max_iterations: int | None reload: bool break_on_calls: bool + break_on_thunk: bool def __init__( self, @@ -51,6 +52,7 @@ def __init__( max_iterations: int | None = None, reload: bool = False, break_on_calls: bool = False, + break_on_thunk: bool = False, ) -> None: self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None self.bug_report = bug_report @@ -58,6 +60,7 @@ def __init__( self.max_iterations = max_iterations self.reload = reload self.break_on_calls = break_on_calls + self.break_on_thunk = break_on_thunk @dataclass @@ -79,6 +82,7 @@ def __init__( smir: bool = False, start_symbol: str = 'main', break_on_calls: bool = False, + break_on_thunk: 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 +94,7 @@ def __init__( self.smir = smir self.start_symbol = start_symbol self.break_on_calls = break_on_calls + self.break_on_thunk = break_on_thunk @dataclass From 4e663c4d8563c6e3abe9ee58c8410cee5898d1bd Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 31 Oct 2025 02:58:35 +1000 Subject: [PATCH 2/5] Added --break-every-statement --- kmir/src/kmir/__main__.py | 7 +++++++ kmir/src/kmir/kdist/mir-semantics/kmir.md | 2 +- kmir/src/kmir/kmir.py | 7 ++++++- kmir/src/kmir/options.py | 5 +++++ 4 files changed, 19 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 07160a916..3e739c437 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -251,6 +251,12 @@ def _arg_parser() -> ArgumentParser: 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', + ) proof_args = ArgumentParser(add_help=False) proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') @@ -423,6 +429,7 @@ def _parse_args(ns: Namespace) -> KMirOpts: start_symbol=ns.start_symbol, break_on_calls=ns.break_on_calls, break_on_thunk=ns.break_on_thunk, + break_every_statement=ns.break_every_statement, ) case 'link': return LinkOpts( diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 177cf8d94..4691c1e19 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/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 #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN)) + rule [execStmt]: #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN)) => #setLocalValue(PLACE, RVAL) ... diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 413726915..4ba65c1b3 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -57,12 +57,15 @@ def __init__( def cut_point_rules( break_on_calls: bool, break_on_thunk: bool, + break_every_statement: bool, ) -> list[str]: cut_point_rules = [] if break_on_calls: cut_point_rules.append('KMIR-CONTROL-FLOW.call') if break_on_thunk: cut_point_rules.append('RT-DATA.thunk') + if break_every_statement: + cut_point_rules.append('KMIR-CONTROL-FLOW.execStmt') return cut_point_rules @staticmethod @@ -197,7 +200,9 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: return apr_proof cut_point_rules = KMIR.cut_point_rules( - break_on_calls=opts.break_on_calls, break_on_thunk=opts.break_on_thunk + break_on_calls=opts.break_on_calls, + break_on_thunk=opts.break_on_thunk, + break_every_statement=opts.break_every_statement, ) with kmir.kcfg_explore(label) as kcfg_explore: diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 7f68acbfd..56d858036 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -43,6 +43,7 @@ class ProveOpts(KMirOpts): reload: bool break_on_calls: bool break_on_thunk: bool + break_every_statement: bool def __init__( self, @@ -53,6 +54,7 @@ def __init__( reload: bool = False, break_on_calls: bool = False, break_on_thunk: bool = False, + break_every_statement: bool = False, ) -> None: self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None self.bug_report = bug_report @@ -61,6 +63,7 @@ def __init__( self.reload = reload self.break_on_calls = break_on_calls self.break_on_thunk = break_on_thunk + self.break_every_statement = break_every_statement @dataclass @@ -83,6 +86,7 @@ def __init__( start_symbol: str = 'main', break_on_calls: bool = False, break_on_thunk: bool = False, + break_every_statement: bool = False, ) -> None: self.rs_file = rs_file self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None @@ -95,6 +99,7 @@ def __init__( self.start_symbol = start_symbol self.break_on_calls = break_on_calls self.break_on_thunk = break_on_thunk + self.break_every_statement = break_every_statement @dataclass From 9d44563a2139e24ca443264a98cb0fbfaea2b13b Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 31 Oct 2025 03:27:00 +1000 Subject: [PATCH 3/5] added many commands to break on terminator (and improved --break-on-calls) --- kmir/src/kmir/__main__.py | 56 +++++++++++++++++++++++ kmir/src/kmir/kdist/mir-semantics/kmir.md | 20 ++++---- kmir/src/kmir/kmir.py | 39 +++++++++++++++- kmir/src/kmir/options.py | 40 ++++++++++++++++ 4 files changed, 143 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 3e739c437..ed122f715 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -257,6 +257,54 @@ def _arg_parser() -> ArgumentParser: 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', + ) proof_args = ArgumentParser(add_help=False) proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') @@ -430,6 +478,14 @@ def _parse_args(ns: Namespace) -> KMirOpts: break_on_calls=ns.break_on_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, ) case 'link': return LinkOpts( diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 4691c1e19..776b51bff 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -139,7 +139,7 @@ function call, pushing a new stack frame and returning to a different block after the call returns. ```k - rule #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT + rule [termGoto]: #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT => #execBlockIdx(I) @@ -154,7 +154,7 @@ will be `129`. ```k syntax KItem ::= #selectBlock ( SwitchTargets , Evaluation ) [strict(2)] - rule #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT + rule [termSwitchInt]: #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT => #selectBlock(TARGETS, DISCR) @@ -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 #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + rule [termReturnSome]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET) @@ -205,7 +205,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK // no value to return, skip writing - rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + rule [termReturnNone]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #execBlockIdx(TARGET) @@ -279,14 +279,14 @@ where the returned result should go. ```k // Intrinsic function call - execute directly without state switching - rule #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _ + rule [termCallIntrinsic]: #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _ => #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET) requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC))) // Regular function call - full state switching and stack setup - rule #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _ + rule [termCallFunction]: #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _ => #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS) @@ -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]: #setUpCalleeData( + rule [setupCalleeData]: #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 #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT + rule [termAssert]: #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT => #expect(COND, EXPECTED, MSG) ~> #execBlockIdx(TARGET) @@ -430,7 +430,7 @@ 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 #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) + rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) => #execBlockIdx(TARGET) ... @@ -438,7 +438,7 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre syntax MIRError ::= "ReachedUnreachable" - rule #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) + rule [termUnreachable]: #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) => ReachedUnreachable ... diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 4ba65c1b3..5a779f341 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -58,14 +58,41 @@ def cut_point_rules( break_on_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, ) -> list[str]: cut_point_rules = [] - if break_on_calls: - cut_point_rules.append('KMIR-CONTROL-FLOW.call') if break_on_thunk: cut_point_rules.append('RT-DATA.thunk') if break_every_statement: cut_point_rules.append('KMIR-CONTROL-FLOW.execStmt') + if break_on_terminator_goto or break_every_terminator: + cut_point_rules.append('KMIR-CONTROL-FLOW.termGoto') + if break_on_terminator_switch_int or break_every_terminator: + cut_point_rules.append('KMIR-CONTROL-FLOW.termSwitchInt') + if break_on_terminator_return or break_every_terminator: + cut_point_rules.extend( + [ + 'KMIR-CONTROL-FLOW.termReturnSome', + 'KMIR-CONTROL-FLOW.termReturnNone', + 'KMIR-CONTROL-FLOW.endprogram-return', + 'KMIR-CONTROL-FLOW.endprogram-no-return', + ] + ) + if break_on_calls or break_on_terminator_call or break_every_terminator: + cut_point_rules.extend(['KMIR-CONTROL-FLOW.termCallIntrinsic', 'KMIR-CONTROL-FLOW.termCallFunction']) + if break_on_terminator_assert or break_every_terminator: + cut_point_rules.append('KMIR-CONTROL-FLOW.termAssert') + if break_on_terminator_drop or break_every_terminator: + cut_point_rules.append('KMIR-CONTROL-FLOW.termDrop') + if break_on_terminator_unreachable or break_every_terminator: + cut_point_rules.append('KMIR-CONTROL-FLOW.termUnreachable') return cut_point_rules @staticmethod @@ -203,6 +230,14 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: break_on_calls=opts.break_on_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, ) with kmir.kcfg_explore(label) as kcfg_explore: diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 56d858036..f0df755d1 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -44,6 +44,14 @@ class ProveOpts(KMirOpts): break_on_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 def __init__( self, @@ -55,6 +63,14 @@ def __init__( break_on_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, ) -> None: self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None self.bug_report = bug_report @@ -64,6 +80,14 @@ def __init__( self.break_on_calls = break_on_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 @dataclass @@ -87,6 +111,14 @@ def __init__( break_on_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, ) -> None: self.rs_file = rs_file self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None @@ -100,6 +132,14 @@ def __init__( self.break_on_calls = break_on_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 @dataclass From 584b377bf6b111ef383feeea3806a57244a7adde Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 31 Oct 2025 03:33:19 +1000 Subject: [PATCH 4/5] Added --break-on-function-calls and --break-on-intrinsic-calls to add finer control for calls --- kmir/src/kmir/__main__.py | 16 +++++++++++++++- kmir/src/kmir/kmir.py | 10 ++++++++-- kmir/src/kmir/options.py | 10 ++++++++++ 3 files changed, 33 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index ed122f715..4b584702f 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -246,7 +246,19 @@ 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' @@ -476,6 +488,8 @@ 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, diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 5a779f341..fcbbf0dce 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -56,6 +56,8 @@ 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, @@ -85,8 +87,10 @@ def cut_point_rules( 'KMIR-CONTROL-FLOW.endprogram-no-return', ] ) - if break_on_calls or break_on_terminator_call or break_every_terminator: - cut_point_rules.extend(['KMIR-CONTROL-FLOW.termCallIntrinsic', 'KMIR-CONTROL-FLOW.termCallFunction']) + if break_on_intrinsic_calls or break_on_calls or break_on_terminator_call or break_every_terminator: + 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: + cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunction') if break_on_terminator_assert or break_every_terminator: cut_point_rules.append('KMIR-CONTROL-FLOW.termAssert') if break_on_terminator_drop or break_every_terminator: @@ -228,6 +232,8 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: 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, diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index f0df755d1..7189137cd 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -42,6 +42,8 @@ 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 @@ -61,6 +63,8 @@ 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, @@ -78,6 +82,8 @@ def __init__( 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 @@ -109,6 +115,8 @@ 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, @@ -130,6 +138,8 @@ 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 From 9baba04707655921c94377802f03a809a29f4ca3 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 31 Oct 2025 03:45:11 +1000 Subject: [PATCH 5/5] Added --break-every-step which breaks on MIR statements and terminators --- kmir/src/kmir/__main__.py | 7 +++++++ kmir/src/kmir/kmir.py | 32 +++++++++++++++++++++++--------- kmir/src/kmir/options.py | 5 +++++ 3 files changed, 35 insertions(+), 9 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 4b584702f..bcc3adbae 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -317,6 +317,12 @@ def _arg_parser() -> ArgumentParser: 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) proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') @@ -500,6 +506,7 @@ def _parse_args(ns: Namespace) -> KMirOpts: 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( diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index fcbbf0dce..53265f6c6 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -68,17 +68,18 @@ def cut_point_rules( 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_thunk: cut_point_rules.append('RT-DATA.thunk') - if break_every_statement: + 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: + 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: + 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: + if break_on_terminator_return or break_every_terminator or break_every_step: cut_point_rules.extend( [ 'KMIR-CONTROL-FLOW.termReturnSome', @@ -87,15 +88,27 @@ def cut_point_rules( 'KMIR-CONTROL-FLOW.endprogram-no-return', ] ) - if break_on_intrinsic_calls or break_on_calls or break_on_terminator_call or break_every_terminator: + 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: + 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: + 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: + 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: + 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 @@ -244,6 +257,7 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: 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: diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 7189137cd..cda622524 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -54,6 +54,7 @@ class ProveOpts(KMirOpts): break_on_terminator_drop: bool break_on_terminator_unreachable: bool break_every_terminator: bool + break_every_step: bool def __init__( self, @@ -75,6 +76,7 @@ def __init__( 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 @@ -94,6 +96,7 @@ def __init__( 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 @@ -127,6 +130,7 @@ def __init__( 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 @@ -150,6 +154,7 @@ def __init__( 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