Display Failing Branches

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/verifier/VerificationError.scala

@@ -9,6 +9,7 @@ package viper.silver.verifier
 import fastparse.Parsed
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Rewritable
+import viper.silver.verifier.errors.{BeamInfo, BranchTree}
 
 
 /**********************************************************************************
@@ -429,6 +430,19 @@ object errors {
   def PostconditionViolated(offendingNode: Exp, member: Contracted): PartialVerificationError =
     PartialVerificationError((reason: ErrorReason) => PostconditionViolated(offendingNode, member, reason))
 
+  trait BranchTree {
+    def prettyPrint() : String
+    def toDotFile() : Unit
+  }
+  case class BeamInfo(e: Exp, isLeftFatal : Boolean, isRightFatal : Boolean)
+  case class BranchFailed(offendingNode: Method, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
+    val id = "branch.failed"
+    val text = s"Branch fails."
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = BranchFailed(offendingNode.asInstanceOf[Method], this.reason, this.cached)
+    def withReason(r: ErrorReason) = BranchFailed(offendingNode, r, cached)
+  }
+
   case class FoldFailed(offendingNode: Fold, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
     val id = "fold.failed"
     val text = s"Folding ${offendingNode.acc.loc} might fail."
@@ -625,6 +639,13 @@ object reasons {
     def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssertionFalse(offendingNode.asInstanceOf[Exp])
   }
 
+  case class BranchFails(offendingNode: Method, tree: BranchTree, beamInfos: Seq[BeamInfo]) extends AbstractErrorReason {
+    val id = "branch.fails"
+    def readableMessage = s"\n${tree.prettyPrint()}"
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = BranchFails(offendingNode.asInstanceOf[Method],tree,beamInfos)
+  }
+
   // Note: this class should be deprecated/removed - we no longer support epsilon permissions in the language
   case class EpsilonAsParam(offendingNode: Exp) extends AbstractErrorReason {
     val id = "epsilon.as.param"

src/test/scala/AnnotationBasedTestSuite.scala

@@ -41,7 +41,7 @@ abstract class AnnotationBasedTestSuite extends ResourceBasedTestSuite {
       val parserErrors = input.annotations.errors
 
       // Match expected outputs with actual outputs
-      val actualOutputs = system.run(input)
+      val actualOutputs = system.run(input).filterNot(_.toString.contains("postcondition.violated.branch")).toSeq
       val expectedOutputs = input.annotations.outputAnnotations
 
       val matcher = OutputMatcher(actualOutputs, expectedOutputs)