From 8600061046003793e5d5260e3df550420c3ad83a Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 31 Jul 2024 14:42:31 +0200
Subject: [PATCH] Fix bad generated Java code when using
 --legacy-data-constructors (#5657)

### Description
- Fix bad generated Java code when using --legacy-data-constructors

### How has this been tested?
- Updated existing test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 .../Backends/Java/JavaCodeGenerator.cs        | 24 ++++++++++++-------
 .../Inputs/producer/timesTwo.dfy              |  3 +++
 2 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
index 45fb88a9ad..6566819db2 100644
--- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
@@ -424,8 +424,7 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree
         }
         cw.StaticMemberWriter.Write($"public static {TypeParameters(sst.TypeArgs, " ")}{typeName} defaultValue(");
         var typeDescriptorParams = sst.TypeArgs.Where(NeedsTypeDescriptor);
-        cw.StaticMemberWriter.Write(typeDescriptorParams.Comma(tp =>
-          $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}"));
+        cw.StaticMemberWriter.Write(typeDescriptorParams.Comma(TypeDescriptorVariableDeclaration));
         var w = cw.StaticMemberWriter.NewBlock(")");
         w.WriteLine($"return {witness};");
       }
@@ -433,6 +432,10 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree
       GenerateIsMethod(sst, cw.StaticMemberWriter);
     }
 
+    private string TypeDescriptorVariableDeclaration(TypeParameter tp) {
+      return $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}";
+    }
+
     protected class ClassWriter : IClassWriter {
       public readonly JavaCodeGenerator CodeGenerator;
       public readonly ConcreteSyntaxTree InstanceMemberWriter;
@@ -557,7 +560,8 @@ protected ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiati
       wr.Write("{0} {1}", targetReturnTypeReplacement ?? "void", IdName(m));
       wr.Write("(");
       var sep = "";
-      WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, m.EnclosingClass, m, lookasideBody), wr, ref sep, tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp)}");
+      WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, m.EnclosingClass, m, lookasideBody), wr, ref sep,
+        TypeDescriptorVariableDeclaration);
       if (customReceiver) {
         DeclareFormal(sep, "_this", receiverType, m.tok, true, wr);
         sep = ", ";
@@ -602,7 +606,7 @@ protected override ConcreteSyntaxTree EmitMethodReturns(Method m, ConcreteSyntax
       wr.Write(TypeParameters(TypeArgumentInstantiation.ToFormals(ForTypeParameters(typeArgs, member, lookasideBody)), " "));
       wr.Write($"{TypeName(resultType, wr, tok)} {name}(");
       var sep = "";
-      var argCount = WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, member.EnclosingClass, member, lookasideBody), wr, ref sep, tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp)}");
+      var argCount = WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, member.EnclosingClass, member, lookasideBody), wr, ref sep, TypeDescriptorVariableDeclaration);
       if (customReceiver) {
         DeclareFormal(sep, "_this", receiverType, tok, true, wr);
         sep = ", ";
@@ -1944,6 +1948,9 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         if (Options.Get(JavaBackend.LegacyDataConstructors)) {
           wr.WriteLine("@Deprecated()");
           w = wr.NewBlock($"public static{justTypeArgs} {simplifiedTypeName} Default({typeParameters})");
+          foreach (var typeParameter in dt.TypeArgs) {
+            w.WriteLine(TypeDescriptorVariableDeclaration(typeParameter) + " = null;");
+          }
           w.Write("return ");
           wLegacyDefault = w.Fork();
           w.WriteLine(";");
@@ -1960,12 +1967,11 @@ 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 (dt.TypeArgs.Any() && 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);
+      if (wLegacyDefault != null) {
+        foreach (var node in wDefault.Nodes) {
+          wLegacyDefault.Append(node);
         }
       }
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy
index f674cf496e..d3860e9ea4 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy
@@ -10,6 +10,9 @@ module {:options "--function-syntax:4"} LibraryModule {
   // Record type
   datatype Pair<+T, +U> = Pair(first: T, second: U)
 
+  datatype NestedTypeConstructorRecord<+T> = First(value: Pair<T, T>)
+  datatype NestedTypeConstructorClass<+T> = First2(value: Pair<T, T>) | Second2(value: Pair<T, T>)
+
   datatype NoTypeArgs = Success2 | Failure2
 
 }