From df1f6830b4c2bc41787bc6e9c3e17f8bc387549d Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <sasha.fedchin@gmail.com>
Date: Wed, 24 May 2023 19:42:24 -0700
Subject: [PATCH] (Test Generation) Fix #3726 bug leading to stack overflow
 during test generation (#3727)

Fixes #3726

This PR fixes a situation in which test generation gets into infinite
recursion when trying to construct a potentially self-referential object
that the verifier gives no information about (see the test, which is
also the example in the linked issue). The main problem was that
existing code compared types by reference in one instance in which a
comparison of the types's string representations should have been used.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

---------

Co-authored-by: Aleksandr Fedchin <fedchina@amazon.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
---
 Source/DafnyTestGeneration.Test/Various.cs | 37 ++++++++++++++++++++++
 Source/DafnyTestGeneration/TestMethod.cs   |  8 +++--
 Source/DafnyTestGeneration/Utils.cs        |  4 ++-
 docs/dev/3727.fix                          |  1 +
 4 files changed, 47 insertions(+), 3 deletions(-)
 create mode 100644 docs/dev/3727.fix

diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs
index 0ff89fff7a9..9d95d1657b2 100644
--- a/Source/DafnyTestGeneration.Test/Various.cs
+++ b/Source/DafnyTestGeneration.Test/Various.cs
@@ -338,6 +338,43 @@ class List {
         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 = @"
diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs
index 889e8b52915..c2ea243f414 100644
--- a/Source/DafnyTestGeneration/TestMethod.cs
+++ b/Source/DafnyTestGeneration/TestMethod.cs
@@ -499,8 +499,12 @@ public class TestMethod {
           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);
     }
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index 8ca6392701d..88576ea83ee 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -41,7 +41,9 @@ public static class Utils {
       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));
     }
 
diff --git a/docs/dev/3727.fix b/docs/dev/3727.fix
new file mode 100644
index 00000000000..5616950fbaf
--- /dev/null
+++ b/docs/dev/3727.fix
@@ -0,0 +1 @@
+Avoid infinite recursion when trying to construct a potentially self-referential object during test generation
\ No newline at end of file