Repository navigation
fix(auto): stop false-positive generators in effect summarization - #79
MilesCranmerBot wants to merge 11 commits into
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.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: b31d74222c
ℹ️ About Codex in GitHub
Codex has been enabled to automatically 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 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
|
Responses to all four comments (dd37a8e): Fixed point for recursive summaries — implemented. Re-entrant lookups now read the provisional summary published by the previous pass, and Per-callsite budget isolation — implemented. Each statement's effect resolution gets a fresh tracker; one deep chain no longer changes how unrelated statements are treated. Documented default — updated in both the Consumes on budget exhaustion — kept as writes, deliberately. Reverting to consume-on-budget is what made every DynamicExpressions entry point unusable before this PR: consume violations do not require aliasing or later-use evidence at the call site (bind barriers create phantom aliases), so unresolved calls deep inside third-party packages flagged unrelated user code. The write fallback preserves mutation detection (e.g. broadcast mutation through views still throws) while requiring alias evidence. The tradeoff you describe \u2014 a genuine escape of an otherwise-unique argument past the depth limit goes undiagnosed \u2014 is real and accepted for now; if it matters in practice, a follow-up could attribute consumes only when the callee summary was cached from a prior full analysis rather than truncated. |
|
Update on the two open threads (fe98bc7): 1. Consumes on budget exhaustion — resolved via a 2. Documented default — already updated in dd37a8e: the Also in this push: fixed-point refinement passes are gated on an atomic cycle-hit counter (non-recursive functions pay zero extra passes) and skip when a pass produces no summary, which resolves the JET |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fe98bc73d8
ℹ️ About Codex in GitHub
Codex has been enabled to automatically 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 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
75044f4 to
0199033
Compare
Remove the 1.13 ceiling from the version gate in src/BorrowChecker.jl and the auto-test gate in test/runtests.jl. Verified on 1.13.0-rc3: full suite passes (227 pass, 2 pre-existing broken) and 1.12.7 remains green. Link BorrowChecker into test/Project.toml as a relative path source so the test environment resolves on any Julia version.
Post-1.13-rc nightly moved local inference lookup to get_indices(cache, mi) over an InferenceCache. Our BCInterp uses a plain Vector{InferenceResult}, so provide a matching get_indices overload when the compiler defines the function.
Nightly wraps cached edge results in LocalInferenceResult before pushing into the interpreter's local cache, so the cache element type must accept both InferenceResult and LocalInferenceResult.
- Nightly narrows constprop_cache_lookup to InferenceCache; provide a mirror implementation for our plain-vector local cache. - Nightly requires a LineNumberNode argument to generated_body_to_codeinfo; pick the applicable method at runtime.
- get_indices and constprop_cache_lookup unwrap LocalInferenceResult before reading linfo. - Use Compiler.proof_worlds for wrapped entries and a real LineNumberNode for generated_body_to_codeinfo on nightly.
Nightly indexes cache.results, which only exists on InferenceCache. Provide a BCInterp-specific implementation that scans our plain vector directly.
Port of bless-lockables onto the dissolved-module layout. Locks serialize access without consuming or writing through their arguments: register Base.lock/unlock/trylock/islocked in the builtin effect registry, and model the callback-taking lock(f, l) form as a transparent higher-order call that propagates callback effects (capture writes surface as functor writes) while granting payload writes. Co-authored-by: Miles Cranmer <miles.cranmer@gmail.com>
0199033 to
e846230
Compare
Port of pr/string-tracking. On 1.12+, ismutabletype(String) is true (memory-based layout), so the generic mutable-type rule misclassifies strings as owned and flags harmless string forwarding/escapes. Exempt exactly String and SubString; AbstractString stays tracked so user-defined mutable string subtypes keep their diagnostics. Co-authored-by: Miles Cranmer <miles.cranmer@gmail.com>
Restrict compiler-IR checking to Julia 1.12 and 1.13, matching the documented support range. Julia 1.14 and newer now load the warn-and-pass-through stubs, with a regression test covering that contract. Co-authored-by: Miles Cranmer <miles.cranmer@gmail.com>
…ment Port of pr/auto-fp-generators onto the dissolved-module layout: - generator calls no longer poison callers with spurious consumes - recursive effect summaries refine to a fixed point (bounded passes) - per-callsite depth budgets are isolated so one deep chain cannot change how unrelated statements are treated - new budget_fallback config (:consume default, :write to soften) Suite green on 1.13.0-rc3 and 1.12.7. Co-authored-by: Miles Cranmer <miles.cranmer@gmail.com>
e846230 to
aabbeb7
Compare
This branch has not been deployed
1 participant
Summary
Dogfooding
@safeon real packages (DynamicExpressions, DifferentiationInterface + ForwardDiff) surfaced three false-positive generators in the effect summarizer. Every entry point of DynamicExpressions' public API tripped the checker; after these fixes the same dogfood drivers run clean.nothing, so the conservative "unknown call consumes its owned arguments" fallback fired at the recursion edge, and the poisoned summary was cached. Any recursive function taking a tracked argument (all of DynamicExpressions' tree walks) became a violation generator. Re-entry now contributes no effects (optimistic fixed point); a cycle is also no longer treated as budget exhaustion.max_summary_depth, the same fallback fired and cached. Budget-limited calls now fall back to writes instead of consumes: writes require aliasing evidence to violate, so unrelated code stops being flagged while genuine mutations through unanalyzable calls are still caught.max_summary_depth12 → 24. Base's broadcast chain needs ~20 hops to resolve into precise write effects; at 12, detection of broadcast mutation depended on where the budget ran out.Also updates the
DynamicExpressionsintegration test: the known-brokencopy(::Expression)case passes for real now, and thebat()expectation is unchanged (still correctly throws).Test plan
BORROWCHECKER_ONLY_AUTO=1 julia --project=. -e 'using Pkg; Pkg.test()': 224 pass, 0 broken (was 221 pass / 2 broken on main).@test_brokento@test.