diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index b835fd689..deba08031 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -237,15 +237,15 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] /* Write proof-query CSV if requested */ config.recordProofQueries.toOption.foreach { path => - val header = "isAssert,member,file,line,column,kind,durationMs,succeeded,description" + val header = "kind,member,file,line,column,category,durationMs,succeeded,description" val rows = ProofQueryCollector.records.map { r => val (file, line, col) = r.pos match { case sp: viper.silver.ast.AbstractSourcePosition => (sp.file.toString, sp.line.toString, sp.column.toString) case _ => ("?", "?", "?") } - Seq(r.isAssert, r.member.getOrElse("?"), file, line, col, - r.kind, "%.3f".format(r.durationMs), r.succeeded, + Seq(r.kind, r.member.getOrElse("?"), file, line, col, + r.category, "%.3f".format(r.durationMs), r.succeeded, r.description.getOrElse("")).mkString(",") } java.nio.file.Files.write( diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 007502839..0ce8bf1cf 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -47,10 +47,11 @@ trait Decider { def debugVariableTypes: Map[String, PType] - def pushScope(): Unit - def popScope(): Unit + def pushScope(member: Option[String] = None, description: Option[String] = None): Unit + def popScope(member: Option[String] = None, description: Option[String] = None): Unit def checkSmoke(isAssert: Boolean = false, + kind: ProofQueryKind, pos: ast.Position = ast.NoPosition, member: Option[String] = None, description: Option[String] = None): Boolean @@ -247,19 +248,41 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => /* Assumption scope handling */ - def pushScope(): Unit = { + def pushScope(member: Option[String] = None, description: Option[String] = None): Unit = { //val commentRecord = new CommentRecord("push", null, null) //val sepIdentifier = symbExLog.openScope(commentRecord) pathConditions.pushScope() + val t0 = System.nanoTime() _prover.push(timeout = Verifier.config.pushTimeout.toOption) + val durMs = (System.nanoTime() - t0) / 1e6 + if (Verifier.config.recordProofQueries.isDefined) + ProofQueryCollector.record(ProofQueryRecord( + kind = QueryKind.Push, + member = member, + pos = ast.NoPosition, + category = ProofQueryKind.ScopeManagement, + durationMs = durMs, + succeeded = true, + description = description)) //symbExLog.closeScope(sepIdentifier) } - def popScope(): Unit = { + def popScope(member: Option[String] = None, description: Option[String] = None): Unit = { //val commentRecord = new CommentRecord("pop", null, null) //val sepIdentifier = symbExLog.openScope(commentRecord) + val t0 = System.nanoTime() _prover.pop() + val durMs = (System.nanoTime() - t0) / 1e6 pathConditions.popScope() + if (Verifier.config.recordProofQueries.isDefined) + ProofQueryCollector.record(ProofQueryRecord( + kind = QueryKind.Pop, + member = member, + pos = ast.NoPosition, + category = ProofQueryKind.ScopeManagement, + durationMs = durMs, + succeeded = true, + description = description)) //symbExLog.closeScope(sepIdentifier) } @@ -376,6 +399,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => /* Asserting facts */ def checkSmoke(isAssert: Boolean = false, + kind: ProofQueryKind, pos: ast.Position = ast.NoPosition, member: Option[String] = None, description: Option[String] = None): Boolean = { @@ -385,10 +409,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => val dur = (System.nanoTime() - t0) / 1e6 if (Verifier.config.recordProofQueries.isDefined) ProofQueryCollector.record(ProofQueryRecord( - isAssert = false, + kind = QueryKind.Check, member = member, pos = pos, - kind = ProofQueryKind.PathInfeasibility, + category = kind, durationMs = dur, succeeded = res, description = description)) @@ -400,7 +424,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => pos: ast.Position = ast.NoPosition, member: Option[String] = None, description: Option[String] = None): Boolean = - deciderAssert(t, Some(timeout), kind, pos, member, description, isAssert = false) + deciderAssert(t, Some(timeout), kind, pos, member, description, queryKind = QueryKind.Check) def assert(t: Term, kind: ProofQueryKind, @@ -410,7 +434,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => description: Option[String] = None )(Q: Boolean => VerificationResult): VerificationResult = { - val success = deciderAssert(t, timeout, kind, pos, member, description, isAssert = true) + val success = deciderAssert(t, timeout, kind, pos, member, description, queryKind = QueryKind.Assert) // If the SMT query was not successful, store it (possibly "overwriting" // any previously saved query), otherwise discard any query we had saved @@ -429,7 +453,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => pos: ast.Position = ast.NoPosition, member: Option[String] = None, description: Option[String] = None, - isAssert: Boolean = true) = { + queryKind: QueryKind = QueryKind.Assert) = { val assertRecord = new DeciderAssertRecord(t, timeout) val sepIdentifier = symbExLog.openScope(assertRecord) @@ -440,10 +464,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => if (Verifier.config.recordProofQueries.isDefined && !alreadyKnown) ProofQueryCollector.record(ProofQueryRecord( - isAssert = isAssert, + kind = queryKind, member = member, pos = pos, - kind = kind, + category = kind, durationMs = durMs, succeeded = result, description = description)) diff --git a/src/main/scala/interfaces/decider/ProofQueryKind.scala b/src/main/scala/interfaces/decider/ProofQueryKind.scala index ca6bde4aa..cb64c392d 100644 --- a/src/main/scala/interfaces/decider/ProofQueryKind.scala +++ b/src/main/scala/interfaces/decider/ProofQueryKind.scala @@ -30,7 +30,16 @@ object ProofQueryKind { * whether the current execution path is reachable at all. */ case object PathInfeasibility extends ProofQueryKind + /** (e') Heap-infeasibility checks: smoke checks issued as a consequence of heap operations + * (chunk lookup, consume, exhale, etc.) — i.e. path-feasibility queries whose origin is + * a heap manipulation rather than generic control flow. */ + case object HeapInfeasibility extends ProofQueryKind + /** (f) Unknown: used when the purpose of the query does not clearly fall into any of the * above categories, or has not yet been classified. */ case object Unknown extends ProofQueryKind + + /** (g) Scope-management operations: push and pop of the prover assertion stack + * used to bound the scope of branch assumptions, contract checks, etc. */ + case object ScopeManagement extends ProofQueryKind } diff --git a/src/main/scala/interfaces/decider/QueryKind.scala b/src/main/scala/interfaces/decider/QueryKind.scala new file mode 100644 index 000000000..abf959406 --- /dev/null +++ b/src/main/scala/interfaces/decider/QueryKind.scala @@ -0,0 +1,17 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2019 ETH Zurich. + +package viper.silicon.interfaces.decider + +/** Identifies the kind of solver interaction recorded in a [[viper.silicon.reporting.ProofQueryRecord]]. */ +sealed trait QueryKind + +object QueryKind { + case object Assert extends QueryKind { override def toString = "assert" } + case object Check extends QueryKind { override def toString = "check" } + case object Push extends QueryKind { override def toString = "push" } + case object Pop extends QueryKind { override def toString = "pop" } +} diff --git a/src/main/scala/reporting/ProofQueryRecord.scala b/src/main/scala/reporting/ProofQueryRecord.scala index 9c0470c72..5cfeb0c21 100644 --- a/src/main/scala/reporting/ProofQueryRecord.scala +++ b/src/main/scala/reporting/ProofQueryRecord.scala @@ -7,31 +7,35 @@ package viper.silicon.reporting import viper.silver.ast -import viper.silicon.interfaces.decider.ProofQueryKind +import viper.silicon.interfaces.decider.{ProofQueryKind, QueryKind} import java.util.concurrent.ConcurrentLinkedQueue import scala.jdk.CollectionConverters._ /** - * One recorded SMT query (assert or check) with contextual information. + * One recorded solver interaction (assert, check, push, or pop) with contextual information. * - * @param isAssert true = emitted from [[viper.silicon.decider.Decider#assert]], - * false = emitted from [[viper.silicon.decider.Decider#check]] or - * [[viper.silicon.decider.Decider#checkSmoke]]. + * @param kind Which solver interaction this is — assert, check, push, or pop. See [[QueryKind]]. + * `assert` is emitted from [[viper.silicon.decider.Decider#assert]]; + * `check` from [[viper.silicon.decider.Decider#check]] or + * [[viper.silicon.decider.Decider#checkSmoke]]; + * `push`/`pop` from [[viper.silicon.decider.Decider#pushScope]] / + * [[viper.silicon.decider.Decider#popScope]]. * @param member Name of the program member (method/function/predicate/domain) whose * verification triggered this query, if known. * @param pos Source position of the proof obligation. - * @param kind Category of the query (see [[ProofQueryKind]]). + * @param category Category of the query (see [[ProofQueryKind]]) — e.g. PathInfeasibility for + * smoke checks, FunctionalCorrectness for user assertions, etc. * @param durationMs Wall-clock duration in milliseconds (includes prover call only, not * path-condition trivial-check short-circuit). - * @param succeeded Whether the query returned true / Unsat. + * @param succeeded Whether the query returned true / Unsat. Always true for push/pop. * @param description Optional free-text description of the specific proof obligation, * populated on demand at call sites where extra clarity is useful. */ case class ProofQueryRecord( - isAssert: Boolean, + kind: QueryKind, member: Option[String], pos: ast.Position, - kind: ProofQueryKind, + category: ProofQueryKind, durationMs: Double, succeeded: Boolean, description: Option[String] = None diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 0d6430a75..82e97018b 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -150,7 +150,7 @@ object brancher extends BranchingRules { } elseBranchVerifier = v0.uniqueId - executionFlowController.locally(s, v0)((s1, v1) => { + executionFlowController.locally(s, v0, description = Some("else-branch verification"))((s1, v1) => { v1.decider.prover.comment(s"[else-branch: $cnt | $negatedCondition]") v1.decider.setCurrentBranchCondition(negatedCondition, (negatedConditionExp, negatedConditionExpNew)) @@ -200,7 +200,7 @@ object brancher extends BranchingRules { val res = { val thenRes = if (executeThenBranch) { v.symbExLog.markReachable(uidBranchPoint) - executionFlowController.locally(s, v)((s1, v1) => { + executionFlowController.locally(s, v, description = Some("then-branch verification"))((s1, v1) => { v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") v1.decider.setCurrentBranchCondition(condition, conditionExp) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index dc8f9cbc6..1c45742c0 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -145,7 +145,8 @@ object chunkSupporter extends ChunkSupportRules { case _ => None } QS(s2.copy(h = s.h), h2, snap, v1) - case _ if v1.decider.checkSmoke(true, member = s1.currentMember.map(_.name), + case _ if v1.decider.checkSmoke(true, kind = ProofQueryKind.HeapInfeasibility, + member = s1.currentMember.map(_.name), description = Some("smoke check after consume")) => Success() // TODO: Mark branch as dead? case _ => @@ -273,7 +274,8 @@ object chunkSupporter extends ChunkSupportRules { member = s.currentMember.map(_.name), description = Some("lookup: chunk has permission")) => Q(s, ch.snap, v) - case _ if v.decider.checkSmoke(true, pos = resource.pos, member = s.currentMember.map(_.name), + case _ if v.decider.checkSmoke(true, kind = ProofQueryKind.HeapInfeasibility, + pos = resource.pos, member = s.currentMember.map(_.name), description = Some("smoke check at lookup")) => if (s.isInPackage) { val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown())) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 39346bec3..218c25532 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -562,7 +562,8 @@ object evaluator extends EvaluationRules { Q(s2, tQuant, eQuantNew, v1) case (s1, _, _, _, _, None, v1) => // This should not happen unless the current path is dead. - if (v1.decider.checkSmoke(true, pos = sourceQuant.pos, member = s1.currentMember.map(_.name), + if (v1.decider.checkSmoke(true, kind = ProofQueryKind.PathInfeasibility, + pos = sourceQuant.pos, member = s1.currentMember.map(_.name), description = Some("smoke check: quantifier body"))) { Unreachable() } else { @@ -1091,7 +1092,7 @@ object evaluator extends EvaluationRules { recordPossibleTriggers = true, possibleTriggers = Map.empty) // TODO: Why reset possibleTriggers if they are merged with s.possibleTriggers later anyway? type R = (State, Seq[Term], Option[Seq[ast.Exp]], Option[(Seq[Term], Option[Seq[ast.Exp]], Seq[Trigger], (Seq[Term], Seq[Quantification]), Option[(InsertionOrderedSet[DebugExp], InsertionOrderedSet[DebugExp])], Map[ast.Exp, Term])]) - executionFlowController.locallyWithResult[R](s1, v)((s2, v1, QB) => { + executionFlowController.locallyWithResult[R](s1, v, description = Some("quantified expression evaluation"))((s2, v1, QB) => { val preMark = v1.decider.setPathConditionMark() evals(s2, es1, _ => pve, v1)((s3, ts1, es1New, v2) => { val bc = And(ts1) diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 96d4a4de7..8f38469b7 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -15,12 +15,12 @@ import viper.silicon.supporters.AnnotationSupporter import viper.silicon.verifier.Verifier trait ExecutionFlowRules extends SymbolicExecutionRules { - def locallyWithResult[R](s: State, v: Verifier) + def locallyWithResult[R](s: State, v: Verifier, description: Option[String] = None) (block: (State, Verifier, R => VerificationResult) => VerificationResult) (Q: R => VerificationResult) : VerificationResult - def locally(s: State, v: Verifier) + def locally(s: State, v: Verifier, description: Option[String] = None) (block: (State, Verifier) => VerificationResult) : VerificationResult @@ -50,14 +50,15 @@ trait ExecutionFlowRules extends SymbolicExecutionRules { } object executionFlowController extends ExecutionFlowRules { - def locallyWithResult[R](s: State, v: Verifier) + def locallyWithResult[R](s: State, v: Verifier, description: Option[String] = None) (block: (State, Verifier, R => VerificationResult) => VerificationResult) (Q: R => VerificationResult) : VerificationResult = { var optBlockData: Option[R] = None - v.decider.pushScope() + val member = s.currentMember.map(_.name) + v.decider.pushScope(member = member, description = description) val blockResult: VerificationResult = block(s, v, blockData => { @@ -69,7 +70,7 @@ object executionFlowController extends ExecutionFlowRules { Success()}) - v.decider.popScope() + v.decider.popScope(member = member, description = description) blockResult match { case _: FatalResult => @@ -93,11 +94,11 @@ object executionFlowController extends ExecutionFlowRules { } } - def locally(s: State, v: Verifier) + def locally(s: State, v: Verifier, description: Option[String] = None) (block: (State, Verifier) => VerificationResult) : VerificationResult = - locallyWithResult[VerificationResult](s, v)((s1, v1, QL) => QL(block(s1, v1)))(Predef.identity) + locallyWithResult[VerificationResult](s, v, description)((s1, v1, QL) => QL(block(s1, v1)))(Predef.identity) private def tryOrFailWithResult[R](s: State, v: Verifier) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index ca6c72489..3fbe8ea83 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -256,7 +256,7 @@ object executor extends ExecutionRules { type PhaseData = (State, RecordedPathConditions, Set[FunctionDecl], Seq[MacroDecl]) var phase1data: Vector[PhaseData] = Vector.empty - (executionFlowController.locally(sBody, v)((s0, v0) => { + (executionFlowController.locally(sBody, v, description = Some("loop head: invariant well-definedness check"))((s0, v0) => { v0.decider.prover.comment("Loop head block: Check well-definedness of invariant") val mark = v0.decider.setPathConditionMark() produces(s0, freshSnap, invs, ContractNotWellformed, v0)((s1, v1) => { @@ -266,7 +266,7 @@ object executor extends ExecutionRules { v1.decider.freshMacros /* [BRANCH-PARALLELISATION] */) Success() })}) - combine executionFlowController.locally(s, v)((s0, v0) => { + combine executionFlowController.locally(s, v, description = Some("loop head: establish invariant"))((s0, v0) => { v0.decider.prover.comment("Loop head block: Establish invariant") consumes(s0, invs, false, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => { v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)") @@ -274,12 +274,13 @@ object executor extends ExecutionRules { case (result, _) if !result.continueVerification => result case (intermediateResult, (s1, pcs, ff1, fm1)) => /* [BRANCH-PARALLELISATION] ff1, m1 */ val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts) - intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => { + intermediateResult combine executionFlowController.locally(s2, v1, description = Some("loop head: execute statements in invariant state"))((s3, v2) => { v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */ v2.decider.declareAndRecordAsFreshMacros(fm1.filter(!v2.decider.freshMacros.contains(_))) /* [BRANCH-PARALLELISATION] */ v2.decider.assume(pcs.assumptions, Option.when(withExp)(DebugExp.createInstance("Loop invariant", pcs.assumptionExps)), false) v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) - if (v2.decider.checkSmoke(member = s3.currentMember.map(_.name), + if (v2.decider.checkSmoke(kind = ProofQueryKind.PathInfeasibility, + member = s3.currentMember.map(_.name), description = Some("smoke check: post-statement"))) Success() else { @@ -289,7 +290,7 @@ object executor extends ExecutionRules { edgeConditions.foldLeft(Success(): VerificationResult) { case (result, _) if !result.continueVerification => result case (intermediateResult, eCond) => - intermediateResult combine executionFlowController.locally(s4, v3)((s5, v4) => { + intermediateResult combine executionFlowController.locally(s4, v3, description = Some("loop head: edge-condition well-definedness"))((s5, v4) => { eval(s5, eCond, WhileFailed(eCond), v4)((_, _, _, _) => Success()) }) @@ -434,7 +435,8 @@ object executor extends ExecutionRules { case assert @ ast.Assert(a: ast.FalseLit) if !s.isInPackage => /* "assert false" triggers a smoke check. If successful, we backtrack. */ executionFlowController.tryOrFail0(s.copy(h = magicWandSupporter.getEvalHeap(s)), v)((s1, v1, QS) => { - if (v1.decider.checkSmoke(true, pos = assert.pos, member = s1.currentMember.map(_.name), + if (v1.decider.checkSmoke(true, kind = ProofQueryKind.PathInfeasibility, + pos = assert.pos, member = s1.currentMember.map(_.name), description = Some("smoke check: assert statement"))) QS(s1.copy(h = s.h), v1) else diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala index c2dbdb6a9..0d416ac6e 100644 --- a/src/main/scala/rules/Joiner.scala +++ b/src/main/scala/rules/Joiner.scala @@ -54,7 +54,7 @@ object joiner extends JoiningRules { val joiningRecord = new JoiningRecord(s, v.decider.pcs) val uidJoin = v.symbExLog.openScope(joiningRecord) - executionFlowController.locally(s, v)((s1, v1) => { + executionFlowController.locally(s, v, description = Some("join-point coordination"))((s1, v1) => { val preMark = v1.decider.setPathConditionMark() val s2 = s1.copy(underJoin = true) diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 41775af9e..e928a7ae4 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -197,7 +197,8 @@ object magicWandSupporter extends SymbolicExecutionRules { * from heap, i.e. that tEq does not result in already having the required permissions before * consuming from heap. */ - if (v.decider.checkSmoke(member = sOut.currentMember.map(_.name), + if (v.decider.checkSmoke(kind = ProofQueryKind.PathInfeasibility, + member = sOut.currentMember.map(_.name), description = Some("smoke check: magic wand"))) { (Complete(), sOut, h +: hps, cch +: cchs) } else { @@ -355,7 +356,7 @@ object magicWandSupporter extends SymbolicExecutionRules { }) } - val tempResult = executionFlowController.locally(sEmp, v)((s1, v1) => { + val tempResult = executionFlowController.locally(sEmp, v, description = Some("magic wand: package operation"))((s1, v1) => { /* A snapshot (binary tree) will be constructed using First/Second datatypes, * that preserves the original root. The leafs of this tree will later appear * in the snapshot of the RHS at the appropriate places. Thus equating @@ -428,7 +429,7 @@ object magicWandSupporter extends SymbolicExecutionRules { ) // We execute the continuation Q in a new scope with all branch conditions and all conserved path conditions. - executionFlowController.locally(s1, v)((s2, v1) => { + executionFlowController.locally(s1, v, description = Some("magic wand: continuation in branch scope"))((s2, v1) => { val exp = viper.silicon.utils.ast.BigAnd(branchConditionsExp.map(_._1)) val expNew = Option.when(withExp)(viper.silicon.utils.ast.BigAnd(branchConditionsExp.map(_._2.get))) // Set the branch conditions diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index a676efb8c..8713d73b4 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -209,7 +209,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq if (relevantChunks.isEmpty) { - if (v.decider.checkSmoke(true, pos = resource.pos, member = s.currentMember.map(_.name), + if (v.decider.checkSmoke(true, kind = ProofQueryKind.HeapInfeasibility, + pos = resource.pos, member = s.currentMember.map(_.name), description = Some("MCE smoke check"))) { if (s.isInPackage) { val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown())) diff --git a/src/main/scala/supporters/CfgSupporter.scala b/src/main/scala/supporters/CfgSupporter.scala index eb37ae205..c1175928e 100644 --- a/src/main/scala/supporters/CfgSupporter.scala +++ b/src/main/scala/supporters/CfgSupporter.scala @@ -54,7 +54,7 @@ trait DefaultCfgVerificationUnitProvider extends VerifierComponent { v: Verifier } val result = { - executionFlowController.locally(s, v)((s3, v3) => { + executionFlowController.locally(s, v, description = Some("CFG execution"))((s3, v3) => { exec(s3, cfg, v3)((_, _) => Success())}) } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 1b478ec4d..1452ce94d 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -81,11 +81,11 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif /* Combined the well-formedness check and the execution of the body, which are two separate * rules in Smans' paper. */ - executionFlowController.locally(s, v)((s1, v1) => { + executionFlowController.locally(s, v, description = Some("method: precondition production and body verification"))((s1, v1) => { produces(s1, freshSnap, pres, ContractNotWellformed, v1)((s2, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) val s2a = s2.copy(oldHeaps = s2.oldHeaps + (Verifier.PRE_STATE_LABEL -> s2.h)) - ( executionFlowController.locally(s2a, v2)((s3, v3) => { + ( executionFlowController.locally(s2a, v2, description = Some("method: postcondition well-formedness"))((s3, v3) => { val s4 = s3.copy(h = v3.heapSupporter.getEmptyHeap(s3.program)) val impLog = new WellformednessCheckRecord(posts, s, v.decider.pcs) val sepIdentifier = symbExLog.openScope(impLog) @@ -93,7 +93,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif symbExLog.closeScope(sepIdentifier) Success()})}) && { - executionFlowController.locally(s2a, v2)((s3, v3) => { + executionFlowController.locally(s2a, v2, description = Some("method: body execution and postcondition check"))((s3, v3) => { exec(s3, body, v3)((s4, v4) => { BenchmarkMetrics.incPaths(method.name) consumes(s4, posts, false, postViolated, v4)((_, _, _) => diff --git a/src/main/scala/supporters/PredicateVerificationUnit.scala b/src/main/scala/supporters/PredicateVerificationUnit.scala index 803cd5814..d3b6123a6 100644 --- a/src/main/scala/supporters/PredicateVerificationUnit.scala +++ b/src/main/scala/supporters/PredicateVerificationUnit.scala @@ -122,7 +122,7 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve case Some(body) => /* locallyXXX { magicWandSupporter.checkWandsAreSelfFraming(σ.γ, σ.h, predicate, c)} - &&*/ executionFlowController.locally(s, v)((s1, _) => { + &&*/ executionFlowController.locally(s, v, description = Some("predicate: body production"))((s1, _) => { produce(s1, toSf(snap), body, err, v)((s2, v2) => { // PredicateVerificationMetrics.incPath(predicate.name) BenchmarkMetrics.incPaths(predicate.name) diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 31a198faa..3a22961e9 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -229,7 +229,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver var phase1Data: Seq[Phase1Data] = Vector.empty var recorders: Seq[FunctionRecorder] = Vector.empty - val result = executionFlowController.locally(s, v)((s0, _) => { + val result = executionFlowController.locally(s, v, description = Some("function: precondition and postcondition production"))((s0, _) => { val preMark = decider.setPathConditionMark() produces(s0, toSf(`?s`), pres, ContractNotWellformed, v)((s1, _) => { val relevantPathConditionStack = decider.pcs.after(preMark) @@ -264,7 +264,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver val result = phase1data.foldLeft(Success(): VerificationResult) { case (fatalResult: FatalResult, _) => fatalResult case (intermediateResult, Phase1Data(sPre, bcsPre, bcsPreExp, pcsPre, pcsPreExp)) => - intermediateResult && executionFlowController.locally(sPre, v)((s1, _) => { + intermediateResult && executionFlowController.locally(sPre, v, description = Some("function: body evaluation and postcondition check"))((s1, _) => { decider.setCurrentBranchCondition(And(bcsPre), (BigAnd(bcsPreExp.map(_._1)), Option.when(wExp)(BigAnd(bcsPreExp.map(_._2.get))))) decider.assume(pcsPre, Option.when(wExp)(DebugExp.createInstance(s"precondition of ${function.name}", pcsPreExp.get)), enforceAssumption = false) v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)