Merge branch 'master' into parse-exp-without-decimal

boogie-org · Apr 9, 2024 · 44e2251 · 44e2251
2 parents 01ca761 + acc4377
commit 44e2251
Show file tree

Hide file tree

Showing 6 changed files with 34 additions and 26 deletions.
diff --git a/Source/Core/base.bpl b/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);

diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/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}");
-              }
             });
           }
         }

diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
@@ -327,10 +327,6 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.
       this.handler = handler;
 
       await thmProver.Reset(gen);
-      if (0 < rlimit)
-      {
-        timeout = 0;
-      }
       SetTimeout(timeout);
       SetRlimit(rlimit);
 

diff --git a/Test/civl/samples/treiber-stack.bpl b/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();

diff --git a/Test/prover/timelimit-and-rlimit.bpl b/Test/prover/timelimit-and-rlimit.bpl
@@ -0,0 +1,10 @@
+// RUN: %boogie /proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
+// CHECK: (set-option :timeout 1000)
+// CHECK: (set-option :rlimit 10000)
+procedure
+{:timeLimit 1}
+{:rlimit 10000}
+P1(a: int, b: int) {
+  assert (a + b) - (a * b) == (b + a) - (a * b);
+}
diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl
@@ -1,7 +1,7 @@
 // We use boogie here because parallel-boogie doesn't work well with -proverLog
 // RUN: %boogie -rlimit:800000 -proverLog:"%t.smt2" "%s"
 // RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
-// CHECK-L: (set-option :timeout 0)
+// CHECK-L: (set-option :timeout 4000)
 // CHECK-L: (set-option :rlimit 800000)
 // CHECK-L: (set-option :timeout 0)
 // CHECK-L: (set-option :rlimit 900000)
@@ -11,7 +11,7 @@
 // Depends on all output going to a single file, so incompatible with
 // batch mode.
 // UNSUPPORTED: batch_mode
-procedure {:timeLimit 4} /* timeLimit overridden by rlimit */ TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
+procedure {:timeLimit 4} TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
   requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
   requires 0 < len;
   ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);