Merge branch 'master' into no-fork-fuzzing

Source/DafnyDriver/CliCompilation.cs

@@ -315,4 +315,6 @@ record VerificationStatistics {
   public int OutOfResourceCount;
   public int OutOfMemoryCount;
   public int SolverExceptionCount;
+  public int TotalResourcesUsed;
+  public int MaxVcResourcesUsed;
 }

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -20,8 +20,15 @@ static VerifyCommand() {
     // they can't be specified when building a doo file.
     OptionRegistry.RegisterOption(FilterSymbol, OptionScope.Cli);
     OptionRegistry.RegisterOption(FilterPosition, OptionScope.Cli);
+    OptionRegistry.RegisterOption(PerformanceStatisticsOption, OptionScope.Cli);
   }
 
+  public static readonly Option<int> PerformanceStatisticsOption = new("--performance-stats",
+    "Report a summary of the verification performance. " +
+    "The given argument is used to divide all the output with, which can help ignore small differences.") {
+    IsHidden = true
+  };
+
   public static readonly Option<string> FilterSymbol = new("--filter-symbol",
     @"Filter what gets verified by selecting only symbols whose fully qualified name contains the given argument. For example: ""--filter-symbol=MyNestedModule.MyFooFunction""");
 
@@ -40,6 +47,7 @@ public static Command Create() {
 
   private static IReadOnlyList<Option> VerifyOptions =>
     new Option[] {
+        PerformanceStatisticsOption,
         FilterSymbol,
         FilterPosition,
         DafnyFile.DoNotVerifyDependencies
@@ -80,6 +88,10 @@ public static async Task ReportVerificationSummary(
     verificationResults.Subscribe(result => {
       foreach (var taskResult in result.Results) {
         var runResult = taskResult.Result;
+        Interlocked.Add(ref statistics.TotalResourcesUsed, runResult.ResourceCount);
+        lock (statistics) {
+          statistics.MaxVcResourcesUsed = Math.Max(statistics.MaxVcResourcesUsed, runResult.ResourceCount);
+        }
 
         switch (runResult.Outcome) {
           case SolverOutcome.Valid:
@@ -114,6 +126,16 @@ public static async Task ReportVerificationSummary(
     });
     await verificationResults.WaitForComplete();
     await WriteTrailer(cliCompilation, statistics);
+    var performanceStatisticsDivisor = cliCompilation.Options.Get(PerformanceStatisticsOption);
+    if (performanceStatisticsDivisor != 0) {
+      int Round(int number) {
+        var numberForUpRounding = number + performanceStatisticsDivisor / 2;
+        return (numberForUpRounding / performanceStatisticsDivisor) * performanceStatisticsDivisor;
+      }
+      var output = cliCompilation.Options.OutputWriter;
+      await output.WriteLineAsync($"Total resources used is {Round(statistics.TotalResourcesUsed)}");
+      await output.WriteLineAsync($"Max resources used by VC is {Round(statistics.MaxVcResourcesUsed)}");
+    }
   }
 
   private static async Task WriteTrailer(CliCompilation cliCompilation,

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

@@ -1650,8 +1650,8 @@ impl<V: DafnyTypeEq> PartialOrd<Multiset<V>> for Multiset<V> {
     fn partial_cmp(&self, other: &Multiset<V>) -> Option<Ordering> {
         match self.cardinality().cmp(&other.cardinality()) {
             Ordering::Less => {
-                for value in other.data.keys() {
-                    if !self.contains(value) || self.get(value) > other.get(value) {
+                for value in self.data.keys() {
+                    if !other.contains(value) || self.get(value) > other.get(value) {
                         return None;
                     }
                 }
@@ -1666,8 +1666,8 @@ impl<V: DafnyTypeEq> PartialOrd<Multiset<V>> for Multiset<V> {
                 Some(Ordering::Equal)
             }
             Ordering::Greater => {
-                for value in self.data.keys() {
-                    if !other.contains(value) || self.get(value) < other.get(value) {
+                for value in other.data.keys() {
+                    if !self.contains(value) || self.get(value) < other.get(value) {
                         return None;
                     }
                 }

Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs

@@ -1,4 +1,3 @@
-pub mod experimental;
 // Test module
 #[cfg(test)]
 mod tests {
@@ -132,6 +131,73 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_dafny_multisubset() {
+        let s = multiset! {55, 56, 57, 58, 59};
+        let t = multiset! {55, 56, 57, 58};
+        assert!(t < s);
+        assert!(t <= s);
+        assert!(s > t);
+        assert!(s >= t);
+        assert!(s != t);
+        assert!(t != s);
+
+        assert!(!(t > s));
+        assert!(!(t >= s));
+        assert!(!(s < t));
+        assert!(!(s <= t));
+        assert!(!(s == t));
+        assert!(!(t == s));
+
+        let s = multiset! {55, 56, 57, 58, 58};
+        let t = multiset! {55, 56, 57, 58};
+        assert!(t < s);
+        assert!(t <= s);
+        assert!(s > t);
+        assert!(s >= t);
+        assert!(s != t);
+        assert!(t != s);
+
+        assert!(!(t > s));
+        assert!(!(t >= s));
+        assert!(!(s < t));
+        assert!(!(s <= t));
+        assert!(!(s == t));
+        assert!(!(t == s));
+
+        let s = multiset! {55, 56, 57, 58, 59};
+        let t = multiset! {55, 56, 57, 58, 59};
+        assert!(t <= s);
+        assert!(s <= t);
+        assert!(s >= t);
+        assert!(t >= s);
+        assert!(s == t);
+        assert!(t == s);
+
+        assert!(!(t < s));
+        assert!(!(t > s));
+        assert!(!(s > t));
+        assert!(!(s < t));
+        assert!(!(s != t));
+        assert!(!(t != s));
+
+        let s = multiset! {55, 56, 57, 58, 59};
+        let s = multiset! {55, 56, 57, 58, 58};
+        assert!(s != t);
+        assert!(t != s);
+
+        assert!(!(t < s));
+        assert!(!(t <= s));
+        assert!(!(t > s));
+        assert!(!(t >= s));
+        assert!(!(s < t));
+        assert!(!(s <= t));
+        assert!(!(s > t));
+        assert!(!(s >= t));
+        assert!(!(s == t));
+        assert!(!(t == s));
+    }
+
     #[test]
     fn test_dafny_multiset() {
         let s = multiset! {55, 56, 57, 56, 58};

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1
 
 
 codatatype Stream<T> = Cons(head: T, tail: Stream)

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect

@@ -31,3 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that
 CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 23 verified, 12 errors
+Total resources used is 770731
+Max resources used by VC is 60262

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %build "%s" --relax-definite-assignment --allow-axioms > "%t"
+// RUN: %exits-with 4 %verify "%s" --performance-stats=10 --relax-definite-assignment --allow-axioms > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module AssignmentToNat {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect

@@ -63,10 +63,10 @@ SubsetTypes.dfy(318,18): Error: value does not satisfy the subset constraints of
 SubsetTypes.dfy(323,20): Error: value does not satisfy the subset constraints of 'nat'
 SubsetTypes.dfy(330,20): Error: result of operation might violate newtype constraint for 'Nat'
 SubsetTypes.dfy(337,20): Error: result of operation might violate newtype constraint for 'Nat'
-SubsetTypes.dfy(343,18): Error: value does not satisfy the subset constraints of 'Nat'
 SubsetTypes.dfy(342,7): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
-SubsetTypes.dfy(348,18): Error: result of operation might violate newtype constraint for 'Nat'
+SubsetTypes.dfy(343,18): Error: value does not satisfy the subset constraints of 'Nat'
 SubsetTypes.dfy(347,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+SubsetTypes.dfy(348,18): Error: result of operation might violate newtype constraint for 'Nat'
 SubsetTypes.dfy(352,7): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
 SubsetTypes.dfy(360,21): Error: possible division by zero
 SubsetTypes.dfy(365,23): Error: possible division by zero
@@ -91,3 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold
 SubsetTypes.dfy(464,13): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
+Total resources used is 738270
+Max resources used by VC is 67520

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --performance-stats=1
 
 
 // Rustan Leino

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect

@@ -1,2 +1,4 @@
 
 Dafny program verifier finished with 15 verified, 0 errors
+Total resources used is 26054893
+Max resources used by VC is 15592113

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect

@@ -0,0 +1,4 @@
+
+Dafny program verifier finished with 15 verified, 0 errors
+Total resources used is 28044428
+Max resources used by VC is 16505967