[hermes] Reject annotated items in blocks #3046
Conversation
gherrit-pr-id: G3j7gcwkk2kr2uix4cyeyxid6egsuoa4e
Summary of ChangesHello @joshlf, I'm Gemini Code Assist1! I'm currently reviewing this pull request and will post my feedback shortly. In the meantime, here's a summary to help you and other reviewers quickly get up to speed! This pull request significantly improves the robustness and correctness of the Hermes tool by addressing how it handles Rust items defined within blocks and complex module structures. It introduces a mechanism to explicitly reject annotated items that are not reliably nameable within Rust's module system, preventing potential issues with verification. Furthermore, it enhances the module scanning process to correctly handle and detect cyclic module dependencies, avoiding infinite loops, and refines the way entry points are passed to Charon, ensuring that all relevant annotated items are considered for verification, even if they require falling back to their parent module. Highlights
🧠 New Feature in Public Preview: You can now enable Memory to help Gemini Code Assist learn from your team's feedback. This makes future code reviews more consistent and personalized to your project's style. Click here to enable Memory in your admin console. Changelog
Activity
Using Gemini Code AssistThe full guide for Gemini Code Assist can be found on our documentation page, here are some quick tips. Invoking Gemini You can request assistance from Gemini at any point by creating a comment using either
Customization To customize Gemini Code Assist for GitHub experience, repository maintainers can create a configuration file and/or provide a custom code review style guide (such as PEP-8 for Python) by creating and adding files to a Limitations & Feedback Gemini Code Assist may make mistakes. Please leave feedback on any instances where its feedback is incorrect or counter productive. You can react with 👍 and 👎 on @gemini-code-assist comments. If you're interested in giving your feedback about your experience with Gemini Code Assist for Github and other Google products, sign up here. You can also get AI-powered code generation, chat, as well as code reviews directly in the IDE at no cost with the Gemini Code Assist IDE Extension. Footnotes
|
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request introduces a significant change to reject Hermes annotations on items defined within blocks (like function bodies), which is an important correctness fix to avoid unsound verification. The implementation correctly uses the syn visitor to track whether it's inside a block and raises an error for annotated items.
The PR also includes several valuable refactorings and improvements:
- A new fallback strategy for items in
implblocks, which are hard to name reliably. Instead of complex path construction, it now uses the parent module path, with deduplication to keep the argument list clean. - Improved module processing logic, replacing a global visited set with per-path ancestor tracking. This correctly handles files included as modules in multiple places while still preventing infinite recursion from cyclic module declarations.
- Better differentiation of compilation targets by including the target kind in
HermesTargetNameand the generated.llbcfilename hash.
The changes are well-supported by a comprehensive set of new and updated tests that cover the new error conditions, the fallback strategy, and edge cases in module resolution.
I have a couple of minor suggestions for improving panic robustness in channel communication.
| // back to naming the parent module. | ||
| Impl(_) | ImplItemFn(_) | TraitItemFn(_) => { | ||
| let start_from = full_path.join("::"); | ||
| path_tx.send((name.clone(), start_from)).unwrap(); |
There was a problem hiding this comment.
Using .unwrap() here could cause a panic if the receiving end of the channel is dropped, for example, if another part of the program panics. It would be more robust to handle the Result of send, for instance by ignoring the error, similar to how err_tx.send is handled. This prevents a double panic.
| path_tx.send((name.clone(), start_from)).unwrap(); | |
| let _ = path_tx.send((name.clone(), start_from)); |
| full_path.push(item_name); | ||
| let start_from = full_path.join("::"); | ||
| log::debug!("Found entry point: {}", start_from); | ||
| path_tx.send((name.clone(), start_from)).unwrap(); |
There was a problem hiding this comment.
Similar to the comment above, using .unwrap() here could cause a panic. It's safer to ignore the result of the send operation.
| path_tx.send((name.clone(), start_from)).unwrap(); | |
| let _ = path_tx.send((name.clone(), start_from)); |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gegf4fywvkwtqzwzektqc5lett4skoxvx #3046 +/- ##
====================================================================
Coverage ? 91.87%
====================================================================
Files ? 20
Lines ? 6057
Branches ? 0
====================================================================
Hits ? 5565
Misses ? 492
Partials ? 0 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
2 participants
This PR is on branch hermes.
#[cfg_attr(..., path = "...")]#3045unsaferedaction #3034mod foo;declarations #3008⬇️ Download this PR
Branch
git fetch origin refs/heads/G3j7gcwkk2kr2uix4cyeyxid6egsuoa4e && git checkout -b pr-G3j7gcwkk2kr2uix4cyeyxid6egsuoa4e FETCH_HEADCheckout
git fetch origin refs/heads/G3j7gcwkk2kr2uix4cyeyxid6egsuoa4e && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G3j7gcwkk2kr2uix4cyeyxid6egsuoa4e && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.