From 354f48c49a504cbf95207103113787eab0f8129f Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 00:05:32 -0700 Subject: [PATCH] fix: reject cyclic predicate definitions, guard evaluation depth A predicate redefinition could introduce a reference cycle that only becomes visible after the fact (e.g. define q: is p, then define p: is q), since each `define` only checks that the referenced name exists at that moment, not what it eventually resolves to. Evaluating such a cycle recursed forever and raised a bare RecursionError instead of a structured LiminateResult. Add a static cycle check in analyzer._check_define that walks the reference graph of a predicate body being (re)defined and rejects it if the walk reaches the name being defined. As a defensive backstop, cap predicate evaluation depth in the interpreter at 64 so any cycle the analyzer misses still surfaces as ERROR_SEMANTIC rather than a raw exception. --- src/liminate/analyzer.py | 61 +++++++++++++++++++ src/liminate/interpreter.py | 24 +++++++- tests/test_define.py | 117 +++++++++++++++++++++++++++++++++++- 3 files changed, 199 insertions(+), 3 deletions(-) diff --git a/src/liminate/analyzer.py b/src/liminate/analyzer.py index 1e50646..6c08d6c 100644 --- a/src/liminate/analyzer.py +++ b/src/liminate/analyzer.py @@ -1858,6 +1858,13 @@ def _check_define(node: DefineNode, symtab: dict[str, SymbolEntry]) -> None: (there is no iterator context to resolve them against). """ _check_define_condition(node.condition, symtab) + # Cycle check runs only after the forward-declaration check above has + # passed clean — every predicate_name reachable in one hop is already + # confirmed to exist, so a first-ever `define p: is p` still hits the + # "I don't know a definition" error above, unchanged. Only reachability + # back to `node.name` itself (direct or via a chain of already-defined + # predicates, as happens on redefinition) is new territory here. + _check_predicate_definition_cycle(node.name, node.condition, symtab) def _check_define_condition( @@ -1879,6 +1886,60 @@ def _check_define_condition( raise _SemanticError(f"Unknown comparison operator '{cond.op}'.") +def _check_predicate_definition_cycle( + name: str, + condition: ASTNode, + symtab: dict[str, SymbolEntry], +) -> None: + """Reject a definition whose body reaches back to its own name through + a chain of predicate references (redefinition can introduce this even + though `_check_define_condition` never sees it, since each hop only + checks that the *next* name already exists — not what that name's own + body eventually leads back to).""" + path = _find_predicate_cycle(name, condition, symtab, [], set()) + if path is None: + return + if not path: + raise _SemanticError(f"Definition '{name}' can't depend on itself.") + chain = ", ".join(f"'{step}'" for step in path) + raise _SemanticError( + f"Definition '{name}' refers back to itself through {chain}. " + f"A definition can't depend on itself." + ) + + +def _find_predicate_cycle( + target: str, + cond: ASTNode, + symtab: dict[str, SymbolEntry], + path: list[str], + visited: set[str], +) -> list[str] | None: + """Walk the reference graph from `cond`, resolving each + PredicateApplicationNode against `symtab` as it stands at this + definition site. Returns the intermediate-name path to `target` if + reached, else None. Reuses the visited-set pattern from + `_composition_void_result_verb` to keep the walk cycle-safe.""" + if isinstance(cond, CompoundConditionNode): + found = _find_predicate_cycle(target, cond.left, symtab, path, visited) + if found is not None: + return found + return _find_predicate_cycle(target, cond.right, symtab, path, visited) + if isinstance(cond, PredicateApplicationNode): + ref = cond.predicate_name + if ref == target: + return path + if ref in visited: + return None + visited.add(ref) + if ref in symtab and symtab[ref].type == "predicate": + return _find_predicate_cycle( + target, symtab[ref].value, symtab, path + [ref], visited, + ) + return None + return None + + # --------------------------------------------------------------------------- # when / finish (v3a §108, §109, §112) # --------------------------------------------------------------------------- diff --git a/src/liminate/interpreter.py b/src/liminate/interpreter.py index 2ae9583..f5287d4 100644 --- a/src/liminate/interpreter.py +++ b/src/liminate/interpreter.py @@ -64,6 +64,17 @@ _live_value_names_ctx: ContextVar[set[str] | None] = ContextVar( "liminate_live_value_names", default=None, ) +# Defensive depth guard for predicate application (belt-and-braces against +# analyzer._check_predicate_definition_cycle): that static check rejects +# cyclic `define`s at registration time, so this cap should be unreachable +# in practice. It exists so any path the analyzer misses — a hand-built +# symbol table, a future caller that skips analysis — still surfaces a +# structured ERROR_SEMANTIC instead of a bare RecursionError. 64 is far +# above any plausible legitimate predicate-composition depth. +_predicate_eval_depth: ContextVar[int] = ContextVar( + "liminate_predicate_eval_depth", default=0, +) +_MAX_PREDICATE_EVAL_DEPTH = 64 from .parser import ( AddNode, ArithmeticNode, @@ -2273,8 +2284,19 @@ def _eval_condition( raise _RuntimeError( f"I don't have a definition for '{cond.predicate_name}'." ) + depth = _predicate_eval_depth.get() + if depth >= _MAX_PREDICATE_EVAL_DEPTH: + raise _RuntimeError( + f"Predicate '{cond.predicate_name}' is nested more than " + f"{_MAX_PREDICATE_EVAL_DEPTH} levels deep — this usually " + f"means two or more definitions refer back to each other." + ) subject_val = _eval_field(cond.subject, current_item, symtab) - result = _eval_condition(entry.value, subject_val, symtab) + token = _predicate_eval_depth.set(depth + 1) + try: + result = _eval_condition(entry.value, subject_val, symtab) + finally: + _predicate_eval_depth.reset(token) return (not result) if cond.negated else result raise _RuntimeError(f"Can't evaluate condition {type(cond).__name__}.") diff --git a/tests/test_define.py b/tests/test_define.py index 20c70fe..f057e58 100644 --- a/tests/test_define.py +++ b/tests/test_define.py @@ -16,7 +16,7 @@ from __future__ import annotations -from liminate.analyzer import SymbolEntry +from liminate.analyzer import SymbolEntry, analyze from liminate.cli import Session from liminate.interpreter import execute as _execute from liminate.lexer import tokenize @@ -39,7 +39,7 @@ ) from liminate.renderer import render from liminate.reorderer import reorder -from liminate.result import ResultStatus +from liminate.result import LiminateResult, ResultStatus from liminate.run import run as run_program from liminate.vocabulary import ALL_RESERVED, DECLARATIONS, TOMBSTONES, reserved_category @@ -359,3 +359,116 @@ def test_predicate_containing_forbid_does_not_crash_prepass(): ]) contract = run_program(source, enter_phase2=False) assert contract.results[-1].status is ResultStatus.SUCCESS + + +# --------------------------------------------------------------------------- +# Cyclic predicate rejection +# +# A predicate body may reference another predicate (§84 composition), and +# redefinition overwrites in place (v1d §58). Together, those two rules let +# a redefinition introduce a cycle a later `define` never sees coming: +# `define q: is p` only checks that `p` exists *right now* — it says +# nothing about what `p` itself might later be redefined to. Evaluating a +# cyclic predicate chain recurses forever, so this must be caught before +# it ever reaches evaluation. +# --------------------------------------------------------------------------- + + +def test_cyclic_redefinition_two_hop_is_rejected_not_a_recursion_error(): + s = Session() + s.run_line("remember a number called x with 5") + s.run_line("define p: is above 1") + s.run_line("define q: is p") + r = s.run_line("define p: is q") + assert r.status is ResultStatus.ERROR_SEMANTIC + assert r.message == ( + "Definition 'p' refers back to itself through 'q'. " + "A definition can't depend on itself." + ) + # The rejected redefinition must not have overwritten `p` — the + # earlier, non-cyclic definition stays live and evaluates normally. + verdict = s.run_line("require x is p") + assert verdict.status is ResultStatus.SUCCESS + + +def test_three_way_cycle_is_rejected(): + s = Session() + s.run_line("define p: is above 1") + s.run_line("define q: is p") + s.run_line("define r: is q") + result = s.run_line("define p: is r") + assert result.status is ResultStatus.ERROR_SEMANTIC + assert "Definition 'p' refers back to itself through" in result.message + assert "'r'" in result.message + assert "'q'" in result.message + + +def test_direct_self_reference_on_first_definition_hits_forward_declaration_check(): + # Mirrors test_undefined_predicate_reference_raises_clear_error: the + # decoupled parse()/analyze() path with an explicit predicate_names + # set produces a PredicateApplicationNode even though `p` has never + # actually been defined. In the normal Session/run() flow this can't + # happen — predicate_names is always derived live from the symbol + # table, so a first-ever `define p: is p` parses as harmless string + # equality instead. This decoupled construction is what exercises the + # forward-declaration path directly: it must still raise the + # ORIGINAL "I don't know a definition" error, not the new + # cycle-rejection error — the cycle check must never shadow it. + ast = parse(tokenize("define p: is p"), predicate_names={"p"}) + result = analyze(ast, {}) + assert isinstance(result, LiminateResult) + assert result.status is ResultStatus.ERROR_SEMANTIC + assert "I don't know a definition for 'p'" in result.message + + +def test_legal_redefinition_without_a_cycle_still_works(): + s = Session() + s.run_line("define p: is above 1") + r = s.run_line("define p: is above 2") + assert r.status is ResultStatus.SUCCESS + + +def test_legal_composition_still_works(): + s = Session() + r1 = s.run_line("define adult: age is above 17") + assert r1.status is ResultStatus.SUCCESS + r2 = s.run_line("define eligible: is adult") + assert r2.status is ResultStatus.SUCCESS + + +def test_depth_guard_catches_a_hand_constructed_cyclic_symbol_table(): + # Belt-and-braces: the analyzer's cycle check makes this unreachable + # through normal `define` usage, but a symbol table built directly — + # bypassing analysis entirely, exactly the way a caller could misuse + # the parse()/execute() split — must still surface a structured + # ERROR_SEMANTIC instead of a bare RecursionError. + symtab = { + "x": SymbolEntry(name="x", value=5, type="number"), + "p": SymbolEntry( + name="p", + value=PredicateApplicationNode(subject=EachPronoun(), predicate_name="q"), + type="predicate", + ), + "q": SymbolEntry( + name="q", + value=PredicateApplicationNode(subject=EachPronoun(), predicate_name="p"), + type="predicate", + ), + } + ast = RequireNode( + condition=PredicateApplicationNode(subject=NameRef(name="x"), predicate_name="p"), + ) + result = _execute(ast, symtab) + assert result.status is ResultStatus.ERROR_SEMANTIC + assert "nested more than 64 levels deep" in result.message + + +def test_legal_ten_deep_predicate_chain_still_passes(): + s = Session() + s.run_line("define p0: is above 1") + for i in range(1, 11): + r = s.run_line(f"define p{i}: is p{i - 1}") + assert r.status is ResultStatus.SUCCESS + s.run_line("remember a number called x with 5") + verdict = s.run_line("require x is p10") + assert verdict.status is ResultStatus.SUCCESS