(Test Generation) Fix #3726 bug leading to stack overflow during test generation

Source/DafnyTestGeneration.Test/Various.cs

@@ -338,6 +338,43 @@ decreases 3 - counter {
         m.ValueCreation.Count == 2)));
     }
 
+    /// <summary>
+    /// This test addresses the situation in which there is a class-type object
+    /// that does not matter for the construction of a counterexample.
+    /// Furthermore, this class-type object is self-referential,
+    /// with a field of the same type. Test generation must not enter infinite
+    /// loop and must figure out that it needs to set the field of the object
+    /// to itself.
+    /// </summary>
+    [Fact]
+    public async Task TestByDefaultConstructionOfSelfReferentialValue() {
+      var source = @"
+module M {
+
+    class LoopingList {
+
+        var next:LoopingList;
+        var value:int;
+
+        constructor() {
+            value := 0;
+            next := this;
+        }
+
+        method getValue() returns (value:int) {
+            return this.value;
+        }
+    }
+}
+".TrimStart();
+      var options = Setup.GetDafnyOptions(output);
+      var program = Utils.Parse(options, source);
+      options.TestGenOptions.TargetMethod =
+        "M.LoopingList.getValue";
+      var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
+      Assert.Single(methods);
+    }
+
     [Fact]
     public async Task RecursivelyExtractDatatypeFields() {
       var source = @"

Source/DafnyTestGeneration/TestMethod.cs

@@ -499,8 +499,12 @@ private string GetFieldValue((string name, Type type, bool mutable, string/*?*/
           variable.Children[field.name].Count == 1) {
         return ExtractVariable(variable.Children[field.name].First(), null);
       }
-      if (ValueCreation.Any(obj => obj.type == field.type)) {
-        return ValueCreation.First(obj => obj.type == field.type).id;
+
+      var previouslyCreated = ValueCreation.FirstOrDefault(obj =>
+        DafnyModelTypeUtils.GetNonNullable(obj.type).ToString() ==
+        DafnyModelTypeUtils.GetNonNullable(field.type).ToString(), (null, null, null)).id;
+      if (previouslyCreated != null) {
+        return previouslyCreated;
       }
       return GetDefaultValue(field.type, field.type);
     }

Source/DafnyTestGeneration/Utils.cs

@@ -41,7 +41,9 @@ public static Type UseFullName(Type type) {
       return DafnyModelTypeUtils
         .ReplaceType(type, _ => true, typ => new UserDefinedType(
           new Token(),
-          typ?.ResolvedClass?.FullName ?? typ.Name,
+          typ?.ResolvedClass?.FullName == null ?
+            typ.Name :
+            typ.ResolvedClass.FullName + (typ.Name.Last() == '?' ? "?" : ""),
           typ.TypeArgs));
     }