diff --git a/project/plugins.sbt b/project/plugins.sbt index 9f62810..288c51c 100644 --- a/project/plugins.sbt +++ b/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 diff --git a/src/main/scala/viper/server/VerificationWorker.scala b/src/main/scala/viper/server/VerificationWorker.scala index 15f86bc..b18ae39 100644 --- a/src/main/scala/viper/server/VerificationWorker.scala +++ b/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 })) } 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/ViperIDEProtocol.scala b/src/main/scala/viper/server/ViperIDEProtocol.scala index 1dfb69e..ca3050c 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,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 ) }) diff --git a/src/main/scala/viper/server/ViperServer.scala b/src/main/scala/viper/server/ViperServer.scala index cb4b6f4..1ab3545 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).") ) @@ -396,10 +396,8 @@ 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) @@ -407,12 +405,12 @@ 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"ViperServer online at http://localhost:$port") - + println(s"ViperServer online at http://$host:$port") } // method main def init(cmdArgs: Seq[String]) {