[Civl] Improvements to pool-based quantifier instantiation (#862)

- Added a pool hint to nondeterministic output parameter of One_New.
Since this procedure is polymorphic, the pool name "One_New" may
correspond to many types. Therefore, pool-based quantifier instantiation
is updated so that it can handle the same pool name attached to bound
variables of several types. The main idea is to be permissive in the
construction of instantiations but prune out illegal instances just
before the instantiation.

- Changed AtomicAllocNode in treiber-stack.bpl so that the output
variable ```success``` is explicitly initialized. This prevents
quantification over the initial (nondeterministic) value of
```success``` in the construction of the gate of AtomicAllocNode.
Ultimately, this results in better behaved VCs.

Together the two changes above reduce flakiness in the proof of
treiber-stack.bpl.

---------

Co-authored-by: Shaz Qadeer <[email protected]>

Source/Core/base.bpl

@@ -320,8 +320,9 @@ pure procedure {:inline 1} Map_Assume<K,V>({:linear} src: Map K V, {:linear} dst
 
 type Loc _;
 
-pure procedure {:inline 1} One_New<V>() returns ({:linear} l: One (Loc V))
+pure procedure {:inline 1} One_New<V>() returns ({:linear} {:pool "One_New"} l: One (Loc V))
 {
+  assume {:add_to_pool "One_New", l} true;
 }
 
 procedure create_async<T>(PA: T);

Source/VCExpr/QuantifierInstantiationEngine.cs

@@ -51,7 +51,7 @@ public QuantifierInstantiationInfo(Dictionary<VCExprVar, HashSet<string>> boundV
     private string skolemConstantNamePrefix;
     internal VCExpressionGenerator vcExprGen;
     private Boogie2VCExprTranslator exprTranslator;
-    internal static ConcurrentDictionary<string, Type> labelToType = new();
+    internal static ConcurrentDictionary<string, HashSet<Type>> labelToTypes = new(); // pool name may map to multiple types
 
     public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr)
     {
@@ -199,18 +199,11 @@ public static HashSet<string> FindInstantiationHints(Variable v)
             if (x is string poolName)
             {
               labels.Add(poolName);
-              if (labelToType.ContainsKey(poolName))
+              if (!labelToTypes.ContainsKey(poolName))
               {
-                if (!v.TypedIdent.Type.Equals(labelToType[poolName]))
-                {
-                  Console.WriteLine(
-                    $"{tok.filename}({tok.line},{tok.col}): conflicting type for pool {poolName} used earlier with type {labelToType[poolName]}");
-                }
-              }
-              else
-              {
-                labelToType[poolName] = v.TypedIdent.Type;
+                labelToTypes[poolName] = new();
               }
+              labelToTypes[poolName].Add(v.TypedIdent.Type);
             }
             else
             {
@@ -457,6 +450,16 @@ private void InstantiateQuantifierAtInstance(VCExprQuantifier quantifierExpr, Li
       {
         return;
       }
+
+      // Since a pool name may be used with multiple types, we have to prune invalid instances
+      for (int i = 0; i < quantifierExpr.BoundVars.Count; i++)
+      {
+        if (!quantifierExpr.BoundVars[i].Type.Equals(instance[i].Type))
+        {
+          return;
+        }
+      }
+
       var subst = new VCExprSubstitution(
         Enumerable.Range(0, quantifierExpr.BoundVars.Count).ToDictionary(
           x => quantifierExpr.BoundVars[x],
@@ -852,20 +855,16 @@ private void FindInstantiationSources(ICarriesAttributes o)
       {
         if (iter.Key == "add_to_pool")
         {
-          if (iter.Params[0] is string poolName && QuantifierInstantiationEngine.labelToType.ContainsKey(poolName))
+          if (iter.Params[0] is string poolName && QuantifierInstantiationEngine.labelToTypes.ContainsKey(poolName))
           {
             var tok = iter.tok;
-            var type = QuantifierInstantiationEngine.labelToType[poolName];
+            var poolTypes = QuantifierInstantiationEngine.labelToTypes[poolName];
             iter.Params.Skip(1).ForEach(x =>
             {
-              if (x is Expr e && e.Type.Equals(type))
+              if (x is Expr e && poolTypes.Contains(e.Type))
               {
                 hasInstances = true;
               }
-              else
-              {
-                Console.WriteLine($"{tok.filename}({tok.line},{tok.col}): expected expression of type {type}");
-              }
             });
           }
         }

Test/civl/samples/treiber-stack.bpl

@@ -138,7 +138,9 @@ modifies ts;
   var {:linear} stack: Map (Loc (Node X)) (Node X);
   var {:linear} one_loc_n: One (Loc (Node X));
 
-  if (success) {
+  success := false;
+  if (*) {
+    success := true;
     call one_loc_t, treiber := Map_Get(ts, loc_t);
     Treiber(top, stack) := treiber;
     call one_loc_n := One_New();