Record push/pop operations and refactor proof query tracking

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(

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))

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
 }

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"    }
+}

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

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)
 

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()))

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)

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)