Monomorphic Field and collection types #4597
Conversation
Doesn't cause completeness issues.
The one remaining polymorphic one loses its trigger if it doesn't quantify over anything.
This removes a trigger, but probably one that’s no longer needed.
| @@ -188,26 +190,26 @@ axiom (forall bx : Box :: | |||
| // generated programmatically. Except, Bv0 is given here. | |||
| axiom (forall bx : Box :: | |||
| { $IsBox(bx, TBitvector(0)) } | |||
| ( $IsBox(bx, TBitvector(0)) ==> $Box($Unbox(bx) : Bv0) == bx && $Is($Unbox(bx) : Set Box, TBitvector(0)))); | |||
| ( $IsBox(bx, TBitvector(0)) ==> $Box($Unbox(bx) : Bv0) == bx && $Is($Unbox(bx) : Bv0, TBitvector(0)))); | |||
There was a problem hiding this comment.
This rewriting is surprising, I would have expected this instead:
| ( $IsBox(bx, TBitvector(0)) ==> $Box($Unbox(bx) : Bv0) == bx && $Is($Unbox(bx) : Bv0, TBitvector(0)))); | |
| ( $IsBox(bx, TBitvector(0)) ==> $Box($Unbox(bx) : Bv0) == bx && $Is($Unbox(bx) : Set, TBitvector(0)))); |
There was a problem hiding this comment.
Huh. That is weird. I'll give it a closer look.
There was a problem hiding this comment.
I thought Set Box looked like a copy-paste error, but maybe I am missing something...
There was a problem hiding this comment.
You're probably right, but this mean that this particular type cast was probably untested then until now.
There was a problem hiding this comment.
Yes, maybe it makes more sense to have that as another PR with proper tests, not to have this as a hidden change here.
There was a problem hiding this comment.
Not having a test for now is ok since it was not tested anyway, but if you had a test, indeed, you could move it to another PR. For now, let's piggy back on this PR to perform this bug fix if it's correct.
| /// </summary> | ||
| private static string GetTrueTypeName(Model.Element element) { | ||
| string name = null; |
There was a problem hiding this comment.
What's happening with the test (name == null) || name.Contains("$") || name.StartsWith("#") || name.Contains("@"? Why is it no longer necessary?
There was a problem hiding this comment.
Good question. I'll have to look at it more carefully. I'm not sure off the top of my head.
There was a problem hiding this comment.
I think it is no longer possible for name to have these special characters after monomorphization. I remember asking @Dargones to review the changes in this part of the PR as they affect test generation, and if I recall correctly he mentioned that he tested them on his branch and were ok.
| fSeqTake = new ModelFuncWrapper(this, "Seq#Take", 2, tyArgMultiplier); | ||
| fSeqIndex = new ModelFuncWrapper(this, "Seq#Index", 2, tyArgMultiplier); | ||
| fSeqUpdate = new ModelFuncWrapper(this, "Seq#Update", 3, tyArgMultiplier); | ||
| fSeqLength = new ModelFuncWrapper(this, "Seq#Length", 1, 0); |
There was a problem hiding this comment.
What is the tyArgMultipler?
There was a problem hiding this comment.
It specifies how many arguments exist in the SMT-Lib function definitions for each type argument. At the moment, it's either 0 or 1, depending on the value of TypeEncoding. This seemed easier than having conditionals everywhere.
| @@ -1537,7 +1537,7 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA | |||
| // assume (forall i0,i1,i2,... :: { nw[i0,i1,i2,...] } | |||
| // 0 <= i0 < ... && ... ==> nw[i0,i1,i2,...] == init.requires(i0,i1,i2,...)); | |||
| var ai = ReadHeap(tok, etran.HeapExpr, nw, GetArrayIndexFieldName(tok, indices)); | |||
| var ai_prime = UnboxIfBoxed(ai, elementType); | |||
| var ai_prime = TrType(elementType) == predef.BoxType ? ai : ApplyUnbox(tok, ai, TrType(elementType)); | |||
There was a problem hiding this comment.
I liked having only one function here, even if it was used only once. Would you consider re-adding it?
| @@ -16,7 +16,6 @@ ReadsOnMethods.dfy(183,25): Error: insufficient reads clause to read field | |||
| ReadsOnMethods.dfy(245,9): Error: insufficient reads clause to read field | |||
| ReadsOnMethods.dfy(304,33): Error: insufficient reads clause to read field | |||
| ReadsOnMethods.dfy(308,22): Error: insufficient reads clause to invoke function | |||
| ReadsOnMethods.dfy(313,13): Error: call might violate context's modifies clause | |||
There was a problem hiding this comment.
I wouldn't have expected that this error would go away. Can you explain a bit?
There was a problem hiding this comment.
Ultimately, the issue is that Boogie isn't guaranteed to report all errors in a given procedure. If it determines that some code is dead code (because a previous assertion was equivalent, in the current context, to assert false, for example), it may not even generate verification conditions for that part of the code.
There was a problem hiding this comment.
I checked with @robin-aws, who wrote this test, and this error wasn't an essential one for the test to cover. There's another test, for the concurrent attribute, that I refactored so that the two different errors occurred in different definitions and were therefore guaranteed to be reported.
Removes the type argument from
Field, and from all collection types. All heap and collection elements are now always of typeBox.This has the effect of very slightly increasing brittleness on some particularly brittle examples, though it has minimal effect on most code. The benefits of the simplification (and the opportunities it opens for future optimization) seem worth the tradeoff, however.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.