[codex] Ship LSP forward propagation floor#491
Conversation
|
Warning Rate limit exceeded
You’ve run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (7)
WalkthroughThis PR adds cross-language forward-propagation analysis: constraint state, baseline entries with deterministic CIDs, source lowering (floor v1), diagnostic emission on callsite precondition failures, LSP wiring in Go/PHP/Rust servers, fixtures, unit and integration tests, and CI job-result artifacts. ChangesForward Propagation Analysis
CI Job Results
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related issues
Possibly related PRs
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 unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
TSavo
force-pushed
the
codex/main-20260508-104659
branch
from
5ad4bdd to
c99bfe7
Compare
|
@coderabbitai review |
✅ Actions performedReview triggered.
|
![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: 65753f3823
ℹ️ 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".
|
|
||
| for (line_idx, line) in source.lines().enumerate() { | ||
| let trimmed = line.trim_start(); | ||
| let is_function_definition = trimmed.starts_with("fn "); |
There was a problem hiding this comment.
lower_floor_source only emits Stmt::Reset when a line starts with fn , but Rust functions often start with qualifiers such as pub fn, pub(crate) fn, or async fn. Those functions will be analyzed without a reset, so facts from a previous function can leak into the next one; for example, a prior checkPositive(5) can leave x > 0 in state and suppress the expected diagnostic on a later pub fn call to checkPositive(-1).
Useful? React with 👍 / 👎.
|
|
||
| foreach (explode("\n", $source) as $lineIdx => $line) { | ||
| $trimmed = ltrim($line); | ||
| $isFunctionDefinition = preg_match('/^function\s+/', $trimmed) === 1; |
There was a problem hiding this comment.
lowerFloorSource only treats lines matching ^function\s+ as function boundaries, so class methods declared as public/protected/private function ... are missed. This allows forward-propagation state to carry across methods, which can hide real precondition violations (e.g., a satisfied call in one method can make a violating call in a later method appear satisfied).
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (1)
.provekit/ci/accepted/ts/blake3-512:cf2632156ae353e1b6e263e8a5278476d15337d8fb7310297eccdce0476021db91086e63a869e08aeb3115ec2fa57d6f9b617377e7720b15493f1a2d61089f43.job-result.json (1)
13-19: 💤 Low valueConsider normalizing
inputCidsordering across language artifacts.The
inputCidsarray ordering differs across the three job result files:
- TS:
[policyCid, blastRadiusCid, logCid, runnerIdentityCid, outputCid]- Go:
[outputCid, blastRadiusCid, policyCid, logCid, runnerIdentityCid]- Rust:
[policyCid, outputCid, runnerIdentityCid, logCid, blastRadiusCid]If the ordering is semantically irrelevant to the CICP protocol, standardizing to a consistent order (e.g., sorted lexicographically or by a defined field order) would improve maintainability and make diffs clearer.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In @.provekit/ci/accepted/ts/blake3-512:cf2632156ae353e1b6e263e8a5278476d15337d8fb7310297eccdce0476021db91086e63a869e08aeb3115ec2fa57d6f9b617377e7720b15493f1a2d61089f43.job-result.json around lines 13 - 19, The inputCids arrays are inconsistently ordered across job result artifacts; normalize the ordering for the symbol inputCids by choosing a deterministic rule (e.g., lexicographic sort of CID strings or a fixed semantic order such as [policyCid, blastRadiusCid, logCid, runnerIdentityCid, outputCid]) and apply that rule to all language artifacts (TS/Go/Rust) so the same ordered list appears in each job-result.json; update the generation code or post-processing step that emits inputCids to produce the chosen deterministic order.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/php/provekit-lift/src/ForwardPropagator.php`:
- Around line 397-408: The checkPositiveCalls function is scanning raw lines
with strpos and thus matches occurrences inside comments or string literals;
update checkPositiveCalls (used by lowerFloorSource) to ignore non-code text by
tokenizing the PHP source instead of raw substring search—use PHP's
token_get_all to walk tokens, detect a T_STRING token with content
"checkPositive" followed by a '(' punctuation token, then capture the argument
tokens until the matching ')' while skipping tokens inside comments (T_COMMENT,
T_DOC_COMMENT) and string tokens (T_CONSTANT_ENCAPSED_STRING); return the same
array shape ([start, arg]) but derived from token positions so false positives
in comments/strings are eliminated.
- Around line 358-384: The suppression flag topBlockDepth is being cleared when
a loop/header line has no braces, so an unbraced loop body (e.g. while ($c) \n
checkPositive($x);) loses top-fallback suppression; change the logic in
ForwardPropagator so that when startsTopFallbackBlock($trimmed) detects a header
with no '{' on the same line you set topBlockDepth to braceDepth+1 (or mark a
one-statement-applies flag) and ensure that this topBlockDepth is not nulled
until after the next statement is processed (i.e., delay clearing topBlockDepth
used by the checkPositiveCalls loop until after you consume a following unbraced
statement), referencing symbols: startsTopFallbackBlock, $topBlockDepth,
$braceDepth, checkPositiveCalls, isFunctionDefinition and the block that
currently nulls topBlockDepth at the end of the line.
- Around line 316-325: The code currently calls
$this->checkCallsite($stmt->calleeId, $currentPost, $stmt->range) and then
always merges $entry->post into $currentPost even when a diagnostic was
returned; change the logic in the 'case "call"' branch so that after calling
checkCallsite() you only merge $entry->post into $currentPost when no diagnostic
was produced (i.e., when $diagnostic is falsy) and $entry && $entry->post exist;
this prevents propagating callee postconditions after a failed precondition
(references: checkCallsite(), $diagnostic, $entry, $currentPost,
$this->index[$stmt->calleeId], $stmt->calleeId, $stmt->range).
In `@implementations/rust/provekit-lsp-rust/src/forward_propagator.rs`:
- Around line 310-314: The current function-header check (is_function_definition
= trimmed.starts_with("fn ")) misses qualified headers like "pub fn", "async
fn", "unsafe fn", "const fn" (and visibility forms like "pub(crate) fn"),
causing Stmt::Reset and top_block_depth clearing to be skipped; update the check
in forward_propagator.rs to recognize function headers with optional
qualifiers/visibility before "fn" (e.g., use a regex or token-based check that
matches start-of-line optional qualifiers/visibility/keywords followed by "fn"
and a space/paren) so that when such a header is detected you still push
Stmt::Reset and set top_block_depth = None (references: the variables trimmed,
is_function_definition, Stmt::Reset, and top_block_depth).
---
Nitpick comments:
In
@.provekit/ci/accepted/ts/blake3-512:cf2632156ae353e1b6e263e8a5278476d15337d8fb7310297eccdce0476021db91086e63a869e08aeb3115ec2fa57d6f9b617377e7720b15493f1a2d61089f43.job-result.json:
- Around line 13-19: The inputCids arrays are inconsistently ordered across job
result artifacts; normalize the ordering for the symbol inputCids by choosing a
deterministic rule (e.g., lexicographic sort of CID strings or a fixed semantic
order such as [policyCid, blastRadiusCid, logCid, runnerIdentityCid, outputCid])
and apply that rule to all language artifacts (TS/Go/Rust) so the same ordered
list appears in each job-result.json; update the generation code or
post-processing step that emits inputCids to produce the chosen deterministic
order.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 47634786-1879-44e6-b331-3bc7d0772d4f
📒 Files selected for processing (15)
.provekit/ci/accepted/go/blake3-512:275735848a3086ec6a984040a4ab54230576aa2b643250ebe49fe7ccec811defcfb7d0d7d24997385b7c9af54c7bc92fd87f449cd96a9aff9896e13f5dee7819.job-result.json.provekit/ci/accepted/rust/blake3-512:f3146fb0af9400276e30507d046038344fa7b21b0f33003799d252b41f7edeaeeedc0a3d9d48841387481d00ee81ded0896bcb31e21ce6033ae618a88253a5f8.job-result.json.provekit/ci/accepted/ts/blake3-512:cf2632156ae353e1b6e263e8a5278476d15337d8fb7310297eccdce0476021db91086e63a869e08aeb3115ec2fa57d6f9b617377e7720b15493f1a2d61089f43.job-result.jsonimplementations/go/cmd/provekit-lsp-go/forward_propagator.goimplementations/go/cmd/provekit-lsp-go/forward_propagator_test.goimplementations/go/cmd/provekit-lsp-go/main.goimplementations/php/provekit-lift/src/ForwardPropagator.phpimplementations/php/provekit-lift/src/lspd.phpimplementations/php/provekit-lift/tests/ForwardPropagatorTest.phpimplementations/rust/provekit-lsp-rust/src/forward_propagator.rsimplementations/rust/provekit-lsp-rust/src/main.rsimplementations/rust/provekit-lsp-rust/tests/round_trip.rstests/lsp/floor-fixture/go.gotests/lsp/floor-fixture/php.phptests/lsp/floor-fixture/rust.rs
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 364f549d0d
ℹ️ 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".
| for prefix in ["async ", "unsafe ", "const "] { | ||
| if let Some(next) = rest.strip_prefix(prefix) { |
There was a problem hiding this comment.
lower_floor_source depends on is_rust_function_header to insert Stmt::Reset between functions, but the qualifier parser only consumes async, unsafe, and const before requiring fn. Valid headers like pub extern "C" fn ... are therefore missed, so forward facts can leak from the previous function into the extern-qualified one and skew diagnostics (false positives/false negatives) across function boundaries.
Useful? React with 👍 / 👎.
| fn check_positive_calls(line: &str) -> Vec<(usize, String)> { | ||
| let mut calls = Vec::new(); | ||
| let mut search_from = 0usize; | ||
| while let Some(relative_start) = line[search_from..].find("checkPositive(") { |
There was a problem hiding this comment.
check_positive_calls scans raw source lines with find("checkPositive(") and no tokenization, so occurrences inside comments/strings (or inside longer identifiers) are lowered as real callsites. That makes parse emit implication-failed diagnostics for non-executable text such as // checkPositive(-1), creating deterministic false positives in normal Rust files.
Useful? React with 👍 / 👎.
| calls := []checkPositiveCall{} | ||
| searchFrom := 0 | ||
| for { | ||
| relativeStart := strings.Index(line[searchFrom:], "checkPositive(") |
There was a problem hiding this comment.
checkPositiveCalls uses a plain substring search on each raw line, so checkPositive( inside comments/strings (or embedded in longer identifiers) is treated as a real callsite. During parse, this can produce implication-failed diagnostics even when no executable checkPositive call exists, which turns ordinary documentation/log text into user-visible false positives.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (4)
implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs (1)
159-181: ⚡ Quick winStrengthen this test beyond count-only validation.
Line 180 checks only cardinality, so semantic regressions could still pass. Assert core diagnostic fields for each emitted item.
Suggested assertion hardening
assert_eq!(diagnostics.len(), 3, "{diagnostics:#?}"); + for diagnostic in &diagnostics { + assert_eq!(diagnostic.code, "implication-failed"); + assert_eq!(diagnostic.source, "provekit"); + assert_eq!(diagnostic.data.callee, "checkPositive"); + assert_eq!(diagnostic.data.missing_conjuncts, vec!["x > 0"]); + } }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs` around lines 159 - 181, The test floor_lowering_resets_on_qualified_function_headers currently only asserts diagnostics.len(), so enhance it to verify each diagnostic's core fields: iterate the diagnostics produced by ForwardPropagator::floor_v1_seed_index().emit_diagnostics(&ForwardPropagator::lower_floor_source(source)) and assert expected values for diagnostic.message (or title), diagnostic.severity, and diagnostic.span/range (matching the function locations like public_violates, crate_visible_violates, async_violates) and/or any diagnostic.code; keep the existing diagnostics variable and replace the single count-only check with concrete assertions that the three expected diagnostics target the correct function names and spans and have the expected severity/messages.implementations/go/cmd/provekit-lsp-go/forward_propagator_test.go (1)
154-169: ⚡ Quick winTighten the method-reset test to assert diagnostic identity, not only count.
TestLowerFloorSourceResetsOnGoMethodscurrently checks onlylen(diagnostics) == 1, which can false-pass if a different single diagnostic is emitted.Proposed assertion hardening
func TestLowerFloorSourceResetsOnGoMethods(t *testing.T) { @@ diagnostics := FloorV1SeedForwardPropagator().EmitDiagnostics(LowerFloorSource(source)) if len(diagnostics) != 1 { t.Fatalf("expected qualified method body to reset state and diagnose, got %#v", diagnostics) } + diagnostic := diagnostics[0] + if diagnostic.Code != "implication-failed" { + t.Fatalf("code = %q, want implication-failed", diagnostic.Code) + } + if diagnostic.Data.Callee != "checkPositive" { + t.Fatalf("callee = %q, want checkPositive", diagnostic.Data.Callee) + } }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/go/cmd/provekit-lsp-go/forward_propagator_test.go` around lines 154 - 169, TestLowerFloorSourceResetsOnGoMethods only checks len(diagnostics) and can false-pass; instead, after verifying FloorV1SeedForwardPropagator().EmitDiagnostics(LowerFloorSource(source)) yields exactly one diagnostic, assert the diagnostic's identity (e.g., diagnostic.ID or diagnostic.Code or diagnostic.Message) matches the expected diagnostic emitted for the qualified method reset. Update the test to first assert len(diagnostics) == 1 and then compare diagnostics[0].(use the project’s diagnostic identity field such as ID/Code/Message) against the expected value so the test verifies the exact diagnostic produced.implementations/php/provekit-lift/src/ForwardPropagator.php (1)
412-416: ⚡ Quick win
foreachanddo { … } whileare not recognized as top-fallback loops.
startsTopFallbackBlockmatches onlyfor/for(/while/while(. Aforeach (...) { checkPositive(-1); }body or ado { checkPositive(-1); } while (...)body with a literal-negative argument therefore lowers to a realassign(x <= 0)+call, producing an implication-failed diagnostic that thefor/whileequivalent suppresses. For v1 floor consistency it's worth either extending the prefix list to includeforeach/foreach(/do/do{/do\nor documenting the intentional gap.Suggested extension
private static function startsTopFallbackBlock(string $trimmed): bool { return str_starts_with($trimmed, 'for ') || str_starts_with($trimmed, 'for(') - || str_starts_with($trimmed, 'while ') || str_starts_with($trimmed, 'while('); + || str_starts_with($trimmed, 'while ') || str_starts_with($trimmed, 'while(') + || str_starts_with($trimmed, 'foreach ') || str_starts_with($trimmed, 'foreach(') + || $trimmed === 'do' || str_starts_with($trimmed, 'do ') || str_starts_with($trimmed, 'do{'); }Note:
do { … }opens a brace on the header line, so it would land in the$topBlockDepthbranch rather than the pending branch — that's the desired behavior.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/php/provekit-lift/src/ForwardPropagator.php` around lines 412 - 416, The startsTopFallbackBlock function currently only checks for 'for' and 'while' prefixes, missing 'foreach' and 'do' loop headers which causes foreach and do-while blocks to be misclassified; update startsTopFallbackBlock to also detect 'foreach ' and 'foreach(' and the 'do' forms (e.g. 'do ', 'do{' and 'do\n') so those loop headers are treated as top-fallback blocks by the existing logic in ForwardPropagator::startsTopFallbackBlock.implementations/php/provekit-lift/tests/ForwardPropagatorTest.php (1)
185-208: ⚡ Quick winAdd a read timeout to the lspd subprocess test to prevent indefinite hangs.
fgets($pipes[1])will block forever iflspd.phpcrashes before writing a response, fails to flush, or starts behaving differently in the future. Settingstream_set_timeouton the read pipe (and asserting viastream_get_meta_data) keeps CI from hanging on a regression.Suggested guard
assert_true(is_resource($proc), 'lspd process should start'); + stream_set_timeout($pipes[1], 5); $request = json_encode([ @@ $line = fgets($pipes[1]); + $meta = stream_get_meta_data($pipes[1]); fclose($pipes[1]); $stderr = stream_get_contents($pipes[2]); fclose($pipes[2]); $code = proc_close($proc); + assert_true(empty($meta['timed_out']), 'lspd response timed out'); assert_same(0, $code, 'lspd process exit code: ' . $stderr); assert_true(is_string($line), 'lspd should emit one response line');Note: the OpenGrep "command injection" hint on lines 185–189 is a false positive —
proc_openwith an array$cmddoes not invoke a shell.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/php/provekit-lift/tests/ForwardPropagatorTest.php` around lines 185 - 208, The test currently blocks on fgets($pipes[1]) if the lspd subprocess never writes; before calling fgets in ForwardPropagatorTest.php set a short stream timeout on $pipes[1] via stream_set_timeout($pipes[1], <seconds>) and after reading check stream_get_meta_data($pipes[1]) for the timed_out flag and assert false if timed_out is true (include the captured stderr in the assertion message). Ensure you still close pipes and proc_close($proc) in the same test flow so the timeout path cleans up the subprocess.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/php/provekit-lift/src/ForwardPropagator.php`:
- Around line 363-371: The loop-body suppression breaks when the loop header and
opening brace are on separate lines; update the logic so that if
$topSingleStatementPending is true and the current $scanLine contains a '{' (and
the line is not a new function definition), promote the pending state into a
real block by setting $topBlockDepth = $braceDepth (use the braceDepth value
computed before applying the current line's brace counts) and clear
$topSingleStatementPending so suppression persists until the matching '}' is
found; apply this change where the code handles lines with '{' (the same pattern
near the block handling around startsTopFallbackBlock and the similar block at
the other occurrence mentioned for lines 393-401), ensuring you compute the
before-update depth via $braceDepth + substr_count($scanLine, '{') -
substr_count($scanLine, '}') or equivalent and only promote when a '{' exists on
the current line and it's not a function definition.
---
Nitpick comments:
In `@implementations/go/cmd/provekit-lsp-go/forward_propagator_test.go`:
- Around line 154-169: TestLowerFloorSourceResetsOnGoMethods only checks
len(diagnostics) and can false-pass; instead, after verifying
FloorV1SeedForwardPropagator().EmitDiagnostics(LowerFloorSource(source)) yields
exactly one diagnostic, assert the diagnostic's identity (e.g., diagnostic.ID or
diagnostic.Code or diagnostic.Message) matches the expected diagnostic emitted
for the qualified method reset. Update the test to first assert len(diagnostics)
== 1 and then compare diagnostics[0].(use the project’s diagnostic identity
field such as ID/Code/Message) against the expected value so the test verifies
the exact diagnostic produced.
In `@implementations/php/provekit-lift/src/ForwardPropagator.php`:
- Around line 412-416: The startsTopFallbackBlock function currently only checks
for 'for' and 'while' prefixes, missing 'foreach' and 'do' loop headers which
causes foreach and do-while blocks to be misclassified; update
startsTopFallbackBlock to also detect 'foreach ' and 'foreach(' and the 'do'
forms (e.g. 'do ', 'do{' and 'do\n') so those loop headers are treated as
top-fallback blocks by the existing logic in
ForwardPropagator::startsTopFallbackBlock.
In `@implementations/php/provekit-lift/tests/ForwardPropagatorTest.php`:
- Around line 185-208: The test currently blocks on fgets($pipes[1]) if the lspd
subprocess never writes; before calling fgets in ForwardPropagatorTest.php set a
short stream timeout on $pipes[1] via stream_set_timeout($pipes[1], <seconds>)
and after reading check stream_get_meta_data($pipes[1]) for the timed_out flag
and assert false if timed_out is true (include the captured stderr in the
assertion message). Ensure you still close pipes and proc_close($proc) in the
same test flow so the timeout path cleans up the subprocess.
In `@implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs`:
- Around line 159-181: The test
floor_lowering_resets_on_qualified_function_headers currently only asserts
diagnostics.len(), so enhance it to verify each diagnostic's core fields:
iterate the diagnostics produced by
ForwardPropagator::floor_v1_seed_index().emit_diagnostics(&ForwardPropagator::lower_floor_source(source))
and assert expected values for diagnostic.message (or title),
diagnostic.severity, and diagnostic.span/range (matching the function locations
like public_violates, crate_visible_violates, async_violates) and/or any
diagnostic.code; keep the existing diagnostics variable and replace the single
count-only check with concrete assertions that the three expected diagnostics
target the correct function names and spans and have the expected
severity/messages.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: bbf5c5a7-1895-46ed-a669-58cda31c06ba
📒 Files selected for processing (8)
.provekit/ci/accepted/go/blake3-512:6bb052cd30d79c9680ac36bff34429108c1746f3b22b63e196d5837f9462732c4b0739a46e53e82510697ef6bdefbbdf1883bef5652c8e713337a9d0d434189a.job-result.json.provekit/ci/accepted/rust/blake3-512:803d931ad3484aab0eff88d76404dd1f369a0a3bbcc2be877b2c7fa71478e2c77f10e71843c5a8eb3d9170da467a3f2a2925fe622463b4d6b3fb5ab8131138d7.job-result.jsonimplementations/go/cmd/provekit-lsp-go/forward_propagator.goimplementations/go/cmd/provekit-lsp-go/forward_propagator_test.goimplementations/php/provekit-lift/src/ForwardPropagator.phpimplementations/php/provekit-lift/tests/ForwardPropagatorTest.phpimplementations/rust/provekit-lsp-rust/src/forward_propagator.rsimplementations/rust/provekit-lsp-rust/tests/forward_propagator.rs
✅ Files skipped from review due to trivial changes (2)
- .provekit/ci/accepted/rust/blake3-512:803d931ad3484aab0eff88d76404dd1f369a0a3bbcc2be877b2c7fa71478e2c77f10e71843c5a8eb3d9170da467a3f2a2925fe622463b4d6b3fb5ab8131138d7.job-result.json
- .provekit/ci/accepted/go/blake3-512:6bb052cd30d79c9680ac36bff34429108c1746f3b22b63e196d5837f9462732c4b0739a46e53e82510697ef6bdefbbdf1883bef5652c8e713337a9d0d434189a.job-result.json
🚧 Files skipped from review as they are similar to previous changes (2)
- implementations/rust/provekit-lsp-rust/src/forward_propagator.rs
- implementations/go/cmd/provekit-lsp-go/forward_propagator.go
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 22c107c54d
ℹ️ 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".
| { | ||
| $calls = []; | ||
| $searchFrom = 0; | ||
| while (($relativeStart = strpos($line, 'checkPositive(', $searchFrom)) !== false) { |
There was a problem hiding this comment.
checkPositiveCalls accepts any substring match of checkPositive(, so identifiers like notcheckPositive(-1) are lowered as baseline checkPositive callsites. That produces false implication-failed diagnostics for unrelated functions and also perturbs propagated state (assign/call) based on the wrong symbol. Add identifier-boundary checks (as done in the Go/Rust scanners) before recording a match.
Useful? React with 👍 / 👎.
| while (($relativeStart = strpos($line, 'checkPositive(', $searchFrom)) !== false) { | ||
| $start = $relativeStart; | ||
| $argsStart = $start + strlen('checkPositive('); |
There was a problem hiding this comment.
The matcher only looks for the exact token checkPositive(, so valid PHP call syntax like checkPositive (-1) is ignored and no diagnostic is emitted even when the precondition is violated. In editor buffers you cannot assume PSR formatting, so this creates real false negatives; the parser should skip optional spaces/tabs between the callee name and (.
Useful? React with 👍 / 👎.
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ac30a45128
ℹ️ 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".
| } else if bytes[idx] == b'\'' || bytes[idx..].starts_with(b"b'") { | ||
| idx = mask_escaped_delimited(bytes, idx, b'\'', &mut out); |
There was a problem hiding this comment.
The Rust masker currently treats any ' byte as the start of a quoted literal, so common lifetime syntax like fn f<'a>(...) is parsed as an unterminated char literal and masked until end-of-line. Because lower_floor_source relies on this masked text for brace depth and call lowering, lines containing lifetimes can lose {/} and other tokens, which can leak facts across functions or misclassify loop regions and diagnostics. This affects ordinary Rust code that uses lifetime annotations, not just edge cases.
Useful? React with 👍 / 👎.
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a2107cc76a
ℹ️ 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".
| for prefix in ["async ", "unsafe ", "const ", "extern "] { | ||
| if let Some(next) = rest.strip_prefix(prefix) { | ||
| rest = next.trim_start(); |
There was a problem hiding this comment.
is_rust_function_header consumes the extern qualifier but never skips the ABI literal, so valid headers like pub unsafe extern "C" fn ... are not recognized as function boundaries. In lower_floor_source this prevents emitting Stmt::Reset, which leaks postconditions from the previous function into the extern function body and can suppress expected implication-failed diagnostics there.
Useful? React with 👍 / 👎.
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1d07299c6e
ℹ️ 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".
| if ($start > 0 && self::isIdentifierByte($line[$start - 1])) { | ||
| $searchFrom = $start + $nameLen; |
There was a problem hiding this comment.
The call scanner treats any standalone checkPositive( as the baseline callee, but the boundary check only excludes identifier characters, so qualified calls like $obj->checkPositive(-1) and Foo::checkPositive(-1) are still lowered as the seeded global checkPositive. In those cases we can emit implication-failed diagnostics for unrelated methods, which is a false positive in normal OO PHP code.
Useful? React with 👍 / 👎.
| func startsTopFallbackBlock(trimmed string) bool { | ||
| return strings.HasPrefix(trimmed, "for ") || strings.HasPrefix(trimmed, "for{") |
There was a problem hiding this comment.
startsTopFallbackBlock only matches lines beginning with for, so valid labeled loops like outer: for ... { ... } are not marked as top-fallback. That means callsites inside labeled loops are analyzed as precise flow and can produce implication-failed diagnostics that the loop fallback is supposed to suppress.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (2)
implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs (2)
153-156: ⚡ Quick winMake this assertion order-independent to avoid brittle tests.
This currently depends on diagnostics being emitted in a fixed index order. Assert on the callee set (and kind/code) instead of positional indices.
Suggested adjustment
- assert_eq!(diagnostics.len(), 2, "{diagnostics:#?}"); - assert_eq!(diagnostics[0].data.callee, "checkPositive"); - assert_eq!(diagnostics[1].data.callee, "consumeReturn"); + assert_eq!(diagnostics.len(), 2, "{diagnostics:#?}"); + let actual_callees: std::collections::BTreeSet<&str> = + diagnostics.iter().map(|d| d.data.callee.as_str()).collect(); + let expected_callees: std::collections::BTreeSet<&str> = + ["checkPositive", "consumeReturn"].into_iter().collect(); + assert_eq!(actual_callees, expected_callees); + assert!(diagnostics.iter().all(|d| d.code == "implication-failed"));🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs` around lines 153 - 156, The test currently asserts diagnostics by index (assert_eq!(diagnostics[0].data.callee, "checkPositive") etc.), which is brittle; instead collect the diagnostics' identifying fields (e.g., diagnostics.iter().map(|d| (d.data.callee.clone(), d.kind.clone(), d.code.clone())) into a HashSet or sorted Vec) and assert that this set equals the expected set {("checkPositive", kind_x, code_x), ("consumeReturn", kind_y, code_y)} so order is ignored; update the assertions that reference diagnostics, diagnostics[0], and diagnostics[1] to use this set comparison.
180-181: ⚡ Quick winStrengthen count-only checks with semantic assertions.
len()checks alone can still pass with incorrect diagnostic content. Add at leastcode == "implication-failed"and expected callee assertions for these floor-lowering tests.Example for one test (apply similarly to others)
assert_eq!(diagnostics.len(), 3, "{diagnostics:#?}"); + assert!(diagnostics.iter().all(|d| d.code == "implication-failed")); + assert!(diagnostics.iter().all(|d| d.data.callee == "checkPositive"));Also applies to: 197-198, 226-227
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs` around lines 180 - 181, Replace the bare count-only assertions on the test-local diagnostics vector with semantic checks: after asserting diagnostics.len() == 3, iterate the diagnostics and assert each diagnostic.code (or diagnostic.code.as_deref()) equals "implication-failed" and assert the callee/target field (the field you use to record the expected function/term in these floor-lowering tests) matches the expected callee for each diagnostic; update the three test blocks in tests/forward_propagator.rs that currently only do assert_eq!(diagnostics.len(), ...) (the one at the shown location and the two others flagged) so they validate diagnostic.code == "implication-failed" and the expected callee identifier for each diagnostic entry rather than relying on count-only checks.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/go/cmd/provekit-lsp-go/forward_propagator.go`:
- Around line 377-390: The current match for the function name checkPositive
records selector-qualified calls like pkg.checkPositive because it only rejects
when the byte immediately before start is an identifier; update the matching
logic (around variables start, searchFrom, cursor, and function
isIdentifierByte) to also reject selector-qualified invocations by checking for
a '.' immediately before the name (e.g. if start>0 && line[start-1]=='.' then
set searchFrom = start+len(name) and continue), or more robustly skip any
whitespace backwards and if the first non-space byte before start is '.' treat
it as a selector and skip the match; apply this change where checkPositive
invocations are detected so only bare function calls are recorded.
- Around line 333-337: The current code calls SingleLineRange with raw byte
offsets (call.start and call.start+len("checkPositive")), which must be
converted to UTF-16 code unit offsets for LSP positions; modify the code that
appends the ForwardStmt so you compute UTF-16 column offsets for the start and
end by iterating the line up to the byte index, decoding runes and summing 1 for
BMP runes or 2 for supplementary runes (use utf16.EncodeRune helper) to get
startUTF16 and endUTF16, then call SingleLineRange(lineIdx, startUTF16,
endUTF16) when constructing the ForwardStmt (symbols: ForwardStmt,
ForwardStmtCall, call.start, SingleLineRange).
In `@implementations/php/provekit-lift/src/ForwardPropagator.php`:
- Around line 420-424: The startsTopFallbackBlock predicate currently only
matches for/while and should be extended to also detect foreach, switch and
do-while constructs so the propagator treats their bodies as top-fallback
regions; update startsTopFallbackBlock to return true for strings starting with
'foreach', 'switch', and 'do' (and for 'do{' / 'do {' variants) and also adjust
the logic that handles the closing brace so a bare 'while(...)' immediately
following a '}' from a do-block does not open a new topSingleStatementPending —
run/add a regression mirroring testNextLineLoopBraceUsesTopFallbackForWholeBody
to cover foreach, switch and do/while cases and ensure
topBlockDepth/topSingleStatementPending are set/cleared consistently for these
constructs.
- Around line 459-470: The identifier-boundary check in ForwardPropagator.php
misses method/static-call prefixes (-> and ::), so add an explicit check around
the existing isIdentifierByte usage in the loop that looks for $name: if the
char before $start is '>' or ':' (i.e. $line[$start-1] === '>' ||
$line[$start-1] === ':'), treat it as a non-global identifier and skip lowering
by advancing $searchFrom (same behavior as when isIdentifierByte returns true);
update the while loop that uses $relativeStart/$start/$nameLen/$cursor and
isIdentifierByte to include this condition (and similarly ensure the cursor-side
check still applies), and add a regression test like "$obj->checkPositive(-1);
Foo::checkPositive(-1);" asserting zero diagnostics.
---
Nitpick comments:
In `@implementations/rust/provekit-lsp-rust/tests/forward_propagator.rs`:
- Around line 153-156: The test currently asserts diagnostics by index
(assert_eq!(diagnostics[0].data.callee, "checkPositive") etc.), which is
brittle; instead collect the diagnostics' identifying fields (e.g.,
diagnostics.iter().map(|d| (d.data.callee.clone(), d.kind.clone(),
d.code.clone())) into a HashSet or sorted Vec) and assert that this set equals
the expected set {("checkPositive", kind_x, code_x), ("consumeReturn", kind_y,
code_y)} so order is ignored; update the assertions that reference diagnostics,
diagnostics[0], and diagnostics[1] to use this set comparison.
- Around line 180-181: Replace the bare count-only assertions on the test-local
diagnostics vector with semantic checks: after asserting diagnostics.len() == 3,
iterate the diagnostics and assert each diagnostic.code (or
diagnostic.code.as_deref()) equals "implication-failed" and assert the
callee/target field (the field you use to record the expected function/term in
these floor-lowering tests) matches the expected callee for each diagnostic;
update the three test blocks in tests/forward_propagator.rs that currently only
do assert_eq!(diagnostics.len(), ...) (the one at the shown location and the two
others flagged) so they validate diagnostic.code == "implication-failed" and the
expected callee identifier for each diagnostic entry rather than relying on
count-only checks.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: cd458bdc-7f52-47c2-b872-df983427379a
📒 Files selected for processing (10)
.provekit/ci/accepted/go/blake3-512:81c69046c282a4c4fe84051dc79e9986144a12358ec2a0e2b4d3154ed9241bb73b2a8480c75df9c3b9f39744b8dff7bc8e743f95442be329297a3698715fa3e1.job-result.json.provekit/ci/accepted/rust/blake3-512:1664fd99978d6da7bca9d54a1d2d635d2d4e76ed486c07021cd8bbbc60a51d7615b030fac25ef24e2228ca0e35d4815db959b507f25eb47ad81d698f4430ff88.job-result.json.provekit/ci/accepted/rust/blake3-512:2ac53de148161672d99e0302fc1d939a35a82af744300ec5f74df71b56ff77b18bca047e1556026816f2866fe55b01cf988b40079b283cf14ed27dffc7f3303c.job-result.json.provekit/ci/accepted/rust/blake3-512:cd7e1e2855389cab7c28af88541e7cb1950bf3ee9b119b73fb7f03bf60d6dc939e8e4071f3e792e02520b4b9dc0adc1c2e6f663a56e6387623fea9364c8fbc28.job-result.jsonimplementations/go/cmd/provekit-lsp-go/forward_propagator.goimplementations/go/cmd/provekit-lsp-go/forward_propagator_test.goimplementations/php/provekit-lift/src/ForwardPropagator.phpimplementations/php/provekit-lift/tests/ForwardPropagatorTest.phpimplementations/rust/provekit-lsp-rust/src/forward_propagator.rsimplementations/rust/provekit-lsp-rust/tests/forward_propagator.rs
✅ Files skipped from review due to trivial changes (4)
- .provekit/ci/accepted/rust/blake3-512:cd7e1e2855389cab7c28af88541e7cb1950bf3ee9b119b73fb7f03bf60d6dc939e8e4071f3e792e02520b4b9dc0adc1c2e6f663a56e6387623fea9364c8fbc28.job-result.json
- .provekit/ci/accepted/rust/blake3-512:1664fd99978d6da7bca9d54a1d2d635d2d4e76ed486c07021cd8bbbc60a51d7615b030fac25ef24e2228ca0e35d4815db959b507f25eb47ad81d698f4430ff88.job-result.json
- .provekit/ci/accepted/go/blake3-512:81c69046c282a4c4fe84051dc79e9986144a12358ec2a0e2b4d3154ed9241bb73b2a8480c75df9c3b9f39744b8dff7bc8e743f95442be329297a3698715fa3e1.job-result.json
- .provekit/ci/accepted/rust/blake3-512:2ac53de148161672d99e0302fc1d939a35a82af744300ec5f74df71b56ff77b18bca047e1556026816f2866fe55b01cf988b40079b283cf14ed27dffc7f3303c.job-result.json
🚧 Files skipped from review as they are similar to previous changes (2)
- implementations/go/cmd/provekit-lsp-go/forward_propagator_test.go
- implementations/rust/provekit-lsp-rust/src/forward_propagator.rs
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
|
@coderabbitai review |
|
✅ Actions performedReview triggered.
|
Summary
tests/lsp/floor-fixture/.implication-faileddiagnostics for the v1 forward-propagation floor.rust,go, andtsblast radii on this PR closure.Notes
docs/lsp/diagnostic-shape-v1.mdanddocs/lsp/callsite-resolution-v1.md.lspd.phpinclude paths now resolve the shared PHP IR files from the parent kit directory so the daemon can run in-process tests.make prove-rust,make prove-go, andmake prove-ts; PHP is not in the checked-in CICP accept kit set yet.Validation
cargo test -p provekit-lsp-rustcargo check --workspacefromimplementations/rust(exit 0; existing unrelated warnings remain)go test ./cmd/provekit-lsp-go/...php -l implementations/php/provekit-lift/src/ForwardPropagator.phpphp -l implementations/php/provekit-lift/src/lspd.phpphp implementations/php/provekit-lift/tests/ForwardPropagatorTest.phppnpm testmake prove-rustmake prove-gomake prove-tsimplementations/rust/target/release/provekit ci accept --repo . --all-kits --clean --check --json(existingCount: 11,missingCount: 0,verifiedCount: 11)git diff --checkgit diff --cached --checkmake conformancewas not run end-to-end in this pass.Summary by CodeRabbit
New Features
Tests
Chores