From eb3a0444eadd719b89a07a8725405d40bed11483 Mon Sep 17 00:00:00 2001 From: Philippe Voinov Date: Thu, 14 Mar 2019 14:59:15 +0100 Subject: [PATCH 1/4] Make the HTTP bind interface configurable. --- src/main/scala/viper/server/ViperConfig.scala | 8 ++++++++ src/main/scala/viper/server/ViperServer.scala | 5 +++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala index ded55bf..be2cf3e 100644 --- a/src/main/scala/viper/server/ViperConfig.scala +++ b/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}]" diff --git a/src/main/scala/viper/server/ViperServer.scala b/src/main/scala/viper/server/ViperServer.scala index 7c124ef..b6b2da8 100644 --- a/src/main/scala/viper/server/ViperServer.scala +++ b/src/main/scala/viper/server/ViperServer.scala @@ -409,12 +409,13 @@ object ViperServerRunner { 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"Writing [level:${config.logLevel()}] logs into ${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}") - println(s"ViperServer online at http://localhost:$port") + println(s"ViperServer online at http://$host:$port") } // method main From fa9449d2d161b906d510e477beb934a3ccc6073f Mon Sep 17 00:00:00 2001 From: Philippe Voinov Date: Fri, 12 Apr 2019 14:02:03 +0200 Subject: [PATCH 2/4] Start introducing timing log feature. --- project/plugins.sbt | 1 + .../viper/server/VerificationWorker.scala | 18 +++++++++++++----- .../scala/viper/server/ViperIDEProtocol.scala | 18 ++++++++++++++---- src/main/scala/viper/server/ViperServer.scala | 2 +- 4 files changed, 29 insertions(+), 10 deletions(-) diff --git a/project/plugins.sbt b/project/plugins.sbt index af0977c..288c51c 100644 --- a/project/plugins.sbt +++ b/project/plugins.sbt @@ -1,2 +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") // for Silicon diff --git a/src/main/scala/viper/server/VerificationWorker.scala b/src/main/scala/viper/server/VerificationWorker.scala index 15f86bc..44d374f 100644 --- a/src/main/scala/viper/server/VerificationWorker.scala +++ b/src/main/scala/viper/server/VerificationWorker.scala @@ -20,6 +20,7 @@ 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 scala.language.postfixOps @@ -119,7 +120,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,7 +220,7 @@ class ViperBackend(private val _frontend: SilFrontend) { }).mapValues(_.size) def execute(args: Seq[String]) { - _frontend.setStartTime() + val tStartWhole = TimingLog.mark() // create the verifier _frontend.setVerifier( _frontend.createVerifier(args.mkString(" ")) ) @@ -235,6 +235,7 @@ class ViperBackend(private val _frontend: SilFrontend) { // run the parser, typechecker, and verifier _frontend.parsing() + return _frontend.semanticAnalysis() _frontend.translation() _frontend.consistencyCheck() @@ -265,15 +266,22 @@ class ViperBackend(private val _frontend: SilFrontend) { } _frontend.verifier.stop() + val tEndWhole = TimingLog.mark() - // finish by reporting the overall outcome + _frontend.timingLog.saveDuration("Whole program verification", tStartWhole, tEndWhole) + val wholeVerificationMillis = TimingLog.durationMillis(tStartWhole, tEndWhole) + // 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 })) } diff --git a/src/main/scala/viper/server/ViperIDEProtocol.scala b/src/main/scala/viper/server/ViperIDEProtocol.scala index ef12287..cf1c056 100644 --- a/src/main/scala/viper/server/ViperIDEProtocol.scala +++ b/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,25 @@ 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] = jsonFormat6(DurationEvent) + + 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 ) }) diff --git a/src/main/scala/viper/server/ViperServer.scala b/src/main/scala/viper/server/ViperServer.scala index b6b2da8..e85b406 100644 --- a/src/main/scala/viper/server/ViperServer.scala +++ b/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).") ) From 2be3c1a9396115387c8fc853f8fc4720fb22847a Mon Sep 17 00:00:00 2001 From: Philippe Voinov Date: Fri, 12 Apr 2019 15:01:21 +0200 Subject: [PATCH 3/4] Log and report timings for things the Silver frontend does. --- .../viper/server/VerificationWorker.scala | 42 +++++++++++++++---- .../scala/viper/server/ViperIDEProtocol.scala | 13 +++++- 2 files changed, 47 insertions(+), 8 deletions(-) diff --git a/src/main/scala/viper/server/VerificationWorker.scala b/src/main/scala/viper/server/VerificationWorker.scala index 44d374f..b18ae39 100644 --- a/src/main/scala/viper/server/VerificationWorker.scala +++ b/src/main/scala/viper/server/VerificationWorker.scala @@ -21,6 +21,7 @@ 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 @@ -220,33 +221,45 @@ class ViperBackend(private val _frontend: SilFrontend) { }).mapValues(_.size) def execute(args: Seq[String]) { - val tStartWhole = TimingLog.mark() - + 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() - return + 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), @@ -257,19 +270,34 @@ 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 tEndWhole = TimingLog.mark() - - _frontend.timingLog.saveDuration("Whole program verification", tStartWhole, tEndWhole) - val wholeVerificationMillis = TimingLog.durationMillis(tStartWhole, tEndWhole) + 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 { diff --git a/src/main/scala/viper/server/ViperIDEProtocol.scala b/src/main/scala/viper/server/ViperIDEProtocol.scala index b08e8d4..ca3050c 100644 --- a/src/main/scala/viper/server/ViperIDEProtocol.scala +++ b/src/main/scala/viper/server/ViperIDEProtocol.scala @@ -120,7 +120,18 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs "result" -> obj.result.toJson) }) - implicit val durationEvent_writer: RootJsonFormat[DurationEvent] = jsonFormat6(DurationEvent) + 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 { From 649e3331e1fd38cb14618b2238e0d8f3c71b70d0 Mon Sep 17 00:00:00 2001 From: Viper Admin Date: Wed, 19 Feb 2020 12:19:14 +0100 Subject: [PATCH 4/4] Create branch tehwalris/viperserver/default