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

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 = @"

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);
  }

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));
  }
 

docs/dev/3727.fix

@@ -0,0 +1 @@
+Avoid infinite recursion when trying to construct a potentially self-referential object during test generation