(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 <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>

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