Display failing branches

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -54,7 +54,7 @@ trait SilFrontend extends DefaultFrontend {
     if (_state >= DefaultStates.Verification) {
       _appExitReason = result match {
         case Success => ApplicationExitReason.VERIFICATION_SUCCEEDED
-        case Failure(_) => ApplicationExitReason.VERIFICATION_FAILED
+        case Failure(_,_) => ApplicationExitReason.VERIFICATION_FAILED
       }
     }
   }
@@ -283,9 +283,9 @@ trait SilFrontend extends DefaultFrontend {
     val res = plugins.beforeFinish(tRes)
     val filteredRes = res match {
       case Success => res
-      case Failure(errors) =>
+      case Failure(errors,exploredBranches) =>
         // Remove duplicate errors
-        Failure(errors.distinctBy(failureFilterAndGroupingCriterion))
+        Failure(errors.distinctBy(failureFilterAndGroupingCriterion),exploredBranches)
     }
     _verificationResult = Some(filteredRes)
     filteredRes match {

src/main/scala/viper/silver/parser/MacroExpander.scala

@@ -338,8 +338,11 @@ object MacroExpander {
       var bodyWithReplacedParams = replacer.execute[PNode](bodyWithRenamedVars, context)
       bodyWithReplacedParams = adaptPositions(bodyWithReplacedParams, pos)
 
-      // Return expanded macro's body
-      bodyWithReplacedParams
+      // Return expanded macro's body wrapped inside annotation
+      bodyWithReplacedParams match {
+        case b: PExp => PExpandedMacroExp(b)(pos)
+        case b: PStmt => PExpandedMacroStmt(b)(pos)
+      }
     }
 
     def ExpandMacroIfValid(macroCall: PNode, ctx: ContextA[PNode]): PNode = {

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -70,6 +70,10 @@ trait PNode extends Where with Product with Rewritable with HasExtraValList {
   def deepCollect[A](f: PartialFunction[PNode, A]): Seq[A] =
     Visitor.deepCollect(Seq(this), PNode.callSubnodes)(f)
 
+  /** Same as deep collect except that subnodes are visited only if f1 returns true at the current node */
+  def deepCollectOpt[A](f1: PNode => Boolean, f2: PartialFunction[PNode, A]): Seq[A] =
+    Visitor.deepCollect(Seq(this), (n : PNode) => if (f1(n)) PNode.callSubnodes(n) else Seq.empty)(f2)
+
   /** @see [[Visitor.shallowCollect()]] */
   def shallowCollect[R](f: PartialFunction[PNode, R]): Seq[R] =
     Visitor.shallowCollect(Seq(this), PNode.callSubnodes)(f)
@@ -89,6 +93,10 @@ trait PNode extends Where with Product with Rewritable with HasExtraValList {
   def deepCopyAll[A <: PNode]: PNode =
     StrategyBuilder.Slim[PNode]({ case n => n }).forceCopy().execute[PNode](this)
 
+  /** @see [[Visitor.find()]] */
+  def find[A](f: PartialFunction[PNode, A]): Option[A] =
+    Visitor.find(this, PNode.callSubnodes)(f)
+
   private val _children = scala.collection.mutable.ListBuffer[PNode]()
 
   def getParent: Option[PNode] = parent
@@ -1440,6 +1448,15 @@ case class PSeqn(ss: PDelimited.Block[PStmt])(val pos: (Position, Position)) ext
   override def pretty = ss.prettyLines
 }
 
+///////////////////////////////////////////////////////////////////////////
+// Wrapper for expanded macros
+trait PExpandedMacro
+case class PExpandedMacroExp(exp: PExp)(val pos: (Position, Position)) extends PExp with PExpandedMacro {
+  override def typeSubstitutions: collection.Seq[PTypeSubstitution] = exp.typeSubstitutions
+  override def forceSubstitution(ts: PTypeSubstitution): Unit = exp.forceSubstitution(ts)
+}
+case class PExpandedMacroStmt(stmt: PStmt)(val pos: (Position, Position)) extends PStmt with PExpandedMacro
+
 /**
   * PSeqn representing the expanded body of a statement macro.
   * Unlike a normal PSeqn, it does not represent its own scope.
@@ -1471,7 +1488,9 @@ sealed trait PIfContinuation extends PStmt
 case class PIf(keyword: PReserved[PKeywordIf], cond: PGrouped.Paren[PExp], thn: PSeqn, els: Option[PIfContinuation])(val pos: (Position, Position)) extends PStmt with PIfContinuation
 case class PElse(k: PKw.Else, els: PSeqn)(val pos: (Position, Position)) extends PStmt with PIfContinuation
 
-case class PWhile(keyword: PKw.While, cond: PGrouped.Paren[PExp], invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]], body: PSeqn)(val pos: (Position, Position)) extends PStmt
+trait PMemberWithSpec
+
+case class PWhile(keyword: PKw.While, cond: PGrouped.Paren[PExp], invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]], body: PSeqn)(val pos: (Position, Position)) extends PStmt with PMemberWithSpec
 
 case class PVars(keyword: PKw.Var, vars: PDelimited[PLocalVarDecl, PSym.Comma], init: Option[(PSymOp.Assign, PExp)])(val pos: (Position, Position)) extends PStmt {
   def assign: Option[PAssign] = init map (i => PAssign(vars.update(vars.toSeq.map(_.toIdnUse)), Some(i._1), i._2)(pos))
@@ -1713,7 +1732,7 @@ case class PPredicate(annotations: Seq[PAnnotation], keyword: PKw.Predicate, idn
 }
 
 case class PMethod(annotations: Seq[PAnnotation], keyword: PKw.Method, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], returns: Option[PMethodReturns], pres: PDelimited[PSpecification[PKw.PreSpec], Option[PSym.Semi]], posts: PDelimited[PSpecification[PKw.PostSpec], Option[PSym.Semi]], body: Option[PSeqn])
-                  (val pos: (Position, Position)) extends PSingleMember with PGlobalCallableNamedArgs with PPrettySubnodes {
+                  (val pos: (Position, Position)) extends PSingleMember with PMemberWithSpec with PGlobalCallableNamedArgs with PPrettySubnodes {
   def formalReturns: Seq[PFormalReturnDecl] = returns.map(_.formalReturns.inner.toSeq).getOrElse(Nil)
   override def returnNodes = returns.toSeq
 }

src/main/scala/viper/silver/parser/Resolver.scala

@@ -210,6 +210,8 @@ case class TypeChecker(names: NameAnalyser) {
     stmt match {
       case PAnnotatedStmt(_, s) =>
         check(s)
+      case PExpandedMacroStmt(s) =>
+        check(s)
       case s@PSeqn(ss) =>
         checkMember(s) {
           ss.inner.toSeq foreach check
@@ -646,6 +648,9 @@ case class TypeChecker(names: NameAnalyser) {
       case PAnnotatedExp(_, e) =>
         checkInternal(e)
         setType(e.typ)
+      case PExpandedMacroExp(e) =>
+        checkInternal(e)
+        setType(e.typ)
       case psl: PSimpleLiteral=>
         psl match {
           case r@PResultLit(_) =>

src/main/scala/viper/silver/parser/Translator.scala

@@ -324,6 +324,7 @@ case class Translator(program: PProgram) {
           ann.values.inner.toSeq.map(_.str)
         }
         (resPexp, innerMap.updated(ann.key.str, combinedValue))
+      case PExpandedMacroExp(s) => extractAnnotation(s)
       case _ => (pexp, Map())
     }
   }
@@ -338,6 +339,7 @@ case class Translator(program: PProgram) {
           ann.values.inner.toSeq.map(_.str)
         }
         (resPStmt, innerMap.updated(ann.key.str, combinedValue))
+      case PExpandedMacroStmt(s) => extractAnnotationFromStmt(s)
       case _ => (pStmt, Map())
     }
   }

src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala

@@ -103,11 +103,11 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
   private def translateVerificationResult(input: VerificationResult): VerificationResult = {
     input match {
       case Success => input
-      case Failure(errors) =>
+      case Failure(errors,exploredBranches) =>
         Failure(errors.map {
           case e@PreconditionInAppFalse(_, _, _) => e.transformedError()
           case e => e
-        })
+        },exploredBranches)
     }
   }
 

src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala

@@ -74,12 +74,14 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
     mapVerificationResultsForNode(program, input)
 
   private def mapVerificationResultsForNode(n: Node, input: VerificationResult): VerificationResult = {
-    val (refutesForWhichErrorOccurred, otherErrors) = input match {
-      case Success => (Seq.empty, Seq.empty)
-      case Failure(errors) => errors.partitionMap {
+    val (refutesForWhichErrorOccurred, otherErrors, exploredBranches_) = input match {
+      case Success => (Seq.empty, Seq.empty,None)
+      case Failure(errors,exploredBranches) =>
+        val partErrs = errors.partitionMap {
         case AssertFailed(NodeWithRefuteInfo(RefuteInfo(r)), _, _) => Left((r, r.pos))
         case err => Right(err)
       }
+      (partErrs._1, partErrs._2, exploredBranches)
     }
     val refutesContainedInNode = n.collect {
       case NodeWithRefuteInfo(RefuteInfo(r)) => (r, r.pos)
@@ -93,7 +95,7 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
 
     val errors = otherErrors ++ missingErrorsInNode
     if (errors.isEmpty) Success
-    else Failure(errors)
+    else Failure(errors, exploredBranches_)
   }
 }
 

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -297,10 +297,10 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
     input match {
       case Success => input
-      case Failure(errors) => Failure(errors.map({
+      case Failure(errors,exploredBranches) => Failure(errors.map({
         case a@AssertFailed(Assert(_), _, _) => a.transformedError()
         case e => e
-      }))
+      }),exploredBranches)
     }
   }
 

src/main/scala/viper/silver/reporter/Message.scala

@@ -8,7 +8,7 @@ package viper.silver.reporter
 
 import viper.silver.reporter.BackendSubProcessStages.BackendSubProcessStage
 import viper.silver.verifier._
-import viper.silver.ast.{QuantifiedExp, Trigger}
+import viper.silver.ast.{Method, QuantifiedExp, Trigger}
 import viper.silver.parser.PProgram
 
 /**
@@ -169,7 +169,17 @@ case class BranchFailureMessage(verifier: String, concerning: Entity,
     s"result=${result.toString}, cached=$cached)"
 }
 
-case class StatisticsReport(nOfMethods: Int, nOfFunctions: Int, nOfPredicates: Int, 
+case class ExploredBranches(method: Method, paths: Vector[(Vector[(String, Boolean)], Boolean)], var cached : Boolean = false)
+case class ExploredBranchesReport(exploredBranches : ExploredBranches)
+  extends Message {
+
+  override lazy val toString: String = s"explored_branches_report(" +
+    s"method=${exploredBranches.method.name}, paths=${exploredBranches.paths}"
+
+  override val name = "explored_branches"
+}
+
+case class StatisticsReport(nOfMethods: Int, nOfFunctions: Int, nOfPredicates: Int,
                             nOfDomains: Int, nOfFields: Int)
   extends Message {
 

src/main/scala/viper/silver/reporter/Reporter.scala

@@ -68,6 +68,8 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
 
       case BranchFailureMessage(_, concerning, _, cached) =>
         csv_file.write(s"BranchFailureMessage,${concerning.name},${cached}\n")
+      case ExploredBranchesReport(eb) =>
+        csv_file.write(s"ExploredBranchesReport,${eb.method.name},${eb.paths}, ${eb.cached}\n")
 
       case _: SimpleMessage | _: CopyrightReport | _: MissingDependencyReport | _: BackendSubProcessReport |
            _: InternalWarningMessage | _: ConfigurationConfirmation=> // Irrelevant for reporting
@@ -125,15 +127,15 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
 
       case ExceptionReport(e) =>
         /** Theoretically, we may encounter an exceptional message that has
-          * not yet been reported via AbortedExceptionally. This can happen
-          * if we encounter exeptions in e.g. the parser. */
+         * not yet been reported via AbortedExceptionally. This can happen
+         * if we encounter exeptions in e.g. the parser. */
         println( s"Verification aborted exceptionally: ${e.toString}" )
         e.printStackTrace(System.out);
         Option(e.getCause) match {
           case Some(cause) => println( s"  Cause: ${cause.toString}" )
           case None =>
         }
-        //println( s"  See log file for more details: ..." )
+      //println( s"  See log file for more details: ..." )
 
       case ExternalDependenciesReport(deps) =>
         val s: String = (deps map (dep => {
@@ -179,12 +181,13 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
       case EntitySuccessMessage(_, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
       case EntityFailureMessage(_, _, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
       case BranchFailureMessage(_, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
+      case ExploredBranchesReport(_) =>
       case ConfigurationConfirmation(_) =>     // TODO  use for progress reporting
-        //println( s"Configuration confirmation: $text" )
+      //println( s"Configuration confirmation: $text" )
       case InternalWarningMessage(_) =>        // TODO  use for progress reporting
-        //println( s"Internal warning: $text" )
+      //println( s"Internal warning: $text" )
       case _: SimpleMessage =>
-        //println( sm.text )
+      //println( sm.text )
       case _: QuantifierInstantiationsMessage => // too verbose, do not print
       case _: QuantifierChosenTriggersMessage => // too verbose, do not print
       case _: VerificationTerminationMessage =>

src/main/scala/viper/silver/testing/BackendTypeTest.scala

@@ -265,7 +265,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val (prog, assertNode) = generateTypeCombinationTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case Failure(Seq(AssertFailed(a, _, _)),_) if a == assertNode => true
       case _ => false
     })
   }
@@ -286,7 +286,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val (prog, assertNode) = generateFieldTypeTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case Failure(Seq(AssertFailed(a, _, _)),_) if a == assertNode => true
       case _ => false
     })
   }
@@ -301,7 +301,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val (prog, assertNode) = generateBvOpTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case Failure(Seq(AssertFailed(a, _, _)),_) if a == assertNode => true
       case _ => false
     })
   }
@@ -322,7 +322,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val (prog, assertNode) = generateFloatOpTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case Failure(Seq(AssertFailed(a, _, _)),_) if a == assertNode => true
       case _ => false
     })
   }
