Add support to --function to rmc script (#169)
#523
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
4 tasks
tedinski
approved these changes
Sep 27, 2021
Contributor
tedinski
left a comment
tedinski
left a comment
There was a problem hiding this comment.
I was just writing docs about --function.
I'll add the note about #[no_mangle] to what I wrote.
zhassan-aws
reviewed
Sep 27, 2021
src/tools/dashboard/src/util.rs
Outdated
Contributor
Author
There was a problem hiding this comment.
Good catch... I wonder when this gets run. I should check with @adpaco-aws to make sure we have test coverage in our regression.
Contributor
There was a problem hiding this comment.
We have the dashboard set to only run after merges. I think there are concerns right now about prolonging CI times.
Contributor
Author
There was a problem hiding this comment.
Can we create a parallel workflow to do those things?
Contributor
Author
There was a problem hiding this comment.
Anyway, I fixed it and I ran the dashboard script locally. The output is a bit hard to parse, but it seemed to work.
This changes the compilation to use crate type lib instead of binary when we are running rmc on a single .rs file. This allow us to use any public function as a verification target. We have also changed the tests to use pub main so it is exported and it can be used as the entry point of the proof. Fix cargo-rmc and the current testcase to support library build.
zhassan-aws
approved these changes
Sep 28, 2021
This was referenced Nov 19, 2021
tedinski
pushed a commit
to tedinski/rmc
that referenced
this pull request
Apr 26, 2022
…-checking#523) This changes the compilation to use crate type lib instead of binary when we are running rmc on a single .rs file. This allow us to use any public function as a verification target. We have also changed the tests to use pub main so it is exported and it can be used as the entry point of the proof. Fix cargo-rmc and the current testcase to support library build.
tedinski
pushed a commit
that referenced
this pull request
Apr 27, 2022
This changes the compilation to use crate type lib instead of binary when we are running rmc on a single .rs file. This allow us to use any public function as a verification target. We have also changed the tests to use pub main so it is exported and it can be used as the entry point of the proof. Fix cargo-rmc and the current testcase to support library build.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This changes the compilation to use crate type lib instead of binary when
we are running rmc on a single .rs file. This allow us to use
any public function as a verification target.
We have also changed the tests to use pub main so it is exported and it
can be used as the entry point of the proof.
Fix cargo-rmc and the current testcase to support library build.
Description of changes:
1- RMC users will need to ensure their main function is public in order to use them as verification harness. Note that this not affect proof harness with attribute
#[no_mangle]since this attribute actually exports the function.2- Users can now invoke rmc with the
--functionattribute. They can select any public function as their starting point. Note that the function still has to have the#[no_mangle]attribute.Resolved issues:
Resolves #169
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.