[hermes] Invoke Aeneas #3048
[hermes] Invoke Aeneas #3048
Conversation
gherrit-pr-id: G4uato76xa2ezceilkolqtzoxhlxmxbg2
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 enhances the Hermes tool's capabilities by integrating the Aeneas formal verification tool. This integration establishes a complete pipeline where Rust code is first processed by Charon to produce Low-Level Bytecode (LLBC), which is then automatically translated into Lean code by Aeneas. This streamlines the process of formally verifying Rust programs within the Hermes ecosystem, providing a more robust and organized output structure for generated artifacts. 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 the invocation of Aeneas after Charon runs, which is a key step in the verification toolchain. The changes include a new aeneas.rs module, updates to directory structures for build artifacts, and significant enhancements to the integration testing framework to support aeneas. The code is well-structured and the refactoring to create an artifact_slug is a nice improvement.
However, I've identified a couple of issues in the test runner (integration.rs) that will prevent the new tests for aeneas from working as intended. One issue is with how test expectations are loaded, and another is with parsing the arguments logged by the new aeneas shim. I've left a specific comment on the latter. Addressing these will be important to ensure the new functionality is properly tested.
| r#"#!/bin/sh | ||
| echo "AENEAS INVOKED" >> "{0}" | ||
| for arg in "$@"; do | ||
| echo "AENEAS_ARG:$arg" >> "{0}" |
There was a problem hiding this comment.
The aeneas shim logs arguments with the prefix AENEAS_ARG:. However, the existing parse_command_log function in this file only parses arguments with the ARG: prefix. This means that any command expectations for aeneas will not be checked correctly.
To fix this, you should either update parse_command_log to handle AENEAS_ARG: (and potentially other prefixes for future shims), or change the prefix here to ARG:. If you change it to ARG:, be aware that charon and aeneas invocations will be logged to the same file and might be hard to distinguish if the order of execution is not guaranteed.
| echo "AENEAS_ARG:$arg" >> "{0}" | |
| echo "ARG:$arg" >> "{0}" |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gmkf32xtwlqyoky63oeo4l5id2hqup3os #3048 +/- ##
==================================================================
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:
|
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/G4uato76xa2ezceilkolqtzoxhlxmxbg2 && git checkout -b pr-G4uato76xa2ezceilkolqtzoxhlxmxbg2 FETCH_HEADCheckout
git fetch origin refs/heads/G4uato76xa2ezceilkolqtzoxhlxmxbg2 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G4uato76xa2ezceilkolqtzoxhlxmxbg2 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.