Fixed error reporting counter example + avoid null pointer exceptions (…

…#2650)

Fixes #2026

RELEASE_NOTES.md

@@ -4,7 +4,7 @@
 - feat: Support for plugin-based code actions on the IDE (https://github.com/dafny-lang/dafny/pull/2021)
 - fix: Added missing error reporting position on string prefix check (https://github.com/dafny-lang/dafny/pull/2652)
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
-
+- fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)
 
 # 3.8.0
 

Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs

@@ -871,6 +871,8 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
       return result;
     }
 
+    private const string PleaseEnableModelCompressFalse = "Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.";
+
     /// <summary>
     /// Return the name of the field represented by the given element.
     /// Special care is required if the element represents an array index
@@ -893,16 +895,24 @@ private List<string> GetFieldNames(Model.Element elt) {
         Model.FuncTuple dimTuple;
         if (i == 0) {
           dimTuple = fIndexField.AppWithResult(elt);
+          if (dimTuple == null) {
+            Console.Out.WriteLine(PleaseEnableModelCompressFalse);
+            continue;
+          }
           indices[i] = dimTuple.Args[0];
         } else {
           dimTuple = fMultiIndexField.AppWithResult(elt);
+          if (dimTuple == null) {
+            Console.Out.WriteLine(PleaseEnableModelCompressFalse);
+            continue;
+          }
           indices[i] = dimTuple.Args[1];
           elt = dimTuple.Args[0];
         }
       }
       return new List<string>() {
         "[" + string.Join(",",
-          indices.ToList().ConvertAll(element => element.ToString())) + "]"
+          indices.ToList().ConvertAll(element => element == null ? "null" : element.ToString())) + "]"
       };
     }
 

Test/git-issues/git-issue-2026.dfy

@@ -0,0 +1,21 @@
+// RUN: %dafny_0 /compile:0 "%s" /extractCounterexample /mv model  > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method foo(n: nat) returns (ret: array<string>)
+{
+    ret := new string[n];
+
+    var i := 0;
+    while i < n
+        invariant 0 <= i <= n
+        invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even"
+        invariant forall j :: 0 <= j < i ==> j % 2 == 1 ==> ret[j] == "odd"
+    {
+        if i % 2 == 0 {
+            ret[i] := "odd";
+        } else {
+            ret[i] := "even";
+        }
+        i := i + 1;
+    }
+}

Test/git-issues/git-issue-2026.dfy.expect

@@ -0,0 +1,37 @@
+git-issue-2026.dfy(11,18): Error: This loop invariant might not be maintained by the loop.
+git-issue-2026.dfy(11,18): Related message: loop invariant violation
+git-issue-2026.dfy(12,18): Error: This loop invariant might not be maintained by the loop.
+git-issue-2026.dfy(12,18): Related message: loop invariant violation
+
+Dafny program verifier finished with 0 verified, 2 errors
+Counterexample for first failing assertion: 
+git-issue-2026.dfy(5,0): initial state:
+	n : int = 5854
+	ret : ? = ()
+git-issue-2026.dfy(6,24):
+Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.
+	n : int = 5854
+	ret : ? = ([null] := @0)
+	@0 : ? = ()
+git-issue-2026.dfy(8,14):
+Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.
+	n : int = 5854
+	ret : ? = ([null] := @0)
+	i : int = 0
+	@0 : ? = ()
+git-issue-2026.dfy(9,4): after some loop iterations:
+	n : int = 5854
+	ret : ? = ()
+	i : int = 0
+git-issue-2026.dfy(15,27):
+Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.
+	n : int = 5854
+	ret : ? = ([null] := @0)
+	i : int = 0
+	@0 : ? = ()
+git-issue-2026.dfy(19,18):
+Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.
+	n : int = 5854
+	ret : ? = ([null] := @0)
+	i : int = 1
+	@0 : ? = ()