[hermes] Initial commit #2968
[hermes] Initial commit #2968
Conversation
gherrit-pr-id: Gb0d4d182a8f82f845a81ba9cd36038cef442a30e
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 establishes the foundational framework for formal verification of Rust programs by introducing 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. 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 the initial commit for the hermes tool, a verification orchestrator for Rust. The changes include the core logic for parsing verification annotations, orchestrating Charon and Aeneas, and stitching generated Lean code, along with integration tests.
My review has identified several critical issues that need to be addressed:
- The test case files contain unresolved merge conflict markers, which will cause the build to fail.
- The integration tests have a hardcoded absolute path, making them non-portable.
- There are several instances of
.unwrap()onPathto&strconversions that can lead to panics on non-Windows systems. - The integration tests use
env::set_varin an unsafe manner, which can cause data races when tests are run in parallel.
Additionally, there are some medium-severity issues regarding the use of the unstable 2024 Rust edition and a dependency on a main branch which affects reproducibility.
Please address these points to improve the robustness, portability, and correctness of the new tool.
| <<<<<<< Updated upstream | ||
| spec id (T : Type) (x : T) | ||
| : id T x = ok x | ||
| @*/ | ||
| /*@ proof | ||
| ======= | ||
| spec id {T : Type} (x : T) | ||
| ensures |ret| ret = x | ||
| @*/ | ||
| /*@ proof | ||
| := by | ||
| >>>>>>> Stashed changes |
There was a problem hiding this comment.
This file, along with several other test case files in this PR (incorrect_proof.rs, syntax_error_in_spec.rs, undefined_variable.rs, add.rs, checked_add.rs, struct_method.rs, unchecked_wrapper.rs), contains git merge conflict markers (<<<<<<<, =======, >>>>>>>). These markers make the files syntactically incorrect and will cause build failures. Please resolve the merge conflicts and remove these markers.
| let cases_dir = manifest_dir.join("tests/cases"); | ||
|
|
||
| let aeneas_path = | ||
| PathBuf::from("/usr/local/google/home/joshlf/workspace/zerocopy/hermes2/aeneas"); |
There was a problem hiding this comment.
This hardcoded absolute path makes the tests unrunnable on any machine other than the author's. This path should be made configurable, for example, through an environment variable. The test could then read this environment variable and be skipped if it's not set.
| PathBuf::from("/usr/local/google/home/joshlf/workspace/zerocopy/hermes2/aeneas"); | |
| std::env::var("AENEAS_PATH").expect("AENEAS_PATH must be set for integration tests").into() |
| let crate_root = crate_root.to_str().unwrap(); | ||
| let dest_file = dest_file.to_str().unwrap(); |
There was a problem hiding this comment.
Using .unwrap() on Path::to_str() can cause a panic if a path contains non-UTF-8 characters, which is possible on non-Windows systems. It's safer to handle this possibility. crate_root is used with println! and current_dir, both of which can work directly with &Path, so its conversion to &str is unnecessary. For dest_file, you should handle the potential conversion failure gracefully by returning an error.
| let crate_root = crate_root.to_str().unwrap(); | |
| let dest_file = dest_file.to_str().unwrap(); | |
| let dest_file = dest_file.to_str().ok_or_else(|| anyhow!("destination path is not valid UTF-8"))?; |
| let llbc_path = llbc_path.to_str().unwrap(); | ||
| let dest = dest.to_str().unwrap(); |
There was a problem hiding this comment.
Using .unwrap() on Path::to_str() can cause a panic if a path contains non-UTF-8 characters. It's safer to handle this possibility by returning an error.
| let llbc_path = llbc_path.to_str().unwrap(); | |
| let dest = dest.to_str().unwrap(); | |
| let llbc_path = llbc_path.to_str().ok_or_else(|| anyhow!("llbc path is not valid UTF-8"))?; | |
| let dest = dest.to_str().ok_or_else(|| anyhow!("destination path is not valid UTF-8"))?; |
| unsafe { | ||
| env::set_var("PATH", new_path); | ||
| } |
There was a problem hiding this comment.
Using env::set_var is not thread-safe and can lead to race conditions if tests are run in parallel, which Cargo might do. The unsafe block here hides this danger. Instead of modifying the PATH for the whole process, it's safer to set the environment for the Commands that need it. Since charon and aeneas are executed via std::process::Command in orchestration.rs, you could pass the required PATH to those commands using Command::env. If that's not feasible, consider using a std::sync::Mutex to ensure exclusive access when modifying the environment variable.
| [package] | ||
| name = "cargo-hermes" | ||
| version = "0.1.0" | ||
| edition = "2024" |
There was a problem hiding this comment.
The 2024 Rust edition is not yet stable. Using it might cause build failures on stable or beta toolchains. It's recommended to use the latest stable edition, '2021', unless this project is explicitly intended to be built only with a nightly Rust toolchain.
| edition = "2024" | |
| edition = "2021" |
| if let Some(path) = manifest_path { | ||
| // If it's a script, we just use the filename. | ||
| if path.extension().map_or(false, |e| e == "rs") { | ||
| return Ok(path.file_stem().unwrap().to_string_lossy().to_string()); |
There was a problem hiding this comment.
.unwrap() can panic if the path has no file stem (e.g., it's a directory like . or .., or a file like .bashrc). It's safer to handle this case gracefully by returning an error.
| return Ok(path.file_stem().unwrap().to_string_lossy().to_string()); | |
| return Ok(path.file_stem().ok_or_else(|| anyhow!("script path has no file stem: {:?}", path))?.to_string_lossy().to_string()); |
| let require_line = if let Some(path) = aeneas_path { | ||
| format!("require aeneas from \"{}\"", path.display()) | ||
| } else { | ||
| r#"require aeneas from git "https://github.com/AeneasVerif/aeneas" @ "main""#.to_string() |
There was a problem hiding this comment.
Depending on the main branch of a git repository can lead to non-reproducible builds, as main can change at any time. It's recommended to pin this dependency to a specific commit hash or tag to ensure builds are reproducible, for example: ... @ "a1b2c3d4...".
1 participant
Latest Update: v5 — Compare vs v4
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gb0d4d182a8f82f845a81ba9cd36038cef442a30e && git checkout -b pr-Gb0d4d182a8f82f845a81ba9cd36038cef442a30e FETCH_HEADCheckout
git fetch origin refs/heads/Gb0d4d182a8f82f845a81ba9cd36038cef442a30e && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gb0d4d182a8f82f845a81ba9cd36038cef442a30e && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.