From f23d3f986dbc251ff816f31c1c0562ae05609bed Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Thu, 29 Oct 2026 18:46:41 +0100 Subject: [PATCH] feat(access-control-prover): 9.4 exact evidence paths from summaries --- .kiro/specs/access-control-prover/tasks.md | 2 +- .../semantic/obligations/summaries.py | 117 +++++++++++- tests/test_obligation_summaries.py | 177 ++++++++++++++++++ 3 files changed, 293 insertions(+), 3 deletions(-) diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index f3cf647..e9748e0 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -156,7 +156,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Requirements: 3.8, 6.2, 6.3, 7.2_ - _Boundary: Function Summaries, Context Cache_ - _Depends: 9.2_ -- [ ] 9.4 Materialise exact evidence paths from summaries +- [x] 9.4 Materialise exact evidence paths from summaries - Emit concrete entry-to-operation hops only through exact target edges. - Preserve every complete chain independently and retain candidate-edge diagnostics separately. - Done when guarded and unguarded paths to one operation remain separate and candidate edges never complete a path. diff --git a/src/openultrasast/semantic/obligations/summaries.py b/src/openultrasast/semantic/obligations/summaries.py index de57469..28e6285 100644 --- a/src/openultrasast/semantic/obligations/summaries.py +++ b/src/openultrasast/semantic/obligations/summaries.py @@ -8,8 +8,11 @@ stable, so direct and mutual recursion terminate with the accumulated evidence. Task 9.3 (Reqs 3.8, 6.2, 6.3, 7.2): an exploration budget bounds the fixpoint; depth, fan-out and deadline cutoffs stop growth, record the exact cutoff reason and leave the affected summaries incomplete while -preserving the evidence accumulated so far. Summaries are deterministic and -carry no target names beyond fact identifiers (Req 11.7). +preserving the evidence accumulated so far. Task 9.4 (Reqs 3.9, 3.10, 11.4, +11.5): concrete evidence paths run from recognised entries to operations only +through exact target edges, every complete chain stays independent, and +candidate edges are diagnostics that never complete a path. Summaries are +deterministic and carry no target names beyond fact identifiers (Req 11.7). """ from collections.abc import Iterable, Iterator, Mapping @@ -373,3 +376,113 @@ def monotone_summaries( members = tuple(summaries_by_symbol[member] for member in component) _stabilise_component(members, summaries_by_symbol, edges, bounded) return tuple(summaries_by_symbol[summary.symbol] for summary in local) + + +@dataclass(frozen=True) +class EvidenceHop: + """One exact caller-to-callee transition with its call site line.""" + + caller: SymbolId + callee: SymbolId + line: int + + +@dataclass(frozen=True) +class EvidencePath: + """A concrete entry-to-operation chain of exact hops (Req 3.9).""" + + entry: SymbolId + target: SymbolId + hops: tuple[EvidenceHop, ...] = () + + +@dataclass(frozen=True) +class CandidateEdge: + """An ambiguous or unresolved call kept as a diagnostic (never a path edge).""" + + caller: SymbolId + candidates: tuple[SymbolId, ...] + line: int + reason: str + + +def exact_call_edges( + functions_by_module: Mapping[str, Iterable[FunctionIR]], + index: SymbolIndex, +) -> tuple[EvidenceHop, ...]: + """Caller-to-callee hops over complete single-target resolutions only.""" + hops: set[EvidenceHop] = set() + for module, functions in functions_by_module.items(): + for function_ir in functions: + caller = _function_symbol(index, module, function_ir) + for call in function_ir.calls: + target_set = resolve_call(call, module=module, index=index) + if target_set.completeness.is_complete and len(target_set.targets) == 1: + hops.add(EvidenceHop(caller, target_set.targets[0], call.line)) + return tuple(sorted(hops, key=lambda hop: (hop.caller.sort_key, hop.line, hop.callee.sort_key))) + + +def candidate_call_edges( + functions_by_module: Mapping[str, Iterable[FunctionIR]], + index: SymbolIndex, +) -> tuple[CandidateEdge, ...]: + """Every ambiguous or unresolved call as a diagnostic candidate edge.""" + edges: list[CandidateEdge] = [] + for module, functions in functions_by_module.items(): + for function_ir in functions: + caller = _function_symbol(index, module, function_ir) + for call in function_ir.calls: + target_set = resolve_call(call, module=module, index=index) + if target_set.completeness.is_complete and len(target_set.targets) == 1: + continue + reason = target_set.completeness.reasons[0] if target_set.completeness.reasons else "resolution:unresolved" + edges.append(CandidateEdge(caller, target_set.targets, call.line, reason)) + return tuple(sorted(edges, key=lambda edge: (edge.caller.sort_key, edge.line, edge.reason))) + + +def exact_evidence_paths( + entries: Iterable[SymbolId], + edges: Iterable[EvidenceHop], + *, + operations_by_symbol: Mapping[SymbolId, tuple[Operation, ...]] | None = None, +) -> tuple[EvidencePath, ...]: + """Materialise every concrete entry-to-operation chain through exact edges. + + Req 3.9: each chain carries the call site of every hop. Req 3.10: chains + to the same operation stay independent. Req 11.5: candidate edges never + complete a path, so they cannot make an enumeration look complete. + """ + operations_by_symbol = operations_by_symbol or {} + adjacency: dict[SymbolId, list[EvidenceHop]] = {} + for hop in sorted(edges, key=lambda hop: (hop.caller.sort_key, hop.line, hop.callee.sort_key)): + adjacency.setdefault(hop.caller, []).append(hop) + paths: list[EvidencePath] = [] + for entry in sorted(entries, key=lambda symbol: symbol.sort_key): + _walk_exact_paths(entry, entry, (), adjacency, operations_by_symbol, paths, frozenset({entry})) + return tuple(paths) + + +def _walk_exact_paths( + entry: SymbolId, + symbol: SymbolId, + hops_so_far: tuple[EvidenceHop, ...], + adjacency: Mapping[SymbolId, list[EvidenceHop]], + operations_by_symbol: Mapping[SymbolId, tuple[Operation, ...]], + paths: list[EvidencePath], + visited: frozenset[SymbolId], +) -> None: + """Depth-first walk emitting one path per operation-holding symbol reached.""" + if operations_by_symbol.get(symbol): + paths.append(EvidencePath(entry=entry, target=symbol, hops=hops_so_far)) + for hop in adjacency.get(symbol, ()): + if hop.callee in visited: + continue + _walk_exact_paths( + entry, + hop.callee, + hops_so_far + (hop,), + adjacency, + operations_by_symbol, + paths, + visited | {hop.callee}, + ) diff --git a/tests/test_obligation_summaries.py b/tests/test_obligation_summaries.py index e668d68..2ac74c9 100644 --- a/tests/test_obligation_summaries.py +++ b/tests/test_obligation_summaries.py @@ -15,8 +15,12 @@ from openultrasast.semantic.obligations.abstract_domain import Completeness from openultrasast.semantic.obligations.operations import Discharge, Operation from openultrasast.semantic.obligations.resolution import SymbolId, SymbolIndex from openultrasast.semantic.obligations.summaries import ( + EvidencePath, ExplorationBudget, FunctionSummary, + candidate_call_edges, + exact_call_edges, + exact_evidence_paths, local_summaries, monotone_summaries, ) @@ -499,3 +503,176 @@ def test_cutoff_reasons_join_existing_incompleteness() -> None: reasons = by_name["helper1"].completeness.reasons assert "resolution:no_candidate" in reasons assert "summaries:deadline_cutoff" in reasons + + +# --- Task 9.4: exact evidence paths (Reqs 3.9, 3.10, 11.4, 11.5) --- + +JAVA_ENTRY_CHAIN = """class Handler { + public void handle() { + this.run("job"); + } + public void run(String command) { + this.persist(command); + } + public void persist(String payload) { + } +} +""" + +JAVA_TWO_ROUTES = """class Gate { + public void enter() { + this.left(); + this.right(); + } + public void left() { + this.vault(); + } + public void right() { + this.vault(); + } + public void vault() { + } +} +""" + + +JAVA_AUDITOR = """class Auditor { + public void check() { + } +} +""" + + +def _chain_index() -> SymbolIndex: + return SymbolIndex.build( + ( + ("src/Handler.java", JAVA_ENTRY_CHAIN, "java"), + ("src/Auditor.java", JAVA_AUDITOR, "java"), + ) + ) + + +def _routes_index() -> SymbolIndex: + return SymbolIndex.build((("src/Gate.java", JAVA_TWO_ROUTES, "java"),)) + + +def _chain_functions() -> dict[str, tuple[FunctionIR, ...]]: + return { + "src/Handler.java": ( + FunctionIR("handle", (), 2, 4, (), (CallSite("run", 3, (), (), (), False, 0, receiver="this", arity=1),)), + FunctionIR("run", ("command",), 5, 7, (), (CallSite("persist", 6, (), (), (), False, 0, receiver="this", arity=1),)), + FunctionIR("persist", ("payload",), 8, 9, (), ()), + ) + } + + +def _routes_functions() -> dict[str, tuple[FunctionIR, ...]]: + return { + "src/Gate.java": ( + FunctionIR( + "enter", + (), + 2, + 5, + (), + ( + CallSite("left", 3, (), (), (), False, 0, receiver="this"), + CallSite("right", 4, (), (), (), False, 0, receiver="this"), + ), + ), + FunctionIR("left", (), 6, 8, (), (CallSite("vault", 7, (), (), (), False, 0, receiver="this"),)), + FunctionIR("right", (), 9, 11, (), (CallSite("vault", 10, (), (), (), False, 0, receiver="this"),)), + FunctionIR("vault", (), 12, 13, (), ()), + ) + } + + +def _symbol(index: SymbolIndex, name: str) -> SymbolId: + return next(symbol for symbol in index.by_name[name] if symbol.module == "src/Handler.java") + + +def _routes_symbol(index: SymbolIndex, name: str) -> SymbolId: + return next(symbol for symbol in index.by_name[name] if symbol.module == "src/Gate.java") + + +def test_exact_edges_carry_call_site_lines() -> None: + index = _chain_index() + edges = exact_call_edges(_chain_functions(), index) + pairs = {(edge.caller.name, edge.callee.name): edge.line for edge in edges} + assert pairs[("handle", "run")] == 3 + assert pairs[("run", "persist")] == 6 + + +def test_entry_chain_emits_hops_from_entry_to_operation() -> None: + index = _chain_index() + edges = exact_call_edges(_chain_functions(), index) + persist_symbol = _symbol(index, "persist") + paths = exact_evidence_paths( + (_symbol(index, "handle"),), + edges, + operations_by_symbol={persist_symbol: (_java_operation("persist", 9),)}, + ) + assert len(paths) == 1 + assert paths[0].entry.name == "handle" + assert paths[0].target.name == "persist" + assert [hop.callee.name for hop in paths[0].hops] == ["run", "persist"] + assert paths[0].hops[0].line == 3 + + +def test_entry_itself_holding_an_operation_emits_a_zero_hop_path() -> None: + index = _chain_index() + edges = exact_call_edges(_chain_functions(), index) + handle_symbol = _symbol(index, "handle") + paths = exact_evidence_paths( + (handle_symbol,), + edges, + operations_by_symbol={handle_symbol: (_java_operation("handle", 3),)}, + ) + assert paths == (EvidencePath(entry=handle_symbol, target=handle_symbol, hops=()),) + + +def test_two_complete_chains_to_one_operation_stay_independent() -> None: + index = _routes_index() + edges = exact_call_edges(_routes_functions(), index) + enter = _routes_symbol(index, "enter") + vault = _routes_symbol(index, "vault") + paths = exact_evidence_paths( + (enter,), + edges, + operations_by_symbol={vault: (_java_operation("vault", 12),)}, + ) + routes = sorted(tuple(hop.callee.name for hop in path.hops) for path in paths) + assert routes == [("left", "vault"), ("right", "vault")] + assert all(path.target == vault for path in paths) + + +def test_candidate_edges_never_complete_a_path() -> None: + index = _chain_index() + functions = { + "src/Handler.java": (FunctionIR("handle", (), 2, 4, (), (CallSite("check", 3, (), (), (), False, 0, receiver="auditor"),)),) + + _chain_functions()["src/Handler.java"][1:] + } + edges = exact_call_edges(functions, index) + auditor = next(symbol for symbol in index.by_name["check"] if symbol.module == "src/Auditor.java") + paths = exact_evidence_paths( + (_symbol(index, "handle"),), + edges, + operations_by_symbol={auditor: (_java_operation("check", 1),)}, + ) + assert paths == () + diagnostics = candidate_call_edges(functions, index) + assert len(diagnostics) == 1 + assert diagnostics[0].caller.name == "handle" + assert diagnostics[0].reason == "resolution:receiver_type_unknown" + assert any(candidate.enclosing_type == "Auditor" for candidate in diagnostics[0].candidates) + + +def test_exact_evidence_paths_are_deterministic() -> None: + index = _routes_index() + edges = exact_call_edges(_routes_functions(), index) + enter = _routes_symbol(index, "enter") + vault = _routes_symbol(index, "vault") + operations = {vault: (_java_operation("vault", 12),)} + assert exact_evidence_paths((enter,), edges, operations_by_symbol=operations) == exact_evidence_paths( + (enter,), edges, operations_by_symbol=operations + )