Java compiler produces constructors that won't play well with native Java code

[davidcok]

The Java compiler produces wrong output regarding constructors for a current test (comp/Class.dfy). In particular the code below produces a zero-argument constructor that initializes a, b, c, but then produces a method named __ctor that is the translation of the given Dafny constructor

class MyClass {
  var a: int
  const b: int
  const c := 17
  static const d: int
  static const e := 18
  constructor (x: int) {
    a := 100 + x;
    b := 200 + x;
  }

function method F(): int { 8 }
  static function method G(): int { 9 }
  method M() returns (r: int) { r := 69; }
  static method N() returns (r: int) { return 70; }
}

method Main() {
  var m := new MyClass.MyClass(10);
  print m.a, " ", m.b, "\n";
}

[RustanLeino]

Yes? That is one possible way to implement object construction, right? Or, is the __ctor not called when an object is allocated?

[robin-aws]

I submit that this indicates a disagreement about the compiler requirements: currently the code it outputs just has to be functionally correct, but some folks may expect that it should output "logical" or "idiomatic" code, such as directly mapping a Dafny constructor to a Java constructor.

I think this needs to written down explicitly somewhere in the source and/or the documentation.

[davidcok]

Fair enough point. Some additional requirements coming from the [Amazon internal] project: - The output Java code must be reviewable by Java engineers who do not care about Dafny, to assist in the adoption of Dafny-verified, auto-generated Java implementations - The output Java code must be efficient - The output Java code should be provable with Java verification tools. The first one is helped significantly if the compiler produces typical, “idiomatic”, readable code The second is as well, though sometimes non-typical code is acceptable, if it directly contributes to better performance. As for the third, functionally correct code “ought” to be provable, but Java-based tools will likely be more successful if usual Java idioms are used. - A fourth potential requirement not relevant to us at the moment is if the Dafny-produced Java is meant to be used as a library — then the library’s API should be recognizable Java - David

…

On Jan 30, 2020, at 4:35 PM, Robin Salkeld ***@***.***> wrote: I submit that this indicates a disagreement about the compiler requirements: currently the code it outputs just has to be functionally correct, but some folks may expect that it should output "logical" or "idiomatic" code, such as directly mapping a Dafny constructor to a Java constructor. I think this needs to written down explicitly somewhere in the source and/or the documentation. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#502?email_source=notifications&email_token=ABITDQB62VA4ZGHOWYW2T6TRANBZ3A5CNFSM4KGYYFP2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKMURWA#issuecomment-580471000>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQB7CDH47PEMEA3GPKLRANBZ3ANCNFSM4KGYYFPQ>.

[richardlford]

I'm curious which Java verification tools you are referring to. Does the Java output from Dafny have JML markup so that the Java can be proven? Rich

…

On Fri, Jan 31, 2020 at 11:27 AM David Cok ***@***.***> wrote: Fair enough point. Some additional requirements coming from the [Amazon internal] project: - The output Java code must be reviewable by Java engineers who do not care about Dafny, to assist in the adoption of Dafny-verified, auto-generated Java implementations - The output Java code must be efficient - The output Java code should be provable with Java verification tools. The first one is helped significantly if the compiler produces typical, “idiomatic”, readable code The second is as well, though sometimes non-typical code is acceptable, if it directly contributes to better performance. As for the third, functionally correct code “ought” to be provable, but Java-based tools will likely be more successful if usual Java idioms are used. - A fourth potential requirement not relevant to us at the moment is if the Dafny-produced Java is meant to be used as a library — then the library’s API should be recognizable Java - David > On Jan 30, 2020, at 4:35 PM, Robin Salkeld ***@***.***> wrote: > > I submit that this indicates a disagreement about the compiler requirements: currently the code it outputs just has to be functionally correct, but some folks may expect that it should output "logical" or "idiomatic" code, such as directly mapping a Dafny constructor to a Java constructor. > > I think this needs to written down explicitly somewhere in the source and/or the documentation. > > — > You are receiving this because you authored the thread. > Reply to this email directly, view it on GitHub < #502?email_source=notifications&email_token=ABITDQB62VA4ZGHOWYW2T6TRANBZ3A5CNFSM4KGYYFP2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKMURWA#issuecomment-580471000>, or unsubscribe < https://github.com/notifications/unsubscribe-auth/ABITDQB7CDH47PEMEA3GPKLRANBZ3ANCNFSM4KGYYFPQ >. > — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#502?email_source=notifications&email_token=ABUDID3WXZRS2X4TNQV44KTRARNQFA5CNFSM4KGYYFP2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKPMCNI#issuecomment-580829493>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABUDID4GGUB6XDOCVGFX3LDRARNQFANCNFSM4KGYYFPQ> .

