Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 61 additions & 0 deletions src/liminate/analyzer.py
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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)
# ---------------------------------------------------------------------------
Expand Down
24 changes: 23 additions & 1 deletion src/liminate/interpreter.py
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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__}.")

Expand Down
117 changes: 115 additions & 2 deletions tests/test_define.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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