Java fixes #459
Merged
Java fixes #459
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 12 commits
December 12, 2019 13:28
There was a problem if a Dafny module happened to be called Random. Now, there's still a problem if a Dafny module is called BigInteger, Array, ArrayList, Arrays, or Function, but at least the issue is limited to those.
Now the user is free to have modules with such illustrious names as Array, Arrays, ArrayList, Function, or BigInteger.
In Java, ill-typed code was generated for the special case of |s| as int8 (or any native type) when s is a sequence, map, set, or multiset. Go had a wrong type in the runtime library, leading to a similar issue. Tests included.
The previous implementation of generics for Java assumed that each type parameter corresponds to a field, whose name is the same but lowercase, and that either all type parameters need to be reified as type descriptors or none do.
Test included.
I was getting weird behavior (possibly a Mono bug) with characters at the end being copied twice. Fortunately, this is the right way anyway.
If an extern class includes Dafny code, the generated code is now put into an abstract base class, whose name is prefixed with `_ExternBase_`, so that the user-provided class can extend it.
FIXME: Currently there is nothing to detect whether a class has *only* Dafny
methods. Which means that any pure-Dafny module with an `{:extern}`
declaration (even just to give it an external name) requires the user to
provide a `__default` class (extending `_ExternBase___default`).
FIXME: The included tests break Go and JavaScript, which don't correctly
implement extern constructors.
Includes test.
It's useful to declare a module as {:extern} even if it has no extern members,
just to give it an externally-visible name. Unfortunately, this causes its
default class to be considered (by Compiler.Compile()) to be extern as well,
and for Java this means forcing the user to provide an implementation of the
__default class that does nothing but extend _ExternBase___default. This patch
makes sure that at least one member carries a zero- or one-argument {:extern}
before considering a class to be extern.
Why not a two-argument {:extern}?
module {:extern "Library"} Library {
static method Method() { ... }
static method {:extern "Library.Class", "ExternMethod"} ExternMethod()
}
Here the user has specified that the method Method lives not in
Library.__default but in Library.Class (presumably because __default looks
weird). Since Library.__default has no methods that need to be filled in
by the user, it would be silly to force them to write
package Library
public class __default extends _ExternBase___default {
}
Note that there is still a corner case:
module {:extern "Library"} Library {
class {:extern "Class"} Class {
static method Method() { ... }
static method {:extern "Library.Class.InnerClass", "ExternMethod"} ExternMethod()
}
}
Now we *do* need to generate _ExternBase_Class so that the user can supply
Library.Class so that they can define Library.Class.InnerClass. It's not clear
this will ever come up, though (whereas the first example comes from the wild),
and in any case the workaround is just to define a dummy extern method.
Extern constructors are currently broken on Go and JavaScript, so I'm moving that functionality from the tests in Extern.dfy and moving it to the new ExternCtors.dfy, which only has RUN lines for C# and Java. I've included the extern code that *should* make the tests work (but currently doesn't).
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
RustanLeino
requested changes
Dec 13, 2019
Source/Dafny/Compiler-java.cs
Outdated
Comment on lines
621
to
660
| else if (cl is TupleTypeDecl tupleDecl) | ||
| { |
There was a problem hiding this comment.
Move L622 curly brace to end of L621.
Source/Dafny/Compiler-java.cs
Outdated
Comment on lines
624
to
663
| } | ||
| else if (cl.Module.CompileName == ModuleName || cl.Module.IsDefaultModule) { |
There was a problem hiding this comment.
Move L625 to end of 624.
lukemaurer
force-pushed
the
java-fixes
branch
from
b505d02 to
0ee2500
Compare
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
robin-aws
reviewed
Dec 19, 2019
Effectively reverts 42466b5, though I kept the change to the test case (and adjusted the JavaScript extern for the test so that it still works). See issue dafny-lang#469 for a better solution.
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a pile of bug fixes coming from getting a sizable real-world Dafny project to compile to Java. (Also there are places where I discovered a bug in another backend when I added a test, and fixing the bug was easier than adapting the test.)