Merge

.github/workflows/update-submodules.yml

@@ -0,0 +1,65 @@
+# This Source Code Form is subject to the terms of the Mozilla Public
+# License, v. 2.0. If a copy of the MPL was not distributed with this
+# file, You can obtain one at http://mozilla.org/MPL/2.0/.
+#
+# Copyright (c) 2011-2022 ETH Zurich.
+
+name: Update Submodules
+
+on:
+  workflow_dispatch: # allow to manually trigger this workflow
+  schedule:
+    - cron: '0 6 * * *' # run every day at 06:00 UTC
+
+jobs:
+  # Update silver and create a PR if there are any changes
+  update:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out the repo
+        uses: actions/checkout@v3
+        with:
+          submodules: true
+
+      - name: Get current commits
+        run: echo "PREV_SILVER_REF=$(git -C silver rev-parse HEAD)" >> $GITHUB_ENV
+
+      - name: Update Silver submodule
+        run: git checkout master && git pull
+        working-directory: silver
+
+      - name: Get new commits
+        run: echo "CUR_SILVER_REF=$(git -C silver rev-parse HEAD)" >> $GITHUB_ENV
+
+      - name: Create PR body
+        run: |
+          if [[ "${{ env.PREV_SILVER_REF }}" != "${{ env.CUR_SILVER_REF }}" ]]; then
+            echo 'PR_BODY_LINE=* Updates Silver from `${{ env.PREV_SILVER_REF }}` to `${{ env.CUR_SILVER_REF }}`.' >> $GITHUB_ENV
+          else
+            echo 'PR_BODY_LINE=' >> $GITHUB_ENV
+          fi
+
+      - name: Open a pull request
+        id: pr
+        uses: peter-evans/create-pull-request@v4
+        if: (env.PREV_SILVER_REF != env.CUR_SILVER_REF)
+        with:
+          # Use viper-admin's token to workaround a restriction of GitHub.
+          # See: https://github.com/peter-evans/create-pull-request/issues/48
+          token: ${{ secrets.UPDATE_SILVER }}
+          commit-message: Updates submodules
+          title: Update Submodules
+          branch: auto-update-submodules
+          delete-branch: true
+          labels: |
+            automated pr
+          body: |
+            ${{ env.PR_BODY_LINE1 }}
+
+      - name: Enable auto-merge of PR
+        uses: peter-evans/create-or-update-comment@v2
+        if: (env.PREV_SILVER_REF != env.CUR_SILVER_REF)
+        with:
+          token: ${{ secrets.UPDATE_SILVER }}
+          issue-number: ${{ steps.pr.outputs.pull-request-number }}"
+          body: bors merge

src/main/scala/Config.scala

@@ -672,6 +672,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
+    descr = "Enable more joins using a more complete implementation of state merging.",
+    default = Some(false),
+    noshort = true
+  )
+
   val exhaleModeOption: ScallopOption[ExhaleMode] = opt[ExhaleMode]("exhaleMode",
     descr = "Exhale mode. Options are 0 (greedy, default), 1 (more complete exhale), 2 (more complete exhale on demand).",
     default = None,
@@ -700,8 +706,10 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   )(singleArgConverter(mode => StateConsolidationMode(mode.toInt)))
 
   val numberOfParallelVerifiers: ScallopOption[Int] = opt[Int]("numberOfParallelVerifiers",
-    descr = (  "Number of verifiers run in parallel. This number plus one is the number of provers "
-             + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()})"),
+    descr = ( "Number of verifiers (and therefore also prover instances) run in parallel for method verification." +
+              "A value of 1 leads to sequential method verification. " +
+              "Functions and predicates are always verified sequentially on a separate prover instance. " +
+             s"Default: ${Runtime.getRuntime.availableProcessors()}"),
     default = Some(Runtime.getRuntime.availableProcessors()),
     noshort = true
   )
@@ -831,6 +839,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => Right(())
   }
 
+  validateOpt(numberOfParallelVerifiers) {
+    case Some(n) if n <= 0 => Left(s"Number of parallel verifiers must be positive, but $n was provided")
+    case _ => Right()
+  }
+
   validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)
   validateFileOpt(multisetAxiomatizationFile)

src/main/scala/decider/Decider.scala

@@ -22,6 +22,7 @@ import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage}
 
 import scala.collection.immutable.HashSet
