Cut point rules and section edge command in KMIR (#780)

This PR adds:
- The option `--break-on-calls` to `kmir prove` which will break the
proof at the rule `#setUpCalleeData` for easy linking of proof to source
code
- The command `kmir section-edge` which can be provided an existing
proof and an edge (two linked nodes in the kcfg) as a tuple (e.g. `4,5`)
and will proof an amount of nodes breaking the edge up. In particular I
find this may be useful if we can identify when a thunk is written to
`<locals>` and we can section out the edge between the node it appears
and the call above it. If the distance between the nodes is `n` steps,
then the max sections is `n - 1` which will take 1 step.

### Current Problems
- `--break-on-calls` is outputing the node at `#setUpCalleeData` but is
also outputting the node afterwards `#setArgsFromStack` which is
doubling the amount of output - I did look but can't understand why this
is happening currently, however it is also not a deal breaker for me
right now - I am still able to see the nodes I want and just some extra.
UPDATE: This behaviour is also the same with Kontrol so I think this is
a broader thing with K pr pyk

---------

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Author: dkcumming

kmir/src/kmir/__main__.py

@@ -24,6 +24,7 @@
     ProveRSOpts,
     PruneOpts,
     RunOpts,
+    SectionEdgeOpts,
     ShowOpts,
     ViewOpts,
 )
@@ -141,6 +142,38 @@ def _kmir_prune(opts: PruneOpts) -> None:
     proof.write_proof_data()
 
 
+def _kmir_section_edge(opts: SectionEdgeOpts) -> None:
+    # Proof dir is checked to be some in arg parsing for instructive errors
+    assert opts.proof_dir is not None
+
+    if not APRProof.proof_data_exists(opts.id, opts.proof_dir):
+        raise ValueError(f'Proof id {opts.id} not found in proof dir {opts.proof_dir}')
+
+    target_path = opts.proof_dir / opts.id
+
+    _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {opts.id}')
+    apr_proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
+
+    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)
+
+    source_id, target_id = opts.edge
+    _LOGGER.info(f'Attempting to add {opts.sections} sections from node {source_id} to node {target_id}')
+
+    with kmir.kcfg_explore(apr_proof.id) as kcfg_explore:
+        node_ids = kcfg_explore.section_edge(
+            apr_proof.kcfg,
+            source_id=int(source_id),
+            target_id=int(target_id),
+            logs=apr_proof.logs,
+            sections=opts.sections,
+        )
+        _LOGGER.info(f'Added nodes on edge {(source_id, target_id)}: {node_ids}')
+
+    apr_proof.write_proof_data()
+
+
 def _kmir_info(opts: InfoOpts) -> None:
     smir_info = SMIRInfo.from_file(opts.smir_file)
 
@@ -171,6 +204,8 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_show(opts)
         case PruneOpts():
             _kmir_prune(opts)
+        case SectionEdgeOpts():
+            _kmir_section_edge(opts)
         case ProveRSOpts():
             _kmir_prove_rs(opts)
         case LinkOpts():
@@ -210,6 +245,9 @@ def _arg_parser() -> ArgumentParser:
         '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take'
     )
     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'
+    )
 
     proof_args = ArgumentParser(add_help=False)
     proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view')
@@ -287,6 +325,16 @@ def _arg_parser() -> ArgumentParser:
     )
     prune_parser.add_argument('node_id', metavar='NODE', type=int, help='The node to prune')
 
+    section_edge_parser = command_parser.add_parser(
+        'section-edge', help='Break an edge into sections', parents=[kcli_args.logging_args, proof_args]
+    )
+    section_edge_parser.add_argument(
+        'edge', type=lambda s: tuple(s.split(',')), help='Edge to section in CFG (format: `source,target`)'
+    )
+    section_edge_parser.add_argument(
+        '--sections', type=int, default=2, help='Number of sections to make from edge (>= 2, default: 2)'
+    )
+
     prove_rs_parser = command_parser.add_parser(
         'prove-rs', help='Prove a rust program', parents=[kcli_args.logging_args, prove_args]
     )
@@ -354,6 +402,11 @@ def _parse_args(ns: Namespace) -> KMirOpts:
         case 'prune':
             proof_dir = Path(ns.proof_dir)
             return PruneOpts(proof_dir, ns.id, ns.node_id)
+        case 'section-edge':
+            if ns.proof_dir is None:
+                raise ValueError('Must pass --proof-dir to section-edge command')
+            proof_dir = Path(ns.proof_dir)
+            return SectionEdgeOpts(proof_dir, ns.id, ns.edge, ns.sections)
         case 'prove-rs':
             return ProveRSOpts(
                 rs_file=Path(ns.rs_file),
@@ -365,6 +418,7 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 save_smir=ns.save_smir,
                 smir=ns.smir,
                 start_symbol=ns.start_symbol,
+                break_on_calls=ns.break_on_calls,
             )
         case 'link':
             return LinkOpts(

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -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 <k> #setUpCalleeData(
+  rule [call]: <k> #setUpCalleeData(
               monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
               ARGS
               )

kmir/src/kmir/kmir.py

@@ -53,6 +53,19 @@ def __init__(
         KParse.__init__(self, definition_dir)
         self.llvm_library_dir = llvm_library_dir
 
+    @staticmethod
+    def cut_point_rules(
+        break_on_calls: bool,
+    ) -> list[str]:
+        cut_point_rules = []
+        if break_on_calls:
+            cut_point_rules.extend(
+                [
+                    'KMIR-CONTROL-FLOW.call',
+                ]
+            )
+        return cut_point_rules
+
     @staticmethod
     def from_kompiled_kore(
         smir_info: SMIRInfo, target_dir: Path, bug_report: Path | None = None, symbolic: bool = True
@@ -184,8 +197,10 @@ 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)
+
             with kmir.kcfg_explore(label) as kcfg_explore:
-                prover = APRProver(kcfg_explore, execute_depth=opts.max_depth)
+                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
 

kmir/src/kmir/options.py

@@ -41,6 +41,7 @@ class ProveOpts(KMirOpts):
     max_depth: int | None
     max_iterations: int | None
     reload: bool
+    break_on_calls: bool
 
     def __init__(
         self,
@@ -49,12 +50,14 @@ def __init__(
         max_depth: int | None = None,
         max_iterations: int | None = None,
         reload: bool = False,
+        break_on_calls: 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
 
 
 @dataclass
@@ -75,6 +78,7 @@ def __init__(
         save_smir: bool = False,
         smir: bool = False,
         start_symbol: str = 'main',
+        break_on_calls: bool = False,
     ) -> None:
         self.rs_file = rs_file
         self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
@@ -85,6 +89,7 @@ def __init__(
         self.save_smir = save_smir
         self.smir = smir
         self.start_symbol = start_symbol
+        self.break_on_calls = break_on_calls
 
 
 @dataclass
@@ -187,6 +192,26 @@ def __init__(self, smir_file: Path, types: str | None = None) -> None:
         self.types = tuple(int(t.strip()) for t in types.split(',')) if types is not None else None
 
 
+@dataclass
+class SectionEdgeOpts(ProofOpts):
+    edge: tuple[str, str]
+    sections: int
+
+    def __init__(
+        self,
+        proof_dir: Path | str,
+        id: str,
+        edge: tuple[str, str],
+        sections: int = 2,
+        bug_report: Path | None = None,
+    ) -> None:
+        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
+        self.id = id
+        self.edge = edge
+        self.sections = sections
+        self.bug_report = bug_report
+
+
 @dataclass
 class LinkOpts(KMirOpts):
     smir_files: list[Path]