Java transpilation of extern module has incorrect class identifier

[hillcg-aws]

Dafny version

4.9.1

Code to produce this issue

module {:extern "com.dafnyuser.foo.bar"} Foo.Bar {
  function TopLevelFunction<T>(t: T): bool {
    true
  }
  
  function {:extern "NativeTop"} TopLevelExtern<T>(t: T): bool
  // body to be supplied directly in the target language

  function CallIt<T>(t: T): bool {
    TopLevelFunction(t) && TopLevelExtern(t)
  }

  class {:extern "YourClass"} MyClass {
    static function FunctionInClass<T>(t: T): bool
    {
      true
    }
    
    static function {:extern "NativeInClass"} ExternInClass<T>(t: T): bool
    // body to be supplied directly in the target language
      
    static function CallIt<T>(t: T): bool {
      FunctionInClass(t) && ExternInClass(t)
    }
  }
}

method Main() {
  var a := Foo.Bar.CallIt(true);
  var b := Foo.Bar.MyClass.CallIt(true);
  print a, " ", b, "\n";
}

Command to run and resulting output

$ dafny translate java foo.dfy

What happened?

Usage of __default instead of _ExternBase___default.

For example in foo-java/com/dafnyuser/foo/bar/_ExternBase___default.java (generated from the supplied code example) one will see CallIt fails to compile due to the incorrect class name being used:

// Class _ExternBase___default
// Dafny class __default compiled into Java
package com.dafnyuser.foo.bar;


@SuppressWarnings({"unchecked", "deprecation"})
public abstract class _ExternBase___default {
  public _ExternBase___default() {
  }
  public static <__T> boolean TopLevelFunction(dafny.TypeDescriptor<__T> _td___T, __T t)
  {
    return true;
  }
  public static <__T> boolean CallIt(dafny.TypeDescriptor<__T> _td___T, __T t)
  {
    return (__default.<__T>TopLevelFunction(_td___T, t)) && (__default.<__T>NativeTop(_td___T, t));
  }
  @Override
  public java.lang.String toString() {
    return "Foo.Bar._default";
  }
}

What type of operating system are you experiencing the problem on?

Linux, Mac

[robin-aws]

As it turns out this is operating correctly, but the feature is not intuitive and there is a large documentation gap.

For some backends you can define a mix of Dafny-implemented and externally-implemented things in a class (including the implicit "default class" at the root of a module, which in Java is translated to __default). To make this possible in Java, for a given Dafny class C, Dafny outputs not a C Java class but an _ExternBase_C class. Whoever implements the externally-implemented declarations is expected to write the actual C class themselves and extend _ExternBase_C in order to pick up the Dafny-implemented versions. This is true even if you ONLY have Dafny-implemented methods on something marked {:extern}. That means the dangling __default references in the output are as-designed and not errors.

I believe @leino told you to cut this issue as an implementation bug because of confusion between multiple names in this example: the MyClass Dafny class has {:extern "YourClass"} so Dafny emits an _ExternBase_YourClass, but the default class in the Foo.Bar module doesn't have an {:extern} attribute (and can't since the default class is implicit), so Dafny also emits an _ExternBase___default class.

Reclassifying this as documentation, but note also that we have newer attributes to replace {:extern} in the works that improve the UX here.

[robin-aws]

Keeping bug after all because I really think failing to talk about this anywhere in the reference manual or https://dafny.org/dafny/DafnyRef/integration-java/IntegrationJava is enough of a miss given how non-obvious this is. :)