-
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: Fix naming of formals in Translator #2266
Conversation
Thanks @Dargones! This LGTM in general, although I also don't fully understand the In the meantime, can you add a new test case to expose the issue somehow? I'd like to get to the bottom of why this only shows up when you manually verify the Boogie code separately - it might point to the Dafny pipeline failing to pass an option to catch this error more strictly. |
Thank you, @robin-aws. I have added a test case and it succeeds when I run it with This test also adds additional overhead of having to build Boogie but I think it could be useful for more extensive testing of the Dafny -> Boogie file -> Verify with Boogie pipeline. More about the bug: the reason the verification succeeds when running Dafny alone is because all parameters have names, one of these names happens to be an empty string. However, when this empty string name is printed to file along with other parameter banes, which are not empty, Boogie cannot parse it back. If, on the other hand, none of the parameters have names, then Boogie can successfully parse the function definition. More specifically, the bug seems to be triggered by adding a reads clause for a function type parameter, hence the test case: function Test(f: (int ~> bool)): (b:bool) reads f.reads { true } As for the |
Great, thanks for the explanation. I fully agree being able to automatically test the Dafny -> Boogie file -> Verify with Boogie workflow is extremely useful, given many contributors will use that to debug issues with the translator (I know I have :). Rather than building Boogie from source we could just install the corresponding release of the
I think you accidentally a few words :) |
I believe I have been able to fix the testing process (pending integration tests rerun, which was successful on my fork). @robin-aws - let me know if there is anything else I could do to merge this in! |
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 love the fix/test ratio on this one. ;)
Thank you for approving, @atomb! I have synced the PR with master so it should be good to go |
This reverts commit 889e051.
This reverts commit 889e051. The implementation of configuring Z3 for `%boogie` wasn't working in the nightly build. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
This is a new version of #2266 with changes that should make it pass all tests, both on the PR stage and during the nightly build. The reason #2266 failed during nightly build was that path to Z3 used to be different for different operation systems and modes of testing. This PR adds symbolic links that ensure there is a path to Z3 applicable to all cases. More specifically, right now Z3 resides at `dafny/Binaries/z3/bin/z3` if testing on Ubuntu outside the nightly build (see [here](https://github.com/dafny-lang/dafny/blob/0d78ab50330d64dd769b674cd0125a9ffc994b20/.github/workflows/integration-tests-reusable.yml#L114-L120)), at `unzippedRelease/dafny/z3/bin/z3` if testing on Ubuntu/MacOS during the nightly build (see [here](https://github.com/dafny-lang/dafny/blob/0d78ab50330d64dd769b674cd0125a9ffc994b20/.github/workflows/integration-tests-reusable.yml#L111-L113)) and at `unzippedRelease/dafny/z3/bin/z3.exe` when testing on Windows ([here](https://github.com/dafny-lang/dafny/blob/0d78ab50330d64dd769b674cd0125a9ffc994b20/.github/workflows/integration-tests-reusable.yml#L107-L110)). This PR modifies the [workflow file](https://github.com/dafny-lang/dafny/blob/master/.github/workflows/integration-tests-reusable.yml) to have symbolic links to ensure that `unzippedRelease\dafny\z3\bin\z3` always points to Z3, whatever the operations system and testing strategy. Aside from the Z3 path this PR is identical to #2266 and fixes #2263. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Fixes #2263, which is due to inconsistent naming of formal parameters in automatically generated function handles.
Explanation: The syntax of
MkTyParamFormals
was changed with commit 81cf582 fromto
But the call to the method on this line was left unchanged, so the method is now being called with
named
field set to the defaulttrue
. Elsewhere the formal parameters of the a function handle don't get a name. The result is a mix-match of named and unnamed formals that causes the bug reported in the linked issue.I don't completely understand the meaning of
includeWhereClause
in this context but I thinkfalse
is the correct value for this call?By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.