[davidcok]

Part of my projects is to add such capability to the compiler — I have done a successful small proof of concept already. - David

…

On Jan 31, 2020, at 12:58 PM, Richard L Ford ***@***.***> wrote: I'm curious which Java verification tools you are referring to. Does the Java output from Dafny have JML markup so that the Java can be proven? Rich On Fri, Jan 31, 2020 at 11:27 AM David Cok ***@***.***> wrote: > Fair enough point. Some additional requirements coming from the [Amazon > internal] project: > > - The output Java code must be reviewable by Java engineers who do not > care about Dafny, to assist in the adoption of Dafny-verified, > auto-generated Java implementations > - The output Java code must be efficient > - The output Java code should be provable with Java verification tools. > > The first one is helped significantly if the compiler produces typical, > “idiomatic”, readable code > The second is as well, though sometimes non-typical code is acceptable, if > it directly contributes to better performance. > As for the third, functionally correct code “ought” to be provable, but > Java-based tools will likely be more successful if usual Java idioms are > used. > > - A fourth potential requirement not relevant to us at the moment is if > the Dafny-produced Java is meant to be used as a library — then the > library’s API should be recognizable Java > > - David > > > On Jan 30, 2020, at 4:35 PM, Robin Salkeld ***@***.***> > wrote: > > > > I submit that this indicates a disagreement about the compiler > requirements: currently the code it outputs just has to be functionally > correct, but some folks may expect that it should output "logical" or > "idiomatic" code, such as directly mapping a Dafny constructor to a Java > constructor. > > > > I think this needs to written down explicitly somewhere in the source > and/or the documentation. > > > > — > > You are receiving this because you authored the thread. > > Reply to this email directly, view it on GitHub < > #502?email_source=notifications&email_token=ABITDQB62VA4ZGHOWYW2T6TRANBZ3A5CNFSM4KGYYFP2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKMURWA#issuecomment-580471000>, > or unsubscribe < > https://github.com/notifications/unsubscribe-auth/ABITDQB7CDH47PEMEA3GPKLRANBZ3ANCNFSM4KGYYFPQ > >. > > > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#502?email_source=notifications&email_token=ABUDID3WXZRS2X4TNQV44KTRARNQFA5CNFSM4KGYYFP2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKPMCNI#issuecomment-580829493>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/ABUDID4GGUB6XDOCVGFX3LDRARNQFANCNFSM4KGYYFPQ> > . > — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#502?email_source=notifications&email_token=ABITDQD6KEOHEQCYHDXX4BLRARRGHA5CNFSM4KGYYFP2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKPPAOA#issuecomment-580841528>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQC7AXVXSYXMS4JLPMTRARRGHANCNFSM4KGYYFPQ>.

[robin-aws]

@davidcok To play devil's advocate, given your requirements would it perhaps make sense to just write Java code with JML markup? I worry that if the output Java code needs to be understood and developed like a "normal" Java code base, the benefits of using Dafny will be largely lost, because changes will have to either be back-ported to Dafny, or the connection to Dafny will ultimately have to be severed at some point.

Coming from the perspective of another [Amazon internal] project :) I would love for the compiler to produce idiomatic code, but I'm also wary of how far the current compilers are from that goal. For us your fourth requirement about having an idiomatic API is more relevant, and allows us to encapsulate the compiler-generated source and not target idiomatic output for now. I think it's fine to make requests for improvement like this but I don't think it's fair to label them as bugs.

As for the third, functionally correct code “ought” to be provable, but Java-based tools will likely be more successful if usual Java idioms are used.

I'd actually argue that using fewer constructs in a target language might make it easier for Java-based tools to successfully prove assertions. For example, if it's possible to compile a block of code without using object references somehow, you could eliminate any possibility of aliasing and probably make proofs much easier, even if the idiomatic implementation using objects is far simpler and understandable.

[davidcok]

Reviewed again. Current behavior works, but needs to be reevaluated for FFI. In particular

• If the anonymous constructor is given the attribute {:extern MyClass}, the compilation fails.
• If a Java programmer wants to use the constructor as Java: new MyClass(10), such constructor is not defined.