Repository navigation
Arena/8fcd3755 apodeixis jl - #3
Conversation
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Caution Review failedThe pull request is closed. Walkthrough
Merge Risk:
 |
|
![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: d90fde4974
ℹ️ 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".
| is_function_definition = x.head === :function || _is_short_function_definition(x) | ||
| child_verified = is_function_definition && !nested_function ? false : verified |
There was a problem hiding this comment.
When an @verified function contains a closure such as f = B -> (@inbounds B[1]), the :-> expression is not recognized as a function definition, so its body inherits verified=true and passes with a sufficient mutation score even though the closure itself was never annotated. Handle anonymous functions, including those generated for do blocks, as independent boundaries just like nested named methods.
Useful? React with 👍 / 👎.
| const _FORBIDDEN_MACROS = Set(( | ||
| Symbol("@generated"), Symbol("@eval"), Symbol("@fastmath"), | ||
| )) |
There was a problem hiding this comment.
On supported Julia versions, @ccall is a standard way to invoke foreign code, but it is absent from the forbidden macro set. Consequently, a top-level @ccall libc.printf(...)::Cint is treated as an ordinary unknown macro outside @verified and the audit reports :policy_clean, despite the documented rule that unmodeled foreign calls are rejected.
Useful? React with 👍 / 👎.
| elseif x.head === :call && !isempty(x.args) | ||
| callee = _callee_symbol(first(x.args)) | ||
| if callee in _FORBIDDEN_CALLS |
There was a problem hiding this comment.
Forbidden callees are checked only when the AST head is :call, while Julia represents dotted calls such as eval.([:x]), Base.invokelatest.(fs, xs), and unsafe_load.(ptrs) with a broadcast :. expression. These forms execute the same prohibited operations but currently produce no finding, allowing the fail-closed dynamic-escape policy to be bypassed.
Useful? React with 👍 / 👎.
| # The MVP rejects global declarations only within the annotated body. | ||
| @test is_policy_clean(audit_source("global mutable_state = 1")) | ||
| @test is_policy_clean(audit_source("function f(); global mutable_state = 1; end")) |
There was a problem hiding this comment.
These assertions require top-level and unannotated-function global declarations to be policy-clean, but lines 105–113 in the same test file require those inputs to be rejected, and _walk! unconditionally emits APX_GLOBAL_MUTATION for every :global node. Therefore Pkg.test() must fail whenever this testset runs; the expectations should be aligned with the documented rule that global declarations are rejected.
Useful? React with 👍 / 👎.
| for arg in x.args | ||
| if arg isa LineNumberNode | ||
| current_line = Int(arg.line) | ||
| else | ||
| current_line = _walk!(arg, child_verified, mutation_score, current_line, findings) |
There was a problem hiding this comment.
The recursive walk treats the call-shaped signature of every method definition as an executed call. Valid definitions such as function API.eval(x); x; end or API.unsafe_load(x) = x therefore emit APX_DYNAMIC_ESCAPE, even though the forbidden function is only being defined and never invoked; distinguish the signature child of long- and short-form definitions from executable call expressions.
Useful? React with 👍 / 👎.
| elseif x isa Expr && x.head === :. && !isempty(x.args) | ||
| lastarg = last(x.args) | ||
| lastarg isa QuoteNode && return lastarg.value isa Symbol ? lastarg.value : nothing | ||
| lastarg isa Symbol && return lastarg | ||
| end |
There was a problem hiding this comment.
Macro classification discards the entire qualifier and keeps only the final symbol, so an unrelated Other.@verified establishes a verified boundary and Other.@pre, Other.@inbounds, or similar macros are treated as reviewed contract markers. Inside an annotated function this lets arbitrary third-party macros evade APX_UNMODELED_MACRO—and a spoofed @verified can make unsafe constructs appear to be in an approved scope—so recognized markers must be restricted to the intended unqualified or registered module identities.
Useful? React with 👍 / 👎.
Summary
Changes
RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
*_chora.deed)(status)/(maturity)updated (if project state changed)(ecosystem)updated (if integrations changed)(meta)and/ordocs/decisions/updated (if architectural decisions changed)docs/status/ROADMAP.adocupdated (if milestones or next actions changed)TOPOLOGY.mdupdated (if architecture changed)CHANGELOGor release notes updatedsrc/interface/abi/andsrc/interface/ffi/consistent)Testing
Screenshots
Summary by CodeRabbit