[Experimental] Classify each SMT-query

src/main/scala/Config.scala

@@ -691,6 +691,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val recordProofQueries: ScallopOption[String] = opt[String]("recordProofQueries",
+    descr = "Path to a CSV file to which SMT query statistics (kind, member, source position, duration) are written at the end of verification",
+    default = None,
+    noshort = true
+  )
+
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {

src/main/scala/Silicon.scala

@@ -19,7 +19,7 @@ import viper.silver.reporter._
 import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.interfaces.Failure
 import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger}
-import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
+import viper.silicon.reporting.{MultiRunRecorders, ProofQueryCollector, condenseToViperResult}
 import viper.silicon.verifier.DefaultMainVerifier
 import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
 import viper.silver.cfg.silver.SilverCfg
@@ -234,6 +234,27 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
       }
 
       assert(result.nonEmpty, "The result of the verification run wasn't stored appropriately")
+
+      /* Write proof-query CSV if requested */
+      config.recordProofQueries.toOption.foreach { path =>
+        val header = "isAssert,member,file,line,column,kind,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,
+              r.description.getOrElse("")).mkString(",")
+        }
+        java.nio.file.Files.write(
+          java.nio.file.Paths.get(path),
+          (header +: rows).mkString("\n").getBytes(java.nio.charset.StandardCharsets.UTF_8)
+        )
+        ProofQueryCollector.clear()
+      }
+
       result.get
     }
   }

src/main/scala/decider/Decider.scala

@@ -13,6 +13,7 @@ import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
 import viper.silicon.interfaces.decider._
 import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord}
+import viper.silicon.reporting.{ProofQueryCollector, ProofQueryRecord}
 import viper.silicon.state._
 import viper.silicon.state.terms.{Term, _}
 import viper.silicon.utils.ast.{extractPTypeFromExp, simplifyVariableName}
