Merge pull request #562 from viperproject/symb-ex-logger

Scope-based SymbExLogger Take 2

Author: ArquintL

.gitignore

@@ -1,5 +1,6 @@
 .idea
 .idea_modules
+common/target
 project/project
 project/target
 target
@@ -18,5 +19,7 @@ utils/scripts/tidy_smtlib.jar
 silicon_classpath.txt
 lib/
 silver
+src/test/resources/symbExLogTests/*.alog
+.DS_Store
 viper_tutorial_examples
 .bsp/

build.sbt

@@ -29,6 +29,7 @@ lazy val silicon = (project in file("."))
     // External dependencies
     libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.9.2",
     libraryDependencies += "org.apache.commons" % "commons-pool2" % "2.9.0",
+    libraryDependencies += "io.spray" %%  "spray-json" % "1.3.6",
 
     // Only get a few compilation errors at once
     maxErrors := 5,

src/main/scala/Config.scala

@@ -196,13 +196,6 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     valueName = "level"
   )
 
-  val writeSymbexLogFile: ScallopOption[Boolean] = opt[Boolean]("writeSymbexLogFile",
-    descr = "Report the symbolic execution log as ExecutionTraceReport",
-    default = Some(false),
-    noshort = true,
-    hidden = true
-  )
-
   val timeout: ScallopOption[Int] = opt[Int]("timeout",
     descr = ( "Time out after approx. n seconds. The timeout is for the whole verification, "
             + "not per method or proof obligation (default: 0, i.e. no timeout)."),
@@ -486,6 +479,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val logConfig: ScallopOption[String] = opt[String]("logConfig",
+    descr = "Path to config file specifying SymbExLogger options",
+    default = None,
+    noshort = true,
+    hidden = false
+  )
+
   val disableCatchingExceptions: ScallopOption[Boolean] = opt[Boolean]("disableCatchingExceptions",
     descr =s"Don't catch exceptions (can be useful for debugging problems with ${Silicon.name})",
     default = Some(false),
@@ -553,6 +553,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       sys.error(s"Unexpected combination: $other")
   }
 
+  validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)
   validateFileOpt(multisetAxiomatizationFile)
   validateFileOpt(sequenceAxiomatizationFile)

src/main/scala/Silicon.scala

@@ -20,6 +20,7 @@ import viper.silver.reporter._
 import viper.silver.verifier.{DefaultDependency => SilDefaultDependency, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.Failure
+import viper.silicon.logger.SymbExLogger
 import viper.silicon.reporting.condenseToViperResult
 import viper.silicon.verifier.DefaultMasterVerifier
 import viper.silver.cfg.silver.SilverCfg
@@ -206,8 +207,14 @@ 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 =>
+        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())
+          }
           result = Some(SilFailure(SilTimeoutOccurred(config.timeout(), "second(s)") :: Nil))
+        }
         case exception: Exception if !config.disableCatchingExceptions() =>
           config.assertVerified() // Raises an exception itself, if it fails