analysis: check return-type compatibility (OWN035)
An external review of the very first main flagged two analyzer/codegen
divergences that survived into the current tree: lower_return silently
dropped a non-owned or empty return symbol to None, so the analyzer treated
the function as a valid terminal while codegen printed the raw AST return x;
-- emitting uncompilable C# the checker had accepted:
* fn f(n: int) -> Buffer { return n; } -> Buffer f(int n){ return n; }
* fn f() -> Buffer { return; } -> Buffer f(){ return; }
Diagnose the mismatch instead of dropping it (new OWN035): a ).
#5
Merged
Conversation
An external review of the very first main flagged two analyzer/codegen
divergences that survived into the current tree: `lower_return` silently
dropped a non-owned or empty return symbol to None, so the analyzer treated
the function as a valid terminal while codegen printed the raw AST `return x;`
-- emitting uncompilable C# the checker had accepted:
* `fn f(n: int) -> Buffer { return n; }` -> `Buffer f(int n){ return n; }`
* `fn f() -> Buffer { return; }` -> `Buffer f(){ return; }`
Diagnose the mismatch instead of dropping it (new OWN035): a value-less
`return;` in a function with a return type, a value returned from a function
with none, and a non-owned value returned where an owned resource is required.
`emit` then refuses (its existing contract), so no bad C# is produced. Returning
an owned resource into a `-> Resource` stays clean (still escapes), and a
returned borrow stays OWN004.
Tests: 3 OWN035 cases + a clean bare-`return;`-in-void case (analysis 104/104).
(The deeper fix the review recommends -- generate from the checked CFG/effects
rather than the raw AST so the two cannot diverge -- remains roadmap; catching
it in the checker + refusing to emit is the sound MVP behaviour.)
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Repository UI Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
🚧 Files skipped from review as they are similar to previous changes (2)
📝 WalkthroughWalkthroughAdds ChangesOWN035 Return Type Mismatch Validation
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![chatgpt-codex-connector[bot]](https://cdn.github.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ab291b7449
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Bringing the ownership checker -- the core of the PoC -- to a trustworthy state. An adversarial pass over the loans/permissions rules (~30 hand-built edge cases) found zero false negatives and zero false positives: every ownership/borrow violation is flagged, every safe program is accepted. The holes we had been finding all lived in codegen and the return-type edge, not in the ownership lattice itself. Capture the genuinely-new corners as permanent regression cases (16): borrow of a moved-from name, a void return that leaks inside a borrow, double consume, consuming/moving a borrow binding, a mutating call under a live shared borrow (OWN006), an inner acquire that leaks inside a borrow, shadowed binding names, return-of-moved + leak, and five clean programs guarding against the checker becoming over-strict (sequential exclusive borrows, consume on both arms, move chains, nested shared borrows). Analysis suite: 120/120.
Follow-up to the OWN035 return-type check: it only verified that a value
returned from a resource-typed function was *owned*, so a different owned
resource still slipped through -- `fn f() -> Buffer { let c = acquire Conn(1);
return c; }` produced no diagnostic and codegen emitted a `Buffer`-returning
method handing back a Conn, recreating the analyzer/codegen mismatch this
check exists to close.
Thread the resource type onto owned symbols (set on `acquire`, propagated
through `move`; params already carried it) and compare it to the declared
return type. Buffers keep their own escape rules (OWN015/016/017), so they are
left to the analyzer rather than reported here. A wrong-typed owned resource is
kept as escaped (not nulled) so it is not also spuriously reported as a leak --
the type mismatch is the single error.
Tests: wrong-resource return (acquired + param), plus a clean `-> Conn` return.
Analysis suite 123/123.
Closed
PhysShell
pushed a commit
that referenced
this pull request
Jul 3, 2026
Both reviewers converged; all corrections are factual/design refinements (no forks): - Crate DAG: own-codegen is a SIBLING of own-diagnostics (both consume own-cfg/own-analysis), not chained through it. Codegen is verdict-independent (AST/CFG-driven, matching Python codegen.generate), so the old own-diagnostics -> own-codegen edge would have forced diagnostics to re-export solver internals. Added a fitness function locking codegen !-> diagnostics (and !-> analysis for now). (Codex P2, CodeRabbit #1) - Oracle: do NOT reuse scripts/oracle_compare.py as the parity oracle — it is cross-tool fuzzy (leak-only, +-N line tolerance, coarse severity) and would mask off-by-one/label/subject/exit-status divergences. Spec a new exact harness over status+stdout+stderr+SARIF/JSON, with an exit/crash gate first, exact set-equality incl. evidence label text, and intra-tie ordering. (Codex P1, CodeRabbit #4) - CFG seam does not exist yet: python cfg prints human text, not JSON. Add+freeze a canonical cfg --format json before the ratchet uses that seam; added as migration step 0. (Codex P2) - State: arena+CoW likely wins this procedural workload; bench largest real function, wall-clock + RSS. Prior art: clippy lint-pass registry, prusti-viper encoding boundary. Repo-layout revisit trigger. (CodeRabbit #2/#3/#5/#6)
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
2 participants
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 by CodeRabbit
returnstatements to match each function’s declared return type and expected resource kind.OWN035(“return type mismatch”) for invalidreturnusage, including barereturn;where a value is required, returning a value from void-style contexts, and returning incompatible owned resources.OWN035, including additional soundness guard scenarios (including cases expectingOWN001).