@@ -49,7 +50,10 @@ trait Decider {
   def pushScope(): Unit
   def popScope(): Unit
 
-  def checkSmoke(isAssert: Boolean = false): Boolean
+  def checkSmoke(isAssert: Boolean = false,
+                 pos: ast.Position = ast.NoPosition,
+                 member: Option[String] = None,
+                 description: Option[String] = None): Boolean
 
   def setCurrentBranchCondition(t: Term, te: (ast.Exp, Option[ast.Exp])): Unit
   def setPathConditionMark(): Mark
@@ -67,13 +71,23 @@ trait Decider {
   def assume(assumptions: InsertionOrderedSet[(Term, Option[DebugExp])], enforceAssumption: Boolean = false, isDefinition: Boolean = false): Unit
   def assume(terms: Iterable[Term], debugExp: Option[DebugExp], enforceAssumption: Boolean): Unit
 
-  def check(t: Term, timeout: Int): Boolean
+  def check(t: Term, timeout: Int,
+            kind: ProofQueryKind,
+            pos: ast.Position = ast.NoPosition,
+            member: Option[String] = None,
+            description: Option[String] = None): Boolean
 
   /* TODO: Consider changing assert such that
    *         1. It passes State and Operations to the continuation
    *         2. The implementation reacts to a failing assertion by e.g. a state consolidation
    */
-  def assert(t: Term, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
+  def assert(t: Term,
+             kind: ProofQueryKind,
+             timeout: Option[Int] = None,
+             pos: ast.Position = ast.NoPosition,
+             member: Option[String] = None,
+             description: Option[String] = None
+            )(Q: Boolean => VerificationResult): VerificationResult
 
   def fresh(id: String, sort: Sort, ptype: Option[PType]): Var
   def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function
@@ -361,18 +375,42 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     /* Asserting facts */
 
-    def checkSmoke(isAssert: Boolean = false): Boolean = {
+    def checkSmoke(isAssert: Boolean = false,
+                   pos: ast.Position = ast.NoPosition,
+                   member: Option[String] = None,
+                   description: Option[String] = None): Boolean = {
       val timeout = if (isAssert) Verifier.config.assertTimeout.toOption else Verifier.config.checkTimeout.toOption
-      prover.check(timeout) == Unsat
-    }
-
-    def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout))
-
-    def assert(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
-              (Q: Boolean => VerificationResult)
-              : VerificationResult = {
-
-      val success = deciderAssert(t, timeout)
+      val t0  = System.nanoTime()
+      val res = prover.check(timeout) == Unsat
+      val dur = (System.nanoTime() - t0) / 1e6
+      if (Verifier.config.recordProofQueries.isDefined)
+        ProofQueryCollector.record(ProofQueryRecord(
+          isAssert    = false,
+          member      = member,
+          pos         = pos,
+          kind        = ProofQueryKind.PathInfeasibility,
+          durationMs  = dur,
+          succeeded   = res,
+          description = description))
+      res
+    }
+
+    def check(t: Term, timeout: Int,
+              kind: ProofQueryKind,
+              pos: ast.Position = ast.NoPosition,
+              member: Option[String] = None,
+              description: Option[String] = None): Boolean =
+      deciderAssert(t, Some(timeout), kind, pos, member, description, isAssert = false)
+
+    def assert(t: Term,
+               kind: ProofQueryKind,
+               timeout: Option[Int] = Verifier.config.assertTimeout.toOption,
+               pos: ast.Position = ast.NoPosition,
+               member: Option[String] = None,
+               description: Option[String] = None
+              )(Q: Boolean => VerificationResult): VerificationResult = {
+
+      val success = deciderAssert(t, timeout, kind, pos, member, description, isAssert = true)
 
       // If the SMT query was not successful, store it (possibly "overwriting"
       // any previously saved query), otherwise discard any query we had saved
@@ -386,12 +424,29 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       Q(success)
     }
 
-    private def deciderAssert(t: Term, timeout: Option[Int]) = {
+    private def deciderAssert(t: Term, timeout: Option[Int],
+                               kind: ProofQueryKind,
+                               pos: ast.Position = ast.NoPosition,
+                               member: Option[String] = None,
+                               description: Option[String] = None,
+                               isAssert: Boolean = true) = {
       val assertRecord = new DeciderAssertRecord(t, timeout)
       val sepIdentifier = symbExLog.openScope(assertRecord)
 
-      val asserted = isKnownToBeTrue(t)
-      val result = asserted || proverAssert(t, timeout)
+      val alreadyKnown = isKnownToBeTrue(t)
+      val t0     = System.nanoTime()
+      val result = alreadyKnown || proverAssert(t, timeout)
+      val durMs  = (System.nanoTime() - t0) / 1e6
+
+      if (Verifier.config.recordProofQueries.isDefined && !alreadyKnown)
+        ProofQueryCollector.record(ProofQueryRecord(
+          isAssert    = isAssert,
+          member      = member,
+          pos         = pos,
+          kind        = kind,
+          durationMs  = durMs,
+          succeeded   = result,
+          description = description))
 
       symbExLog.closeScope(sepIdentifier)
       result

src/main/scala/interfaces/decider/ProofQueryKind.scala

@@ -0,0 +1,36 @@
+// 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
+
+/** Categorises the purpose of an SMT query (assert or check) issued by the verifier. */
+sealed trait ProofQueryKind
+
+object ProofQueryKind {
+  /** (a) Consistency checks: non-negative/positive permission assertions, injectivity checks
+   *  in quantified permissions, and similar well-formedness obligations. */
+  case object Consistency extends ProofQueryKind
+
+  /** (b) Heap proof obligations: chunk-existence checks, permission-amount checks during
+   *  consume/produce operations, and related heap-access correctness queries. */
+  case object Heap extends ProofQueryKind
+
+  /** (c) Functional-correctness queries: pre/postcondition checks, assert-statement assertions,
+   *  array-index bounds, divisor non-zero, and similar user-visible proof obligations. */
+  case object FunctionalCorrectness extends ProofQueryKind
+
+  /** (d) Axiomatisation queries: consistency of function, domain, or predicate axioms
+   *  (rare – axioms are mostly assumed, not asserted). */
+  case object Axiomatization extends ProofQueryKind
+
+  /** (e) Path-infeasibility checks: smoke checks and branch-feasibility tests that determine
+   *  whether the current execution path is reachable at all. */
+  case object PathInfeasibility 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
+}

src/main/scala/reporting/ProofQueryRecord.scala

@@ -0,0 +1,54 @@
+// 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.reporting
+
+import viper.silver.ast
+import viper.silicon.interfaces.decider.ProofQueryKind
+import java.util.concurrent.ConcurrentLinkedQueue
+import scala.jdk.CollectionConverters._
+
+/**
+ * One recorded SMT query (assert or check) 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 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 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 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,
+  member:      Option[String],
+  pos:         ast.Position,
+  kind:        ProofQueryKind,
+  durationMs:  Double,
+  succeeded:   Boolean,
+  description: Option[String] = None
+)
+
+/**
+ * Thread-safe global collector for [[ProofQueryRecord]]s.
+ *
+ * Records are appended concurrently during parallel verification and can be
+ * retrieved at the end via [[records]]. Call [[clear]] between verification runs.
+ */
+object ProofQueryCollector {
+  private val _records = new ConcurrentLinkedQueue[ProofQueryRecord]()
+
+  def record(r: ProofQueryRecord): Unit = _records.add(r)
+
+  def records: Seq[ProofQueryRecord] = _records.iterator().asScala.toSeq
+
+  def clear(): Unit = _records.clear()
+}

src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala

@@ -8,13 +8,15 @@ package viper.silicon.resources
 
 import viper.silicon.Map
 import viper.silicon.interfaces.state._
+import viper.silicon.interfaces.decider.ProofQueryKind
 import viper.silicon.state.terms.Term
 import viper.silicon.state.{QuantifiedBasicChunk, terms}
 import viper.silicon.utils.ast.{BigAnd, replaceVarsInExp}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
 
-class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier) extends PropertyInterpreter {
+class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier,
+                                        member: Option[String] = None) extends PropertyInterpreter {
 
   protected case class Info(pm: Map[ChunkPlaceholder, GeneralChunk], resourceID: ResourceID) {
     def addMapping(cp: ChunkPlaceholder, ch: GeneralChunk) = Info(pm + (cp -> ch), resourceID)
@@ -120,7 +122,9 @@ class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier
                                     otherwise: PropertyExpression[K],
                                     info: Info): (Term, Option[ast.Exp]) = {
     val conditionTerm = buildPathCondition(condition, info)._1
-    if (verifier.decider.check(conditionTerm, Verifier.config.checkTimeout())) {
+    if (verifier.decider.check(conditionTerm, Verifier.config.checkTimeout(),
+                               kind = ProofQueryKind.Heap, member = member,
+                               description = Some("chunk property condition"))) {
       buildPathCondition(thenDo, info)
     } else {
       buildPathCondition(otherwise, info)

src/main/scala/rules/Brancher.scala

@@ -10,6 +10,7 @@ import java.util.concurrent._
 import viper.silicon.common.concurrency._
 import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Unreachable, VerificationResult}
+import viper.silicon.interfaces.decider.ProofQueryKind
 import viper.silicon.reporting.condenseToViperResult
 import viper.silicon.state.State
 import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term}
@@ -59,13 +60,21 @@ object brancher extends BranchingRules {
     /* True if the then-branch is to be explored */
     val executeThenBranch = (
          skipPathFeasibilityCheck
-      || !v.decider.check(negatedCondition, Verifier.config.checkTimeout()))
+      || !v.decider.check(negatedCondition, Verifier.config.checkTimeout(),
+                          kind = ProofQueryKind.PathInfeasibility,
+                          pos = conditionExp._1.pos,
+                          member = s.currentMember.map(_.name),
+                          description = Some("else-branch feasibility")))
 
     /* False if the then-branch is to be explored */
     val executeElseBranch = (
          !executeThenBranch /* Assumes that ast least one branch is feasible */
       || skipPathFeasibilityCheck
-      || !v.decider.check(condition, Verifier.config.checkTimeout()))
+      || !v.decider.check(condition, Verifier.config.checkTimeout(),
+                          kind = ProofQueryKind.PathInfeasibility,
+                          pos = conditionExp._1.pos,
+                          member = s.currentMember.map(_.name),
+                          description = Some("then-branch feasibility")))
 
     val parallelizeElseBranch = s.parallelizeBranches && executeThenBranch && executeElseBranch