-
Notifications
You must be signed in to change notification settings - Fork 261
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
Fix: Emit constraints for compiled quantifier expressions, and nested subset types #1997
Conversation
# Conflicts: # Source/Dafny/Compilers/Compiler.cs # Source/Dafny/Resolver.cs # Test/libraries
Fixing tests that depended on it.
…g/dafny into fix-1604-only-compiler
If we're compiling a comprehension, then we're never in a ghost context right? Shouldn't |
Right, and after your remark, I saw that this bounded pool ought to be better computed for integer pools as well, else the subset type was taken instead. I refactored the code so that now ElementType is a method of a pool to ensure it's implemented by every pool |
/// [[bodyWriter]] | ||
/// </summary> | ||
/// where | ||
/// * "[[bodyWriter]]" is the block writer returned |
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.
Returned? The return type is void
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.
* "[[bodyWriter]]" is where the writer wr's position will be next
/// [[bodyWriter]] | ||
/// </summary> | ||
/// where | ||
/// * "[[bodyWriter]]" is the block writer returned | ||
/// Option: |
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.
What does option mean? Neither of the two following parameters are optional right?
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.
/// <summary>
/// Emit an (already verified) downcast assignment like:
///
/// var boundVarName:boundVarType := tmpVarName as boundVarType;
/// [[bodyWriter]]
///
/// where
/// * "[[bodyWriter]]" is where the writer wr's position will be next
/// </summary>
/// <param name="boundVarName">Name of the variable after casting</param>
/// <param name="boundVarType">Expected variable type</param>
/// <param name="tmpVarName">The collection's variable name</param>
/// <param name="collectionElementType">type this variable is casted from, in case it is useful</param>
/// <param name="introduceBoundVar">Whether or not to declare the variable, in languages requiring declarations</param>
/// <param name="tok">A position in the AST</param>
/// <param name="wr">The concrete syntax tree writer</param>
```
…pe of an IntBoundedPool" This reverts commit 8abdf29.
…into fix-1604-only-compiler
…into fix-1604-only-compiler
…g/dafny into fix-1604-only-compiler
Fixes #1604
Previously, the test
https://github.com/dafny-lang/dafny/pull/1997/files#diff-3650380410d4f90c335dd7eaf17caf895d7630fe4720fdc0a58889666ac58fdf
would verify, compile, but none of the generated code of JavaScript, C#, Go or Java would work. Go, C# and Java would crash, and JavaScript would fail silently
Now everything works correctly.
I also fixed another soundness issue never reported. The compiler wasn't emitting nested constraints for nested subset types, so this file was crashing at run-time.
https://github.com/dafny-lang/dafny/pull/1997/files#diff-2a4f58bf9ce20437d573ece58c942499118c4b9745c7784373725b9302b78caf
Now it works correctly.
Changes in the backend-compiler
CreateForeachLoop
that was responsible for both iterating over a collection and ensuring subtype constraint. First, the compilation of forall expressions was relying on a library method and a lambda, so these subtype constraints were not checked, which was the root cause of the soundness issue Reference types in comprehension soundness issue #1604. But second and this is most important, it was putting the specification of doing these checks to the overridden methodCreateForeachLoop
, which makes it impossible to reuse somewhere else (such as these lambda), to add language-independent checks (such as the ones brought by this PR for subset types whose constraint is compilable) and of course not at all friendly if we want to make an intermediate language for compilation.CreateGuardedForeachLoop
that emits the loops and the constraints. It also integratesMaybeInjectSubtypeConstraint
defined here which optionally test the type usingEmitSubtypeCondition
(see below for the definition). It also injectsMaybeInjectSubsetConstraint
defined here. This method that inlines compilable constraints now takes correctly care of nested subset types as tested here.CreateForeachLoop
into three methods that every compiler needs to implement.CreateForeachLoop
that only creates the loop structure. Refactored for C#, C++, Go, Java, JavaScript, Python (to be implemented of course).EmitSubtypeCondition
that check if a variable satisfies the subtype constraint needed by the loop. That way, we can just reuse every compiler's if rather than hard-coding it as it was done previously. Refactored in C#, C++, Go, Java and JavaScript.EmitDowncastVariableAssignment
, that is now executed after the subtype constraint check has been validated, both for forall and exists expressions as well as for set and map comprehensions and assign-such-that statements. Refactored in C#, C++, Go, Java, and JavaScript.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.