Fix self-referencing issue

Source/DafnyTestGeneration.Test/Various.cs

@@ -229,6 +229,85 @@ 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>
+ [TestMethod]
+ 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();
+ var program = Utils.Parse(options, source);
+ options.TestGenOptions.TargetMethod =
+ "M.LoopingList.getValue";
+ var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
+ Assert.IsTrue(methods.Count == 1);
+ }
+
+ /// <summary>
+ /// This test models 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 potentially self-referential,
+ /// with a field of the same (nullable) type.
+ /// Test generation must not enter infinite loop and must figure out
+ /// that it needs to set the field to null (with self-referencing being
+ /// prohibited by a precondition).
+ /// </summary>
+ [TestMethod]
+ public async Task TestByDefaultConstructionOfPotentiallySelfReferentialValue() {
+ var source = @"
+module M {
+
+ class List {
+
+ var next:List?;
+ var value:int;
+
+ predicate isEndOfList() reads this {
+ next == null
+ }
+
+ method getValue() 
+ returns (value:int) 
+ requires isEndOfList()
+ {
+ return this.value;
+ }
+ }
+}
+".TrimStart();
+ var options = Setup.GetDafnyOptions();
+ var program = Utils.Parse(options, source);
+ options.TestGenOptions.TargetMethod =
+ "M.List.getValue";
+ var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
+ Assert.IsTrue(methods.Count == 1);
+ Assert.IsTrue(methods[0].ValueCreation.Count == 1);
+ Assert.IsTrue(methods[0].Assignments.Exists(assignment => assignment.fieldName == "next" && assignment.childId == "null"));
+ }
+
  [TestMethod]
  public async Task RecursivelyExtractDatatypeFields() {
  var source = @"

Source/DafnyTestGeneration/TestMethod.cs

@@ -499,8 +499,8 @@ 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;
+ if (ValueCreation.Any(obj => obj.type.ToString() == field.type.ToString())) {
+ return ValueCreation.First(obj => obj.type.ToString() == field.type.ToString()).id;
  }
  return GetDefaultValue(field.type, field.type);
  }

Source/DafnyTestGeneration/Utils.cs

@@ -23,7 +23,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));
  }