feat: Implement frame-related asserted exprs and TraitDecreases #5542
Conversation
| /// Builds an expression that represents whether (the relevant subset of) the given `supersetFrames` | ||
| /// permit read/modification access to all objects, arrays, and/or sets of objects/arrays in the `subsetFrames`. | ||
| /// </summary> | ||
| public static Expression MakeDafnyMultiFrameCheck(List<FrameExpression> supersetFrames, List<FrameExpression> subsetFrames) { |
There was a problem hiding this comment.
The detail required in methods like these make me very much want to share this code with the Boogie translation eventually (i.e., have the Boogie generator work by constructing this expression and then translating it). But that's a task for another day.
| @@ -0,0 +1,8 @@ | |||
| modify-frame-subset.dfy(15,2): Error: modify statement might violate context's modifies clause | |||
| Asserted expression: (s[0] == s[3] || s[0] in {s[4]} || s[0] in {s[5]}) && (forall obj: C | obj in {s[1]} :: obj == s[3] || obj in {s[4]}) && forall obj: C | obj in {s[2]} :: obj == s[3] || obj in {s[5]} | |||
There was a problem hiding this comment.
I think things like this are going to be super useful! With more complicated code, constructing the equivalent of this expression in your head can really be a pain.
| @@ -786,10 +822,16 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA | |||
| } | |||
| if (wfOptions.DoReadsChecks) { | |||
| // check that the callee reads only what the caller is already allowed to read | |||
| var s = new Substituter(null, new Dictionary<IVariable, Expression>(), e.GetTypeArgumentSubstitutions()); | |||
|
|
|||
| // substitute actual args for parameter is frames for the description expression... | |||
There was a problem hiding this comment.
Not critical, but this comment isn't super clear to me. Maybe it could be reworded?
There was a problem hiding this comment.
Oops, there was a typo (and generally unclear wording). I've fixed this in the latest commit.
Description
This PR implements
GetAssertedExprfor the following five proof obligation description types:How has this been tested?
This PR adds integration tests for each of the implemented asserted expressions.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.