fix(borrow): close #554 use-after-move through a callee-returned borrow#595
Merged
Conversation
🔍 Hypatia Security ScanFindings: 40 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
force-pushed
the
fix/554-callee-returned-borrow
branch
from
62ddc06 to
5a0566e
Compare
🔍 Hypatia Security ScanFindings: 40 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
🔍 Hypatia Security ScanFindings: 40 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
A call whose result borrows one of its arguments now registers the borrow-graph edge that was missing. Each function carries a return-borrow summary (compute_ret_borrow_params): the parameter indices whose borrow may flow out via the return value (a returned `&p` / `return p` for a `ref`/`mut` parameter, directly, via a let-bound ref-local chain, or through an `if`/`match`/block tail in return position). At a call site those argument borrows stay live exactly like a plain `&` borrow — claimed into the result binder (NLL-governed) or lingering to block exit — so `let r = pick(a); consume(a); *r` is now MoveWhileBorrowed while the legitimate NLL reorderings still pass. The control (plain double-consume) and the whole pre-existing valid corpus are unaffected: only calls to functions that actually return a borrow of a parameter change behaviour. Hardened across two adversarial-verification rounds: the aggregate-storage, assign-path, summary-via-arm-tail, and `return`-statement-form holes a first cut missed were all found and closed. Residuals — interprocedural-through- call-result; the branch-merged / copy-out claim (proven `&`-symmetric, a pre-existing lexical limitation inherited not introduced); and a reassign old-loan over-rejection (sound direction) — are documented in-code and closed properly by Polonius (#553); the mechanized proof is tracked as #515. 7 regression fixtures + Alcotest cases added; full suite 393/393 green. ADR-022 reframed (residual = soundness, not precision; status ratified). Closes #554. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…old-loan Follow-up hardening on the #554 return-borrow summaries, closing two of the three documented residuals. (a) interprocedural-through-call-result — compute_ret_borrow_params now resolves a returned call result through the callee's summary, and build_context drives all summaries to a monotone fixpoint (seed empty, recompute against callees until stable; origins only grow and are bounded by arity, so it terminates). So `fn wrap(ref x){ let t = pick(x); return t }` inherits pick's origin and `let r = wrap(a); consume(a); *r` is rejected — transitively through any wrapper depth, and across self- and mutual-recursion. (c) reassignment precision — `r = f(b)` reassigning an existing ref-binder now releases the binder's prior loan (ref-counted by b_id, so a borrow a ref-to-ref alias still holds is kept) and rebinds to the escaping call result, symmetric with the plain-& Slice-B reborrow. A later use of the old target is no longer spuriously rejected. The remaining residual (b) — the branch-merged / copy-out claim — is &-symmetric (a pre-existing lexical limitation inherited by the call-result path, not introduced by it) and is closed properly by Polonius (#553). Self-checked: ref-to-ref-alias-keeps-borrow, self/mutual recursion terminate, multi-arg interprocedural origin mapping, NLL precision preserved. Full suite 395/395 green; +2 regression fixtures. Refs #554. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…eassigned-local summary A third adversarial-verification pass on the #554 return-borrow work surfaced two more reachable holes (and confirmed the interprocedural fixpoint is robust: 60-level wrapper chains, mutual recursion, and 3-cycles all terminate in ms and summarise correctly). - Slice-B `&` reassign (a PRE-EXISTING soundness bug, exposed by the #554 (c) block being more correct): `r = &b` ended the binder's old loan UNCONDITIONALLY, so `let r2 = r; r = &b; consume(a); *r2` dropped the borrow `r2` still aliased and accepted a use-after-move. Now ref-counted by b_id (mirroring the (c) block and expire_dead_ref_bindings), so an aliased loan survives the reassign. The `&mut` variant (exclusive aliasing) is caught too. - Reassigned-local summary: the summary walker did not update a reassigned ref-local's origins, so `let mut t = pick(y); t = pick(x); return t` summarised the stale {y}. It now UNIONs origins on reassignment (conservative, flow-insensitive), summarising {x,y}. Two low-severity residuals are documented in-code (Polonius #553 closes them): a summary that cannot bootstrap an origin for a base-case-less divergent recursion (unreachable — the function never returns), and a loop-body reassign to an outer borrow (&-symmetric, predates #554). Full suite 397/397 green; +2 regression fixtures (alias-survives-reassign, reassigned-local-summary). Refs #554. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
force-pushed
the
fix/554-callee-returned-borrow
branch
from
f308ae9 to
e1831b2
Compare
🔍 Hypatia Security ScanFindings: 40 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
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
1 participant
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
Closes #554 — the borrow checker accepted a use-after-move through a callee-returned borrow (
let r = pick(a); consume(a); *rpassed the full pipeline, "Type checking passed", exit 0). This was the core operational soundness hole behind the CORE-01 stamp.Fix
Per-function return-borrow summary (
compute_ret_borrow_params): the parameter indices whose borrow flows out via the return value — a returned&p/return pfor aref/mutparameter, directly, via a let-bound ref-local chain, or through anif/match/block tail in return position. At a call site those argument borrows stay live — in every respect like a plain&borrow — claimed into the result binder (NLL-governed) or lingering to block exit. So the probe is nowMoveWhileBorrowed, while legitimate NLL reorderings still pass. Scope is surgical: only calls to functions that actually return a borrow of a parameter change behaviour — the entire pre-existing valid corpus is unaffected.Hardening — two adversarial-verification rounds
A first cut missed four same-family holes; all were found by adversarial multi-agent verification and closed here:
let t = (pick(a), 0); consume(a); *(t.0)r = pick(a)if/match-arm-tail returnsreturn <branch>;statement form (the idiomatic spelling)Plus a shadowing over-rejection fix.
Residuals (documented in-code; closed properly by Polonius #553)
&-symmetric (the byte-identical plain-&program behaves identically): a pre-existing lexical limitation, inherited not introducedThe mechanized proof of this property is tracked separately as #515.
Verification
Docs
SPDX-License-Identifier: MPL-2.0+ literal-owner header (pre-existing drift). Adding licence/SPDX headers is an owner-only manual task per estate policy — to be landed by the owner.🤖 Generated with Claude Code