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))); } + /// + /// 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. + /// + [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