-
Notifications
You must be signed in to change notification settings - Fork 3.7k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Prover] add support of abort in spec function #14939
Conversation
⏱️ 6h 27m total CI duration on this PR
|
This stack of pull requests is managed by Graphite. Learn more about stacking. Join @rahxephon89 and the rest of your teammates on |
3062b2f
to
2c9bf73
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #14939 +/- ##
=======================================
Coverage 60.1% 60.1%
=======================================
Files 856 856
Lines 211035 211086 +51
=======================================
+ Hits 126896 126938 +42
- Misses 84139 84148 +9 ☔ View full report in Codecov by Sentry. |
c06c408
to
6142f77
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice solution
{%- set S = "'" ~ instance.suffix ~ "'" -%} | ||
{%- set T = instance.name -%} | ||
|
||
function $Uninterpreted_value_of_{{S}}(): {{T}}; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The naming is a bit of off, because "uninterpreted value" does not make a lot of sense in contrast to "uninterpreted function". Perhaps call this "$Arbitrary_value_of"
6142f77
to
3d9cf03
Compare
| ExpData::Mutate(id, ..) | ||
| ExpData::SpecBlock(id, ..) | ||
| ExpData::LoopCont(id, ..) => { | ||
self.env.error( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add a test that illustrates this error?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
@@ -184,6 +184,27 @@ pub fn add_prelude( | |||
sh_instances = vec![]; | |||
bv_instances = vec![]; | |||
} | |||
|
|||
let mut all_types = mono_info |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this going to be very big? Is mono_info every type in the program?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For aptos-framework, there are about 500 uninterpreted functions generated while the generated boogie code is about 300k line. So IMHO as long as the program itself is reasonable, the number of types in the program is not a big concern.
@@ -991,15 +996,31 @@ impl<'env> SpecTranslator<'env> { | |||
self.translate_call(node_id, oper, &[args[args.len() - 1].clone()]); | |||
emit!(self.writer, &")".repeat(count)); | |||
}, | |||
Operation::Abort => { | |||
let exp_bv_flag = global_state.get_node_num_oper(node_id) == Bitwise; | |||
emit!( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we show this error, too?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think you mean the error below. All operations should already be handled in early stages so it is hard to add a test case to generate this error.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I understand that it's fine to use such Move functions (which potentially abort) in ensures
specs because they are evaluated under the condition that the function does not abort.
However, I haven't fully grasped the use of such functions in aborts_if
specs yet. Nevertheless, this shouldn't be an issue as long as we clearly explain this behavior to users in the documentation.
3d9cf03
to
f74a2d2
Compare
* [single-node-performance] Add runner information in the output * adding skip move e2e * recalibration
f74a2d2
to
eafc03f
Compare
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
✅ Forge suite
|
✅ Forge suite
|
✅ Forge suite
|
Description
Currently, when rewriting a Move expression into a spec expression, abort will be rewritten into empty
()
expression. Later when generating boogie, the errorTuple not yet supported
will be raised. This PR introduces uninterpreted functions to the Boogie native for each type generated in the program andabort
operation is translated into calling the corresponding function based on its type.close #14793
How Has This Been Tested?
Key Areas to Review
Type of Change
Which Components or Systems Does This Change Impact?
Checklist