diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index e9748e0..99e30e9 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -165,7 +165,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Depends: 9.3_ - [ ] 10. Strict authorization judgment -- [ ] 10.1 Return abstract dominance relations without prover fallback +- [x] 10.1 Return abstract dominance relations without prover fallback - Return MUST, MAY, NO or UNKNOWN with guard effect and control context. - Keep legacy order dominance unchanged, but return UNKNOWN in prover mode for unavailable graphs or line mappings. - Done when no prover fixture is discharged or flagged solely through textual-order fallback. diff --git a/src/openultrasast/semantic/obligations/cfg_dominance.py b/src/openultrasast/semantic/obligations/cfg_dominance.py index 55df9b4..9a38f56 100644 --- a/src/openultrasast/semantic/obligations/cfg_dominance.py +++ b/src/openultrasast/semantic/obligations/cfg_dominance.py @@ -16,9 +16,11 @@ from __future__ import annotations import re from collections.abc import Mapping, Sequence +from dataclasses import dataclass from typing import Any from ..cfg import ControlContext, FunctionCfg +from .abstract_domain import EvidenceRelation from .dominance import Dominance, OrderDominance from .operations import Discharge, Operation @@ -31,6 +33,15 @@ _EXIT_LINE = re.compile(r"^\s*(?Preturn\b|raise\b|throw\b|abort\(|sys\.exi CfgEntry = FunctionCfg | Sequence[FunctionCfg] | None +@dataclass(frozen=True) +class DominanceEvidence: + """The strict dominance answer for prover mode: a relation, the guard's failure effect, and a reason when unknown.""" + + relation: EvidenceRelation + guard_effect: str | None = None + reason: str | None = None + + class CfgDominance: """Dominance over control-flow graphs keyed by (path, function), with order as the recorded fallback.""" @@ -83,6 +94,36 @@ class CfgDominance: return False return cfg.effect(witness.line, operation.line, throwing=witness.kind in _THROWING) != "value_only" + def evidence(self, witness: Discharge, operation: Operation) -> DominanceEvidence: + """Strict abstract relation (task 10.1): never falls back to order dominance. + + Unavailable graphs, unmapped lines and cross-function witnesses return UNKNOWN with a + reason; the legacy boolean surface keeps its order fallback for non-opt-in callers. + """ + decided = _pre_graph_evidence(witness, operation) + if decided is not None: + return decided + guard_line = witness.line + if guard_line is None: # decided above; kept for line-type narrowing + return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:no_line") + cfg = self.graph(operation.path, operation.function, operation.line) + if cfg is None: + return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "cfg_unavailable") + found = cfg.relation(guard_line, operation.line) + if found is None: + return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "line_without_node") + if found == "all_paths": + effect = cfg.effect(guard_line, operation.line, throwing=witness.kind in _THROWING) + if effect == "value_only": + return DominanceEvidence(EvidenceRelation.NO, effect) + return DominanceEvidence(EvidenceRelation.MUST, effect) + if found == "some_paths": + effect = cfg.effect(guard_line, operation.line, throwing=witness.kind in _THROWING) + return DominanceEvidence(EvidenceRelation.MAY, effect) + if found in ("none", "after"): + return DominanceEvidence(EvidenceRelation.NO, None) + return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:unmapped_relation") + def relation(self, witness: Discharge, operation: Operation) -> str: cfg = self._local(witness, operation) found = cfg.relation(witness.line, operation.line) if cfg is not None and witness.line is not None else None @@ -112,6 +153,23 @@ class CfgDominance: return self.graph(operation.path, operation.function, operation.line) +def _pre_graph_evidence(witness: Discharge, operation: Operation) -> DominanceEvidence | None: + """Relation facts that need no graph: scopes, in-operation kinds, cross-function witnesses, line order.""" + if witness.scope in _SCOPED: + return DominanceEvidence(EvidenceRelation.MUST, "handler") + if witness.scope == "hop" or (witness.path, witness.function) != (operation.path, operation.function): + return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:cross_function") + if witness.kind in _IN_OPERATION: + if witness.line == operation.line: + return DominanceEvidence(EvidenceRelation.MUST, "constrains") + return DominanceEvidence(EvidenceRelation.NO, "constrains") + if witness.line is None: + return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:no_line") + if witness.line >= operation.line: + return DominanceEvidence(EvidenceRelation.NO, None) + return None + + def describe(dominance: Dominance, witness: Discharge, operation: Operation, texts: Mapping[str, str]) -> tuple[str, str]: """A witness's relation to an operation and its failure effect, from the graph when the dominance has one.""" relation = getattr(dominance, "relation", None) @@ -154,4 +212,4 @@ def _order_effect(texts: Mapping[str, str], witness: Discharge, operation: Opera return "value_only" -__all__ = ["CfgDominance", "describe", "operation_context"] +__all__ = ["CfgDominance", "DominanceEvidence", "describe", "operation_context"] diff --git a/tests/test_abstract_dominance.py b/tests/test_abstract_dominance.py new file mode 100644 index 0000000..9b8823b --- /dev/null +++ b/tests/test_abstract_dominance.py @@ -0,0 +1,189 @@ +"""Strict abstract-dominance relations over the CFG (Task 10.1, Reqs 10.1-10.7).""" + +import pytest + +from openultrasast.semantic.cfg import FunctionCfg +from openultrasast.semantic.cst import parse_function_nodes +from openultrasast.semantic.extra import grammar_for +from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation +from openultrasast.semantic.obligations.cfg_dominance import CfgDominance, DominanceEvidence +from openultrasast.semantic.obligations.operations import Discharge, Operation + +PATH = "src/C.java" + +JAVA_GUARD = """class C { + void handle(Request request) { + if (!request.user.isAdmin()) { throw new IllegalStateException(); } + request.store.deleteAll(); + } +} +""" + +JAVA_VALUE_ONLY = """class C { + void handle(Request request) { + boolean admin = request.user.isAdmin(); + request.store.deleteAll(); + } +} +""" + +JAVA_AFTER = """class C { + void handle(Request request) { + request.store.deleteAll(); + if (!request.user.isAdmin()) { throw new IllegalStateException(); } + } +} +""" + +JAVA_SOME_PATHS = """class C { + void handle(Request request) { + if (request.flag) { + if (!request.user.isAdmin()) { throw new IllegalStateException(); } + } + request.store.deleteAll(); + } +} +""" + + +def _witness(line: int | None, *, kind: str = "path_guard", scope: str = "statement") -> Discharge: + return Discharge( + path=PATH, + line=line, + function="handle", + kind=kind, + fact_id="f:guard", + provenance="call", + scope=scope, + detail="", + ) + + +def _operation(line: int) -> Operation: + return Operation( + path=PATH, + line=line, + function="handle", + kind="protected_read", + fact_id="f:op", + resource="store", + requires=("path_guard",), + ) + + +def _dominance(text: str) -> CfgDominance: + if grammar_for("java") is None: + pytest.skip("no Java grammar installed") + nodes = parse_function_nodes(PATH, text, "java") + assert nodes, "the parser read no function" + cfg = FunctionCfg.from_cst(nodes[0], "java") + return CfgDominance({PATH: text}, {(PATH, "handle"): cfg}) + + +def _lines(text: str) -> dict[str, int]: + file_lines = text.splitlines() + return { + "guard": next(number for number, line_text in enumerate(file_lines, start=1) if "isAdmin" in line_text), + "operation": next(number for number, line_text in enumerate(file_lines, start=1) if "deleteAll" in line_text), + } + + +def test_throwing_guard_on_all_paths_is_must() -> None: + dominance = _dominance(JAVA_GUARD) + lines = _lines(JAVA_GUARD) + evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.MUST + assert evidence.guard_effect == "throws" + + +def test_value_only_guard_on_all_paths_is_no() -> None: + dominance = _dominance(JAVA_VALUE_ONLY) + lines = _lines(JAVA_VALUE_ONLY) + evidence = dominance.evidence(_witness(lines["guard"], kind="ownership_check"), _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.NO + assert evidence.guard_effect == "value_only" + + +def test_guard_after_operation_is_no() -> None: + dominance = _dominance(JAVA_AFTER) + lines = _lines(JAVA_AFTER) + evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.NO + + +def test_branch_conditional_guard_is_may() -> None: + dominance = _dominance(JAVA_SOME_PATHS) + lines = _lines(JAVA_SOME_PATHS) + evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.MAY + + +def test_missing_graph_is_unknown_never_order_fallback() -> None: + dominance = CfgDominance({PATH: JAVA_GUARD}, {}) + lines = _lines(JAVA_GUARD) + evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.UNKNOWN + assert evidence.reason == "cfg_unavailable" + + +def test_line_without_graph_node_is_unknown() -> None: + dominance = _dominance(JAVA_GUARD) + lines = _lines(JAVA_GUARD) + evidence = dominance.evidence(_witness(1), _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.UNKNOWN + assert evidence.reason == "line_without_node" + + +def test_cross_function_witness_is_unknown_never_order() -> None: + dominance = _dominance(JAVA_GUARD) + lines = _lines(JAVA_GUARD) + cross_function_witness = Discharge( + path=PATH, + line=lines["guard"], + function="other", + kind="path_guard", + fact_id="f:guard", + provenance="call", + scope="hop", + detail="", + ) + evidence = dominance.evidence(cross_function_witness, _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.UNKNOWN + assert evidence.reason == "dominance:cross_function" + + +def test_scoped_witness_dominates_whole_handler() -> None: + dominance = _dominance(JAVA_GUARD) + lines = _lines(JAVA_GUARD) + scoped = _witness(None, scope="router") + evidence = dominance.evidence(scoped, _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.MUST + + +def test_in_operation_witness_same_line_is_must() -> None: + dominance = _dominance(JAVA_GUARD) + lines = _lines(JAVA_GUARD) + constraint = _witness(lines["operation"], kind="identity_constraint") + evidence = dominance.evidence(constraint, _operation(lines["operation"])) + assert evidence.relation is EvidenceRelation.MUST + + +def test_legacy_boolean_surface_unchanged() -> None: + dominance = CfgDominance({PATH: JAVA_GUARD}, {}) + lines = _lines(JAVA_GUARD) + assert dominance.dominates(_witness(lines["guard"]), _operation(lines["operation"]), ()) is True + assert isinstance(dominance.relation(_witness(lines["guard"]), _operation(lines["operation"])), str) + + +def test_dominance_evidence_is_frozen() -> None: + evidence = DominanceEvidence(relation=EvidenceRelation.MUST, guard_effect="throws", reason=None) + with pytest.raises(Exception): # noqa: B017 - frozen dataclass raises on assignment + evidence.relation = EvidenceRelation.NO # type: ignore[misc] + + +def test_evidence_is_deterministic() -> None: + dominance = _dominance(JAVA_GUARD) + lines = _lines(JAVA_GUARD) + first = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"])) + second = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"])) + assert first == second