verify: warn when recursive self-call return is discarded#580
Merged
Conversation
A recursive self-call followed by another statement in the same body silently discards its return value, since ilo only uses the tail expression as the function's return. The interp1d persona hit this shape (find-idx xs target +i 1; -1) and mis-diagnosed it as a broken braceless guard because the verifier emitted no signal. Add ILO-T043 to close the gap. Narrowly scoped to recursive self-calls (callee name == caller name) with a non-nil declared return type. Bare non-recursive user-fn calls at non-tail position do not warn; the callee may legitimately be side-effecting. Broaden later if reruns surface other classes.
Five cases covering the new warning surface: warns on non-tail recursive self-call (the persona's shape), no-warn on tail recursive self-call, no-warn on non-recursive user-fn call at non-tail, no-warn when the call is wrapped in ret, and two warnings emitted when two non-tail recursive calls appear in a row. examples/recursive-tail-position.ilo pins the canonical fix shape under examples_engines so every engine asserts the same output. The example doubles as the in-context example any future agent reads when ILO-T043 fires; the hint points at this file.
Adds --explain ILO-T043 reachable entry with the canonical fix walk- through (tail-position move, ret-wrap, ?h restructure). SPEC.md tail- call rules section now points at the new warning. ai.txt regenerated by build.rs picks up the SPEC change.
❌ 1 Tests Failed:
View the top 1 failed test(s) by shortest run time
To view more test analytics, go to the Test Analytics Dashboard |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
ILO-T043, a verifier warning that fires when a recursive self-call sits at a non-tail position and its return value is silently discarded. Closes the diagnostic gap surfaced 2026-05-21 by the interp1d persona via #5ba investigation (PR #571): the persona wrote a braceless-guard recursive search where the recursive call was followed by a literal fallback, every call discarded the recursive return, and the function always returned the fallback. With no warning emitted, the persona then mis-diagnosed the bug as broken braceless guards.T043 is narrowly scoped to recursive self-calls (callee name == caller name) with a non-nil declared return type. Bare non-recursive user-fn calls at non-tail position do NOT warn, because the callee may legitimately be side-effecting (logging, file I/O). The narrow surface keeps the false-positive risk near zero; we can broaden later if reruns surface other classes.
Manifesto framing: a missing signal here is paying for itself in agent confusion tokens (the persona spent an entire investigation chasing a phantom braceless-guard bug). Adding the signal once means every future agent who reaches for the same shape gets pointed at the real footgun immediately.
Repro before/after
Before:
ilo checkis silent. Function always returns -1 because the recursive call's return is dropped.After:
Fix shape (
examples/recursive-tail-position.ilo):Recursive call is now the body's last statement (tail position); braceless guards short-circuit above.
What's in the diff
Per-commit:
verify: warn on non-tail recursive self-call return discard- newILO-T043check inverify_body, narrowly scoped to recursive self-calls with non-nil return.test: regression for ILO-T043 recursive discard- cross-engine regression attests/regression_verify_discarded_recursive.rs(5 cases: warns on non-tail self-call, no-warn on tail, no-warn on non-recursive, no-warn onret-wrapped, multiple warns).docs: ILO-T043 registry entry + example + SPEC sync---explain ILO-T043now resolves; SPEC.md tail-position section points at the new code;examples/recursive-tail-position.ilopins the canonical fix shape across every engine viaexamples_engines.Test plan
cargo test --release --features cranelift --test regression_verify_discarded_recursive(5/5 passing)examples/recursive-tail-position.ilo mainreturns3,missingreturns-1(manual run)cargo test --release --features craneliftgreenFollow-ups
=cond recursive-callshapes (assignment in a non-tail position with a recursive RHS) - currentlyStmt::Letisn't covered.