Display failing branches

src/main/scala/decider/Decider.scala

@@ -18,7 +18,7 @@ import viper.silicon.state.terms.{Term, _}
 import viper.silicon.utils.ast.{extractPTypeFromExp, simplifyVariableName}
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silver.ast
-import viper.silver.ast.{LocalVarWithVersion, NoPosition}
+import viper.silver.ast.{Exp, LocalVarWithVersion, NoPosition}
 import viper.silver.components.StatefulComponent
 import viper.silver.parser.{PKw, PPrimitiv, PReserved, PType}
 import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage}
@@ -129,7 +129,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     private var _proverOptions: Map[String, String] = Map.empty
     private var _proverResetOptions: Map[String, String] = Map.empty
     private val _debuggerAssumedTerms: mutable.Set[Term] = mutable.Set.empty
-    
+
     def functionDecls: Set[FunctionDecl] = _declaredFreshFunctions
     def macroDecls: Vector[MacroDecl] = _declaredFreshMacros
 
@@ -256,6 +256,16 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def setPathConditionMark(): Mark = pathConditions.mark()
 
+    def getBranchConditionsExp(): Seq[Exp] = {
+      this.pcs.branchConditionExps.map(_._1)
+        .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */
+        .sortBy(_.pos match {
+          /* Order branchconditions according to source position */
+          case pos: viper.silver.ast.HasLineColumn => (pos.line, pos.column)
+          case _ => (-1, -1)
+        })
+    }
+
     /* Assuming facts */
 
     def startDebugSubExp(): Unit = {

src/main/scala/decider/PathConditions.scala

@@ -13,7 +13,7 @@ import viper.silicon.state.terms._
 import viper.silicon.utils.Counter
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
-import viper.silver.ast.TrueLit
+import viper.silver.ast.{Exp, TrueLit}
 /*
  * Interfaces
  */
@@ -61,6 +61,7 @@ trait RecordedPathConditions {
 
 trait PathConditionStack extends RecordedPathConditions {
   def setCurrentBranchCondition(condition: Term, conditionExp: (ast.Exp, Option[ast.Exp])): Unit
+  def getBranchConditionsExp(): Seq[Exp]
   def add(assumption: Term): Unit
   def addDefinition(assumption: Term): Unit
   def add(declaration: Decl): Unit
@@ -459,6 +460,16 @@ private[decider] class LayeredPathConditionStack
     layers.head.branchConditionExp = conditionExp
   }
 
+  def getBranchConditionsExp(): Seq[Exp] = {
+    branchConditionExps.map(_._1)
+      .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */
+      .sortBy(_.pos match {
+        /* Order branchconditions according to source position */
+        case pos: viper.silver.ast.HasLineColumn => (pos.line, pos.column)
+        case _ => (-1, -1)
+      })
+  }
+
   def startDebugSubExp(): Unit = {
     layers.head.startDebugSubExp()
   }

src/main/scala/interfaces/Verification.scala

@@ -14,7 +14,8 @@ import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Term}
 import viper.silicon.state.{State, Store}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
-import viper.silver.ast.Program
+import viper.silver.ast.{Exp, Program}
+import viper.silver.reporter.ExploredBranches
 import viper.silver.verifier._
 
 /*
@@ -28,9 +29,19 @@ import viper.silver.verifier._
 /* TODO: Make VerificationResult immutable */
 sealed abstract class VerificationResult {
   var previous: Vector[VerificationResult] = Vector() //Sets had problems with equality
+  var exploredBranchPaths: Vector[(Seq[Exp],Boolean)] = Vector()
   val continueVerification: Boolean = true
   var isReported: Boolean = false
 
+  def getExploredBranchPaths(r: VerificationResult = this) : Vector[(Seq[Exp], Boolean)] = {
+    r.exploredBranchPaths ++ r.previous.flatMap(x => x.previous.length match {
+      case 0 => x.exploredBranchPaths
+      case _ =>
+        val recRes = x.previous.flatMap(getExploredBranchPaths)
+        x.exploredBranchPaths ++ recRes
+    })
+  }
+
   def isFatal: Boolean
   def &&(other: => VerificationResult): VerificationResult
 
@@ -61,7 +72,6 @@ sealed abstract class VerificationResult {
       }
       this
     }
-
   }
 }
 
@@ -98,9 +108,8 @@ case class Unreachable() extends NonFatalResult {
 case class Failure/*[ST <: Store[ST],
                    H <: Heap[H],
                    S <: State[ST, H, S]]*/
-                  (message: VerificationError, override val continueVerification: Boolean = true)
+                  (message: VerificationError, override val continueVerification: Boolean = true, var exploredBranches : Option[ExploredBranches] = None)
   extends FatalResult {
-
   override lazy val toString: String = message.readableMessage
 }
 

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, _, exploredBranches) => VprFailure(Seq(message), exploredBranches)
     }
   }
 
@@ -58,7 +58,7 @@ package object reporting {
            .collect { case failure: VprFailure => failure.errors }
            .flatten match {
               case Seq() => VprSuccess
-              case errors => VprFailure(errors)
+              case errors => VprFailure(errors, results.collectFirst({case Failure(_,_,Some(exploredBranches)) => exploredBranches}))
             }
   }
 }

src/main/scala/rules/Consumer.scala

@@ -589,7 +589,6 @@ object consumer extends ConsumptionRules {
     )
   }
 
