diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 8de67ff4f..af2ca4d7d 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -84,6 +84,35 @@ def _kmir_view(opts: ViewOpts) -> None: viewer.run() +def _write_to_module(kmir: KMIR, proof: APRProof, to_module_path: Path) -> None: + """Write proof KCFG as a K module to the specified path.""" + import json + + from pyk.kast.manip import remove_generated_cells + from pyk.kast.outer import KRule + + # Generate K module using KCFG.to_module with defunc_with for proper function inlining + module_name = proof.id.upper().replace('.', '-').replace('_', '-') + '-SUMMARY' + k_module = proof.kcfg.to_module(module_name=module_name, defunc_with=kmir.definition) + + if to_module_path.suffix == '.json': + # JSON format for --add-module: keep for Kore conversion + # Note: We don't use minimize_rule_like here because it creates partial configs + # with dots that cannot be converted back to Kore + to_module_path.write_text(json.dumps(k_module.to_dict(), indent=2)) + else: + # K text format for human readability: remove and + def _process_sentence(sent): # type: ignore[no-untyped-def] + if isinstance(sent, KRule): + sent = sent.let(body=remove_generated_cells(sent.body)) + return sent + + k_module_readable = k_module.let(sentences=[_process_sentence(sent) for sent in k_module.sentences]) + k_module_text = kmir.pretty_print(k_module_readable) + to_module_path.write_text(k_module_text) + _LOGGER.info(f'Module written to: {to_module_path}') + + def _kmir_show(opts: ShowOpts) -> None: from pyk.kast.pretty import PrettyPrinter @@ -92,6 +121,13 @@ def _kmir_show(opts: ShowOpts) -> None: kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR) proof = APRProof.read_proof_data(opts.proof_dir, opts.id) + # Minimize proof KCFG if requested + if opts.minimize_proof: + _LOGGER.info('Minimizing proof KCFG...') + proof.minimize_kcfg() + proof.write_proof_data() + _LOGGER.info('Proof KCFG minimized and saved') + # Use custom KMIR printer by default, switch to standard printer if requested if opts.use_default_printer: printer = PrettyPrinter(kmir.definition) @@ -119,6 +155,7 @@ def _kmir_show(opts: ShowOpts) -> None: nodes=opts.nodes or (), node_deltas=effective_node_deltas, omit_cells=tuple(all_omit_cells), + to_module=opts.to_module is not None, ) if opts.statistics: if lines and lines[-1] != '': @@ -132,7 +169,12 @@ def _kmir_show(opts: ShowOpts) -> None: lines.append('') lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show)) - print('\n'.join(lines)) + # Handle --to-module output + if opts.to_module: + _write_to_module(kmir, proof, opts.to_module) + print(f'Module written to: {opts.to_module}') + else: + print('\n'.join(lines)) def _kmir_prune(opts: PruneOpts) -> None: @@ -410,6 +452,17 @@ def _arg_parser() -> ArgumentParser: ) show_parser.add_argument('--rules', metavar='EDGES', help='Comma separated list of edges in format "source:target"') + show_parser.add_argument( + '--to-module', + type=Path, + metavar='FILE', + help='Output path for K module file (.k for readable, .json for --add-module)', + ) + show_parser.add_argument( + '--minimize-proof', + action='store_true', + help='Minimize the proof KCFG before exporting to module', + ) command_parser.add_parser( 'view', help='View proof information', parents=[kcli_args.logging_args, proof_args, display_args] @@ -443,6 +496,12 @@ def _arg_parser() -> ArgumentParser: prove_rs_parser.add_argument( '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from' ) + prove_rs_parser.add_argument( + '--add-module', + type=Path, + metavar='FILE', + help='K module file to include (.json format from --to-module)', + ) link_parser = command_parser.add_parser( 'link', help='Link together 2 or more SMIR JSON files', parents=[kcli_args.logging_args] @@ -530,6 +589,7 @@ def _parse_args(ns: Namespace) -> KMirOpts: break_every_terminator=ns.break_every_terminator, break_every_step=ns.break_every_step, terminate_on_thunk=ns.terminate_on_thunk, + add_module=ns.add_module, ) case 'link': return LinkOpts( diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 7453c1325..4b0a90c63 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -119,7 +119,11 @@ def cut_point_rules( @staticmethod def from_kompiled_kore( - smir_info: SMIRInfo, target_dir: Path, bug_report: Path | None = None, symbolic: bool = True + smir_info: SMIRInfo, + target_dir: Path, + bug_report: Path | None = None, + symbolic: bool = True, + extra_module: Path | None = None, ) -> KMIR: from .kompile import kompile_smir @@ -128,6 +132,7 @@ def from_kompiled_kore( target_dir=target_dir, bug_report=bug_report, symbolic=symbolic, + extra_module=extra_module, ) return kompiled_smir.create_kmir(bug_report_file=bug_report) @@ -213,7 +218,11 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: smir_info = SMIRInfo.from_file(target_path / 'smir.json') kmir = KMIR.from_kompiled_kore( - smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path + smir_info, + symbolic=True, + bug_report=opts.bug_report, + target_dir=target_path, + extra_module=opts.add_module, ) else: _LOGGER.info(f'Constructing initial proof: {label}') @@ -237,7 +246,11 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}') kmir = KMIR.from_kompiled_kore( - smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path + smir_info, + symbolic=True, + bug_report=opts.bug_report, + target_dir=target_path, + extra_module=opts.add_module, ) apr_proof = kmir.apr_proof_from_smir( @@ -267,7 +280,11 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: ) 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 = APRProver( + kcfg_explore, + execute_depth=opts.max_depth, + cut_point_rules=cut_point_rules, + ) prover.advance_proof( apr_proof, max_iterations=opts.max_iterations, diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index cecd65215..658ed76d2 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -91,11 +91,46 @@ def _digest_file(target_dir: Path) -> Path: return target_dir / 'smir-digest.json' +def _load_extra_module_rules(kmir: KMIR, module_path: Path) -> list[Sentence]: + """Load a K module from JSON and convert rules to Kore axioms. + + Args: + kmir: KMIR instance with the definition + module_path: Path to JSON module file (from --to-module output.json) + + Returns: + List of Kore axioms converted from the module rules + """ + from pyk.kast.outer import KFlatModule, KRule + from pyk.konvert import krule_to_kore + + _LOGGER.info(f'Loading extra module rules: {module_path}') + + if module_path.suffix != '.json': + _LOGGER.warning(f'Only JSON format is supported for --add-module: {module_path}') + return [] + + module_dict = json.loads(module_path.read_text()) + k_module = KFlatModule.from_dict(module_dict) + + axioms: list[Sentence] = [] + for sentence in k_module.sentences: + if isinstance(sentence, KRule): + try: + axiom = krule_to_kore(kmir.definition, sentence) + axioms.append(axiom) + except Exception: + _LOGGER.warning(f'Failed to convert rule to Kore: {sentence}', exc_info=True) + + return axioms + + def kompile_smir( smir_info: SMIRInfo, target_dir: Path, bug_report: Path | None = None, symbolic: bool = True, + extra_module: Path | None = None, ) -> KompiledSMIR: kompile_digest: KompileDigest | None = None try: @@ -120,8 +155,18 @@ def kompile_smir( target_dir.mkdir(parents=True, exist_ok=True) kmir = KMIR(HASKELL_DEF_DIR) - rules = make_kore_rules(kmir, smir_info) - _LOGGER.info(f'Generated {len(rules)} function equations to add to `definition.kore') + smir_rules: list[Sentence] = list(make_kore_rules(kmir, smir_info)) + _LOGGER.info(f'Generated {len(smir_rules)} function equations to add to `definition.kore') + + # Load and convert extra module rules if provided + # These are kept separate because LLVM backend doesn't support configuration rewrites + extra_rules: list[Sentence] = [] + if extra_module is not None: + extra_rules = _load_extra_module_rules(kmir, extra_module) + _LOGGER.info(f'Added {len(extra_rules)} rules from extra module: {extra_module}') + + # Combined rules for Haskell backend (supports both function equations and rewrites) + all_rules = smir_rules + extra_rules if symbolic: # Create output directories @@ -131,11 +176,12 @@ def kompile_smir( target_llvmdt_path.mkdir(parents=True, exist_ok=True) target_hs_path.mkdir(parents=True, exist_ok=True) - # Process LLVM definition + # Process LLVM definition (only SMIR rules, not extra module rules) + # Extra module rules are configuration rewrites that LLVM backend doesn't support _LOGGER.info('Writing LLVM definition file') llvm_def_file = LLVM_LIB_DIR / 'definition.kore' llvm_def_output = target_llvm_lib_path / 'definition.kore' - _insert_rules_and_write(llvm_def_file, rules, llvm_def_output) + _insert_rules_and_write(llvm_def_file, smir_rules, llvm_def_output) # Run llvm-kompile-matching and llvm-kompile for LLVM # TODO use pyk to do this if possible (subprocess wrapper, maybe llvm-kompile itself?) @@ -161,10 +207,10 @@ def kompile_smir( check=True, ) - # Process Haskell definition + # Process Haskell definition (includes both SMIR rules and extra module rules) _LOGGER.info('Writing Haskell definition file') hs_def_file = HASKELL_DEF_DIR / 'definition.kore' - _insert_rules_and_write(hs_def_file, rules, target_hs_path / 'definition.kore') + _insert_rules_and_write(hs_def_file, all_rules, target_hs_path / 'definition.kore') # Copy all files except definition.kore and binary from HASKELL_DEF_DIR to out/hs _LOGGER.info('Copying other artefacts into HS output directory') @@ -183,11 +229,11 @@ def kompile_smir( _LOGGER.info(f'Creating directory {target_llvmdt_path}') target_llvmdt_path.mkdir(parents=True, exist_ok=True) - # Process LLVM definition + # Process LLVM definition (only SMIR rules for concrete execution) _LOGGER.info('Writing LLVM definition file') llvm_def_file = LLVM_LIB_DIR / 'definition.kore' llvm_def_output = target_llvm_path / 'definition.kore' - _insert_rules_and_write(llvm_def_file, rules, llvm_def_output) + _insert_rules_and_write(llvm_def_file, smir_rules, llvm_def_output) import subprocess diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index b50af33e5..97e5864fe 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -114,6 +114,7 @@ class ProveRSOpts(ProveOpts): save_smir: bool smir: bool start_symbol: str + add_module: Path | None def __init__( self, @@ -143,6 +144,7 @@ def __init__( break_every_terminator: bool = False, break_every_step: bool = False, terminate_on_thunk: bool = False, + add_module: Path | None = None, ) -> None: self.rs_file = rs_file self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None @@ -170,6 +172,7 @@ def __init__( self.break_every_terminator = break_every_terminator self.break_every_step = break_every_step self.terminate_on_thunk = terminate_on_thunk + self.add_module = add_module @dataclass @@ -204,6 +207,8 @@ class ShowOpts(DisplayOpts): use_default_printer: bool statistics: bool leaves: bool + to_module: Path | None + minimize_proof: bool def __init__( self, @@ -221,12 +226,16 @@ def __init__( use_default_printer: bool = False, statistics: bool = False, leaves: bool = False, + to_module: Path | None = None, + minimize_proof: bool = False, ) -> None: super().__init__(proof_dir, id, full_printer, smir_info, omit_current_body) self.omit_static_info = omit_static_info self.use_default_printer = use_default_printer self.statistics = statistics self.leaves = leaves + self.to_module = to_module + self.minimize_proof = minimize_proof self.nodes = tuple(int(n.strip()) for n in nodes.split(',')) if nodes is not None else None def _parse_pairs(text: str | None) -> tuple[tuple[int, int], ...] | None: diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json new file mode 100644 index 000000000..9cf02027b --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.json @@ -0,0 +1,901 @@ +{ + "node": "KFlatModule", + "name": "ASSERT-TRUE-MAIN-SUMMARY", + "localSentences": [ + { + "node": "KRule", + "body": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "#execTerminator(_)_KMIR-CONTROL-FLOW_KItem_Terminator", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "terminator(_,_)_BODY_Terminator_TerminatorKind_Span", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "TerminatorKind::Call", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "Operand::Constant", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "span", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "mirConst(_,_,_)_TYPES_MirConst_ConstantKind_Ty_MirConstId", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ConstantKind::ZeroSized", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ty", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "-1", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "mirConstId(_)_TYPES_MirConstId_Int", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 3, + "variable": false + } + ], + "arity": 3, + "variable": false + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "Operands::empty", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "place", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "local", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ProjectionElems::empty", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 2, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "noBasicBlockIdx_BODY_MaybeBasicBlockIdx", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "UnwindAction::Continue", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 5, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "span", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 2, + "variable": false + } + ], + "arity": 1, + "variable": false + }, + "rhs": { + "node": "KSequence", + "items": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "#EndProgram_KMIR-CONTROL-FLOW_KItem", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 1 + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KVariable", + "name": "_RETVAL_CELL" + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KVariable", + "name": "CURRENTFUNC_CELL" + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ty", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "-1", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KVariable", + "name": "_CURRENTBODY_CELL" + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ListItem", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "basicBlock(_,_)_BODY_BasicBlock_Statements_Terminator", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "Statements::empty", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "terminator(_,_)_BODY_Terminator_TerminatorKind_Span", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "TerminatorKind::Return", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "span", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "50", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 2, + "variable": false + } + ], + "arity": 2, + "variable": false + } + ], + "arity": 1, + "variable": false + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KVariable", + "name": "CALLER_CELL" + }, + "rhs": { + "node": "KVariable", + "name": "CURRENTFUNC_CELL", + "sort": { + "node": "KSort", + "name": "Ty" + } + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KVariable", + "name": "DEST_CELL" + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "place", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "local", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ProjectionElems::empty", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 2, + "variable": false + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KVariable", + "name": "TARGET_CELL" + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "noBasicBlockIdx_BODY_MaybeBasicBlockIdx", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KVariable", + "name": "UNWIND_CELL" + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "UnwindAction::Continue", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ListItem", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "newLocal", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ty", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + }, + "rhs": { + "node": "KToken", + "token": "1", + "sort": { + "node": "KSort", + "name": "Int" + } + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KRewrite", + "lhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "Mutability::Not", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "Mutability::Mut", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + } + ], + "arity": 2, + "variable": false + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 6, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KRewrite", + "lhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": ".List", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + }, + "rhs": { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ListItem", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "StackFrame(_,_,_,_,_)_KMIR-CONFIGURATION_StackFrame_Ty_Place_MaybeBasicBlockIdx_UnwindAction_List", + "params": [] + }, + "args": [ + { + "node": "KVariable", + "name": "CALLER_CELL", + "sort": { + "node": "KSort", + "name": "Ty" + } + }, + { + "node": "KVariable", + "name": "DEST_CELL", + "sort": { + "node": "KSort", + "name": "Place" + } + }, + { + "node": "KVariable", + "name": "TARGET_CELL", + "sort": { + "node": "KSort", + "name": "MaybeBasicBlockIdx" + } + }, + { + "node": "KVariable", + "name": "UNWIND_CELL", + "sort": { + "node": "KSort", + "name": "UnwindAction" + } + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ListItem", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "newLocal", + "params": [] + }, + "args": [ + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "ty", + "params": [] + }, + "args": [ + { + "node": "KToken", + "token": "0", + "sort": { + "node": "KSort", + "name": "Int" + } + } + ], + "arity": 1, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "Mutability::Not", + "params": [] + }, + "args": [], + "arity": 0, + "variable": false + } + ], + "arity": 2, + "variable": false + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 5, + "variable": false + } + ], + "arity": 1, + "variable": false + } + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 5, + "variable": false + }, + { + "node": "KApply", + "label": { + "node": "KLabel", + "name": "", + "params": [] + }, + "args": [ + { + "node": "KVariable", + "name": "_GENERATEDCOUNTER_CELL" + } + ], + "arity": 1, + "variable": false + } + ], + "arity": 2, + "variable": false + }, + "requires": { + "node": "KToken", + "token": "true", + "sort": { + "node": "KSort", + "name": "Bool" + } + }, + "ensures": { + "node": "KToken", + "token": "true", + "sort": { + "node": "KSort", + "name": "Bool" + } + }, + "att": { + "node": "KAtt", + "att": { + "priority": "20", + "label": "BASIC-BLOCK-1-TO-3" + } + } + } + ], + "imports": [], + "att": { + "node": "KAtt", + "att": {} + } +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k new file mode 100644 index 000000000..58b96e706 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.to-module.k @@ -0,0 +1,40 @@ +module ASSERT-TRUE-MAIN-SUMMARY + + + rule [BASIC-BLOCK-1-TO-3]: + + ( #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandConstant ( constOperand ( ... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindZeroSized , ty: ty ( -1 ) , id: mirConstId ( 0 ) ) ) ) , args: .Operands , destination: place ( ... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) => #EndProgram ~> .K ) + + + _RETVAL_CELL + + + ( CURRENTFUNC_CELL => ty ( -1 ) ) + + + + ( _CURRENTBODY_CELL => ListItem ( basicBlock ( ... statements: .Statements , terminator: terminator ( ... kind: terminatorKindReturn , span: span ( 50 ) ) ) ) ) + + + ( CALLER_CELL => CURRENTFUNC_CELL:Ty ) + + + ( DEST_CELL => place ( ... local: local ( 0 ) , projection: .ProjectionElems ) ) + + + ( TARGET_CELL => noBasicBlockIdx ) + + + ( UNWIND_CELL => unwindActionContinue ) + + + ListItem ( newLocal ( ty ( ( 0 => 1 ) ) , ( mutabilityNot => mutabilityMut ) ) ) + + + + ( .List => ListItem ( StackFrame ( CALLER_CELL:Ty , DEST_CELL:Place , TARGET_CELL:MaybeBasicBlockIdx , UNWIND_CELL:UnwindAction , ListItem ( newLocal ( ty ( 0 ) , mutabilityNot ) ) ) ) ) + + + [priority(20), label(BASIC-BLOCK-1-TO-3)] + +endmodule \ No newline at end of file diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py index b681e8710..355026a52 100644 --- a/kmir/src/tests/integration/test_cli.py +++ b/kmir/src/tests/integration/test_cli.py @@ -20,9 +20,14 @@ def _prove_and_store( - kmir: KMIR, rs_or_json: Path, tmp_path: Path, start_symbol: str = 'main', is_smir: bool = False + kmir: KMIR, + rs_or_json: Path, + tmp_path: Path, + start_symbol: str = 'main', + is_smir: bool = False, + max_depth: int | None = None, ) -> APRProof: - opts = ProveRSOpts(rs_or_json, proof_dir=tmp_path, smir=is_smir, start_symbol=start_symbol) + opts = ProveRSOpts(rs_or_json, proof_dir=tmp_path, smir=is_smir, start_symbol=start_symbol, max_depth=max_depth) apr_proof = kmir.prove_rs(opts) apr_proof.write_proof_data() return apr_proof @@ -172,3 +177,120 @@ def test_cli_prune_snapshot( assert_or_update_show_output( out, PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-prune.expected', update=update_expected_output ) + + +def test_cli_show_to_module( + kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool +) -> None: + """Test --to-module option with both K text and JSON output formats.""" + rs_file = PROVE_RS_DIR / 'assert-true.rs' + start_symbol = 'main' + apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False) + + # Test K text output + module_k_output = tmp_path / 'summary.k' + show_opts_k = ShowOpts( + proof_dir=tmp_path, + id=apr_proof.id, + full_printer=False, + smir_info=None, + omit_current_body=True, + use_default_printer=False, + to_module=module_k_output, + ) + _kmir_show(show_opts_k) + capsys.readouterr() # Clear captured output + + assert module_k_output.exists(), 'Module K file should be created' + k_content = module_k_output.read_text() + assert_or_update_show_output( + k_content.rstrip(), + PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.k', + update=update_expected_output, + ) + + # Test JSON output (for --add-module) + module_json_output = tmp_path / 'summary.json' + show_opts_json = ShowOpts( + proof_dir=tmp_path, + id=apr_proof.id, + full_printer=False, + smir_info=None, + omit_current_body=True, + use_default_printer=False, + to_module=module_json_output, + ) + _kmir_show(show_opts_json) + capsys.readouterr() # Clear captured output + + assert module_json_output.exists(), 'Module JSON file should be created' + json_content = module_json_output.read_text() + # Verify it's valid JSON + json.loads(json_content) + assert_or_update_show_output( + json_content.rstrip(), + PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.json', + update=update_expected_output, + ) + + +def test_cli_show_minimize_proof(kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str]) -> None: + """Test --minimize-proof option.""" + rs_file = PROVE_RS_DIR / 'symbolic-args-fail.rs' + start_symbol = 'main' + # Use limited depth to create a partial proof with intermediate nodes that can be minimized + apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False, max_depth=5) + + # Get initial node count + from pyk.proof.reachability import APRProof + + initial_proof = APRProof.read_proof_data(tmp_path, apr_proof.id) + initial_node_count = len(list(initial_proof.kcfg.nodes)) + + # Run show with minimize_proof + show_opts = ShowOpts( + proof_dir=tmp_path, + id=apr_proof.id, + full_printer=False, + smir_info=None, + omit_current_body=True, + use_default_printer=False, + minimize_proof=True, + ) + _kmir_show(show_opts) + capsys.readouterr() # Clear captured output + + # Read the minimized proof + minimized_proof = APRProof.read_proof_data(tmp_path, apr_proof.id) + minimized_node_count = len(list(minimized_proof.kcfg.nodes)) + + # Verify minimization reduced (or didn't increase) node count + assert ( + minimized_node_count < initial_node_count + ), f'Minimization should not increase node count: {minimized_node_count} > {initial_node_count}' + + +def test_cli_prove_rs_add_module(kmir: KMIR, tmp_path: Path) -> None: + """Test --add-module option for prove-rs using stored module files.""" + from kmir.kmir import KMIR + + rs_file = PROVE_RS_DIR / 'assert-true.rs' + start_symbol = 'main' + + # Use the stored JSON module file generated by --to-module + stored_module_json = PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.to-module.json' + assert stored_module_json.exists(), f'Stored JSON module file not found: {stored_module_json}' + + # Run prove-rs with --add-module and max_depth=1 + opts_with_module = ProveRSOpts( + rs_file, + proof_dir=tmp_path, + smir=False, + start_symbol=start_symbol, + max_depth=1, + add_module=stored_module_json, + ) + proof_with_module = KMIR.prove_rs(opts_with_module) + + # With depth=1, we should have 3 nodes: init, one step, target + assert len(list(proof_with_module.kcfg.nodes)) == 3