fix: Missing method-reads check in array initializer #6414
Conversation
recover original read-frame-subset.dfy
RustanLeino
left a comment
RustanLeino
left a comment
There was a problem hiding this comment.
Thank you for this prompt contribution! I started adding some comments in the code, but then I realized three things:
- We should check not just lambda expressions. For example, if a lambda expression is assigned to a local variable
initand then thatinitis used as the new-array initializer, then there should still be check. - This check cannot be done syntactically. For example, such a local variable
initdoes not itself carry areadsclause, but the value of the expressioninitdoes. So, instead of doing the check is the resolver, it should be done in the verifier. More about this below. - In looking into this, I found that there are other expressions that are part of new-array allocation that are missing reads checks. I'll add the additional cases I found to the bug report #6410.
The place where the verifier processes new-array allocations is in the AllocateArray case of method TrAssignmentRhs in BoogieGenerator.TrAssignment.cs. For the array initializer, the code ends up calling CheckElementInit. That method has some code
if (!forArray && options.DoReadsChecks) {
...I think this code adds the verifier checks for the initializer of a seq constructor. Something similar should be done for the new-array statement's initializer expression.
| if | ||
| case true => |
There was a problem hiding this comment.
These two lines don't add anything for the test. I suggest you remove them.
| if | ||
| case true => |
| { | ||
| if | ||
| case true => | ||
| var arr := new int[10](_ reads c => c.data); // error: insufficient reads |
There was a problem hiding this comment.
This comment doesn't apply here. Please remove it.
| if (Options.Get(MethodOrConstructor.ReadsClausesOnMethods)) { | ||
| var enclosingMethod = resolutionContext.CodeContext as MethodOrConstructor; | ||
| if (enclosingMethod != null) { | ||
| if (allocateArray.ElementInit is LambdaExpr lambda) { |
There was a problem hiding this comment.
The restriction should also be checked for other expressions, not just lambda expressions, because any (here, function-valued) expression might have read effects.
|
Hey! Thanks for the feedback. I changed it so that it's doing the same thing as the sequence initializer. One thing I noticed was that when a I wasn't sure what the best way forward was from here-- a short term solution would be creating some arbitrary lambda behind the scenes that calls and returns that member function and replace the initialization function with that one, but this seems too 'hacky'. Are there any better ways to approach this? |
2 participants
What was changed?
Method reads are checked in array initializers. Resolves #6410.
How has this been tested?
Test files
read-array-alloation-invalid-readandread-array-allocation-valid-readwere added.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.