benchmarking file in symbex logger

src/main/scala/Config.scala

@@ -784,6 +784,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val benchmark = opt[Boolean]("benchmark",
+    descr = "Prints benchmarking information using the SymbExLogger",
+    default = Some(false),
+    noshort = true,
+    hidden = true
+  )
+
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {
@@ -805,6 +812,15 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       sys.error(s"Unexpected combination: $other")
   }
 
+  validateOpt(benchmark, parallelizeBranches) {
+    case (Some(false), _) => Right(())
+    case (_, Some(false)) => Right(())
+    case (Some(true), Some(true)) =>
+      Left(s"Option ${benchmark.name} is not supported in combination with ${parallelizeBranches.name}")
+    case other =>
+      sys.error(s"Unexpected combination: $other")
+  }
+
   validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
     case (Some(_), Some(false), None) |
          (Some(_), Some(_), Some(ExhaleMode.Greedy)) =>

src/main/scala/Silicon.scala

@@ -206,7 +206,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
         result = Some(condenseToViperResult(failures))
       } catch { /* Catch exceptions thrown during verification (errors are not caught) */
         case _: TimeoutException =>
-          if (config.ideModeAdvanced()) {
+          if (config.ideModeAdvanced() || config.benchmark()) {
             symbExLog.close()
             reporter report ExecutionTraceReport(symbExLog.logs.toSeq, List(), List())
           }

src/main/scala/logger/SymbExLogger.scala

@@ -193,7 +193,7 @@ import scala.util.{Failure, Success, Try}
 
 case object SymbExLogger {
   def ofConfig(config: Config): SymbExLogger[_ <: MemberSymbExLogger] = {
-    if(config.ideModeAdvanced())
+    if(config.ideModeAdvanced() || config.benchmark())
       SymbExLog(parseLogConfig(config))
     else
       NoopSymbExLog
@@ -579,4 +579,4 @@ class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog],
     // no close scope is inserted because branches are not considered scopes
     branchingStack = branchingStack.tail
   }
-}
+}

src/main/scala/logger/benchmarker/SymbExLogBenchmarker.scala

@@ -0,0 +1,18 @@
+package viper.silicon.logger.benchmarker
+
+import viper.silicon.logger.MemberSymbExLogger
+import viper.silicon.logger.SymbExLogger
+import viper.silicon.logger.writer.SymbExLogReportWriter
+import viper.silicon.logger.MemberSymbExLog
+
+object SymbExLogBenchmarker {
+  def analyse(l: SymbExLogger[_ <: MemberSymbExLogger]): Unit = {
+    for (log <- l.logs) {
+      val allRecords = SymbExLogReportWriter.getAllRecords(log.asInstanceOf[MemberSymbExLog].log)
+      for (rec <- allRecords) {
+        println(rec.getClass())
+      }
+    }
+  }
+}
+

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -22,6 +22,7 @@ import viper.silicon.extensions.ConditionalPermissionRewriter
 import viper.silicon.interfaces._
 import viper.silicon.interfaces.decider.ProverLike
 import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger}
+import viper.silicon.logger.writer.SymbExLogReportWriter
 import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
 import viper.silicon.state._
 import viper.silicon.state.terms.{Decl, Sort, Term, sorts}
@@ -34,6 +35,9 @@ import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.cfg.silver.SilverCfg
 import viper.silver.reporter.{AnnotationWarning, ConfigurationConfirmation, ExecutionTraceReport, QuantifierChosenTriggersMessage, Reporter, VerificationResultMessage, VerificationTerminationMessage, WarningsDuringVerification}
 import viper.silver.verifier.VerifierWarning
+import spray.json.JsArray
+import viper.silicon.logger.{LogConfig, MemberSymbExLog}
+import viper.silicon.logger.benchmarker.SymbExLogBenchmarker
 
 /* TODO: Extract a suitable MainVerifier interface, probably including
  *         - def verificationPoolManager: VerificationPoolManager)
@@ -284,6 +288,11 @@ class DefaultMainVerifier(config: Config,
         this.axiomsAfterAnalysis().toList,
         this.postConditionAxioms().toList)
     }
+
+    if (config.benchmark()) {
+      SymbExLogBenchmarker.analyse(rootSymbExLogger)
+      //println(SymbExLogReportWriter.toJSON(rootSymbExLogger.logs.toSeq.asInstanceOf[Seq[MemberSymbExLog]], LogConfig.default()) : JsArray)
+    }
     reporter report VerificationTerminationMessage()
 
     (   functionVerificationResults