[Counterexamples] Fix stack overflow during counterexample extraction…

… for some programs (#4392) Fixes #4391 This PR fixes a potential case of an infinite recursion in Dafny counterexample extraction (exemplified by the added test). The solution is to change the order in which Dafny looks at functions in the counterexample model when trying to deduce the type of a variable. 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]>
dafny-lang · Sep 19, 2023 · e493201 · e493201
1 parent 091ab9f
commit e493201
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 10 deletions.
diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs
@@ -1534,6 +1534,30 @@ class C<T> {
  Assert.True(counterExamples[0].Variables.ContainsKey("this:M.C<M.C$T>"));
  }
 
+ /// <summary>
+ /// This test case would previously lead to stack overflow because of infinite recursion in GetDafnyType
+ /// </summary>
+ [Theory]
+ [MemberData(nameof(OptionSettings))]
+ public async Task GetDafnyTypeInfiniteRecursion(List<Action<DafnyOptions>> optionSettings) {
+ await SetUpOptions(optionSettings);
+ var source = @"
+ class Seq {
+ var s:seq<int>
+ method test(i0:nat, val0:int, i1:nat, val1:int) 
+ modifies this {
+ assume 0 <= i0 < i1 < |s|;
+ s := s[i0 := val0];
+ s := s[i1 := val1];
+ assert s[0] != 0;
+ }
+ }
+ ".TrimStart();
+ var documentItem = CreateTestDocument(source);
+ await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+ (await RequestCounterExamples(documentItem.Uri)).ToList(); ;
+ }
+
  public CounterExampleTest(ITestOutputHelper output) : base(output) {
  }
  }

diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs
@@ -302,6 +302,16 @@ public class DafnyModel {
  /// This method tries to extract the base type (so seq<char> instead of string)
  /// </summary>
  private Type GetDafnyType(Model.Uninterpreted element) {
+ var finalResult = UnknownType;
+ foreach (var typeElement in GetIsResults(element)) {
+ var reconstructedType = ReconstructType(typeElement);
+ if (reconstructedType is not UserDefinedType userDefinedType) {
+ return reconstructedType;
+ }
+ if (finalResult.Name.EndsWith("?") || finalResult == UnknownType) {
+ finalResult = userDefinedType;
+ }
+ }
  var seqOperation = fSeqAppend.AppWithResult(element);
  seqOperation ??= fSeqDrop.AppWithResult(element);
  seqOperation ??= fSeqTake.AppWithResult(element);
@@ -350,16 +360,6 @@ public class DafnyModel {
  if (fCharToInt.OptEval(element) != null) {
  return Type.Char;
  }
- var finalResult = UnknownType;
- foreach (var typeElement in GetIsResults(element)) {
- var reconstructedType = ReconstructType(typeElement);
- if (reconstructedType is not UserDefinedType userDefinedType) {
- return reconstructedType;
- }
- if (finalResult.Name.EndsWith("?") || finalResult == UnknownType) {
- finalResult = userDefinedType;
- }
- }
  if (finalResult != UnknownType) {
  return finalResult;
  }

diff --git a/docs/dev/news/4392.fix b/docs/dev/news/4392.fix
@@ -0,0 +1 @@
+Fixed a bug leading to stack overflow during counterexample extraction on some programs.