Improve SymbExLogger

src/main/scala/Config.scala

@@ -735,19 +735,6 @@ 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")
-    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

@@ -208,7 +208,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
           // verification was interrupted, therefore close the current member's scope:
           SymbExLogger.currentLog().closeMemberScope()
           if (config.ideModeAdvanced()) {
-            reporter report ExecutionTraceReport(SymbExLogger.memberList, List(), List())
+            reporter report ExecutionTraceReport(SymbExLogger.memberList.toIndexedSeq, List(), List())
           }
           result = Some(SilFailure(SilTimeoutOccurred(config.timeout(), "second(s)") :: Nil))
         case exception: Exception if !config.disableCatchingExceptions() =>

src/main/scala/decider/Decider.scala

@@ -263,9 +263,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       val result = prover.assert(t, timeout)
 
       if (SymbExLogger.enabled) {
-        val statistics = prover.statistics()
-        val deltaStatistics = SymbExLogger.getDeltaSmtStatistics(statistics)
-        assertRecord.statistics = Some(statistics ++ deltaStatistics)
+        assertRecord.statistics = Some(prover.deltaStatistics())
       }
 
       SymbExLogger.currentLog().closeScope(sepIdentifier)

src/main/scala/decider/ProverStdIO.scala

@@ -40,6 +40,7 @@ abstract class ProverStdIO(uniqueId: String,
 
   var proverPath: Path = _
   var lastModel : String = _
+  var lastStatistics: Map[String, String] = Map.empty
 
   def name: String
   def minVersion: Version
@@ -319,7 +320,7 @@ abstract class ProverStdIO(uniqueId: String,
     }
   }
 
-  def statistics(): Map[String, String] = {
+  private def queryStatistics(): Map[String, String] = {
     var repeat = true
     var line = ""
     var stats = scala.collection.immutable.SortedMap[String, String]()
@@ -347,6 +348,45 @@ abstract class ProverStdIO(uniqueId: String,
     toMap(stats)
   }
 
+  def statistics(): Map[String, String] = {
+    lastStatistics = queryStatistics()
+    lastStatistics
+  }
+
+  /**
+    * Queries the statistics, and calculates the diff between it and the last statistics query.
+    * The difference is calculated if value can be converted to an int or double
+    * @return map with the current statistics, and the differences (only containing values that could be converted)
+    *         and keys with appended "-delta"
+    */
+  def deltaStatistics(): Map[String, String] = {
+    val currentStatistics = queryStatistics()
+    val deltaStatistics = currentStatistics map getDelta filter { case (_, value) => value.nonEmpty } map {
+      case (key, Some(value)) => (key + "-delta", value)
+      case other => sys.error(s"Unexpected result pair $other")
+    }
+    lastStatistics = lastStatistics ++ currentStatistics
+    currentStatistics ++ deltaStatistics
+  }
+
+  private def getDelta(pair: (String, String)): (String, Option[String]) = {
+    val curValInt = pair._2.toIntOption
+    val prevValInt = lastStatistics.get(pair._1) match {
+      case Some(value) => value.toIntOption
+      case _ => Some(0) // value not found
+    }
+    val curValDouble = pair._2.toDoubleOption
+    val prevValDouble = lastStatistics.get(pair._1) match {
+      case Some(value) => value.toDoubleOption
+      case _ => Some(0.0) // value not found
+    }
+    (curValInt, prevValInt, curValDouble, prevValDouble) match {
+      case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString))
+      case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString))
+      case _ => (pair._1, None)
+    }
+  }
+
   def comment(str: String): Unit = {
     val sanitisedStr =
       str.replaceAll("\r", "")

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 _ => return Some(rc)
+        }
+      }
+    }
+    None
+  }
+}
 
 object LogConfig {
   def default(): LogConfig = LogConfig(