Make the HTTP bind interface configurable

project/plugins.sbt

@@ -1,3 +1,3 @@
 addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.8")
 addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.3.12")
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.9.0")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.9.0") // for Silicon

src/main/scala/viper/server/VerificationWorker.scala

@@ -20,6 +20,8 @@ import viper.silver.reporter
 import viper.silver.reporter.{Reporter, _}
 import viper.silver.verifier.errors._
 import viper.silver.verifier.{AbstractVerificationError, _}
+import viper.silver.utility.TimingLog
+import viper.silver.utility.TimingLog.Marker
 
 import scala.language.postfixOps
 
@@ -119,7 +121,6 @@ class VerificationWorker(private val reporter: ActorRef,
 }
 
 class ViperBackend(private val _frontend: SilFrontend) {
-
   override def toString: String = {
     if ( _frontend.verifier == null )
       s"ViperBackend( ${_frontend.getClass.getName} /with uninitialized verifier/ )"
@@ -220,32 +221,45 @@ class ViperBackend(private val _frontend: SilFrontend) {
     }).mapValues(_.size)
 
   def execute(args: Seq[String]) {
-    _frontend.setStartTime()
-
+    val tBeforeWhole = TimingLog.mark()
     // create the verifier
     _frontend.setVerifier( _frontend.createVerifier(args.mkString(" ")) )
 
+    val tBeforePrepare = TimingLog.mark()
     if (!_frontend.prepare(args)) return
 
+    val tBeforeInit = TimingLog.mark()
     // initialize the translator
     _frontend.init( _frontend.verifier )
 
+    val tBeforeReset = TimingLog.mark()
     // set the file we want to verify
     _frontend.reset( Paths.get(_frontend.config.file()) )
 
     // run the parser, typechecker, and verifier
+    val tBeforeParsing = TimingLog.mark()
     _frontend.parsing()
+    val tBeforeSemanticAnalysis = TimingLog.mark()
     _frontend.semanticAnalysis()
+    val tBeforeTranslation = TimingLog.mark()
     _frontend.translation()
+    val tBeforeConsistencyCheck = TimingLog.mark()
     _frontend.consistencyCheck()
+    val tAfterConsistencyCheck = TimingLog.mark()
 
+    var tBeforeCountInstances: Marker = 0
+    var tBeforeReportingStatistics: Marker = 0
+    var tBeforeVerification: Marker = 0
+    var tAfterVerification: Marker = 0
     if (_frontend.errors.nonEmpty) {
       _frontend.setState( DefaultStates.Verification )
 
     } else {
+      tBeforeCountInstances = TimingLog.mark()
       val prog: Program = _frontend.program.get
       val stats = countInstances(prog)
 
+      tBeforeReportingStatistics = TimingLog.mark()
       _frontend.reporter.report(ProgramOutlineReport(prog.members.toList))
       _frontend.reporter.report(StatisticsReport(
         stats.getOrElse("method", 0),
@@ -256,24 +270,46 @@ class ViperBackend(private val _frontend: SilFrontend) {
       ))
       _frontend.reporter.report(ProgramDefinitionsReport(collectDefinitions(prog)))
 
+      tBeforeVerification = TimingLog.mark()
       if (_frontend.config.disableCaching()) {
         _frontend.verification()
       } else {
         println("start cached verification")
         doCachedVerification()
       }
+      tAfterVerification = TimingLog.mark()
     }
 
+    val tBeforeStop = TimingLog.mark()
     _frontend.verifier.stop()
+    val tAfterWhole = TimingLog.mark()
+
+    _frontend.timingLog.saveDuration("Whole program verification", tBeforeWhole, tAfterWhole)
+    _frontend.timingLog.saveDuration("frontend.createVerifier()", tBeforeWhole, tBeforePrepare)
+    _frontend.timingLog.saveDuration("frontend.prepare()", tBeforePrepare, tBeforeInit)
+    _frontend.timingLog.saveDuration("frontend.init()", tBeforeInit, tBeforeReset)
+    _frontend.timingLog.saveDuration("frontend.reset()", tBeforeReset, tBeforeParsing)
+    _frontend.timingLog.saveDuration("frontend.parsing()", tBeforeParsing, tBeforeSemanticAnalysis)
+    _frontend.timingLog.saveDuration("frontend.semanticAnalysis()", tBeforeSemanticAnalysis, tBeforeTranslation)
+    _frontend.timingLog.saveDuration("frontend.translation()", tBeforeTranslation, tBeforeConsistencyCheck)
+    _frontend.timingLog.saveDuration("frontend.consistencyCheck()", tBeforeConsistencyCheck, tAfterConsistencyCheck)
+    _frontend.timingLog.saveDuration("countInstances(prog)", tBeforeCountInstances, tBeforeReportingStatistics)
+    _frontend.timingLog.saveDuration("Reporting statistics", tBeforeReportingStatistics, tBeforeVerification)
+    _frontend.timingLog.saveDuration("Verification (possibly cached)", tBeforeVerification, tAfterVerification)
+    _frontend.timingLog.saveDuration("frontend.verifier.stop()", tBeforeStop, tAfterWhole)
+    val wholeVerificationMillis = TimingLog.durationMillis(tBeforeWhole, tAfterWhole)
 
     // finish by reporting the overall outcome
-
     _frontend.result match {
       case Success =>
-        _frontend.reporter report OverallSuccessMessage(_frontend.getVerifierName, System.currentTimeMillis() - _frontend.startTime)
+        _frontend.reporter report OverallSuccessMessage(_frontend.getVerifierName,
+          wholeVerificationMillis,
+          _frontend.timingLog.events)
         // TODO: Think again about where to detect and trigger SymbExLogging
       case f@Failure(_) =>
-        _frontend.reporter report OverallFailureMessage(_frontend.getVerifierName, System.currentTimeMillis() - _frontend.startTime,
+        _frontend.reporter report OverallFailureMessage(_frontend.getVerifierName,
+          wholeVerificationMillis,
+          _frontend.timingLog.events,
           // Cached errors will be reporter as soon as they are retrieved from the cache.
           Failure(f.errors.filter { e => !e.cached }))
     }

src/main/scala/viper/server/ViperConfig.scala

@@ -77,6 +77,14 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
 
   dependsOnAll(ideModeAdvanced, ideMode :: Nil)
 
+  var bindInterface: ScallopOption[String] = opt[String]("bind-interface",
+    descr = ("Specifies the interface that ViperServer will listen on."
+      + "The default is \"localhost\" where only connections from the local machine are accepted."
+      + "Use 0.0.0.0 to accept connections from any machine (not a good idea without HTTPS or a firewall)."),
+    default = Some("localhost"),
+    noshort=true
+  )
+
   val port: ScallopOption[Int] = opt[Int]("port", 'p',
     descr = ("Specifies the port on which ViperServer will be started."
       + s"The port must be an integer in range [${viper.server.utility.Sockets.MIN_PORT_NUMBER}-${viper.server.utility.Sockets.MAX_PORT_NUMBER}]"

src/main/scala/viper/server/ViperIDEProtocol.scala

@@ -12,6 +12,7 @@ import akka.stream.scaladsl.Flow
 import akka.util.ByteString
 import spray.json.DefaultJsonProtocol
 import viper.silver.reporter.{InvalidArgumentsReport, _}
+import viper.silver.utility.{DurationEvent, TimingLogEntry}
 import viper.silver.verifier._
 
 
@@ -119,16 +120,36 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
       "result" -> obj.result.toJson)
   })
 
-  implicit val overallSuccessMessage_writer: RootJsonFormat[OverallSuccessMessage] = lift(new RootJsonWriter[OverallSuccessMessage] {
-    override def write(obj: OverallSuccessMessage): JsObject = {
-      JsObject(
-        "time" -> obj.verificationTime.toJson)
+  implicit val durationEvent_writer: RootJsonFormat[DurationEvent] = lift(new RootJsonWriter[DurationEvent] {
+    override def write(obj: DurationEvent): JsValue = obj match {
+      case DurationEvent(name, cat, ph, ts, pid, tid) => JsObject(
+        "name" -> JsString(name),
+        "cat" -> JsString(cat),
+        "ph" -> JsString(ph),
+        "ts" -> JsNumber(ts),
+        "pid" -> JsNumber(pid),
+        "tid" -> JsNumber(tid)
+      )
+    }
+  })
+
+  implicit val timingLogEntry_writer: RootJsonFormat[TimingLogEntry] = lift(new RootJsonWriter[TimingLogEntry] {
+    override def write(obj: TimingLogEntry): JsValue = obj match {
+      case e: DurationEvent => e.toJson
     }
   })
 
+  implicit val overallSuccessMessage_writer: RootJsonFormat[OverallSuccessMessage] = lift(new RootJsonWriter[OverallSuccessMessage] {
+    override def write(obj: OverallSuccessMessage): JsObject = JsObject(
+      "time" -> obj.verificationTime.toJson,
+      "timingLog" -> obj.timingEvents.toJson
+    )
+  })
+
   implicit val overallFailureMessage_writer: RootJsonFormat[OverallFailureMessage] = lift(new RootJsonWriter[OverallFailureMessage] {
     override def write(obj: OverallFailureMessage): JsValue = JsObject(
       "time" -> obj.verificationTime.toJson,
+      "timingLog" -> obj.timingEvents.toJson,
       "result" -> obj.result.toJson
     )
   })

src/main/scala/viper/server/ViperServer.scala

@@ -275,7 +275,7 @@ object ViperServerRunner {
             val new_job_handle: Future[JobHandle] = (main_actor ? ViperServerProtocol.Verify(arg_list)).mapTo[JobHandle]
             new_job_handle
           })
-          complete( VerificationRequestAccept(id) )
+          complete(VerificationRequestAccept(id))
 
         } else {
           complete( VerificationRequestReject(s"the maximum number of active verification jobs are currently running ($MAX_ACTIVE_JOBS).") )
@@ -396,23 +396,21 @@ object ViperServerRunner {
   }
 
   def main(args: Array[String]): Unit = {
-
     try {
       init(args)
-
     } catch { case e: Throwable =>
       println(s"Cannot parse CMD arguments: $e")
       sys.exit(1)
     }
 
     ViperCache.initialize(logger.get, config.backendSpecificCache())
 
+    val host = config.bindInterface()
     val port = config.port()
-    val bindingFuture: Future[Http.ServerBinding] = Http().bindAndHandle(routes(logger), "localhost", port)
+    val bindingFuture: Future[Http.ServerBinding] = Http().bindAndHandle(routes(logger), host, port)
     _term_actor = system.actorOf(Terminator.props(bindingFuture), "terminator")
 
-    println(s"ViperServer online at http://localhost:$port")
-
+    println(s"ViperServer online at http://$host:$port")
   } // method main
 
   def init(cmdArgs: Seq[String]) {