From b15343cbb4521a5a47e909b8f47410cf95856538 Mon Sep 17 00:00:00 2001 From: Dargones Date: Thu, 9 Mar 2023 21:14:41 -0500 Subject: [PATCH 1/5] Fix self-referencing issue --- Source/DafnyTestGeneration.Test/Various.cs | 79 ++++++++++++++++++++++ Source/DafnyTestGeneration/TestMethod.cs | 4 +- Source/DafnyTestGeneration/Utils.cs | 4 +- 3 files changed, 84 insertions(+), 3 deletions(-) diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index e99b4b6dab4..0af40d844c5 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -229,6 +229,85 @@ decreases 3 - counter { 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. + /// + [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); + } + + /// + /// 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). + /// + [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 = @" diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 3681429fb5f..97c7fe75ce6 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -499,8 +499,8 @@ private string GetFieldValue((string name, Type type, bool mutable, string/*?*/ 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); } diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 59927adaa50..f2bc4cef39b 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -23,7 +23,9 @@ public static Type UseFullName(Type type) { 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)); } From 28be2014b463ebcf93d88ced2af39acd1d266802 Mon Sep 17 00:00:00 2001 From: Dargones Date: Thu, 9 Mar 2023 21:54:00 -0500 Subject: [PATCH 2/5] Take nullability into account --- Source/DafnyTestGeneration.Test/Various.cs | 42 ---------------------- Source/DafnyTestGeneration/TestMethod.cs | 8 +++-- 2 files changed, 6 insertions(+), 44 deletions(-) diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index 0af40d844c5..b21693ee8a2 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -266,48 +266,6 @@ method getValue() returns (value:int) { Assert.IsTrue(methods.Count == 1); } - /// - /// 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). - /// - [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 = @" diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 97c7fe75ce6..7ef593ecd2c 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -499,8 +499,12 @@ private string GetFieldValue((string name, Type type, bool mutable, string/*?*/ variable.Children[field.name].Count == 1) { return ExtractVariable(variable.Children[field.name].First(), null); } - if (ValueCreation.Any(obj => obj.type.ToString() == field.type.ToString())) { - return ValueCreation.First(obj => obj.type.ToString() == field.type.ToString()).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); } From 42594818781243752a8145bb550dffe4852743cb Mon Sep 17 00:00:00 2001 From: Dargones Date: Fri, 10 Mar 2023 15:35:23 -0500 Subject: [PATCH 3/5] Use Assert.Single instead of Assert.Equal --- Source/DafnyTestGeneration.Test/Various.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index 5e2b6373e2c..00f751f0c14 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -261,7 +261,7 @@ method getValue() returns (value:int) { options.TestGenOptions.TargetMethod = "M.LoopingList.getValue"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); - Assert.Equal(1, methods.Count); + Assert.Single(methods); } [Fact] From cc5da8e5e0ed005ad120083453acd5795497ca3d Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Tue, 23 May 2023 10:44:35 -0700 Subject: [PATCH 4/5] Fix merge --- Source/DafnyTestGeneration.Test/Various.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index ae83f74454d..9d95d1657b2 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -367,7 +367,7 @@ method getValue() returns (value:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.LoopingList.getValue"; From afd56e2ce3cb9ea198a6e808186119d0f860e93c Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Wed, 24 May 2023 08:20:58 -0700 Subject: [PATCH 5/5] Add release notes --- docs/dev/3727.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/3727.fix 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