diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index 5de692857..fca9da74d 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/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 { diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala index 0a5bcfee9..8402f7e9b 100644 --- a/src/main/scala/viper/silver/parser/MacroExpander.scala +++ b/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 = { diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 9f2134825..77b71e465 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/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 } diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index bc8d402f6..94f4e3f9b 100644 --- a/src/main/scala/viper/silver/parser/Resolver.scala +++ b/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(_) => diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index c03893c06..a0e779a72 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/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()) } } diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala index 450f72ff5..3b2152562 100644 --- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala +++ b/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) } } diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala index 63f4c3070..90e549d96 100644 --- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala +++ b/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_) } } diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index a77b9ff91..119a0f198 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/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) } } diff --git a/src/main/scala/viper/silver/reporter/Message.scala b/src/main/scala/viper/silver/reporter/Message.scala index 441810eee..5e96b1131 100644 --- a/src/main/scala/viper/silver/reporter/Message.scala +++ b/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 { diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index 0c51bd50d..ad0c106d2 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/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 => diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala index 3b070fe09..736e2ce40 100644 --- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala +++ b/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 }) } diff --git a/src/main/scala/viper/silver/verifier/VerificationResult.scala b/src/main/scala/viper/silver/verifier/VerificationResult.scala index 95980f6c5..d4542a8bb 100644 --- a/src/main/scala/viper/silver/verifier/VerificationResult.scala +++ b/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) } /** diff --git a/src/test/scala/PluginTests.scala b/src/test/scala/PluginTests.scala index 1f34f2ef3..8f4717e54 100644 --- a/src/test/scala/PluginTests.scala +++ b/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 diff --git a/src/test/scala/SilSuite.scala b/src/test/scala/SilSuite.scala index a0d87ba3f..84cd8f7fd 100644 --- a/src/test/scala/SilSuite.scala +++ b/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 diff --git a/src/test/scala/StatisticalTestSuite.scala b/src/test/scala/StatisticalTestSuite.scala index bbca77076..5d3f3e080 100644 --- a/src/test/scala/StatisticalTestSuite.scala +++ b/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