-
   private def evalAndAssert(s: State, e: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier)
                            (Q: (State, Option[Term], Verifier) => VerificationResult)
                            : VerificationResult = {
@@ -620,7 +619,9 @@ object consumer extends ConsumptionRules {
         v2.decider.assert(termToAssert) {
           case true =>
             v2.decider.assume(t, Option.when(withExp)(e), eNew)
-            QS(s3, v2)
+            val r = QS(s3, v2)
+            r.exploredBranchPaths +:= (v.decider.pcs.getBranchConditionsExp(),false)
+            r
           case false =>
             val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew)
             if (s3.retryLevel == 0 && v2.reportFurtherErrors()){

src/main/scala/rules/SymbolicExecutionRules.scala

@@ -84,26 +84,20 @@ trait SymbolicExecutionRules {
       None
     }
 
-    val branchconditions = if (Verifier.config.enableBranchconditionReporting()) {
-      v.decider.pcs.branchConditionExps.map(_._1)
-        .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */
-        .sortBy(_.pos match {
-          /* Order branchconditions according to source position */
-          case pos: viper.silver.ast.HasLineColumn => (pos.line, pos.column)
-          case _ => (-1, -1)
-        })
-    } else Seq()
+    val branchConditions = v.decider.pcs.getBranchConditionsExp()
 
     if (Verifier.config.enableDebugging()){
       val assumptions = v.decider.pcs.assumptionExps
       res.failureContexts = Seq(SiliconDebuggingFailureContext(v.decider.pcs.branchConditions, v.decider.pcs.branchConditionExps.map(bce => bce._1 -> bce._2.get),
         counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.prover.preambleAssumptions,
         v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssert, failedAssertExp.get))
     } else {
-      res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown))
+      val branchConditionsReported = if (Verifier.config.enableBranchconditionReporting()) branchConditions else Seq()
+      res.failureContexts = Seq(SiliconFailureContext(branchConditionsReported, counterexample, reasonUnknown))
     }
 
-    Failure(res, v.reportFurtherErrors())
-
+    val f = Failure(res,  v.reportFurtherErrors())
+    f.exploredBranchPaths +:= (branchConditions, true)
+    f
   }
 }

src/main/scala/supporters/MethodSupporter.scala

@@ -18,7 +18,7 @@ import viper.silicon.state.{Heap, State, Store}
 import viper.silicon.state.State.OldHeaps
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silicon.utils.freshSnap
-import viper.silver.reporter.AnnotationWarning
+import viper.silver.reporter.{AnnotationWarning, ExploredBranches, ExploredBranchesReport}
 import viper.silicon.{Map, toMap}
 
 /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */
@@ -117,6 +117,26 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
       v.decider.resetProverOptions()
 
       symbExLog.closeMemberScope()
+
+      val exploredBranchPaths = result.getExploredBranchPaths()
+      result match {
+        case f: Failure if exploredBranchPaths.nonEmpty =>
+          val transformedPaths = exploredBranchPaths.map(eb => {
+            val (exps, isResultFatal) = eb
+            val transformedExps = exps.map(e => {
+              val (exprStr, negated) = e match {
+                case ast.Not(expr) => (expr.toString, true)
+                case _ => (e.toString, false)
+              }
+              (exprStr, negated)
+            }).toVector
+            (transformedExps, isResultFatal)
+          })
+          val exploredBranches = ExploredBranches(method, transformedPaths)
+          f.exploredBranches = Some(exploredBranches)
+          v.reporter.report(ExploredBranchesReport(exploredBranches))
+        case _ =>
+      }
       Seq(result)
     }
 

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -630,4 +630,4 @@ class DefaultMainVerifier(config: Config,
     */
   private def extractAllVerificationResults(res: VerificationResult): Seq[VerificationResult] =
     res :: res.previous.toList
-}
+}

src/test/scala/SiliconQuantifierWeightTests.scala

@@ -112,13 +112,13 @@ class SiliconQuantifierWeightTests extends AnyFunSuite {
     // A small weight should allow the axiom to be instantiated
     verifyUsingWeight(1) match {
       case Success => // Ok
-      case Failure(errors) => assert(false)
+      case Failure(errors,_) => assert(false)
     }
 
     // A big weight should prevent the axiom from being instantiated
     verifyUsingWeight(999) match {
       case Success => assert(false)
-      case Failure(errors) => // Ok
+      case Failure(errors,_) => // Ok
     }
   }
 }

src/test/scala/SymbExLoggerTests.scala

@@ -75,7 +75,7 @@ class SiliconFrontendWithUnitTesting(path: Path) extends SiliconFrontend(NoopRep
         case Nil => super.result
         case s1:Seq[AbstractError] => super.result match{
           case SilSuccess => SilFailure(s1)
-          case SilFailure(s2) => SilFailure(s2 ++ s1)
+          case SilFailure(s2,exploredBranches) => SilFailure(s2 ++ s1,exploredBranches)
         }
       }
     }

src/test/scala/tests.scala

@@ -6,9 +6,10 @@
 
 import java.nio.file.{Path, Paths}
 import viper.silver.ast.Program
-import viper.silver.frontend.{SilFrontend, SilFrontendConfig, DefaultStates}
+import viper.silver.frontend.{DefaultStates, SilFrontend, SilFrontendConfig}
 import viper.silver.verifier.{AbstractError, AbstractVerificationError, VerificationResult, Verifier, Failure => SilFailure}
 import viper.silicon.Silicon
+import viper.silver.reporter.Reporter
 
 package object tests {
   class DummyFrontend extends SilFrontend {
@@ -59,11 +60,11 @@ package object tests {
 
   def verifyProgram(program: Program, frontend: SilFrontend): VerificationResult = {
     frontend.verifier.verify(program) match {
-      case SilFailure(errors) =>
+      case SilFailure(errors,exploredBranches) =>
         SilFailure(errors.map {
           case a: AbstractVerificationError => a.transformedError()
           case rest => rest
-        })
+        },exploredBranches)
       case rest => rest
     }
   }