From ad96b1d11ed41e5ddcfff70e448223820605bd51 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 22 Mar 2024 16:36:03 +0100 Subject: [PATCH 1/2] Added statistics report after plugin transformation --- .../scala/viper/server/core/VerificationWorker.scala | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index ee185e9..7f0b2b7 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/src/main/scala/viper/server/core/VerificationWorker.scala @@ -239,7 +239,14 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, private def beforeVerify(input: Program): Either[Seq[AbstractError], Program] = { if (disablePlugins) Right(input) else _frontend.plugins.beforeVerify(input) match { - case Some(programPlugin) => Right(programPlugin) + case Some(programPlugin) => + val stats = StatisticsReport(programPlugin.methods.size, + programPlugin.functions.size, + programPlugin.predicates.size, + programPlugin.domains.size, + programPlugin.fields.size) + _frontend.reporter.report(stats) + Right(programPlugin) case None => Left(_frontend.plugins.errors) } } From 09c190811f66914e62ee765abdb4c881626c4dba Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 25 Mar 2024 09:20:49 +0100 Subject: [PATCH 2/2] Removed old statistics report and moved new one --- .../viper/server/core/VerificationWorker.scala | 15 +++++++-------- .../utility/ProgramDefinitionsProvider.scala | 18 ------------------ 2 files changed, 7 insertions(+), 26 deletions(-) diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index 7f0b2b7..1b6b0bf 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/src/main/scala/viper/server/core/VerificationWorker.scala @@ -154,6 +154,12 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, val res = for { filteredProgram <- filter(_ast) innerProgram <- beforeVerify(filteredProgram) + stats = StatisticsReport(innerProgram.methods.size, + innerProgram.functions.size, + innerProgram.predicates.size, + innerProgram.domains.size, + innerProgram.fields.size) + _ = _frontend.reporter.report(stats) cachingResult = caching(innerProgram) verificationResult <- verification(cachingResult.transformedProgram) combinedVerificationResult = postCaching(cachingResult, verificationResult) @@ -239,14 +245,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, private def beforeVerify(input: Program): Either[Seq[AbstractError], Program] = { if (disablePlugins) Right(input) else _frontend.plugins.beforeVerify(input) match { - case Some(programPlugin) => - val stats = StatisticsReport(programPlugin.methods.size, - programPlugin.functions.size, - programPlugin.predicates.size, - programPlugin.domains.size, - programPlugin.fields.size) - _frontend.reporter.report(stats) - Right(programPlugin) + case Some(programPlugin) => Right(programPlugin) case None => Left(_frontend.plugins.errors) } } diff --git a/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala b/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala index 9fd48bd..39f4e6f 100644 --- a/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala +++ b/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala @@ -129,27 +129,9 @@ trait ProgramDefinitionsProvider { } flatten) toList } - private def countInstances(p: Program): Map[String, Int] = p.members.groupBy({ - case _: Method => "method" - case _: Function => "function" - case _: Predicate => "predicate" - case _: Domain => "domain" - case _: Field => "field" - case _ => "other" - }).view.mapValues(_.size).toMap - def reportProgramStats(): Unit = { val prog = _frontend.program.get - val stats = countInstances(prog) - _frontend.reporter.report(ProgramOutlineReport(prog.members.toList)) - _frontend.reporter.report(StatisticsReport( - stats.getOrElse("method", 0), - stats.getOrElse("function", 0), - stats.getOrElse("predicate", 0), - stats.getOrElse("domain", 0), - stats.getOrElse("field", 0) - )) _frontend.reporter.report(ProgramDefinitionsReport(collect(prog))) } } \ No newline at end of file