fix: E501 messages render the precondition in call-site terms#731
Merged
Conversation
The description gains an 'At this call site:' line with the callee's
precondition rendered against the actual arguments (callee parameter
slots substituted via slot_table's De Bruijn resolution, formatted
with format_expr), and the Fix: text becomes concrete code — the
guard with the rendered call and the exact requires(...) to add —
instead of the generic two-option advice. Module-qualified callees
and unmappable slots keep the generic wording.
Tests pin the substituted rendering (string_length("") > 0), the
De Bruijn shuffle (@Int.1 > @Int.0 at cmp(1, 2) renders 1 > 2), the
unmappable-slot fallback, and the upgraded LSP instruction-contract
assertions. 4,321 tests total.
Folds into the v0.0.170 release (no version bump; the existing
CHANGELOG [0.0.170] section gains the bullet; the tag moves to the
merge commit on merge).
Co-Authored-By: Claude <noreply@anthropic.invalid>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (2)
📝 WalkthroughWalkthroughE501 precondition-violation diagnostics now render call-site-specific preconditions by substituting callee parameter slots with actual argument expressions; diagnostics include concrete guard code and strengthened ChangesE501 call-site precondition rendering
Sequence DiagramsequenceDiagram
participant Caller
participant Verifier as _report_call_violation
participant PreHelper as _pre_at_call_site
participant SlotTable as slot_table
participant Diagnostic
Caller->>Verifier: call node + callee + args -> violation detected
Verifier->>PreHelper: resolve callee (non-ModuleCall), pass callee.requires and call node
PreHelper->>SlotTable: map callee parameter slots -> caller argument expressions
alt Substitution succeeds
SlotTable-->>PreHelper: substituted expression
PreHelper-->>Verifier: site_pre string
Verifier->>Diagnostic: append "At this call site:" + rendered precondition
Verifier->>Diagnostic: set E501 fix to concrete guard or requires(site_pre)
else Substitution fails
SlotTable-->>PreHelper: None
PreHelper-->>Verifier: site_pre = None
Verifier->>Diagnostic: keep generic fix wording
end
Diagnostic-->>Caller: diagnostic payload (description + fix)
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #731 +/- ##
==========================================
+ Coverage 90.94% 90.95% +0.01%
==========================================
Files 70 70
Lines 24861 24902 +41
Branches 292 292
==========================================
+ Hits 22609 22649 +40
- Misses 2245 2246 +1
Partials 7 7
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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 `@tests/test_lsp.py`:
- Around line 1184-1189: Add an assertion that the diagnostic description
includes the literal "At this call site:" so the rendered call-site line is
explicitly checked; in the test (tests/test_lsp.py) augment the existing
assertions on the message variable to include something like assert "At this
call site:" in message so the description-side clause cannot regress (keep
existing asserts for the guard and requires text).
In `@vera/verifier.py`:
- Around line 1594-1607: The code currently applies call-site substitution
unconditionally after resolving callee_info via
self.env.lookup_function(callee_name), which wrongly substitutes
module-qualified calls; update the logic in the block that computes site_pre so
that you only call _pre_at_call_site when call_node is not an instance of
ast.ModuleCall (i.e., add an explicit guard checking call_node against
ast.ModuleCall before invoking _pre_at_call_site with
callee_info.param_type_exprs, preserving the generic fallback wording for
module-qualified callees).
🪄 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: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: fcaa23f2-180e-4bad-b525-1ddcc1a445e3
📒 Files selected for processing (7)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdtests/test_lsp.pytests/test_obligations.pyvera/verifier.py
…-in (#731 round 1) The substitution now short-circuits for module-qualified callees before the bare-name lookup (a local function sharing the callee's name would supply the wrong parameter table) — enforcing the generic fallback the docstring already promised. The LSP instruction-contract test pins the 'At this call site:' description line. The changelog gate's own test suite is reworked for the fold-in rule: the frozen-history pin moves to an older-than-latest section (still rejected) and the latest-section fold-in case gains its own accepting pin. Skip-changelog: amends behaviour shipped in this PR's own fold-in bullet
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
tests/test_lsp.py (1)
1183-1183:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winPin the concrete description payload, not just the label.
At Line 1183, asserting only
"At this call site:"still permits regressions where the rendered expression is missing or altered in the description. Please assert the full expected description fragment (e.g."At this call site: 0 > 0"), so call-site substitution in the description is genuinely locked.Suggested test tightening
- assert "At this call site:" in message + assert "At this call site: 0 > 0" in messageAs per coding guidelines, diagnostics must preserve full instruction-contract detail across surfaces, including concrete call-site rationale in human-readable output.
🤖 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 `@tests/test_lsp.py` at line 1183, The test currently only asserts that "At this call site:" appears in the diagnostic message, allowing the concrete substitution to regress; update the assertion for the variable/message used in tests/test_lsp.py (the assertion around message at Line 1183) to assert the full expected description fragment (for example "At this call site: 0 > 0") so the rendered expression is pinned rather than just the label.Source: Coding guidelines
🤖 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 `@scripts/check_changelog_updated.py`:
- Around line 175-178: The docstring currently claims that a bare "+##
[Unreleased]" heading counts as a new entry but the implementation explicitly
rejects a bare Unreleased heading and only treats Unreleased as a new entry when
there is actual content beneath it; update the docstring near the "A \"new
entry\" is any of:" section to state that "+## [Unreleased]" only counts if it
contains content (i.e., lines under the Unreleased heading), matching the logic
in the script that ignores an empty Unreleased heading.
---
Duplicate comments:
In `@tests/test_lsp.py`:
- Line 1183: The test currently only asserts that "At this call site:" appears
in the diagnostic message, allowing the concrete substitution to regress; update
the assertion for the variable/message used in tests/test_lsp.py (the assertion
around message at Line 1183) to assert the full expected description fragment
(for example "At this call site: 0 > 0") so the rendered expression is pinned
rather than just the label.
🪄 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: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: c3894529-79c3-411f-9783-4ca1216b28b5
📒 Files selected for processing (7)
README.mdROADMAP.mdTESTING.mdscripts/check_changelog_updated.pytests/test_check_changelog_updated.pytests/test_lsp.pyvera/verifier.py
… rendered substitution at the LSP layer (#731 round 2) The docstring's claim that an added bare [Unreleased] heading counts was a pre-existing inaccuracy (the implementation has always required content beneath it); item 1 now describes versioned headings only. The LSP instruction-contract test pins 'At this call site: 0 > 0' — the rendered expression, not just the label. Skip-changelog: docstring + test-assertion amendments within this PR
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
Follow-up to the PR that closed issues 727/728, prompted by review of the shipped hover: the E501 message was accurate but generic. It now speaks in call-site terms.
Description gains an
At this call site:line — the callee's precondition rendered with the actual arguments substituted for its parameter slots:Fix: becomes concrete code instead of the generic two-option advice:
Mechanics
slot_table's De Bruijn most-recent-first logic and rebuilds the precondition AST with the call's argument expressions (generic frozen-dataclass rebuild), rendered viaformat_expr.Tests (3 new; 4,321 total)
The substituted rendering pinned exactly (
string_length("") > 0plus the guard and requires in the fix), the De Bruijn shuffle (requires(@Int.1 > @Int.0)atcmp(1, 2)renders1 > 2— parameter 1 then parameter 2), the unmappable-slot fallback returning None, and the LSP instruction-contract assertions upgraded to pin the concrete content.Release handling — folds into v0.0.170
No version bump: the bullet is added to the existing CHANGELOG
[0.0.170]section (the changelog gate accepts the amendment — verified by pre-commit). On merge, thev0.0.170tag moves to the merge commit and the GitHub release notes get refreshed from the section.🤖 Generated with Claude Code
Summary by CodeRabbit
Bug Fixes
Tests
Documentation
Chores