+import scala.collection.mutable
 
 /*
  * Interfaces
@@ -75,8 +76,10 @@ trait Decider {
   // slower, so this tradeoff seems worth it.
   def freshFunctions: Set[FunctionDecl]
   def freshMacros: Vector[MacroDecl]
-  def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit
-  def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
+  def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toStack: Boolean): Unit
+  def declareAndRecordAsFreshMacros(functions: Seq[MacroDecl], toStack: Boolean): Unit
+  def pushSymbolStack(): Unit
+  def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl])
   def setPcs(other: PathConditionStack): Unit
 
   def statistics(): Map[String, String]
@@ -99,8 +102,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     private var _prover: Prover = _
     private var pathConditions: PathConditionStack = _
 
-    private var _freshFunctions: Set[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
-    private var _freshMacros: Vector[MacroDecl] = _
+    private var _declaredFreshFunctions: Set[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
+    private var _declaredFreshMacros: Vector[MacroDecl] = _
+
+    private var _freshFunctionStack: Stack[mutable.HashSet[FunctionDecl]] = _
+    private var _freshMacroStack: Stack[mutable.ListBuffer[MacroDecl]] = _
 
     def prover: Prover = _prover
 
@@ -167,16 +173,20 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def start(): Unit = {
       pathConditions = new LayeredPathConditionStack()
-      _freshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
-      _freshMacros = Vector.empty
+      _declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
+      _declaredFreshMacros = Vector.empty
+      _freshMacroStack = Stack.empty
+      _freshFunctionStack = Stack.empty
       createProver()
     }
 
     def reset(): Unit = {
       _prover.reset()
       pathConditions = new LayeredPathConditionStack()
-      _freshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
-      _freshMacros = Vector.empty
+      _declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
+      _declaredFreshMacros = Vector.empty
+      _freshMacroStack = Stack.empty
+      _freshFunctionStack = Stack.empty
     }
 
     def stop(): Unit = {
@@ -332,7 +342,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
       prover.declare(macroDecl)
 
-      _freshMacros = _freshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
+      _declaredFreshMacros = _declaredFreshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
+      _freshMacroStack.foreach(l => l.append(macroDecl))
 
       macroDecl
     }
@@ -368,26 +379,61 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
               HeapDepFun(proverFun.id, proverFun.argSorts, proverFun.resultSort).asInstanceOf[F]
           }
 
-      _freshFunctions = _freshFunctions + FunctionDecl(fun) /* [BRANCH-PARALLELISATION] */
+      val decl = FunctionDecl(fun)
+      _declaredFreshFunctions = _declaredFreshFunctions + decl /* [BRANCH-PARALLELISATION] */
+      _freshFunctionStack.foreach(s => s.add(decl))
 
       fun
     }
 
 
 /* [BRANCH-PARALLELISATION] */
-    def freshFunctions: Set[FunctionDecl] = _freshFunctions
-    def freshMacros: Vector[MacroDecl] = _freshMacros
+    def freshFunctions: Set[FunctionDecl] = _declaredFreshFunctions
+    def freshMacros: Vector[MacroDecl] = _declaredFreshMacros
+
+    def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
+      if (!toSymbolStack) {
+        functions foreach prover.declare
 
-    def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit = {
-      functions foreach prover.declare
+        _declaredFreshFunctions = _declaredFreshFunctions ++ functions
+      } else {
+        for (f <- functions) {
+          if (!_declaredFreshFunctions.contains(f))
+            prover.declare(f)
 
-      _freshFunctions = _freshFunctions ++ functions
+          _declaredFreshFunctions = _declaredFreshFunctions + f
+          _freshFunctionStack.foreach(s => s.add(f))
+        }
+      }
     }
 
-    def declareAndRecordAsFreshMacros(macros: Vector[MacroDecl]): Unit = {
-      macros foreach prover.declare
+    def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = {
+      if (!toStack) {
+        macros foreach prover.declare
+
+        _declaredFreshMacros = _declaredFreshMacros ++ macros
+      } else {
+        for (m <- macros) {
+          if (!_declaredFreshMacros.contains(m))
+            prover.declare(m)
+
+          _declaredFreshMacros = _declaredFreshMacros.appended(m)
+          _freshMacroStack.foreach(l => l.append(m))
+        }
+      }
+    }
+
+    def pushSymbolStack(): Unit = {
+      _freshFunctionStack = _freshFunctionStack.prepended(mutable.HashSet())
+      _freshMacroStack = _freshMacroStack.prepended(mutable.ListBuffer())
+    }
 
-      _freshMacros = _freshMacros ++ macros
+    def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl]) = {
+      val funcDecls = _freshFunctionStack.head.toSet
+      _freshFunctionStack = _freshFunctionStack.tail
+      val macroDecls = _freshMacroStack.head.toSeq
+      _freshMacroStack = _freshMacroStack.tail
+      (funcDecls, macroDecls)
     }
 
     /* Misc */

src/main/scala/decider/PathConditions.scala

@@ -69,12 +69,14 @@ private class PathConditionStackLayer
   private var _globalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _nonGlobalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _globalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
