diff --git a/silver b/silver index b9f727223..4833685a5 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b9f7272234d6c2a2b84e140979d1b282c74ecba1 +Subproject commit 4833685a51d8f3c4e2793103db4121d9e71e0109 diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index fbf93b066..6b2a90b87 100644 --- a/src/main/scala/decider/Decider.scala +++ b/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 = { diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala index de38c28cd..017838618 100644 --- a/src/main/scala/decider/PathConditions.scala +++ b/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() } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index ad52d3bf2..485436ba4 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/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 } diff --git a/src/main/scala/reporting/package.scala b/src/main/scala/reporting/package.scala index 91db94b57..4cc5df725 100644 --- a/src/main/scala/reporting/package.scala +++ b/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})) } } } diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index fd3e34b94..8231a78ca 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/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()){ diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 6f18728d5..d8ce63f08 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -84,15 +84,7 @@ 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 @@ -100,10 +92,12 @@ trait SymbolicExecutionRules { 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 } } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 9b483ff4a..5376319ce 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/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) } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index b395ed213..84df895bb 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/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 -} +} \ No newline at end of file diff --git a/src/test/scala/SiliconQuantifierWeightTests.scala b/src/test/scala/SiliconQuantifierWeightTests.scala index 7382ff87f..e7a0168c3 100644 --- a/src/test/scala/SiliconQuantifierWeightTests.scala +++ b/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 } } } diff --git a/src/test/scala/SymbExLoggerTests.scala b/src/test/scala/SymbExLoggerTests.scala index 55e7e100b..537615e1f 100644 --- a/src/test/scala/SymbExLoggerTests.scala +++ b/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) } } } diff --git a/src/test/scala/tests.scala b/src/test/scala/tests.scala index 4cb16004f..a0d097483 100644 --- a/src/test/scala/tests.scala +++ b/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 } }