Use Boogie's "argument" encoding for polymorphism (dafny-lang#4210)

This generally has better performance than the previously-default
"predicate" encoding, though a few tests need to be updated to pass with
this encoding.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

Source/DafnyCore/DafnyOptions.cs

@@ -243,7 +243,7 @@ public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter
       ErrorWriter = errorWriter;
       ErrorTrace = 0;
       Prune = true;
-      TypeEncodingMethod = Bpl.CoreOptions.TypeEncoding.Predicates;
+      TypeEncodingMethod = Bpl.CoreOptions.TypeEncoding.Arguments;
       NormalizeNames = true;
       EmitDebugInformation = false;
       Backend = new CsharpBackend(this);

Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs

@@ -21,8 +21,7 @@ await VerifyTrace(@"
  | :}
  | :
 [ ]:method {:rlimit 1} Test(s: seq<nat>)
-[=]:  requires |s| >= 1 && s[0] >= 0 {
-[=]:  assert fib(10) == 1; assert {:split_here} s[0] >= 0;
+[=]:  requires |s| >= 1 && s[0] >= 0 { assert fib(10) == 1; assert {:split_here} s[0] >= 0;
 [ ]:}", true, intermediates: false);
   }
 

Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy

@@ -746,7 +746,7 @@ abstract module {:options "/functionSyntax:4"} Dafny {
     }
   }
 
-  method {:tailrecursion} AppendOptimized<T>(builder: Vector<T>, e: Sequence<T>, stack: Vector<Sequence<T>>)
+  method {:tailrecursion} {:vcs_split_on_every_assert} AppendOptimized<T>(builder: Vector<T>, e: Sequence<T>, stack: Vector<Sequence<T>>)
     requires e.Valid()
     requires builder.Valid()
     requires stack.Valid()
@@ -765,24 +765,31 @@ abstract module {:options "/functionSyntax:4"} Dafny {
       // Length() if we add the invariant that no leaf nodes are empty.
       expect SizeAdditionInRange(stack.size, ONE_SIZE);
       stack.AddLast(concat.right);
+      label L1:
       AppendOptimized(builder, concat.left, stack);
+      assert builder.Value() == old@L1(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old@L1(stack.Value()));
     } else if e is LazySequence<T> {
       var lazy := e as LazySequence<T>;
       var boxed := lazy.box.Get();
       AppendOptimized(builder, boxed, stack);
+      assert builder.Value() == old(builder.Value()) + boxed.Value() + ConcatValueOnStack(old(stack.Value()));
     } else if e is ArraySequence<T> {
       var a := e as ArraySequence<T>;
       builder.Append(a.values);
       if 0 < stack.size {
         var next: Sequence<T> := stack.RemoveLast();
+        label L2:
         AppendOptimized(builder, next, stack);
+        assert builder.Value() == old@L2(builder.Value()) + next.Value() + ConcatValueOnStack(old@L2(stack.Value()));
       }
     } else {
       // I'd prefer to just call Sequence.ToArray(),
       // but Dafny doesn't support tail recursion optimization of mutually-recursive functions.
       // Alternatively we could use a datatype, which would be a significant rewrite.
       expect false, "Unsupported Sequence implementation";
+      assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value()));
     }
+    assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value()));
   }
 
   ghost function ConcatValueOnStack<T>(s: seq<Sequence<T>>): seq<T>

Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntimeFromDafny.go

@@ -94,16 +94,20 @@ func (_static *CompanionStruct_Default___) AppendOptimized(builder *Vector, e Se
       panic("dafnyRuntime.dfy[DafnyGo](766,6): " + (SeqOfString("expectation violation")).String())
     }
     (stack).AddLast((_4_concat).Right())
-    var _in0 *Vector = builder
-    _ = _in0
-    var _in1 Sequence = (_4_concat).Left()
-    _ = _in1
-    var _in2 *Vector = stack
-    _ = _in2
-    builder = _in0
-    e = _in1
-    stack = _in2
-    goto TAIL_CALL_START
+    {
+      var _in0 *Vector = builder
+      _ = _in0
+      var _in1 Sequence = (_4_concat).Left()
+      _ = _in1
+      var _in2 *Vector = stack
+      _ = _in2
+      builder = _in0
+      e = _in1
+      stack = _in2
+      goto TAIL_CALL_START
+      goto L0_0;
+    }
+  L0_0:
   } else if (func (_is_3 Sequence) bool {
     return InstanceOf(_is_3, (*LazySequence)(nil))
   }(e)) {
@@ -140,20 +144,24 @@ func (_static *CompanionStruct_Default___) AppendOptimized(builder *Vector, e Se
       _ = _out3
       _out3 = (stack).RemoveLast()
       _8_next = Companion_Sequence_.CastTo_(_out3)
-      var _in6 *Vector = builder
-      _ = _in6
-      var _in7 Sequence = _8_next
-      _ = _in7
-      var _in8 *Vector = stack
-      _ = _in8
-      builder = _in6
-      e = _in7
-      stack = _in8
-      goto TAIL_CALL_START
+      {
+        var _in6 *Vector = builder
+        _ = _in6
+        var _in7 Sequence = _8_next
+        _ = _in7
+        var _in8 *Vector = stack
+        _ = _in8
+        builder = _in6
+        e = _in7
+        stack = _in8
+        goto TAIL_CALL_START
+        goto L1_1_0_0_0;
+      }
+    L1_1_0_0_0:
     }
   } else {
     if (!(false)) {
-      panic("dafnyRuntime.dfy[DafnyGo](784,6): " + (SeqOfString("Unsupported Sequence implementation")).String())
+      panic("dafnyRuntime.dfy[DafnyGo](789,6): " + (SeqOfString("Unsupported Sequence implementation")).String())
     }
   }
 }

