reduced complexity by removing the unneeded second actor. improved th…

…e stability of the ViperServer. improved the shutdown behaviour.

project/build.scala

@@ -1,7 +1,8 @@
 import sbt._
 import Keys._
+import com.typesafe.sbt.packager.archetypes.JavaAppPackaging
 import sbtassembly.AssemblyPlugin.autoImport._
-import de.oakgrove.SbtBrand.{BrandKeys, brandSettings, Val, BrandObject}
+import de.oakgrove.SbtBrand.{BrandKeys, BrandObject, Val, brandSettings}
 import de.oakgrove.SbtHgId.{HgIdKeys, hgIdSettings}
 
 object ViperServerBuild extends Build {
@@ -55,8 +56,8 @@ object ViperServerBuild extends Build {
            * Not sure what to do if Silicon really required so much
            * stack at some point.
            */
-          javaOptions in run ++= Seq("-Xss128M", "-Dfile.encoding=UTF-8"),
-          javaOptions in Test += "-Xss128M",
+          javaOptions in run ++= Seq("-Xss128M", "-Xmx1512M", "-Dfile.encoding=UTF-8"),
+          javaOptions in Test ++= Seq("-Xss128M", "-Xmx1512M"),
           /* Options passed to JVMs forked by test-related Sbt command.
            * See http://www.scala-sbt.org/0.12.4/docs/Detailed-Topics/Forking.html
            * In contrast to what the documentation states, it seemed
@@ -95,6 +96,7 @@ object ViperServerBuild extends Build {
     }
 
     p.aggregate(common)
+    p.enablePlugins(JavaAppPackaging)
   }
 
 
@@ -119,7 +121,7 @@ object ViperServerBuild extends Build {
     dependencies.siliconSrc % "compile->compile;test->test")
 
   def externalDep = (
-    Seq(dependencies.jgrapht , dependencies.commonsIO, dependencies.commonsPool, dependencies.scallop, dependencies.actors)
+    Seq(dependencies.jgrapht, dependencies.commonsIO, dependencies.commonsPool, dependencies.scallop, dependencies.actors)
       ++ dependencies.logging
       ++ (if (isBuildServer) Seq(
       dependencies.silver % "compile->compile;test->test",
@@ -149,4 +151,5 @@ object ViperServerBuild extends Build {
 
     lazy val actors = "com.typesafe.akka" %% "akka-actor" % "2.4.17"
   }
+
 }

project/plugins.sbt

@@ -1 +1 @@
-resolvers +=  Resolver.url("bintray-mschwerhoff-sbt-plugins",               url("https://dl.bintray.com/mschwerhoff/sbt-plugins/"))(Resolver.ivyStylePatterns)addSbtPlugin("com.typesafe.sbteclipse" % "sbteclipse-plugin" % "5.1.0")addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.3")addSbtPlugin("de.oakgrove" % "sbt-hgid" % "0.3")addSbtPlugin("de.oakgrove" % "sbt-brand" % "0.3")
+resolvers +=  Resolver.url("bintray-mschwerhoff-sbt-plugins",               url("https://dl.bintray.com/mschwerhoff/sbt-plugins/"))(Resolver.ivyStylePatterns)addSbtPlugin("com.typesafe.sbteclipse" % "sbteclipse-plugin" % "5.1.0")addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.2.0-M9")addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.3")addSbtPlugin("de.oakgrove" % "sbt-hgid" % "0.3")addSbtPlugin("de.oakgrove" % "sbt-brand" % "0.3")

src/main/scala/VerificationActor.scala

@@ -8,10 +8,8 @@ package viper.server
 
 import java.nio.file.Paths
 
-import akka.actor.{Actor, ActorRef}
 import com.typesafe.scalalogging.LazyLogging
 import viper.carbon.CarbonFrontend
-import viper.server.ViperServerProtocol.Backend
 import viper.silicon.SiliconFrontend
 import viper.silver.ast._
 import viper.silver.ast.utility.Visitor
@@ -20,71 +18,74 @@ import viper.silver.verifier._
 
 import scala.collection.mutable.ListBuffer
 
-class VerificationActor extends Actor with LazyLogging {
+class VerificationWorker(val command: Any) extends Runnable with LazyLogging {
 
   import ViperServerProtocol._
 
-  private var _sender: ActorRef = null
+  //private var _sender: ActorRef = null
 
-  private var _worker: Thread = null
+  //private var _worker: Thread = null
 
-  private var _stopRequested = false
+  //private var _stopRequested = false
 
-  def receive: PartialFunction[Any, Unit] = {
-    case Verify("silicon" :: args) =>
-      _sender = sender()
-      startVerification(args, new ViperSiliconFrontend(), sender())
-    case Verify("carbon" :: args) =>
-      _sender = sender()
-      startVerification(args, new ViperCarbonFrontend(), sender())
-    case Stop =>
-      _stopRequested = true
-      context stop self
-    case Verify(args) => logger.info("invalid arguments: " + args.mkString(" "))
-    case _ => logger.info("invalid arguments")
-  }
+  private var _frontend: ViperFrontend = null
 
-  override def postStop(): Unit = {
-    if (_worker != null) {
-      _worker.interrupt()
+  def run(): Unit = {
+    try {
+      command match {
+        case Verify("silicon" :: args) =>
+          startVerification(args, new ViperSiliconFrontend())
+        case Verify("carbon" :: args) =>
+          startVerification(args, new ViperCarbonFrontend())
+        case Verify(args) =>
+          logger.info("invalid arguments: " + args.mkString(" "))
+        case _ =>
+          logger.info("invalid arguments")
+      }
+    } catch {
+      case e: InterruptedException =>
+      case e: Exception =>
+        e.printStackTrace(System.err)
+    } finally {
+      stop()
+      if (_frontend != null) {
+        _frontend.printStopped()
+      } else {
+        ViperFrontend.printStopped()
+      }
     }
   }
 
-  private def startVerification(args: List[String], frontend: ViperFrontend, sender: ActorRef): Unit = {
-    frontend.setSender(sender)
-    //verify in another thread
-    _worker = new Thread {
-      override def run() {
-        try {
-          frontend.execute(args)
-        } catch {
-          case e: Exception =>
-            if (!_stopRequested) {
-              e.printStackTrace(System.err)
-            }
-        } finally {
-          //stop worker after completed verification
-          if (context != null) {
-            context stop self
-          }
-          _sender ! Stopped
-          frontend.printStopped()
-        }
-      }
+  private def startVerification(args: List[String], frontend: ViperFrontend): Unit = {
+    //frontend.setSender(sender)
+    _frontend = frontend
+    frontend.execute(args)
+  }
+
+  private def stop(): Unit = {
+    try {
+      _frontend.verifier.stop()
+    } catch {
+      case _: Throwable =>
     }
-    _worker.start()
   }
 }
 
+object ViperFrontend extends ViperSiliconFrontend {
+  override def ideMode: Boolean = ViperServerRunner.config.ideMode()
+}
+
 trait ViperFrontend extends SilFrontend {
-  protected var _sender: ActorRef = null
+  //protected var _sender: ActorRef = null
 
-  def setSender(sender: ActorRef): Unit = {
-    _sender = sender
-  }
+  //def setSender(sender: ActorRef): Unit = {
+  //  _sender = sender
+  //}
+
+  def ideMode: Boolean = config.ideMode()
 
   def printStopped(): Unit = {
-    if (config.ideMode()) {
+    if (ideMode) {
       loggerForIde.info(s"""{"type":"Stopped"}\r\n""")
     } else {
       logger.info(s"${_ver.name} stopped")
@@ -97,15 +98,15 @@ trait ViperFrontend extends SilFrontend {
     /* Create the verifier */
     _ver = createVerifier(args.mkString(" "))
 
-    _sender ! Backend(_ver)
+    //_sender ! Backend(_ver)
 
     if (!prepare(args)) return
 
     // initialize the translator
     init(_ver)
 
     // set the file we want to verify
-    reset(Paths.get(_config.file()))
+    reset(Paths.get(config.file()))
 
     // run the parser, typechecker, and verifier
     parse()

src/main/scala/ViperServer.scala

@@ -9,12 +9,12 @@ package viper.server
 import akka.actor.{Actor, ActorRef, ActorSystem, Props, Terminated}
 import ch.qos.logback.classic.Logger
 import com.typesafe.scalalogging.LazyLogging
-import org.rogach.scallop.{ScallopOption, singleArgConverter}
+import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter}
 import org.slf4j.LoggerFactory
 import viper.server.ViperServerProtocol._
 import viper.silicon.Silicon
-import viper.silver.frontend.SilFrontendConfig
 import viper.silver.verifier.Verifier
+
 import scala.collection.mutable.ListBuffer
 import scala.language.postfixOps
 
@@ -125,69 +125,78 @@ object ViperServerRunner {
 
   def parseCommandLine(args: Seq[String]) {
     _config = new ViperConfig(args)
+    _config.verify()
   }
 }
 
 class MainActor extends Actor with LazyLogging {
-  private var _child: ActorRef = null
+  private var _verificationTask: Thread = null
   private var _args: List[String] = null
-  private var _backend: Verifier = null
 
   def receive: PartialFunction[Any, Unit] = {
     case Stop =>
-      if (_backend != null) {
-        try {
-          //takes care of background processes
-          _backend.stop()
-        } catch {
-          case e: Exception => throw e
-        }
-      }
-      if (_child != null) {
-        try {
-          _child ! Stop
-        } catch {
-          case e: Exception => throw e
-        }
+      if (_verificationTask != null  && _verificationTask.isAlive) {
+        _verificationTask.interrupt()
+        _verificationTask.join()
+      }else{
+        ViperFrontend.printStopped()
       }
-      _backend = null
-    case Verify(args)
-    =>
-      if (_child != null) {
+    case Verify(args) =>
+      if (_verificationTask != null && _verificationTask.isAlive) {
         _args = args
-        self ! Stop
-      } else {
-        verify(args)
+        _verificationTask.interrupt()
+        _verificationTask.join()
       }
-    case Stopped
-    =>
-      _child = null
-      if (_args != null) {
-        val args = _args
-        _args = null
-        verify(args)
-      }
-    case Terminated(child) =>
-    case Backend(backend) => _backend = backend
-    case msg => logger.info("Main Actor: unexpected message received: " + msg)
+      _verificationTask = null
+      verify(args)
+    case msg =>
+      throw new Exception("Main Actor: unexpected message received: " + msg)
+
   }
 
   def verify(args: List[String]): Unit = {
-    assert(_child == null)
-    _child = context.actorOf(Props[VerificationActor], "RequestHandlerActor")
-    context.watch(_child)
-    _child ! Verify(args)
+    assert(_verificationTask == null)
+    _verificationTask = new Thread(new VerificationWorker(Verify(args)))
+    _verificationTask.start()
   }
 }
 
-class ViperConfig(args: Seq[String]) extends SilFrontendConfig(args, "Viper") {
+class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
 
   val logLevel: ScallopOption[String] = opt[String]("logLevel",
     descr = "One of the log levels ALL, TRACE, DEBUG, INFO, WARN, ERROR, OFF (default: OFF)",
     default = Some("WARN"),
     noshort = true,
     hidden = Silicon.hideInternalOptions
   )(singleArgConverter(level => level.toUpperCase))
+
+  val ideMode = opt[Boolean]("ideMode",
+    descr = ("Used for VS Code IDE. Report errors in json format, and write"
+      + "errors in the format '<file>,<line>:<col>,<line>:<col>,<message>' to"
+      + "a file (see option ideModeErrorFile)."),
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
+  val disableCaching = opt[Boolean]("disableCaching",
+    descr = ("Used for ViperServer. Cache verification errors to speed up the"
+      + "verification process"),
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
+  val ideModeAdvanced = opt[Boolean]("ideModeAdvanced",
+    descr = ("Used for VS Code IDE. Write symbolic execution log into .vscode/executionTreeData.js file, "
+      + "write execution tree graph into .vscode/dot_input.dot, "
+      + "and output z3's counter example models."),
+    default = Some(false),
+    noshort = true,
+    hidden = true
+  )
+
+  dependsOnAll(ideModeAdvanced, ideMode :: Nil)
 }
 
 object ViperServerProtocol {