+  private var _nonGlobalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _declarations: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
   def branchCondition: Option[Term] = _branchCondition
   def branchConditionExp: Option[Option[ast.Exp]] = _branchConditionExp
   def globalAssumptions: InsertionOrderedSet[Term] = _globalAssumptions
-  def definingAssumptions: InsertionOrderedSet[Term] = _globalDefiningAssumptions
+  def globalDefiningAssumptions: InsertionOrderedSet[Term] = _globalDefiningAssumptions
+  def nonGlobalDefiningAssumptions: InsertionOrderedSet[Term] = _nonGlobalDefiningAssumptions
   def nonGlobalAssumptions: InsertionOrderedSet[Term] = _nonGlobalAssumptions
   def declarations: InsertionOrderedSet[Decl] = _declarations
 
@@ -84,6 +86,9 @@ private class PathConditionStackLayer
   def definitionsOnly(): PathConditionStackLayer = {
     val result = new PathConditionStackLayer
     result._globalAssumptions = _globalDefiningAssumptions
+    result._globalDefiningAssumptions = _globalDefiningAssumptions
+    result._nonGlobalAssumptions = _nonGlobalDefiningAssumptions
+    result._nonGlobalDefiningAssumptions = _nonGlobalDefiningAssumptions
     result._declarations = _declarations
     result
   }
@@ -122,9 +127,13 @@ private class PathConditionStackLayer
       !assumption.isInstanceOf[And],
       s"Unexpectedly found a conjunction (should have been split): $assumption")
 
-    //assert(PathConditions.isGlobal(assumption))
-    _globalAssumptions += assumption
-    _globalDefiningAssumptions += assumption
+    if (PathConditions.isGlobal(assumption)) {
+      _globalAssumptions += assumption
+      _globalDefiningAssumptions += assumption
+    } else {
+      _nonGlobalAssumptions += assumption
+      _nonGlobalDefiningAssumptions += assumption
+    }
   }
 
   def add(declaration: Decl): Unit = _declarations += declaration
@@ -158,7 +167,7 @@ private trait LayeredPathConditionStackLike {
     InsertionOrderedSet(layers.flatMap(_.assumptions)) // Note: Performance?
 
   protected def definingAssumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
-    InsertionOrderedSet(layers.flatMap(_.definingAssumptions)) // Note: Performance?
+    InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++ layers.flatMap(_.nonGlobalDefiningAssumptions)) // Note: Performance?
 
   protected def declarations(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
@@ -202,13 +211,24 @@ private trait LayeredPathConditionStackLike {
     val ignores = ignore.topLevelConjuncts
 
     for (layer <- layers) {
-      globals ++= layer.globalAssumptions
+      val actualBranchCondition = layer.branchCondition.getOrElse(True)
+      val relevantNonGlobals = layer.nonGlobalAssumptions -- ignores
+      val (trueNonGlobals, additionalGlobals) = if (!actualBranchCondition.existsDefined{ case t if qvars.contains(t) => }) {
+        // The branch condition is independent of all quantified variables
+        // Any assumptions that are also independent of all quantified variables can be treated as global assumptions.
+        val (trueNonGlobals, unconditionalGlobals) = relevantNonGlobals.partition(a => a.existsDefined{ case t if qvars.contains(t) => })
+        (trueNonGlobals, unconditionalGlobals.map(Implies(actualBranchCondition, _)))
+      } else {
+        (relevantNonGlobals, Seq())
+      }
+
+      globals ++= layer.globalAssumptions ++ additionalGlobals
 
       nonGlobals :+=
         Quantification(
           quantifier,
           qvars,
-          Implies(layer.branchCondition.getOrElse(True), And(layer.nonGlobalAssumptions -- ignores)),
+          Implies(actualBranchCondition, And(trueNonGlobals)),
           triggers,
           name,
           isGlobal)
@@ -352,7 +372,7 @@ private[decider] class LayeredPathConditionStack
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
 
   def definingAssumptions: InsertionOrderedSet[Term] =
-    InsertionOrderedSet(layers.flatMap(_.definingAssumptions)) // Note: Performance?
+    InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++ layers.flatMap(_.nonGlobalDefiningAssumptions)) // Note: Performance?
 
   def contains(assumption: Term): Boolean = allAssumptions.contains(assumption)
 
@@ -403,7 +423,8 @@ private[decider] class LayeredPathConditionStack
   override def definitionsOnly: RecordedPathConditions = {
     val result = duplicate()
     result.layers = layers map (_.definitionsOnly())
-    result.allAssumptions = InsertionOrderedSet(layers.flatMap(_.definingAssumptions))
+    result.allAssumptions = InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++
+      layers.flatMap(_.nonGlobalDefiningAssumptions))
     result
   }