Counterexamples - fix integer parsing bug and improve code quality

RELEASE_NOTES.md

@@ -6,6 +6,7 @@
   (https://github.com/dafny-lang/dafny/pull/2416)
 - feat: Dafny now supports disjunctive (“or”) patterns in match statements and expressions.  Cases are separated by `|` characters.  Disjunctive patterns may not appear within other patterns and may not bind variables.
   (https://github.com/dafny-lang/dafny/pull/2448)
+- fix: Counterexamples - fix an integer parsing bug and correctly extract datatype and field names (https://github.com/dafny-lang/dafny/pull/2461)
 - feat: New option `-diagnosticsFormat:json` to print Dafny error messages as JSON objects (one per line).
   (https://github.com/dafny-lang/dafny/pull/2363)
 - fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (https://github.com/dafny-lang/dafny/pull/2437)

Source/DafnyDriver/DafnyDriver.cs

@@ -349,7 +349,7 @@ private static void PrintCounterexample(string modelViewFile) {
         var vars = state.ExpandedVariableSet(-1);
         foreach (var variable in vars) {
           Console.WriteLine($"\t{variable.ShortName} : " +
-                            $"{variable.Type.InDafnyFormat()} = " +
+                            $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
                             $"{variable.Value}");
         }
       }

Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs

@@ -863,8 +863,8 @@ method test() {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(1, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,bool>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,bool>"], new Regex("\\(.*3 := false.*"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, bool>"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, bool>"], new Regex("\\(.*3 := false.*"));
     }
 
     [TestMethod]
@@ -881,15 +881,15 @@ method test(value:int) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(4, counterExamples.Length);
       Assert.AreEqual(2, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,int>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,int>"], new Regex("\\(.*3 := -1.*"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, int>"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, int>"], new Regex("\\(.*3 := -1.*"));
       Assert.AreEqual(3, counterExamples[3].Variables.Count);
-      Assert.IsTrue(counterExamples[3].Variables.ContainsKey("m:map<int,int>"));
+      Assert.IsTrue(counterExamples[3].Variables.ContainsKey("m:map<int, int>"));
       Assert.IsTrue(counterExamples[3].Variables.ContainsKey("value:int"));
       Assert.IsTrue(counterExamples[3].Variables.ContainsKey("b:bool"));
       Assert.AreEqual("true", counterExamples[3].Variables["b:bool"]);
       StringAssert.Matches(counterExamples[3].Variables["value:int"], new Regex("[1-9][0-9]*"));
-      StringAssert.Matches(counterExamples[3].Variables["m:map<int,int>"], new Regex("\\(.*3 := [1-9].*"));
+      StringAssert.Matches(counterExamples[3].Variables["m:map<int, int>"], new Regex("\\(.*3 := [1-9].*"));
     }
 
     [TestMethod]
@@ -907,13 +907,13 @@ requires key in m.Keys
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(3, counterExamples.Length);
       Assert.AreEqual(4, counterExamples[2].Variables.Count);
-      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m:map<int,int>"));
-      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m':map<int,int>"));
+      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m:map<int, int>"));
+      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m':map<int, int>"));
       Assert.IsTrue(counterExamples[2].Variables.ContainsKey("val:int"));
       Assert.IsTrue(counterExamples[2].Variables.ContainsKey("key:int"));
       var key = counterExamples[2].Variables["key:int"];
       var val = counterExamples[2].Variables["val:int"];
-      StringAssert.Matches(counterExamples[2].Variables["m':map<int,int>"], new Regex("\\(.*" + key + " := " + val + ".*"));
+      StringAssert.Matches(counterExamples[2].Variables["m':map<int, int>"], new Regex("\\(.*" + key + " := " + val + ".*"));
     }
 
     [TestMethod]
@@ -930,15 +930,15 @@ method T_map0(m:map<int,int>, key:int, val:int)
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(4, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,int>"));
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m':map<int,int>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, int>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m':map<int, int>"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("val:int"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("key:int"));
       var key = counterExamples[1].Variables["key:int"];
       var val = counterExamples[1].Variables["val:int"];
       var mapRegex = new Regex("\\(.*" + key + " := " + val + ".*");
-      Assert.IsTrue(mapRegex.IsMatch(counterExamples[1].Variables["m':map<int,int>"]) ||
-                    mapRegex.IsMatch(counterExamples[1].Variables["m:map<int,int>"]));
+      Assert.IsTrue(mapRegex.IsMatch(counterExamples[1].Variables["m':map<int, int>"]) ||
+                    mapRegex.IsMatch(counterExamples[1].Variables["m:map<int, int>"]));
 
     }
 
@@ -954,9 +954,9 @@ method test(m:map<int,char>) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(2, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,char>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, char>"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("keys:set<int>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,char>"], new Regex("\\(.*25 := .*"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, char>"], new Regex("\\(.*25 := .*"));
       StringAssert.Matches(counterExamples[1].Variables["keys:set<int>"], new Regex("\\{.*25 := true.*"));
     }
 
@@ -972,9 +972,9 @@ method test(m:map<int,char>) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(2, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,char>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, char>"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("values:set<char>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,char>"], new Regex("\\(.* := 'c'.*"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, char>"], new Regex("\\(.* := 'c'.*"));
       StringAssert.Matches(counterExamples[1].Variables["values:set<char>"], new Regex("\\{.*'c' := true.*"));
     }
 
@@ -992,8 +992,8 @@ method test(m:map<bv2,bv3>) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(1, counterExamples.Length);
       Assert.AreEqual(1, counterExamples[0].Variables.Count);
-      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("m:map<bv2,bv3>"));
-      StringAssert.Matches(counterExamples[0].Variables["m:map<bv2,bv3>"], new Regex("\\(.*[0-9]+ := [0-9]+.*"));
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("m:map<bv2, bv3>"));
+      StringAssert.Matches(counterExamples[0].Variables["m:map<bv2, bv3>"], new Regex("\\(.*[0-9]+ := [0-9]+.*"));
     }
 
     [TestMethod]
@@ -1019,61 +1019,73 @@ method test() {
     }
 
     [TestMethod]
-    public void DafnyModelTypeMultipleArguments() {
-      var type = DafnyModelType.FromString("seq<int, char>");
-      Assert.AreEqual("seq", type.Name);
-      Assert.AreEqual(2, type.TypeArgs.Count);
-      Assert.AreEqual("int", type.TypeArgs[0].Name);
-      Assert.AreEqual("char", type.TypeArgs[1].Name);
-      Assert.AreEqual(0, type.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, type.TypeArgs[1].TypeArgs.Count);
-    }
+    public async Task UnboundedIntegers() {
+      var source = @"
+      ghost const NAT64_MAX := 0x7fff_ffff_ffff_ffff
 
+      newtype nat64 = x | 0 <= x <= NAT64_MAX
+
+      function method plus(a: nat64, b: nat64): nat64 {
+        a + b
+      }".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
+      Assert.AreEqual(1, counterExamples.Length);
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("a:int"));
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("b:int"));
+      var a = long.Parse(counterExamples[0].Variables["a:int"]);
+      var b = long.Parse(counterExamples[0].Variables["b:int"]);
+      Assert.IsTrue(a + b < a || a + b < b);
+    }
 
     [TestMethod]
-    public void DafnyModelTypeNestedArguments() {
-      var type = DafnyModelType.FromString("seq<map<char, int>>");
-      Assert.AreEqual("seq", type.Name);
-      Assert.AreEqual(1, type.TypeArgs.Count);
-      Assert.AreEqual("map", type.TypeArgs[0].Name);
-      Assert.AreEqual(2, type.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual("char", type.TypeArgs[0].TypeArgs[0].Name);
-      Assert.AreEqual("int", type.TypeArgs[0].TypeArgs[1].Name);
-      Assert.AreEqual(0, type.TypeArgs[0].TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, type.TypeArgs[0].TypeArgs[1].TypeArgs.Count);
+    public async Task DatatypeWithPredicate() {
+      var source = @"
+      module M {
+        datatype D = C(i:int) {
+          predicate p() {true}
+        }
+
+        method test(d: D) {
+          if (d.p()) {
+            assert d.i != 123;
+          }
+        }
+      }".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
+      Assert.AreEqual(1, counterExamples.Length);
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("d:M.D"));
+      Assert.AreEqual("C(i := 123)", counterExamples[0].Variables["d:M.D"]);
     }
 
+    /// <summary>
+    /// Test a situation in which two fields of an object are equal
+    /// (the value is represented by one Element in the Model)
+    /// </summary>
     [TestMethod]
-    public void DafnyModelTypeComplexCase() {
-      var type = DafnyModelType.FromString("Custom<Value<set<map<bv6, real>>>, map<char, int>, array<bool>>");
-      Assert.AreEqual("Custom", type.Name);
-      Assert.AreEqual(3, type.TypeArgs.Count);
-      var arg = type.TypeArgs[0];
-      Assert.AreEqual("Value", arg.Name);
-      Assert.AreEqual(1, arg.TypeArgs.Count);
-      arg = arg.TypeArgs[0];
-      Assert.AreEqual("set", arg.Name);
-      Assert.AreEqual(1, arg.TypeArgs.Count);
-      arg = arg.TypeArgs[0];
-      Assert.AreEqual("map", arg.Name);
-      Assert.AreEqual(2, arg.TypeArgs.Count);
-      Assert.AreEqual("bv6", arg.TypeArgs[0].Name);
-      Assert.AreEqual("real", arg.TypeArgs[1].Name);
-      Assert.AreEqual(0, arg.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, arg.TypeArgs[1].TypeArgs.Count);
-      arg = type.TypeArgs[1];
-      Assert.AreEqual("map", arg.Name);
-      Assert.AreEqual(2, arg.TypeArgs.Count);
-      Assert.AreEqual("char", arg.TypeArgs[0].Name);
-      Assert.AreEqual("int", arg.TypeArgs[1].Name);
-      Assert.AreEqual(0, arg.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, arg.TypeArgs[1].TypeArgs.Count);
-      arg = type.TypeArgs[2];
-      Assert.AreEqual("array", arg.Name);
-      Assert.AreEqual(1, arg.TypeArgs.Count);
-      arg = arg.TypeArgs[0];
-      Assert.AreEqual("bool", arg.Name);
-      Assert.AreEqual(0, arg.TypeArgs.Count);
+    public async Task EqualFields() {
+      var source = @"
+      module M {
+        class C { 
+          var c1:char;
+          var c2:char;
+        }
+
+        method test(c: C?) {
+          assert c == null || c.c1 != c.c2 || c.c1 != '\u1023';
+        }
+      }".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
+      Assert.AreEqual(1, counterExamples.Length);
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("c:M.C?"));
+      Assert.IsTrue(counterExamples[0].Variables["c:M.C?"] is
+        "(c1 := '\\u1023', c2 := '\\u1023')" or
+        "(c2 := '\\u1023', c1 := '\\u1023')");
     }
   }
 }

Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs

@@ -99,7 +99,7 @@ private CounterExampleItem GetCounterExample(DafnyModelState state) {
         return new(
           new Position(state.GetLineId() - 1, state.GetCharId()),
           vars.WithCancellation(cancellationToken).ToDictionary(
-            variable => variable.ShortName + ":" + variable.Type.InDafnyFormat(),
+            variable => variable.ShortName + ":" + DafnyModelTypeUtils.GetInDafnyFormat(variable.Type),
             variable => variable.Value
           )
         );