Improve SymbExLogger

src/main/scala/Config.scala

@@ -754,19 +754,15 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => Right(())
   }
 
-  validateOpt(ideModeAdvanced, numberOfParallelVerifiers) {
-    case (Some(false), _) =>
-      Right(())
-    case (Some(true), Some(n)) =>
-      if (n == 1)
-        Right(())
-      else
-        Left(  s"Option ${ideModeAdvanced.name} requires setting "
-             + s"${numberOfParallelVerifiers.name} to 1")
+  validateOpt(ideModeAdvanced, parallelizeBranches) {
+    case (Some(false), _) => Right(())
+    case (_, Some(false)) => Right(())
+    case (Some(true), Some(true)) =>
+      Left(s"Option ${ideModeAdvanced.name} is not supported in combination with ${parallelizeBranches.name}")
     case other =>
       sys.error(s"Unexpected combination: $other")
   }
-  
+
   validateOpt(counterexample, enableMoreCompleteExhale) {
     case (Some(_), Some(false)) => Left(  s"Option ${counterexample.name} requires setting "
                                         + s"flag ${enableMoreCompleteExhale.name}")

src/main/scala/Silicon.scala

@@ -8,7 +8,6 @@ package viper.silicon
 
 import java.text.SimpleDateFormat
 import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException}
-
 import scala.collection.immutable.ArraySeq
 import scala.util.{Left, Right}
 import ch.qos.logback.classic.{Level, Logger}
@@ -19,7 +18,7 @@ import viper.silver.frontend.{DefaultStates, SilFrontend}
 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.SymbExLogger
+import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger}
 import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
 import viper.silicon.verifier.DefaultMainVerifier
 import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
@@ -93,6 +92,10 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
   private var _config: Config = _
   final def config = _config
 
+  private var _symbExLog: SymbExLogger[_ <: MemberSymbExLogger] = _
+  final def symbExLog = _symbExLog
+  final def symbExLog_=(log: SymbExLogger[_ <: MemberSymbExLogger]) = { _symbExLog = log }
+
   private sealed trait LifetimeState
 
   private object LifetimeState {
@@ -113,6 +116,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     lifetimeState = LifetimeState.Configured
 
     _config = new Config(args)
+    _symbExLog = SymbExLogger.ofConfig(_config)
   }
 
   def debugInfo(debugInfo: Seq[(String, Any)]): Unit = { this.debugInfo = debugInfo }
@@ -129,7 +133,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
     setLogLevelsFromConfig()
 
-    verifier = new DefaultMainVerifier(config, reporter)
+    verifier = new DefaultMainVerifier(config, reporter, symbExLog)
     verifier.start()
   }
 
@@ -202,10 +206,9 @@ 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 =>
-          // verification was interrupted, therefore close the current member's scope:
-          SymbExLogger.currentLog().closeMemberScope()
           if (config.ideModeAdvanced()) {
-            reporter report ExecutionTraceReport(SymbExLogger.memberList, List(), List())
+            symbExLog.close()
+            reporter report ExecutionTraceReport(symbExLog.logs.toSeq, List(), List())
           }
           result = Some(SilFailure(SilTimeoutOccurred(config.timeout(), "second(s)") :: Nil))
         case exception: Exception if !config.disableCatchingExceptions() =>

src/main/scala/decider/Decider.scala

@@ -183,18 +183,18 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def pushScope(): Unit = {
       //val commentRecord = new CommentRecord("push", null, null)
-      //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord)
+      //val sepIdentifier = symbExLog.openScope(commentRecord)
       pathConditions.pushScope()
       _prover.push(timeout = Verifier.config.pushTimeout.toOption)
-      //SymbExLogger.currentLog().closeScope(sepIdentifier)
+      //symbExLog.closeScope(sepIdentifier)
     }
 
     def popScope(): Unit = {
       //val commentRecord = new CommentRecord("pop", null, null)
-      //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord)
+      //val sepIdentifier = symbExLog.openScope(commentRecord)
       _prover.pop()
       pathConditions.popScope()
-      //SymbExLogger.currentLog().closeScope(sepIdentifier)
+      //symbExLog.closeScope(sepIdentifier)
     }
 
     def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit = {
@@ -223,15 +223,15 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term]) = {
       val assumeRecord = new DeciderAssumeRecord(terms)
-      val sepIdentifier = SymbExLogger.currentLog().openScope(assumeRecord)
+      val sepIdentifier = symbExLog.openScope(assumeRecord)
 
       /* Add terms to Silicon-managed path conditions */
       terms foreach pathConditions.add
 
       /* Add terms to the prover's assumptions */
       terms foreach prover.assume
 
-      SymbExLogger.currentLog().closeScope(sepIdentifier)
+      symbExLog.closeScope(sepIdentifier)
       None
     }
 
@@ -252,21 +252,21 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       // previously (it did not cause a verification failure) and ignore the
       // current one, because it cannot cause a verification error.
       if (success)
-        SymbExLogger.currentLog().discardSMTQuery()
+        symbExLog.discardSMTQuery()
       else
-        SymbExLogger.currentLog().setSMTQuery(t)
+        symbExLog.setSMTQuery(t)
 
       Q(success)
     }
 
     private def deciderAssert(t: Term, timeout: Option[Int]) = {
       val assertRecord = new DeciderAssertRecord(t, timeout)
-      val sepIdentifier = SymbExLogger.currentLog().openScope(assertRecord)
+      val sepIdentifier = symbExLog.openScope(assertRecord)
 
       val asserted = isKnownToBeTrue(t)
       val result = asserted || proverAssert(t, timeout)
 
-      SymbExLogger.currentLog().closeScope(sepIdentifier)
+      symbExLog.closeScope(sepIdentifier)
       result
     }
 
@@ -280,17 +280,15 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     private def proverAssert(t: Term, timeout: Option[Int]) = {
       val assertRecord = new ProverAssertRecord(t, timeout)
-      val sepIdentifier = SymbExLogger.currentLog().openScope(assertRecord)
+      val sepIdentifier = symbExLog.openScope(assertRecord)
 
       val result = prover.assert(t, timeout)
 
-      if (SymbExLogger.enabled) {
-        val statistics = prover.statistics()
-        val deltaStatistics = SymbExLogger.getDeltaSmtStatistics(statistics)
-        assertRecord.statistics = Some(statistics ++ deltaStatistics)
+      symbExLog.whenEnabled {
+        assertRecord.statistics = Some(symbExLog.deltaStatistics(prover.statistics()))
       }
 
-      SymbExLogger.currentLog().closeScope(sepIdentifier)
+      symbExLog.closeScope(sepIdentifier)
 
       result
     }

src/main/scala/logger/LogConfig.scala

@@ -7,10 +7,23 @@
 package viper.silicon.logger
 
 import spray.json._
+import viper.silicon.logger.records.data.DataRecord
 
 case class LogConfig(isBlackList: Boolean,
                      includeStore: Boolean, includeHeap: Boolean, includeOldHeap: Boolean, includePcs: Boolean,
-                     recordConfigs: List[RecordConfig])
+                     recordConfigs: List[RecordConfig]) {
+  def getRecordConfig(d: DataRecord): Option[RecordConfig] = {
+    for (rc <- recordConfigs) {
+      if (rc.kind.equals(d.toTypeString)) {
+        rc.value match {
+          case Some(value) => if (value.equals(d.toSimpleString)) return Some(rc)
+          case None => return Some(rc)
+        }
+      }
+    }
+    None
+  }
+}
 
 object LogConfig {
   def default(): LogConfig = LogConfig(