[hermes] Add Charon step #3014
[hermes] Add Charon step #3014
Conversation
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 extends the Hermes verification tool by integrating the 'Charon' analysis step directly into its workflow. The primary goal is to enable deeper static analysis of Rust code by leveraging Charon on the transformed shadow crate. This involves setting up the execution environment for Charon, ensuring proper argument forwarding, and enhancing the intermediate code generation phase to identify relevant analysis targets. 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 new charon step to the hermes tool. The changes are well-structured and include adding a new charon.rs module, updating main.rs to integrate the new step, and modifying shadow.rs to gather necessary entry points. The addition of env_logger is a good improvement for debugging. I have one suggestion in charon.rs to improve error logging for better diagnostics. Overall, the implementation aligns well with the PR's objective.
tools/hermes/src/charon.rs
Outdated
| let abs_manifest = | ||
| std::fs::canonicalize(original_manifest).unwrap_or_else(|_| original_manifest.clone()); |
There was a problem hiding this comment.
The error from std::fs::canonicalize is silently ignored. If canonicalize fails (for example, because the path does not exist), this will fall back to using the original path. This could lead to unexpected behavior or a less clear error message later on. It would be better to log this failure to aid in debugging.
| let abs_manifest = | |
| std::fs::canonicalize(original_manifest).unwrap_or_else(|_| original_manifest.clone()); | |
| let abs_manifest = std::fs::canonicalize(original_manifest).unwrap_or_else(|e| { | |
| log::warn!("Failed to canonicalize manifest path {:?}: {}. Using original path.", original_manifest, e); | |
| original_manifest.clone() | |
| }); |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G7f8abd90b628d02a6fdc01985535eef50509312e #3014 +/- ##
==========================================================================
Coverage 91.87% 91.87%
==========================================================================
Files 20 20
Lines 6057 6057
==========================================================================
Hits 5565 5565
Misses 492 492 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
joshlf
force-pushed
the
Ge1bd84b5d857e18e3668e809844c6d73b808a020
branch
2 times, most recently
from
1185221 to
3434d56
Compare
joshlf
force-pushed
the
G7f8abd90b628d02a6fdc01985535eef50509312e
branch
from
0fe1018 to
7590938
Compare
joshlf
force-pushed
the
Ge1bd84b5d857e18e3668e809844c6d73b808a020
branch
from
3434d56 to
bc49806
Compare
gherrit-pr-id: Ge1bd84b5d857e18e3668e809844c6d73b808a020
joshlf
force-pushed
the
G7f8abd90b628d02a6fdc01985535eef50509312e
branch
from
7590938 to
b3bfc03
Compare
joshlf
force-pushed
the
Ge1bd84b5d857e18e3668e809844c6d73b808a020
branch
from
bc49806 to
c0c7f26
Compare
2 participants
mod foo;declarations #3008Latest Update: v26 — Compare vs v25
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Ge1bd84b5d857e18e3668e809844c6d73b808a020 && git checkout -b pr-Ge1bd84b5d857e18e3668e809844c6d73b808a020 FETCH_HEADCheckout
git fetch origin refs/heads/Ge1bd84b5d857e18e3668e809844c6d73b808a020 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Ge1bd84b5d857e18e3668e809844c6d73b808a020 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.