diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 060ae0487..bcc3adbae 100644 --- a/kmir/src/kmir/__main__.py +++ b/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( diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 177cf8d94..776b51bff 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) ... @@ -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/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..53265f6c6 100644 --- a/kmir/src/kmir/kmir.py +++ b/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) diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 8e05906a9..cda622524 100644 --- a/kmir/src/kmir/options.py +++ b/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,6 +64,19 @@ 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 @@ -58,6 +84,19 @@ 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 + 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