@@ -337,7 +337,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val (prog, assertNode) = generateFloatMinMaxTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case Failure(Seq(AssertFailed(a, _, _)),_) if a == assertNode => true
       case _ => false
     })
   }
@@ -352,7 +352,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val (prog, fun, exp) = generateFloatOpFunctionTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(PostconditionViolated(e, f, _, _))) if e == exp && fun == f => true
+      case Failure(Seq(PostconditionViolated(e, f, _, _)),_) if e == exp && fun == f => true
       case _ => false
     })
   }

src/main/scala/viper/silver/verifier/VerificationResult.scala

@@ -7,6 +7,7 @@
 package viper.silver.verifier
 
 import viper.silver.ast._
+import viper.silver.reporter.ExploredBranches
 
 import scala.annotation.unused
 
@@ -24,15 +25,15 @@ object Success extends VerificationResult {
 }
 
 /** A non-successful verification.
-  *
-  * @param errors The errors encountered during parsing, translation or verification.
-  */
-case class Failure(errors: Seq[AbstractError]) extends VerificationResult {
+ *
+ * @param errors The errors encountered during parsing, translation or verification.
+ */
+case class Failure(errors: Seq[AbstractError], exploredBranches : Option[ExploredBranches] = None) extends VerificationResult {
   override def toString = {
     s"Verification failed with ${errors.size} errors:\n  " +
       (errors map (e => "[" + e.fullId + "] " + e.readableMessage)).mkString("\n  ")
   }
-  override def transformedResult(): VerificationResult = Failure(errors.map(_.transformedError()))
+  override def transformedResult(): VerificationResult = Failure(errors.map(_.transformedError()), exploredBranches)
 }
 
 /**

src/test/scala/PluginTests.scala

@@ -61,7 +61,7 @@ class TestPluginReportError extends SilverPlugin {
   override def beforeFinish(input: VerificationResult): VerificationResult = {
     input match {
       case Success => assert(false)
-      case Failure(errs) => assert(errs.contains(error))
+      case Failure(errs,_) => assert(errs.contains(error))
     }
     input
   }
@@ -148,7 +148,7 @@ class TestPluginMapErrors extends SilverPlugin with TestPlugin with FakeResult {
 //        println(">>> detected VerificationResult is Success")
         assert(false)
         input
-      case Failure(errors) =>
+      case Failure(errors,_) =>
 //        println(s">>> detected VerificationResult is Failure: ${errors.toString()}")
         assert(errors.contains(error1))
         Failure(Seq(error2))
@@ -161,7 +161,7 @@ class TestPluginMapErrors extends SilverPlugin with TestPlugin with FakeResult {
       case Success =>
 //        println("]]] detected VerificationResult is Success")
         assert(false)
-      case Failure(errors) =>
+      case Failure(errors,_) =>
 //        println(s"]]] detected VerificationResult is Failure: ${errors.toString()}")
         assert(!errors.contains(error1))
         assert(errors.contains(error2))
@@ -200,7 +200,7 @@ class TestPluginMapVsFinish extends SilverPlugin with TestPlugin {
     finish = true
     input match {
       case Success => assert(false)
-      case Failure(errors) =>
+      case Failure(errors,_) =>
         assert(errors.contains(error))
     }
     input

src/test/scala/SilSuite.scala

@@ -109,7 +109,7 @@ abstract class SilSuite extends AnnotationBasedTestSuite with BeforeAndAfterAllC
       info(s"Time required: $tPhases.")
       val actualErrors = fe.result match {
         case Success => Nil
-        case Failure(es) => es collect {
+        case Failure(es,_) => es collect {
           case e: AbstractVerificationError =>
             e.transformedError()
           case rest: AbstractError => rest

src/test/scala/StatisticalTestSuite.scala

@@ -142,7 +142,7 @@ trait StatisticalTestSuite extends SilSuite {
         val actualErrors: Seq[AbstractError] =
           fe.result match {
             case Success => Nil
-            case Failure(es) => es collect {
+            case Failure(es,_) => es collect {
               case e: AbstractVerificationError =>
                 e.transformedError()
               case rest: AbstractError => rest