feat(access-control-prover): 8.2 stable declaration identities and per-change symbol index

This commit is contained in:
Marius Ciepluch
2026-10-29 15:45:29 +01:00
parent 9eee4d7f35
commit 6f2154fae0
5 changed files with 262 additions and 2 deletions
+15 -1
View File
@@ -16,7 +16,7 @@ from ..model.taxonomy import DEFAULT_FAMILIES_PATH, load_families
from ..preprocess import build_file_target, detect_language
from ..semantic.facts import load_facts
from ..semantic.ir import FileIR, parse_file
from ..semantic.obligations import check_obligations, load_obligation_facts
from ..semantic.obligations import check_obligations, load_obligation_facts, resolution
from ..semantic.obligations.dominance import OrderDominance
from ..semantic.obligations.operations import covers, find_operations, valid_witness
from .labels import label_rows
@@ -102,6 +102,20 @@ class Context:
continue
return mapping.analyze_entry_points(self.root, [build_file_target(self.root, self.root / path) for path in self.product_files])
@cached_property
def symbol_index(self) -> resolution.SymbolIndex:
"""Declarations and inheritance for the product tree, read once per change (Req 6.2)."""
files: list[tuple[str, str, str]] = []
for path in self.product_files:
try:
text = self.read(path)
except _Absent:
# Same guard as entry_points: an empty product file is not this index's problem.
continue
language = source.canonical_language(detect_language(self.root / path))
files.append((path, text, language))
return resolution.SymbolIndex.build(files)
@cached_property
def hunks(self) -> dict[str, list[list[int]]]:
"""Line ranges per file that the push changed or added, at head."""
+100
View File
@@ -2,6 +2,7 @@
from __future__ import annotations
from dataclasses import dataclass
from typing import Any
from .ir import Bind, CallSite, FileIR, FunctionIR
@@ -111,6 +112,105 @@ def parse_function_nodes(path: str, text: str, language: str) -> list[Any]:
return [node for node in _walk(tree.root_node) if node.type in kinds["function"]]
@dataclass(frozen=True)
class DeclarationScope:
"""One function declaration with the enclosing type it is declared in and that type's base names."""
function_name: str
params: tuple[str, ...]
start_line: int
enclosing_type: str | None
enclosing_base_types: tuple[str, ...]
_CLASS_KINDS = frozenset({"class_declaration", "class_definition"})
_BASE_NAME_KINDS = frozenset({"identifier", "type_identifier", "name", "property_identifier"})
_BASE_CLAUSE_FIELDS = ("superclass", "interfaces", "superclasses", "base_clause", "class_heritage", "extends_clause")
_BASE_CLAUSE_KINDS = frozenset({"base_clause", "class_heritage", "extends_clause", "superclasses"})
def declaration_scopes(path: str, text: str, language: str) -> tuple[DeclarationScope, ...]:
"""Every function declaration in the file with its enclosing type chain.
The symbol index (task 8.2) needs what the flat FileIR drops: which class a method is declared in and
which bases that class names. An unparsable file or a language without a grammar yields no scopes.
"""
from .extra import grammar_for
kinds = _KIND.get(language)
grammar = grammar_for(_grammar_language(language, path))
if grammar is None or kinds is None:
return ()
try:
from tree_sitter import Parser
tree = Parser(grammar).parse(text.encode())
except Exception:
return ()
if bool(getattr(tree.root_node, "has_error", False)):
return ()
scopes: list[DeclarationScope] = []
_collect_scopes(tree.root_node, kinds, None, (), scopes)
return tuple(scopes)
def _collect_scopes(
node: Any,
kinds: dict[str, frozenset[str]],
enclosing_type: str | None,
enclosing_base_types: tuple[str, ...],
scopes: list[DeclarationScope],
) -> None:
if node.type in _CLASS_KINDS:
name_node = node.child_by_field_name("name")
enclosing_type = _text(name_node) if name_node is not None else None
enclosing_base_types = _class_bases(node)
if node.type in kinds["function"]:
scopes.append(
DeclarationScope(
function_name=_declaration_name(node),
params=_params(node, kinds),
start_line=_line(node),
enclosing_type=enclosing_type,
enclosing_base_types=enclosing_base_types,
)
)
for child in getattr(node, "named_children", ()) or ():
_collect_scopes(child, kinds, enclosing_type, enclosing_base_types, scopes)
def _declaration_name(node: Any) -> str:
"""The declared name for the symbol index.
Same resolution as `_function_name`, plus the property_identifier kind a TypeScript
method_declaration names itself with; the flat FileIR keeps its own naming.
"""
for child in getattr(node, "named_children", ()) or ():
if child.type in {"identifier", "name", "property_identifier"}:
return _text(child)
if child.type == "function_declarator":
for grandchild in getattr(child, "named_children", ()) or ():
if grandchild.type == "identifier":
return _text(grandchild)
return "<anon>"
def _class_bases(node: Any) -> tuple[str, ...]:
"""The base type names a class declaration names, in declaration order, deduplicated."""
clauses: list[Any] = []
for base_field in _BASE_CLAUSE_FIELDS:
clause = node.child_by_field_name(base_field)
if clause is not None:
clauses.append(clause)
clauses.extend(child for child in getattr(node, "named_children", ()) or () if child.type in _BASE_CLAUSE_KINDS)
names: list[str] = []
for clause in clauses:
names.extend(
_text(child) for child in _walk(clause, skip=frozenset()) if child.type in _BASE_NAME_KINDS and not _text(child).startswith("$")
)
return tuple(dict.fromkeys(names))
def _grammar_language(language: str, path: str) -> str:
"""TypeScript ships two grammars; a `.tsx` file needs the JSX-aware one. The FileIR keeps the language it was given."""
return "tsx" if language == "typescript" and path.endswith(".tsx") else language
@@ -0,0 +1,76 @@
"""Stable declaration identities for repository-defined symbols (task 8.2).
The symbol index gives every declaration an identity keyed by module, enclosing type, name, and -- when
the declaration carries them -- parameter names, so same-name targets never merge (Req 3.2) and base-type
declarations attach only through explicit descendant edges (Req 3.5). Engine purity: no framework or
product names appear here; target vocabulary arrives as data through the acquisition pipeline.
"""
from __future__ import annotations
from collections.abc import Iterable, Mapping
from dataclasses import dataclass, field
from ..cst import DeclarationScope, declaration_scopes
@dataclass(frozen=True)
class SymbolId:
"""The stable identity of one declaration: module (repository path), enclosing type, name, signature."""
module: str
enclosing_type: str | None
name: str
signature: tuple[str, ...] | None
@property
def sort_key(self) -> tuple[str, str, str, tuple[str, ...]]:
"""A total-order key; a missing signature sorts before every present one."""
return (self.module, self.enclosing_type or "", self.name, self.signature or ())
def __lt__(self, other: object) -> bool:
if not isinstance(other, SymbolId):
return NotImplemented
return self.sort_key < other.sort_key
@dataclass(frozen=True)
class SymbolIndex:
"""Repository-defined declarations and the inheritance edges between their types."""
declarations: tuple[SymbolId, ...]
base_types: Mapping[tuple[str, str], tuple[str, ...]]
by_name: Mapping[str, tuple[SymbolId, ...]] = field(default_factory=dict)
@classmethod
def build(cls, files: Iterable[tuple[str, str, str]]) -> SymbolIndex:
"""Build the index from (path, text, language) triples; deterministic and deduplicated."""
declarations: set[SymbolId] = set()
base_types: dict[tuple[str, str], tuple[str, ...]] = {}
for path, text, language in files:
scopes = declaration_scopes(path, text, language)
declarations.update(_symbol_id(path, scope) for scope in scopes)
base_types.update(_inheritance_edges(path, scopes))
by_name: dict[str, list[SymbolId]] = {}
for declaration in sorted(declarations):
by_name.setdefault(declaration.name, []).append(declaration)
return cls(
declarations=tuple(sorted(declarations)),
base_types=dict(sorted(base_types.items())),
by_name={name: tuple(symbols) for name, symbols in sorted(by_name.items())},
)
def _symbol_id(module: str, scope: DeclarationScope) -> SymbolId:
"""Parameter names are the signature when present; a declaration without them has none."""
signature = tuple(scope.params) if scope.params else None
return SymbolId(module=module, enclosing_type=scope.enclosing_type, name=scope.function_name, signature=signature)
def _inheritance_edges(module: str, scopes: Iterable[DeclarationScope]) -> dict[tuple[str, str], tuple[str, ...]]:
"""(module, type) -> the base names that type declares, from any method declared inside it."""
edges: dict[tuple[str, str], tuple[str, ...]] = {}
for scope in scopes:
if scope.enclosing_type is not None:
edges[(module, scope.enclosing_type)] = scope.enclosing_base_types
return edges