fix: Legacy datatype constructor compatibility in Java (#5558)

Source/DafnyCore/Backends/Java/JavaBackend.cs

@@ -1,11 +1,14 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -26,6 +29,19 @@ public override string TargetBaseDir(string dafnyProgramName) =>
   public override bool SupportsInMemoryCompilation => false;
   public override bool TextualTargetIsExecutable => false;
 
+  public static readonly Option<bool> LegacyDataConstructors = new("--legacy-data-constructors",
+    @"
+Generate unsafe, deprecated data constructor methods that do not take type descriptors, 
+for backwards compatibility with Java code generated with Dafny versions earlier than 4.3.".TrimStart()) {
+    IsHidden = true
+  };
+  static JavaBackend() {
+    DafnyOptions.RegisterLegacyUi(LegacyDataConstructors, DafnyOptions.ParseBoolean, "Compilation options", legacyName: "legacyDataConstructors", defaultValue: false);
+    DooFile.RegisterNoChecksNeeded(LegacyDataConstructors, false);
+  }
+
+  public override IEnumerable<Option> SupportedOptions => new List<Option> { LegacyDataConstructors };
+
   public override void CleanSourceDirectory(string sourceDirectory) {
     try {
       Directory.Delete(sourceDirectory, true);

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -12,6 +12,7 @@
 using System.IO;
 using System.Diagnostics.Contracts;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Text.RegularExpressions;
 using JetBrains.Annotations;
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
@@ -1912,6 +1913,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
       var defaultMethodTypeDescriptorCount = 0;
       var usedTypeArgs = UsedTypeParameters(dt);
       ConcreteSyntaxTree wDefault;
+      ConcreteSyntaxTree wLegacyDefault = null;
       wr.WriteLine();
       if (dt.TypeArgs.Count == 0) {
         wr.Write($"private static final {simplifiedTypeName} theDefault = ");
@@ -1929,6 +1931,14 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         w.Write("return ");
         wDefault = w.Fork();
         w.WriteLine(";");
+
+        if (Options.Get(JavaBackend.LegacyDataConstructors)) {
+          wr.WriteLine("@Deprecated()");
+          w = wr.NewBlock($"public static{justTypeArgs} {simplifiedTypeName} Default({typeParameters})");
+          w.Write("return ");
+          wLegacyDefault = w.Fork();
+          w.WriteLine(";");
+        }
       }
       var groundingCtor = dt.GetGroundingCtor();
       if (groundingCtor.IsGhost) {
@@ -1941,6 +1951,13 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         EmitDatatypeValue(dt, groundingCtor,
           dt.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(dt.tok, tp)),
           dt is CoDatatypeDecl, $"{wDefaultTypeArguments}", args, wDefault);
+
+        if (Options.Get(JavaBackend.LegacyDataConstructors)) {
+          var nullTypeDescriptorArgs = Enumerable.Repeat("null", defaultMethodTypeDescriptorCount).Comma();
+          EmitDatatypeValue(dt, groundingCtor,
+            dt.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(dt.tok, tp)),
+            dt is CoDatatypeDecl, nullTypeDescriptorArgs, args, wLegacyDefault);
+        }
       }
 
       // create methods
@@ -1954,6 +1971,15 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         var sep = typeDescriptorCount > 0 && formalCount > 0 ? ", " : "";
         wr.NewBlock(")")
           .WriteLine($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({wCallArguments}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
+
+        if (Options.Get(JavaBackend.LegacyDataConstructors)) {
+          wr.WriteLine("@Deprecated()");
+          wr.Write($"public static{justTypeArgs} {DtT_protected} {DtCreateName(ctor)}(");
+          var nullTypeDescriptorArgs = Enumerable.Repeat("null", typeDescriptorCount).Comma();
+          WriteFormals("", ctor.Formals, wr);
+          wr.NewBlock(")")
+            .WriteLine($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({nullTypeDescriptorArgs}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
+        }
       }
 
       if (dt.IsRecordType) {
@@ -1970,6 +1996,15 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         var sep = typeDescriptorCount > 0 && formalCount > 0 ? ", " : "";
         wr.NewBlock(")")
           .WriteLine($"return create({wCallArguments}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
+
+        if (Options.Get(JavaBackend.LegacyDataConstructors)) {
+          wr.WriteLine("@Deprecated()");
+          wr.Write($"public static{justTypeArgs} {DtT_protected} create_{ctor.GetCompileName(Options)}(");
+          var nullTypeDescriptorArgs = Enumerable.Repeat("null", typeDescriptorCount).Comma();
+          WriteFormals("", ctor.Formals, wr);
+          wr.NewBlock(")")
+            .WriteLine($"return create({nullTypeDescriptorArgs}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
+        }
       }
 
       // query properties

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -113,7 +113,7 @@ public virtual string GetCompileName(bool isDefaultModule, string moduleName, st
   protected ReadOnlyCollection<string>? OtherFileNames;
 
   // The following lists are the Options supported by the backend.
-  public virtual IEnumerable<Option<string>> SupportedOptions => new List<Option<string>>();
+  public virtual IEnumerable<Option> SupportedOptions => new List<Option>();
 
   protected IExecutableBackend(DafnyOptions options) {
     Options = options;

Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java

@@ -275,6 +275,11 @@ public static BigInteger unsignedToBigInteger(int i){
     public static BigInteger unsignedToBigInteger(long l){
         return unsignedToBigInteger_h(BigInteger.valueOf(l), ULONG_LIMIT);
     }
+
+    // Alias maintained only for backwards compatability
+    public static BigInteger unsignedLongToBigInteger(long l) {
+        return unsignedToBigInteger(l);
+    }
 
     public static byte divideUnsignedByte(byte a, byte b) {
         return (byte)Integer.divideUnsigned(((int)a) & 0xFF, ((int)b) & 0xFF);

Source/DafnyTestGeneration.Test/Setup.cs

@@ -15,6 +15,14 @@
 using Program = Microsoft.Dafny.Program;
 using Token = Microsoft.Dafny.Token;
 
+// These tests are frequently hanging and timing out for reasons unknown.
+// It seems to be much harder to reproduce locally if tests are run sequentially
+// (as they are in debugging mode by default)
+// so as a stop gap we're trying disabling parallel execution
+// in the hopes it at least reduces the frequency of hanging.
+// See https://github.com/dafny-lang/dafny/issues/5488.
+[assembly: CollectionBehavior(DisableTestParallelization = true)]
+
 namespace DafnyTestGeneration.Test {
 
   public class Setup {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy

@@ -5,4 +5,9 @@ module {:options "--function-syntax:4"} LibraryModule {
     x * 2
   }
 
+  datatype Result<+T, +E> = Success(value: T) | Failure(error: E)
+
+  // Record type
+  datatype Pair<+T, +U> = Pair(first: T, second: U)
+
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/README.md

@@ -0,0 +1,6 @@
+This code was created using Dafny 4.2 in order to capture the existing code that
+`--legacy-data-constructors` needs to still satisfy:
+
+```
+dafny translate java --output=fromDafny42/usesTimesTwo --allow-warnings --library=Inputs/producer/timesTwo.dfy usesTimesTwo.dfy
+```

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/ConsumerModule/__default.java

@@ -0,0 +1,61 @@
+// Class __default
+// Dafny class __default compiled into Java
+package ConsumerModule;
+
+
+@SuppressWarnings({"unchecked", "deprecation"})
+public class __default {
+  public __default() {
+  }
+  public static void Main(dafny.DafnySequence<? extends dafny.DafnySequence<? extends dafny.CodePoint>> __noArgsParameter)
+  {
+    java.math.BigInteger _0_n = java.math.BigInteger.ZERO;
+    _0_n = java.math.BigInteger.valueOf(21L);
+    java.math.BigInteger _1_TwoN = java.math.BigInteger.ZERO;
+    _1_TwoN = LibraryModule.__default.TimesTwo(_0_n);
+    System.out.print((dafny.DafnySequence.asUnicodeString("Two times ")).verbatimString());
+    System.out.print(java.lang.String.valueOf(_0_n));
+    System.out.print((dafny.DafnySequence.asUnicodeString(" is ")).verbatimString());
+    System.out.print(java.lang.String.valueOf(_1_TwoN));
+    System.out.print((dafny.DafnySequence.asUnicodeString("\n")).verbatimString());
+    java.math.BigInteger _2_aNat = java.math.BigInteger.ZERO;
+    java.math.BigInteger _out0 = java.math.BigInteger.ZERO;
+    _out0 = __default.PickANat();
+    _2_aNat = _out0;
+  }
+  public static void __Main(dafny.DafnySequence<? extends dafny.DafnySequence<? extends dafny.CodePoint>> args) {
+    __default.Main(args);
+  }
+  public static java.math.BigInteger PickANat()
+  {
+    java.math.BigInteger n = java.math.BigInteger.ZERO;
+    if(true) {
+      java.math.BigInteger _out1 = java.math.BigInteger.ZERO;
+      _out1 = __default.<java.math.BigInteger>PickSomething(_System.nat._typeDescriptor());
+      n = _out1;
+    }
+    return n;
+  }
+  public static <__T> __T PickSomething(dafny.TypeDescriptor<__T> _td___T)
+  {
+    @SuppressWarnings({"unchecked", "deprecation"})
+    __T t = _td___T.defaultValue();
+    if(true) {
+    }
+    return t;
+  }
+  public static void MakeAResult()
+  {
+    LibraryModule.Result<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _3_r;
+    _3_r = LibraryModule.Result.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create_Success(java.math.BigInteger.valueOf(42L));
+  }
+  public static void MakeAPair()
+  {
+    LibraryModule.Pair<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _4_p;
+    _4_p = LibraryModule.Pair.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create(java.math.BigInteger.ONE, dafny.DafnySequence.asUnicodeString("partridge in a pair tree"));
+  }
+  @Override
+  public java.lang.String toString() {
+    return "ConsumerModule._default";
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/_System/nat.java

@@ -0,0 +1,15 @@
+// Class nat
+// Dafny class nat compiled into Java
+package _System;
+
+import ConsumerModule.*;
+
+@SuppressWarnings({"unchecked", "deprecation"})
+public class nat {
+  public nat() {
+  }
+  private static final dafny.TypeDescriptor<java.math.BigInteger> _TYPE = dafny.TypeDescriptor.<java.math.BigInteger>referenceWithInitializer(java.math.BigInteger.class, () -> java.math.BigInteger.ZERO);
+  public static dafny.TypeDescriptor<java.math.BigInteger> _typeDescriptor() {
+    return (dafny.TypeDescriptor<java.math.BigInteger>) (dafny.TypeDescriptor<?>) _TYPE;
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/usesTimesTwo.java

@@ -0,0 +1,13 @@
+// Dafny program the_program compiled into Java
+
+import ConsumerModule.*;
+import _System.*;
+
+
+
+
+public class usesTimesTwo {
+  public static void main(String[] args) {
+    dafny.Helpers.withHaltHandling(() -> { ConsumerModule.__default.__Main(dafny.Helpers.UnicodeFromMainArguments(args)); } );
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy

@@ -0,0 +1,20 @@
+// NONUNIFORM: Highly target language specific
+
+// Alternate version of usesTimesTwo.dfy as a regression test for https://github.com/dafny-lang/dafny/issues/5555.
+// Relies on having checked in the compilation of the library using Dafny 4.2.
+
+// Java
+
+// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --legacy-data-constructors
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/**/*.java
+
+// Already run using Dafny 4.2: %baredafny translate java --output=%S/fromDafny42/usesTimesTwo --allow-warnings --library=%S/Inputs/producer/timesTwo.dfy %S/usesTimesTwo.dfy
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/fromDafny42/usesTimesTwo-java %S/fromDafny42/usesTimesTwo-java/**/*.java
+
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/fromDafny42/usesTimesTwo-java usesTimesTwo > "%t"
+
+// (Other languages could be added in the future too.)
+
+// Final output check for all runs
+
+// RUN: %diff "%s.expect" "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy.expect

@@ -0,0 +1 @@
+Two times 21 is 42

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy

@@ -12,10 +12,10 @@
 // Java
 
 // RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --outer-module testproducer.dafnyinternal --translation-record-output %S/timesTwo-customName.dtr
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/timesTwo.java %S/Inputs/producer/timesTwo-java/*/*.java
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/**/*.java
 
 // RUN: %baredafny translate java --output=%S/consumer/usesTimesTwo --allow-warnings --library=%S/Inputs/producer/timesTwo.dfy %s --translation-record %S/timesTwo-customName.dtr
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java %S/consumer/usesTimesTwo-java/usesTimesTwo.java %S/consumer/usesTimesTwo-java/*/*.java
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java %S/consumer/usesTimesTwo-java/**/*.java
 
 // RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java usesTimesTwo >> "%t"
 
@@ -68,4 +68,12 @@ module ConsumerModule {
   method PickSomething<T(0)>() returns (t: T) {
     t := *;
   }
+
+  method MakeAResult() {
+    var r: Result<nat, string> := Success(42);
+  }
+
+  method MakeAPair() {
+    var p: Pair<nat, string> := Pair(1, "partridge in a pair tree");
+  }
 }