Improve SymbExLogger (#622)

* Improve SymbExLogger:
- Thread safe as long as silicon parallelizes up to the entity level: SymbLog itself is not thread safe. --ideModeAdvanced accordingly does not require --numberOfParallelVerifiers 1 anymore.
- Change SymbLog to accept a listener for appropriate events.

* move smt delta calculation to ProverStdIO for thread safety

* move smt statistics calculations out of ProverStdIO

* Bump silver submodule to master branch version

* move symbexlogger state into classes, shim the old usage

* make Verifier own a current MemberSymbExLogger

* Give Verifier the capability to open symbexlogs for members
The root symbexlog comes from Silicon and is computed explicitly on configuration, so it can be overridden
From there, the MainVerifier owns the root log, and WorkerVerifiers ask the MainVerifier for a member-scoped symbexlog

* swap out shims

* some bugs:
- do not use newEntityLogger directly, because it's not inserted in the members of the root log
- synchronize on the log instead of the map, because I'm using a var instead of mutable.Map
- delay opening the member scope to avoid using early initializers

* address comment

* make NoopLog do nothing

* also do nothing on whenEnabled for NoopLog

* symbexlogs can be closed: they do not accept further records (now unrelated to closeMemberScope)

* close log on timeout

* SymbExLogger.ofConfig makes the silicon slightly less lazy, so invalid options are not silently ignored when doing nothing

* use NoopMemberSymbExLog if there is no log yet (a bug, but better than crashing)
disallow use of ideModeAdvanced in the presence of parallelizeBranches

* move config to concrete logger; state is always null, so drop it.

* update silver

* change by-name trickery to lambdas

* remove debug println

* namespace Member

* clarify val names for Config vs LogConfig

* Revert "change by-name trickery to lambdas"

This reverts commit 505c61b.

* validateFileOpt already checks whether the file exists

* log a warning when the symbexlog config cannot be parsed

* no delta for values not yet encountered

* use the symbExLog of the current verifier

* resolve warnings: clean up imports; mark unused vals as @unused

* missed merge conflict: just use ours

* adjust documentation

* update silver

Co-authored-by: Pieter Bos <p.h.bos@student.utwente.nl>

Author: pieter-bos

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

@@ -15,7 +15,6 @@ import viper.silicon._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
 import viper.silicon.interfaces.decider._
-import viper.silicon.logger.SymbExLogger
 import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord}
 import viper.silicon.state._
 import viper.silicon.state.terms._
@@ -183,18 +182,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 +222,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 +251,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 +279,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(