Merge pull request #706 from viperproject/meilers_report_early_on_parrBranch

Report errors early with --parallelizeBranches

Author: marcoeilers

src/main/scala/interfaces/Verification.scala

@@ -26,6 +26,7 @@ import viper.silver.ast.Program
 sealed abstract class VerificationResult {
   var previous: Vector[VerificationResult] = Vector() //Sets had problems with equality
   val continueVerification: Boolean = true
+  var isReported: Boolean = false
 
   def isFatal: Boolean
   def &&(other: => VerificationResult): VerificationResult

src/main/scala/rules/Brancher.scala

@@ -10,10 +10,13 @@ import java.util.concurrent._
 import viper.silicon.common.concurrency._
 import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Unreachable, VerificationResult}
+import viper.silicon.reporting.condenseToViperResult
 import viper.silicon.state.State
 import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
+import viper.silver.reporter.{BranchFailureMessage}
+import viper.silver.verifier.Failure
 
 trait BranchingRules extends SymbolicExecutionRules {
   def branch(s: State,
@@ -151,17 +154,25 @@ object brancher extends BranchingRules {
         CompletableFuture.completedFuture(Seq(Unreachable()))
       }
 
-    val res = (if (executeThenBranch) {
-      v.symbExLog.markReachable(uidBranchPoint)
-      executionFlowController.locally(s, v)((s1, v1) => {
-        v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
-        v1.decider.setCurrentBranchCondition(condition, conditionExp)
+    val res = {
+      val thenRes = if (executeThenBranch) {
+          v.symbExLog.markReachable(uidBranchPoint)
+          executionFlowController.locally(s, v)((s1, v1) => {
+            v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
+            v1.decider.setCurrentBranchCondition(condition, conditionExp)
 
-        fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
-      })
-    } else {
-      Unreachable()
-    }).combine({
+            fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
+          })
+        } else {
+          Unreachable()
+        }
+      if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) {
+        thenRes.isReported = true
+        v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable],
+          condenseToViperResult(Seq(thenRes)).asInstanceOf[Failure]))
+      }
+      thenRes
+    }.combine({
 
       /* [BRANCH-PARALLELISATION] */
       var rs: Seq[VerificationResult] = null
@@ -189,6 +200,11 @@ object brancher extends BranchingRules {
       }
 
       assert(rs.length == 1, s"Expected a single verification result but found ${rs.length}")
+      if (rs.head.isFatal && !rs.head.isReported && s.parallelizeBranches && s.isLastRetry) {
+        rs.head.isReported = true
+        v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable],
+          condenseToViperResult(Seq(rs.head)).asInstanceOf[Failure]))
+      }
       rs.head
 
     }, alwaysWaitForOther = parallelizeElseBranch)

src/main/scala/state/State.scala

@@ -20,6 +20,7 @@ import viper.silicon.{Map, Stack}
 final case class State(g: Store = Store(),
                        h: Heap = Heap(),
                        program: ast.Program,
+                       currentMember: Option[ast.Member],
                        predicateData: Map[ast.Predicate, PredicateData],
                        functionData: Map[ast.Function, FunctionData],
                        oldHeaps: OldHeaps = Map.empty,
@@ -64,13 +65,19 @@ final case class State(g: Store = Store(),
                        /* TODO: Isn't this data stable, i.e. fully known after a preprocessing step? If so, move it to the appropriate supporter. */
                        predicateSnapMap: Map[ast.Predicate, terms.Sort] = Map.empty,
                        predicateFormalVarMap: Map[ast.Predicate, Seq[terms.Var]] = Map.empty,
-                       isMethodVerification: Boolean = false,
                        retryLevel: Int = 0,
                        /* ast.Field, ast.Predicate, or MagicWandIdentifier */
                        heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty,
                        moreCompleteExhale: Boolean = false)
     extends Mergeable[State] {
 
+  val isMethodVerification: Boolean = {
+    // currentMember being None means we're verifying a CFG; this should behave like verifying a method.
+    currentMember.isEmpty || currentMember.get.isInstanceOf[ast.Method]
+  }
+
+  val isLastRetry: Boolean = retryLevel == 0
+
   def incCycleCounter(m: ast.Predicate) =
     if (recordVisited) copy(visited = m :: visited)
     else this
@@ -128,7 +135,7 @@ object State {
   def merge(s1: State, s2: State): State = {
     s1 match {
       /* Decompose state s1 */
-      case State(g1, h1, program,
+      case State(g1, h1, program, member,
                  predicateData,
                  functionData,
                  oldHeaps1,
@@ -148,13 +155,13 @@ object State {
                  reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
                  ssCache1, hackIssue387DisablePermissionConsumption1,
                  qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
-                 predicateSnapMap1, predicateFormalVarMap1, hack, retryLevel, useHeapTriggers,
+                 predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
                  moreCompleteExhale) =>
 
         /* Decompose state s2: most values must match those of s1 */
         s2 match {
           case State(`g1`, `h1`,
-                     `program`,
+                     `program`, `member`,
                      `predicateData`, `functionData`,
                      `oldHeaps1`,
                      `parallelizeBranches1`,
@@ -173,7 +180,7 @@ object State {
                      `reserveHeaps1`, `reserveCfgs1`, `conservedPcs1`, `recordPcs1`, `exhaleExt1`,
                      ssCache2, `hackIssue387DisablePermissionConsumption1`,
                      `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`,
-                     `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`, `retryLevel`, `useHeapTriggers`,
+                     `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
                      moreCompleteExhale2) =>
 
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -311,7 +311,7 @@ class DefaultMainVerifier(config: Config,
           qpMagicWands = quantifiedMagicWands,
           predicateSnapMap = predSnapGenerator.snapMap,
           predicateFormalVarMap = predSnapGenerator.formalVarMap,
-          isMethodVerification = member.isInstanceOf[ast.Member],
+          currentMember = Some(member),
           heapDependentTriggers = resourceTriggers,
           moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete)
   }
@@ -326,6 +326,7 @@ class DefaultMainVerifier(config: Config,
 
     State(
       program = program,
+      currentMember = None,
       functionData = functionData,
       predicateData = predicateData,
       qpFields = quantifiedFields,