Report One Error Per Path, Recover From Pure Assertions

src/main/scala/Config.scala

@@ -464,6 +464,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val numberOfErrorsToReport: ScallopOption[Int] = opt[Int]("numberOfErrorsToReport",
+    descr = "Number of errors per member before the verifier stops. If this number is set to 0, all errors are reported.",
+    default = Some(1),
+    noshort = true
+  )
+
   val stateConsolidationMode: ScallopOption[StateConsolidationMode] = opt[StateConsolidationMode]("stateConsolidationMode",
     descr = s"One of the following modes:\n${StateConsolidationMode.helpText}",
     default = Some(StateConsolidationMode.Default),
@@ -502,6 +508,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     default = Some(false),
     noshort = true
   )
+  val enableBranchconditionReporting: ScallopOption[Boolean] = opt[Boolean]("enableBranchconditionReorting",
+    descr = "Report branch conditions (can be useful for assertions that fail on multiple branches)",
+    default = Some(false),
+    noshort = true
+  )
 
   val setAxiomatizationFile: ScallopOption[String] = opt[String]("setAxiomatizationFile",
     descr =s"Source file with set axiomatisation. If omitted, built-in one is used.",

src/main/scala/Silicon.scala

@@ -17,7 +17,7 @@ import org.slf4j.LoggerFactory
 import viper.silver.ast
 import viper.silver.frontend.{DefaultStates, SilFrontend}
 import viper.silver.reporter._
-import viper.silver.verifier.{DefaultDependency => SilDefaultDependency, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
+import viper.silver.verifier.{Counterexample => SilCounterexample, DefaultDependency => SilDefaultDependency, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.Failure
 import viper.silicon.logger.SymbExLogger
@@ -27,6 +27,8 @@ import viper.silver.cfg.silver.SilverCfg
 import viper.silver.logger.ViperStdOutLogger
 import viper.silver.plugin.PluginAwareReporter
 
+import scala.util.chaining._
+
 object Silicon {
   val name = BuildInfo.projectName
 
@@ -247,12 +249,23 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     /*verifier.bookkeeper.*/elapsedMillis = System.currentTimeMillis() - /*verifier.bookkeeper.*/startTime
 
     val failures =
-      results.flatMap(r => r :: r.allPrevious)
-             .collect{ case f: Failure => f } /* Ignore successes */
-             .sortBy(_.message.pos match { /* Order failures according to source position */
-                case pos: ast.HasLineColumn => (pos.line, pos.column)
-                case _ => (-1, -1)
-             })
+      results.flatMap(r => r :: r.previous.toList)
+        .collect{ case f: Failure => f } /* Ignore successes */
+        .pipe(allResults => {
+          /* If branchconditions are to be reported we collect the different failure contexts
+          *  of all failures that report the same error (but on different branches, with different CounterExample)
+          *  and put those into one failure */
+          if (config.enableBranchconditionReporting())
+            allResults.groupBy(_.message.readableMessage(withId = true, withPosition = true)).map{case (_: String, fs:List[Failure]) =>
+              fs.head.message.failureContexts = fs.flatMap(_.message.failureContexts)
+              Failure(fs.head.message)
+            }.toList
+             else allResults.distinctBy(f => f.message.readableMessage(withId = true, withPosition = true))
+        })
+        .sortBy(_.message.pos match { /* Order failures according to source position */
+          case pos: ast.HasLineColumn => (pos.line, pos.column)
+          case _ => (-1, -1)
+        })
 
 //    if (config.showStatistics.isDefined) {
 //      val proverStats = verifier.decider.statistics()
@@ -283,7 +296,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     failures
   }
 
-  private def logFailure(failure: Failure, log: String => Unit): Unit = {
+  private def logFailure(failure: Failure, log: String => Unit): Unit = { //TODO:J log context?
     log("\n" + failure.message.readableMessage(withId = true, withPosition = true))
   }
 

src/main/scala/decider/Decider.scala

@@ -35,7 +35,7 @@ trait Decider {
 
   def checkSmoke(): Boolean
 
-  def setCurrentBranchCondition(t: Term): Unit
+  def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit
   def setPathConditionMark(): Mark
 
   def assume(t: Term): Unit
@@ -166,8 +166,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       //SymbExLogger.currentLog().closeScope(sepIdentifier)
     }
 
-    def setCurrentBranchCondition(t: Term): Unit = {
-      pathConditions.setCurrentBranchCondition(t)
+    def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit = {
+      pathConditions.setCurrentBranchCondition(t, te)
       assume(InsertionOrderedSet(Seq(t)))
     }
 

src/main/scala/decider/PathConditions.scala

@@ -10,7 +10,7 @@ import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.Stack
 import viper.silicon.state.terms._
 import viper.silicon.utils.Counter
-
+import viper.silver.ast
 /*
  * Interfaces
  */
@@ -22,6 +22,7 @@ import viper.silicon.utils.Counter
 
 trait RecordedPathConditions {
   def branchConditions: Stack[Term]
+  def branchConditionExps: Stack[Option[ast.Exp]]
   def assumptions: InsertionOrderedSet[Term]
   def declarations: InsertionOrderedSet[Decl]
 
@@ -39,7 +40,7 @@ trait RecordedPathConditions {
 }
 
 trait PathConditionStack extends RecordedPathConditions {
-  def setCurrentBranchCondition(condition: Term): Unit
+  def setCurrentBranchCondition(condition: Term, conditionExp: Option[ast.Exp]): Unit
   def add(assumption: Term): Unit
   def add(declaration: Decl): Unit
   def pushScope(): Unit
@@ -59,11 +60,13 @@ private class PathConditionStackLayer
     extends Cloneable {
 
   private var _branchCondition: Option[Term] = None
+  private var _branchConditionExp: Option[Option[ast.Exp]] = None
   private var _globalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _nonGlobalAssumptions: 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 nonGlobalAssumptions: InsertionOrderedSet[Term] = _nonGlobalAssumptions
   def declarations: InsertionOrderedSet[Decl] = _declarations
@@ -79,6 +82,14 @@ private class PathConditionStackLayer
     _branchCondition = Some(condition)
   }
 
+  def branchConditionExp_=(condition: Option[ast.Exp]): Unit = {
+    assert(_branchConditionExp.isEmpty,
+      s"Branch condition is already set (to ${_branchConditionExp.get}), "
+        + s"won't override (with $condition).")
+
+    _branchConditionExp = Some(condition)
+  }
+
   def add(assumption: Term): Unit = {
     assert(
       !assumption.isInstanceOf[And],
@@ -116,6 +127,9 @@ private trait LayeredPathConditionStackLike {
   protected def branchConditions(layers: Stack[PathConditionStackLayer]): Stack[Term] =
     layers.flatMap(_.branchCondition)
 
+  protected def branchConditionExps(layers: Stack[PathConditionStackLayer]): Stack[Option[ast.Exp]] =
+    layers.flatMap(_.branchConditionExp)
+
   protected def assumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
     InsertionOrderedSet(layers.flatMap(_.assumptions)) // Note: Performance?
 
@@ -175,6 +189,7 @@ private class DefaultRecordedPathConditions(from: Stack[PathConditionStackLayer]
        with RecordedPathConditions {
 
   val branchConditions: Stack[Term] = branchConditions(from)
+  val branchConditionExps: Stack[Option[ast.Exp]] = branchConditionExps(from)
   val assumptions: InsertionOrderedSet[Term] = assumptions(from)
   val declarations: InsertionOrderedSet[Decl] = declarations(from)
 
@@ -209,10 +224,11 @@ private[decider] class LayeredPathConditionStack
 
   pushScope() /* Create an initial layer on the stack */
 
-  def setCurrentBranchCondition(condition: Term): Unit = {
+  def setCurrentBranchCondition(condition: Term, conditionExp: Option[ast.Exp]): Unit = {
     /* TODO: Split condition into top-level conjuncts as well? */
 
     layers.head.branchCondition = condition
+    layers.head.branchConditionExp = conditionExp
   }
 
   def add(assumption: Term): Unit = {
@@ -275,6 +291,8 @@ private[decider] class LayeredPathConditionStack
 
   def branchConditions: Stack[Term] = layers.flatMap(_.branchCondition)
 
+  override def branchConditionExps: Stack[Option[ast.Exp]] = layers.flatMap(_.branchConditionExp)
+
   def assumptions: InsertionOrderedSet[Term] = allAssumptions
 
   def declarations: InsertionOrderedSet[Decl] =

src/main/scala/interfaces/Verification.scala

@@ -9,8 +9,10 @@ package viper.silicon.interfaces
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.reporting.Converter
 import viper.silicon.state.{State, Store}
-import viper.silver.verifier.{Counterexample, Model, VerificationError}
+import viper.silver.verifier.{Counterexample, FailureContext, Model, VerificationError}
 import viper.silicon.state.terms.Term
+import viper.silicon.verifier.Verifier
+import viper.silver.ast
 
 /*
  * Results
@@ -22,25 +24,34 @@ import viper.silicon.state.terms.Term
 
 /* TODO: Make VerificationResult immutable */
 sealed abstract class VerificationResult {
-  var previous: Option[NonFatalResult] = None
+  var previous: Vector[VerificationResult] = Vector() //Sets had problems with equality
+  val continueVerification: Boolean = true
 
   def isFatal: Boolean
   def &&(other: => VerificationResult): VerificationResult
 
-  def allPrevious: List[VerificationResult] =
-    previous match {
-      case None => Nil
-      case Some(vr) => vr :: vr.allPrevious
-    }
-
-  def append(other: NonFatalResult): VerificationResult =
-    previous match {
-      case None =>
-        this.previous = Some(other)
-        this
-      case Some(vr) =>
-        vr.append(other)
-    }
+  /* Attention: Parameter 'other' of 'combine' is a function! That is, the following
+   * statements
+   *   println(other)
+   *   println(other)
+   * will invoke the function twice, which might not be what you really want!
+   */
+  def combine(other: => VerificationResult): VerificationResult = {
+    if (this.continueVerification){
+      val r: VerificationResult = other
+      /* Result of combining a failure with a non failure should be a failure.
+      *  When combining two failures, the failure with 'continueVerification'
+      *  set to false (if any) should be the 'head' result */
+      (this, r) match {
+        case (_: FatalResult, _: FatalResult) | (_: FatalResult, _: NonFatalResult) if r.continueVerification =>
+          this.previous = (this.previous :+ r) ++ r.previous
+          this
+        case _ =>
+          r.previous = (r.previous :+ this) ++ this.previous
+          r
+      }
+    } else this
+  }
 }
 
 sealed abstract class FatalResult extends VerificationResult {
@@ -60,7 +71,7 @@ sealed abstract class NonFatalResult extends VerificationResult {
    */
   def &&(other: => VerificationResult): VerificationResult = {
     val r: VerificationResult = other
-    r.append(this)
+    r.previous = (r.previous :+ this) ++ this.previous
     r
   }
 }
@@ -76,8 +87,8 @@ case class Unreachable() extends NonFatalResult {
 case class Failure/*[ST <: Store[ST],
                    H <: Heap[H],
                    S <: State[ST, H, S]]*/
-                  (message: VerificationError)
-    extends FatalResult {
+                  (message: VerificationError, override val continueVerification: Boolean = true)
+  extends FatalResult {
 
   /* TODO: Mutable state in a case class? DOOOOOOOOOOOOOON'T! */
   var load: Option[Seq[Term]] = None
@@ -89,6 +100,14 @@ case class Failure/*[ST <: Store[ST],
   override lazy val toString = message.readableMessage
 }
 
+case class SilFailureContext(branchConditions: Seq[ast.Exp], counterExample: Option[Counterexample]) extends FailureContext {
+  lazy val branchConditionString = if(branchConditions.nonEmpty)
+    ("\n\t\tunder branch conditions:\n" +
+      branchConditions.map(bc => (bc.toString + " [ " + bc.pos.toString + " ] ")).mkString("\t\t"," ~~> ","") ) else ""
+  lazy val counterExampleString = if(counterExample.isDefined) "\n\t\tcounterexample:\n" + counterExample.get.toString else ""
+  override lazy val toString = branchConditionString + counterExampleString
+}
+
 trait SiliconCounterexample extends Counterexample {
   val internalStore: Store
   lazy val store: Map[String, Term] = internalStore.values.map{case (k, v) => k.name -> v}

src/main/scala/reporting/package.scala

@@ -46,7 +46,7 @@ package object reporting {
   def convertToViperResult(result: VerificationResult): VprVerificationResult = {
     result match {
       case Success() | Unreachable() => VprSuccess
-      case Failure(message) => VprFailure(Seq(message))
+      case Failure(message, _) => VprFailure(Seq(message))
     }
   }
 

src/main/scala/rpi/inference/teacher/SampleExtractor.scala

@@ -240,10 +240,11 @@ trait SampleExtractor extends AbstractTeacher with LazyLogging {
     */
   private def extractInformation[T](error: VerificationError): (Counter, ast.LocationAccess, Option[T]) = {
     // extract counter example
-    val counter = error.counterexample match {
-      case Some(value: Counter) => value
-      case _ => sys.error("Verification error does not contain a counter example.")
-    }
+    val counters = error.failureContexts.map(_.counterExample).map {case Some(counterexample: SiliconRawCounterexample) => counterexample}
+    // We should only have multiple CEs at the very end of verification when results are merged
+    if (counters.length != 1)
+      sys.error(s"Verification error does not contain exactly one counterexample")
+    val counter =  counters.head
     // extract offending location
     val offending = error.reason match {
       case InsufficientPermission(location) => location

src/main/scala/rules/Brancher.scala

@@ -13,10 +13,12 @@ import viper.silicon.logger.SymbExLogger
 import viper.silicon.state.State
 import viper.silicon.state.terms.{Not, Term}
 import viper.silicon.verifier.Verifier
+import viper.silver.ast
 
 trait BranchingRules extends SymbolicExecutionRules {
   def branch(s: State,
              condition: Term,
+             conditionExp: Option[ast.Exp],
              v: Verifier,
              fromShortCircuitingAnd: Boolean = false)
             (fTrue: (State, Verifier) => VerificationResult,
@@ -27,13 +29,15 @@ trait BranchingRules extends SymbolicExecutionRules {
 object brancher extends BranchingRules {
   def branch(s: State,
              condition: Term,
+             conditionExp: Option[ast.Exp],
              v: Verifier,
              fromShortCircuitingAnd: Boolean = false)
             (fThen: (State, Verifier) => VerificationResult,
              fElse: (State, Verifier) => VerificationResult)
             : VerificationResult = {
 
     val negatedCondition = Not(condition)
+    val negatedConditionExp = conditionExp.fold[Option[ast.Exp]](None)(c => Some(ast.Not(c)(pos = conditionExp.get.pos, info = conditionExp.get.info, ast.NoTrafos)))
     val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin
 
     /* Skip path feasibility check if one of the following holds:
@@ -118,7 +122,7 @@ object brancher extends BranchingRules {
             }
 
             v1.decider.prover.comment(s"[else-branch: $cnt | $negatedCondition]")
-            v1.decider.setCurrentBranchCondition(negatedCondition)
+            v1.decider.setCurrentBranchCondition(negatedCondition, negatedConditionExp)
 
             fElse(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
           })
@@ -151,13 +155,13 @@ object brancher extends BranchingRules {
       SymbExLogger.currentLog().markReachable(uidBranchPoint)
       executionFlowController.locally(s, v)((s1, v1) => {
         v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
-        v1.decider.setCurrentBranchCondition(condition)
+        v1.decider.setCurrentBranchCondition(condition, conditionExp)
 
         fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
       })
     } else {
       Unreachable()
-    }) && {
+    }) combine {
 
       /* [BRANCH-PARALLELISATION] */
       if (parallelizeElseBranch) {