Avoid concurrency errors when combining /randomizeVcIterations and /trackVerificationCoverage

Source/Houdini/HoudiniSession.cs

@@ -1,4 +1,5 @@
 using System;
+using System.Collections.Concurrent;
 using System.Diagnostics.Contracts;
 using System.Collections.Generic;
 using System.IO;
@@ -126,7 +127,7 @@ public class HoudiniStatistics
     private readonly Houdini houdini;
     public HoudiniStatistics stats;
     public List<Counterexample> Counterexamples { get; } = new();
-    public HashSet<TrackedNodeComponent> CoveredElements { get; } = new();
+    public ConcurrentBag<TrackedNodeComponent> CoveredElements { get; } = new();
     private VCExpr conjecture;
     private ProverInterface.ErrorHandler handler;
     VerificationResultCollector collector;

Source/VCGeneration/ProofRun.cs

@@ -1,3 +1,4 @@
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using Microsoft.Boogie;
 
@@ -8,5 +9,5 @@ public interface ProofRun {
 
   List<Counterexample> Counterexamples { get; }
 
-  HashSet<TrackedNodeComponent> CoveredElements { get;  }
+  ConcurrentBag<TrackedNodeComponent> CoveredElements { get;  }
 }

Source/VCGeneration/Split.cs

@@ -1,4 +1,5 @@
 using System;
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Linq;
@@ -912,7 +913,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie
 
       public List<Counterexample> Counterexamples { get; } = new();
 
-      public HashSet<TrackedNodeComponent> CoveredElements { get; } = new();
+      public ConcurrentBag<TrackedNodeComponent> CoveredElements { get; } = new();
 
       /// <summary>
       /// As a side effect, updates "this.parent.CumulativeAssertionCount".

Test/coverage/verificationCoverageConcurrent.bpl

@@ -0,0 +1,106 @@
+// Use many cores to be more likely to trigger concurrent access.
+// Success is simply that it doesn't crash.
+// RUN: %boogie -vcsCores:8 -trackVerificationCoverage -randomizeVcIterations:10 "%s"
+
+procedure testRequiresAssign(n: int)
+  requires {:id "r0"} n > 0; // covered
+  requires {:id "r_not_1"} n < 10; // not covered
+{
+    var x: int;
+    x := {:id "a0"} n + 1; // covered
+    assert {:id "assert_a0"} x == n + 1; // covered
+    x := {:id "a_not_1"} 0; // not covered
+    assert {:id "assert_r0"} n > 0; // covered
+}
+
+procedure sum(n: int) returns (s: int)
+  requires {:id "spre1"} n >= 0; // covered
+  ensures {:id "spost"} s == (n * (n + 1)) div 2; // covered
+{
+  var i: int;
+  var foo: int;
+
+  i := 0;
+  s := 0;
+  foo := 27;
+  while (i < n)
+    invariant {:id "sinv1"} 0 <= i && i <= n; // covered: established, maintained, assumed
+    invariant {:id "sinv2"} s == (i * (i + 1)) div 2; // covered: established, maintained, assumed
+    invariant {:id "sinv_not_1"} n >= 0; // covered: established, maintained, NOT assumed
+  {
+    i := i + 1;
+    s := s + i;
+    foo := {:id "update_foo"} foo * 2; // not covered
+  }
+}
+
+procedure contradictoryAssume(n: int)
+{
+    assume {:id "cont_assume_1"} n > 0; // covered
+    assume {:id "cont_assume_2"} n < 0; // covered
+    assume {:id "unreach_assume_1"} n == 5; // not covered
+    assert {:id "unreach_assert_1"} n < 10; // not covered
+}
+
+// NB: an explicit `requires false` leads to _nothing_ being covered
+procedure falseRequires(n: int)
+  requires {:id "false_req"} n != n; // covered
+{
+    assert {:id "false_assert"} false; // not covered
+}
+
+procedure contradictoryRequires(n: int)
+  requires {:id "cont_req_1"} n > 0; // covered
+  requires {:id "cont_req_2"} n < 0; // covered
+{
+    assume {:id "n_eq_5"} n == 5; // not covered
+    assert {:id "n_lt_10"} n > 10; // not covered
+}
+
+procedure assumeFalse() {
+  assume {:id "assumeFalse"} false; // covered
+  assert {:id "assertSimple"} 1 + 1 == 2; // not covered
+}
+
+procedure testEnsuresCallee(n: int) returns (r: int)
+  requires {:id "ter0"} n > 0; // covered
+  ensures {:id "tee0"} r > n; // covered by this procedure and caller
+  ensures {:id "tee1"} r > 0; // covered when proving this procedure, not from caller
+{
+  r := n + 1;
+}
+
+procedure testEnsuresCaller(n: int) returns (r: int)
+  requires {:id "ter1"} n > 0; // covered
+  ensures {:id "tee_not_1"} r > n; // covered
+{
+  var x: int;
+  var y: int;
+  call {:id "call1"} x := testEnsuresCallee(n+1); // requires and ensures covered
+  call {:id "call2"} y := testEnsuresCallee(n+1); // requires and ensures covered
+  assert {:id "call2_tee1"} y > 0;
+  r := {:id "xy_sum"} x + y; // covered
+}
+
+procedure obviouslyUnconstrainedCode(x: int) returns (a: int, b: int)
+  requires {:id "x_gt_10"} x > 10; // covered
+  requires {:id "x_lt_100"} x < 100; // not covered
+  ensures {:id "a_gt_10"} a > 10; // covered
+{
+  a := {:id "constrained"} x + 1;     // covered: constrained by ensures clause
+  b := {:id "not_constrained"} x - 1; // not covered: not constrained by ensures clause
+}
+
+
+procedure contradictoryEnsuresClause(x: int) returns (r: int);
+  requires {:id "xpos_abs"} x > 1; // covered (established by caller)
+  ensures  {:id "cont_ens_abs"} r > x && r < 0; // covered (used by caller proof)
+
+// Call function that has contradictory ensures clauses.
+procedure callContradictoryFunction(x: int) returns (r: int)
+  requires {:id "xpos_caller"} x > 1; // covered
+  ensures {:id "caller_ensures"} r < 0; // not covered
+{
+  call {:id "call_cont"} r := contradictoryEnsuresClause(x); // requires and ensures covered
+  r := {:id "unreachable_assignment"} r - 1; // not covered
+}