From efef9fe3a519ce1ee61d6d46bc48afa41e884d07 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 12 Nov 2025 00:26:13 +1000 Subject: [PATCH 1/4] Add terminal rule to match `thunk` --- kmir/src/kmir/kmir.py | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 747bc770e..be19d6fe1 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -9,7 +9,7 @@ from pyk.cli.utils import bug_report_arg from pyk.cterm import CTerm, cterm_symbolic -from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst +from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable, Subst from pyk.kast.manip import abstract_term_safely, split_config_from from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore @@ -260,15 +260,30 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: break_every_step=opts.break_every_step, ) - with kmir.kcfg_explore(label) as kcfg_explore: + with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules) prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof class KMIRSemantics(DefaultSemantics): + terminate_on_thunk: bool + + def __init__(self, terminate_on_thunk: bool = False) -> None: + self.terminate_on_thunk = terminate_on_thunk + def is_terminal(self, cterm: CTerm) -> bool: k_cell = cterm.cell('K_CELL') + + if self.terminate_on_thunk: # terminate on `thunk ( ... )` rule + match k_cell: + case KApply(KLabel('thunk(_)_RT-DATA_Value_Evaluation', _)): + return True + if type(k_cell) == KSequence and 0 < k_cell.arity: + match k_cell[0]: + case KApply(KLabel('thunk(_)_RT-DATA_Value_Evaluation', _)): + return True + # #EndProgram if k_cell == KMIR.Symbols.END_PROGRAM: return True From f15533febf9f79d164e0326f2ec27ee7c9c14e72 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 12 Nov 2025 00:26:50 +1000 Subject: [PATCH 2/4] Added `--terminate-on-thunk` option to kmir cli This also sets `--break-on-thunk` in cut point rules as the terminal rule needs the `thunk` on the top of the `` cell to match --- kmir/src/kmir/__main__.py | 7 +++++++ kmir/src/kmir/kmir.py | 6 +++--- kmir/src/kmir/options.py | 5 +++++ 3 files changed, 15 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index bcc3adbae..846cf91ef 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -263,6 +263,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( + '--terminate-on-thunk', + dest='terminate_on_thunk', + action='store_true', + help='Terminate proof when reaching a thunk', + ) prove_args.add_argument( '--break-every-statement', dest='break_every_statement', @@ -507,6 +513,7 @@ def _parse_args(ns: Namespace) -> KMirOpts: break_on_terminator_unreachable=ns.break_on_terminator_unreachable, break_every_terminator=ns.break_every_terminator, break_every_step=ns.break_every_step, + terminate_on_thunk=ns.terminate_on_thunk, ) case 'link': return LinkOpts( diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index be19d6fe1..93fc69910 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -134,7 +134,7 @@ def parser(self) -> Parser: return Parser(self.definition) @contextmanager - def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]: + def kcfg_explore(self, label: str | None = None, terminate_on_thunk: bool = False) -> Iterator[KCFGExplore]: with cterm_symbolic( self.definition, self.definition_dir, @@ -143,7 +143,7 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]: id=label if self.bug_report is not None else None, # NB bug report arg.s must be coherent simplify_each=30, ) as cts: - yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics()) + yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics(terminate_on_thunk=terminate_on_thunk)) def run_smir( self, @@ -247,7 +247,7 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: 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_on_thunk=opts.break_on_thunk or opts.terminate_on_thunk, # must break for terminal rule 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, diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index cda622524..ff6371fdd 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -55,6 +55,7 @@ class ProveOpts(KMirOpts): break_on_terminator_unreachable: bool break_every_terminator: bool break_every_step: bool + terminate_on_thunk: bool def __init__( self, @@ -77,6 +78,7 @@ def __init__( break_on_terminator_unreachable: bool = False, break_every_terminator: bool = False, break_every_step: bool = False, + terminate_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 @@ -97,6 +99,7 @@ def __init__( self.break_on_terminator_unreachable = break_on_terminator_unreachable self.break_every_terminator = break_every_terminator self.break_every_step = break_every_step + self.terminate_on_thunk = terminate_on_thunk @dataclass @@ -131,6 +134,7 @@ def __init__( break_on_terminator_unreachable: bool = False, break_every_terminator: bool = False, break_every_step: bool = False, + terminate_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 @@ -155,6 +159,7 @@ def __init__( self.break_on_terminator_unreachable = break_on_terminator_unreachable self.break_every_terminator = break_every_terminator self.break_every_step = break_every_step + self.terminate_on_thunk = terminate_on_thunk @dataclass From 8b294142f73b68e77d383ad17f600666484d061e Mon Sep 17 00:00:00 2001 From: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Date: Wed, 12 Nov 2025 01:01:43 +1000 Subject: [PATCH 3/4] Update kmir/src/kmir/kmir.py MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tamás Tóth --- kmir/src/kmir/kmir.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 93fc69910..44613c056 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -276,13 +276,10 @@ def is_terminal(self, cterm: CTerm) -> bool: k_cell = cterm.cell('K_CELL') if self.terminate_on_thunk: # terminate on `thunk ( ... )` rule + thunk = KLabel('thunk(_)_RT-DATA_Value_Evaluation') match k_cell: - case KApply(KLabel('thunk(_)_RT-DATA_Value_Evaluation', _)): + case KApply(thunk, _) | KSequence((KApply(thunk, _), *_)): return True - if type(k_cell) == KSequence and 0 < k_cell.arity: - match k_cell[0]: - case KApply(KLabel('thunk(_)_RT-DATA_Value_Evaluation', _)): - return True # #EndProgram if k_cell == KMIR.Symbols.END_PROGRAM: From c5b44f9a83a83441f69846bb821979710a7d98db Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 12 Nov 2025 01:19:11 +1000 Subject: [PATCH 4/4] Moved thunk `KLabel` to KMIR symbols --- kmir/src/kmir/kmir.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 44613c056..c5d629c62 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -128,6 +128,7 @@ def from_kompiled_kore( class Symbols: END_PROGRAM: Final = KApply('#EndProgram_KMIR-CONTROL-FLOW_KItem') + THUNK: Final = KLabel('thunk(_)_RT-DATA_Value_Evaluation') @cached_property def parser(self) -> Parser: @@ -276,9 +277,8 @@ def is_terminal(self, cterm: CTerm) -> bool: k_cell = cterm.cell('K_CELL') if self.terminate_on_thunk: # terminate on `thunk ( ... )` rule - thunk = KLabel('thunk(_)_RT-DATA_Value_Evaluation') match k_cell: - case KApply(thunk, _) | KSequence((KApply(thunk, _), *_)): + case KApply(label, _) | KSequence((KApply(label, _), *_)) if label == KMIR.Symbols.THUNK: return True # #EndProgram