New annotation to give an externally-visible name to a generated Dafny class #469
Labels
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
priority: not yet
Will reconsider working on this when we're looking for work
Comments
lukemaurer
pushed a commit
to lukemaurer/dafny
that referenced
this issue
Dec 30, 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.
RustanLeino
pushed a commit
that referenced
this issue
Jan 2, 2020
* Java: Don't use wildcard imports
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.
* Java: Fully qualify names from JDK; import nothing by default
Now the user is free to have modules with such illustrious names as Array,
Arrays, ArrayList, Function, or BigInteger.
* Java: Include type parameters when declaring tuple as local variable
* Java, Go: Fixes for casts of cardinality operator
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.
* Java: Support arbitrary names for fields of parameter type
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.
* Java: Fix implementation of newtype methods
Test included.
* Go: Use File.Copy to copy externs into place
I was getting weird behavior (possibly a Mono bug) with characters at the end
being copied twice. Fortunately, this is the right way anyway.
* Java: Allow extern classes to mix Dafny and extern code
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.
* Java: Support two-argument extern declarations
Includes test.
* Only consider a class an extern class if it has an extern member
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.
* Split out tests for extern constructors
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).
* JavaSript: Invoke superclass constructor from constructor
* Formatting
* Remove special case for extern classes without extern methods
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 #469 for a better solution.
|
I also think it would be helpful to have two distinct annotations:
Specifying a name would be optional in the first one (and default to the Dafny name), but mandatory in the second one. And if these annotations are redesigned, we should keep in mind that we might need to provide different extern names for different target languages. When I was working on Dafny code which is compiled both to Java and C# last summer, we used a quick and dirty |
|
The more I work on a potential solution to #461 and #463, the more I think that it makes more sense to keep the meaning of |
This was referenced Apr 28, 2020
This was referenced May 14, 2020
robin-aws
added
the
area: ffi
robin-aws
added
the
kind: enhancement
|
The situation is a bit worse than this: the meaning for |
MikaelMayer
added
the
priority: not yet
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Currently, an
{:extern}declaration on a class has two effects: Allowing that class to have{:extern}methods and giving that class a predictable name that external code, written in the target language, can refer to. When generating a library, it makes sense to give an{:extern}declaration even when there are no extern methods, just to give the generated class the right name.Unfortunately, this usage has surprising consequences in the Java and JavaScript backends. A class can have both Dafny methods and extern methods, so somehow the backend has to combine user code and generated code in the same class. The C# backend uses partial classes to do this, whereas Java and JavaScript use inheritance. If there happen to be no methods for the user to implement, the C# backend doesn't need the user to supply any code at all, since C# allows a class to be declared partial even if it's complete. Thus someone can just add
{:extern}to a Dafny class and not have to write any C# code. But the Java and JavaScript backends will fail without a user-supplied class because they generate code that expects both a base class and an derived class. This means that the user must always supply a class, even if it's a silly stub class that does nothing but extend (in the Java case) or be extended by (JavaScript) the generated class. SeeTest/comp/Extern3.js(theAllDafnyclass) andTest/comp/AllDafny.java. (The Go backend would probably have the same problem, but it currently doesn't support mixing Dafny methods and extern methods at all.)Rather than add special logic for extern classes without extern methods, it would make more sense to separate the two effects of the
{:extern}declaration by adding an annotation that just means “give this class the following name, visible to external code.” @robin-aws suggests that this should actually be what{:extern}means, and that{:native}should be the annotation on a method whose implementation is in native code.The text was updated successfully, but these errors were encountered: