[WIP] Shadow crate + unsafe #2972
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 introduces a significant architectural change by implementing a 'shadow crate' strategy to manage 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
|
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 introduces a 'shadow crate' mechanism to Hermes for handling and verifying unsafe Rust code. It involves creating a modified copy of the original crate where 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 and well-designed feature for handling unsafe code by creating a "shadow crate". In this shadow crate, unsafe functions are transformed into safe shims based on their contracts, or unsafe blocks are unwrapped, allowing for verification. The implementation is comprehensive, including parsing, AST transformation, and updates to the verification pipeline. I've found a few areas for improvement, including removing debug statements, enhancing parsing robustness, and addressing a potential bug in path handling within the pipeline. Overall, this is a strong contribution that greatly enhances the tool's capabilities.
| if let Ok(rel) = path.strip_prefix(crate_root) { | ||
| Some(shadow_crate_root.join(rel)) | ||
| } else { | ||
| Some(path.clone()) |
There was a problem hiding this comment.
This else branch seems problematic. If manifest_path is outside crate_root, strip_prefix will fail, and shadow_manifest_path will be set to the original manifest_path. However, run_charon is executed inside the shadow_crate_root. This will likely cause charon to run on the original crate instead of the shadowed one, defeating the purpose of this new mechanism. This case should probably result in an error or be handled differently to ensure the shadowed manifest is always used.
|
|
||
| for attr in attrs { | ||
| if let Some(doc) = parse_doc_attr(attr) { | ||
| println!("DEBUG: Doc attr: {:?}", doc); |
There was a problem hiding this comment.
This println! and others in this function (lines 219, 224) appear to be for debugging. They should be removed before merging to keep the tool's output clean.
| println!("DEBUG: Trimmed line: '{}'", trimmed); | ||
| // Check found marker e.g. "@ lean model" | ||
| if trimmed.starts_with('@') { | ||
| if trimmed.contains("lean model") { |
There was a problem hiding this comment.
Using contains("lean model") is less precise than strip_prefix and could lead to false positives (e.g., on a comment like ///@ lean model_v2). It's also inconsistent with parser.rs, which uses strip_prefix. For improved robustness and consistency, it would be better to use strip_prefix here as well.
| if trimmed.contains("lean model") { | |
| if trimmed.strip_prefix("@ lean model").is_some() { |
There was a problem hiding this comment.
Code Review
This pull request introduces a significant new feature: the creation of a "shadow crate" to handle unsafe code during verification. The core idea is to generate a sanitized version of the user's crate where unsafe blocks are either removed or replaced by safe, model-based shims. This allows the verification toolchain to analyze the code in a safe context. The changes are well-contained within the new shadow module and its integration into the main pipeline. My review focuses on improving the robustness and clarity of the new shadow.rs implementation, addressing issues related to error handling, debug artifacts, and code maintainability.
| fn parse_model_specs(attrs: &[Attribute]) -> (bool, Vec<String>) { | ||
| let mut is_model = false; | ||
| let mut requires = Vec::new(); | ||
|
|
||
| for attr in attrs { | ||
| if let Some(doc) = parse_doc_attr(attr) { | ||
| println!("DEBUG: Doc attr: {:?}", doc); | ||
| for line in doc.lines() { | ||
| let trimmed = line.trim(); | ||
| println!("DEBUG: Trimmed line: '{}'", trimmed); | ||
| // Check found marker e.g. "@ lean model" | ||
| if trimmed.starts_with('@') { | ||
| if trimmed.contains("lean model") { | ||
| is_model = true; | ||
| println!("DEBUG: Found model marker!"); | ||
| } | ||
|
|
||
| if let Some(rest) = trimmed.strip_prefix("@ requires") { | ||
| let content = rest.trim(); | ||
| // Strip binder name if present (e.g. "h : x > 0" -> "x > 0") | ||
| let condition = if let Some((_, expr)) = content.split_once(':') { | ||
| expr.trim() | ||
| } else { | ||
| content | ||
| }; | ||
| requires.push(condition.to_string()); | ||
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
| (is_model, requires) | ||
| } |
There was a problem hiding this comment.
This function contains several println! statements (on lines 216, 219, and 224) that appear to be for debugging. These should be removed from production code to avoid printing unnecessary output to the console when the tool is used.
| let expr = syn::parse_str::<syn::Expr>(&combined_str) | ||
| .unwrap_or_else(|_| parse_quote!(true)); |
There was a problem hiding this comment.
The use of unwrap_or_else(|_| parse_quote!(true)) silently ignores errors when parsing preconditions from @requires annotations. If a precondition is malformed, it will default to true, which could lead to unsound assumptions during verification (i.e., a contract violation check might be skipped). It would be safer to panic with a descriptive error if parsing fails, to alert the user to the malformed annotation.
| let expr = syn::parse_str::<syn::Expr>(&combined_str) | |
| .unwrap_or_else(|_| parse_quote!(true)); | |
| let expr = syn::parse_str::<syn::Expr>(&combined_str) | |
| .expect("Malformed @requires precondition"); |
| fn visit_expr_mut(&mut self, node: &mut Expr) { | ||
| if let Expr::Unsafe(expr_unsafe) = node { | ||
| // Transform `unsafe { ... }` into `{ ... }` | ||
| // We preserve attributes and the inner block | ||
| let new_expr = Expr::Block(ExprBlock { | ||
| attrs: expr_unsafe.attrs.clone(), | ||
| label: None, | ||
| block: expr_unsafe.block.clone(), | ||
| }); | ||
| *node = new_expr; | ||
|
|
||
| // Recurse into the new block (in case there are nested unsafe blocks) | ||
| self.visit_expr_mut(node); | ||
| } else { | ||
| syn::visit_mut::visit_expr_mut(self, node); | ||
| } | ||
| } |
There was a problem hiding this comment.
The implementation of visit_expr_mut is a bit confusing due to the direct recursive call self.visit_expr_mut(node). While correct, it relies on a subtle interaction with the else branch to traverse into the newly created block. A post-order traversal approach would be more conventional and easier to understand. By first visiting child nodes and then transforming the current node, the logic becomes more straightforward and maintainable.
fn visit_expr_mut(&mut self, node: &mut Expr) {
// First, traverse deeper into the AST to handle nested expressions.
syn::visit_mut::visit_expr_mut(self, node);
// After children have been processed, transform the current node if it's `unsafe`.
if let Expr::Unsafe(expr_unsafe) = node {
// Transform `unsafe { ... }` into `{ ... }`
*node = Expr::Block(ExprBlock {
attrs: expr_unsafe.attrs.clone(),
label: None,
block: expr_unsafe.block.clone(),
});
}
}| println!("DEBUG: Trimmed line: '{}'", trimmed); | ||
| // Check found marker e.g. "@ lean model" | ||
| if trimmed.starts_with('@') { | ||
| if trimmed.contains("lean model") { |
There was a problem hiding this comment.
The check trimmed.contains("lean model") is too broad and could lead to false positives. For example, it would match a comment like ///@ this is not a lean model. It would be more robust to use strip_prefix to ensure the annotation is at the beginning of the string, which would also make it consistent with how @ lean spec is handled in parser.rs.
if trimmed.strip_prefix("@ lean model").is_some() {
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G443fc7f8c3623131b48be56a7a16935a9fe8f234 #2972 +/- ##
==========================================================================
Coverage 92.02% 92.02%
==========================================================================
Files 19 19
Lines 6029 6029
==========================================================================
Hits 5548 5548
Misses 481 481 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
joshlf
force-pushed
the
Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31
branch
from
6d9291e to
8f7e2d6
Compare
gherrit-pr-id: Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31
joshlf
force-pushed
the
Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31
branch
from
8f7e2d6 to
9a2da12
Compare
joshlf
force-pushed
the
G443fc7f8c3623131b48be56a7a16935a9fe8f234
branch
from
5ac313d to
a24d41d
Compare
2 participants
Latest Update: v4 — Compare vs v3
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31 && git checkout -b pr-Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31 FETCH_HEADCheckout
git fetch origin refs/heads/Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.