Test/VerifyThis2015/Problem1.dfy

@@ -156,7 +156,7 @@ lemma Prefix<T>(pat: seq<T>, a: seq<T>)
   ensures IsRelaxedPrefixAux(pat, a, 0)
 {
 }
-lemma Same2<T>(pat: seq<T>, a: seq<T>)
+lemma {:vcs_split_on_every_assert} Same2<T>(pat: seq<T>, a: seq<T>)
   requires IsRelaxedPrefixAux(pat, a, 1)
   ensures IRP_Alt(pat, a)
 {

Test/concurrency/11-MutexGuard2.dfy

@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /proverOpt:O:smt.qi.eager_threshold=30 "%s" > "%t"
+// RUN: %dafny /compile:0 /proverOpt:O:smt.qi.eager_threshold=30 /typeEncoding:p "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This program models the ownership of a Rust-like MutexGuard.

Test/dafny0/Fuel.dfy.expect

@@ -1,6 +1,7 @@
 Fuel.dfy(129,8): Error: Fuel can only increase within a given scope.
 Fuel.dfy(407,8): Error: Fuel can only increase within a given scope.
 Fuel.dfy(17,22): Error: assertion might not hold
+Fuel.dfy(65,27): Error: assertion might not hold
 Fuel.dfy(69,27): Error: assertion might not hold
 Fuel.dfy(92,22): Error: assertion might not hold
 Fuel.dfy(93,23): Error: assertion might not hold
@@ -20,13 +21,13 @@ Fuel.dfy(324,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,46): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
 Fuel.dfy(312,58): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(314,46): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
 Fuel.dfy(314,72): Related location
@@ -42,19 +43,19 @@ Fuel.dfy(329,21): Related location
 Fuel.dfy(311,43): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(313,41): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(314,93): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(314,93): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(313,41): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(336,71): Error: index out of range
 Fuel.dfy(397,22): Error: assertion might not hold
 Fuel.dfy(398,22): Error: assertion might not hold
@@ -63,4 +64,4 @@ Fuel.dfy(435,22): Error: assertion might not hold
 Fuel.dfy(436,22): Error: assertion might not hold
 Fuel.dfy(437,23): Error: assertion might not hold
 
-Dafny program verifier finished with 30 verified, 38 errors
+Dafny program verifier finished with 30 verified, 39 errors

Test/dafny1/Rippling.dfy

@@ -594,7 +594,7 @@ lemma P2_alt(n: Nat, xs: List, ys: List)
 
 // ---------
 
-lemma Lemma_RevConcat(xs: List, ys: List)
+lemma {:vcs_split_on_every_assert} Lemma_RevConcat(xs: List, ys: List)
   ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
 {
   match (xs) {

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

@@ -21,7 +21,7 @@ git-issue-1207.dfy(40,9): Error: assertion might not hold
 git-issue-1207.dfy(47,9): Error: assertion might not hold
 git-issue-1207.dfy(48,9): Error: assertion might not hold
 git-issue-1207.dfy(49,9): Error: assertion might not hold
-git-issue-1207.dfy(50,9): Error: assertion might not hold
-git-issue-1207.dfy(51,9): Error: assertion might not hold
+git-issue-1207.dfy(50,49): Error: index out of range
+git-issue-1207.dfy(50,57): Error: index out of range
 
 Dafny program verifier finished with 0 verified, 20 errors

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

@@ -8,24 +8,29 @@ git-issue-2026.dfy(12,0): initial state:
 	ret : _System.array<seq<char>> = ()
 git-issue-2026.dfy(13,24):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
-	@0 : seq<char> = ['o', 'd', 'd']
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 1)] := @0, [0] := @1)
+	@0 : ? = ?
+	@1 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(15,14):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 1)] := @0, [0] := @1)
 	i : int = 0
-	@0 : seq<char> = ['o', 'd', 'd']
+	@0 : ? = ?
+	@1 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(16,4): after some loop iterations:
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 1)] := @0)
 	i : int = 0
+	@0 : ? = ?
 git-issue-2026.dfy(22,27):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 1)] := @0, [0] := @1)
 	i : int = 0
-	@0 : seq<char> = ['o', 'd', 'd']
+	@0 : ? = ?
+	@1 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(26,18):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 1)] := @0, [0] := @1)
 	i : int = 1
-	@0 : seq<char> = ['o', 'd', 'd']
+	@0 : ? = ?
+	@1 : seq<char> = ['o', 'd', 'd']

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

@@ -10,10 +10,10 @@ git-issue-2299.dfy(81,11): Error: assertion might not hold
 git-issue-2299.dfy(27,4): Related location
 git-issue-2299.dfy(10,11): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
-git-issue-2299.dfy(27,18): Related location
-git-issue-2299.dfy(16,4): Related location
-git-issue-2299.dfy(81,11): Error: assertion might not hold
 git-issue-2299.dfy(27,32): Related location
 git-issue-2299.dfy(21,4): Related location
+git-issue-2299.dfy(81,11): Error: assertion might not hold
+git-issue-2299.dfy(27,18): Related location
+git-issue-2299.dfy(16,4): Related location
 
 Dafny program verifier finished with 7 verified, 7 errors

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

@@ -637,7 +637,7 @@ function partitionOfJustHeapRegions(os : set<Object>) : (partition : map<Region,
 }
 
 
-  method {:timeLimit 15}  fNullify(o : Object, f : string) 
+method {:timeLimit 15}  {:vcs_split_on_every_assert} fNullify(o : Object, f : string)
     requires o  in objects
     requires f  in o.fieldModes
     requires f  in o.fields