From e989dc111fe42fb1689096a70608ccba026d8238 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Tue, 11 Mar 2025 16:08:08 +0100 Subject: [PATCH 1/7] Adding a reporter wrapper class that performs plugin message transformations --- .../scala/viper/silver/reporter/Reporter.scala | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index 0c51bd50d..bf15d0475 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -6,6 +6,9 @@ package viper.silver.reporter +import viper.silver.plugin.SilverPluginManager +import viper.silver.verifier.Success + import java.io.FileWriter import scala.collection.mutable._ @@ -20,6 +23,20 @@ object NoopReporter extends Reporter { def report(msg: Message): Unit = () } +case class PluginAwareReporter(plugins: SilverPluginManager, reporter: Reporter) extends Reporter { + + val name = reporter.name + override def report(msg: Message): Unit = msg match { + case esm: EntitySuccessMessage => + val newResult = plugins.mapEntityVerificationResult(esm.concerning, Success) + reporter.report(VerificationResultMessage(esm.verifier, esm.concerning, esm.verificationTime, newResult)) + case efm: EntityFailureMessage => + val newResult = plugins.mapEntityVerificationResult(efm.concerning, efm.result) + reporter.report(VerificationResultMessage(efm.verifier, efm.concerning, efm.verificationTime, newResult)) + case m => reporter.report(m) + } +} + case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv") extends Reporter { def this() = this("csv_reporter", "report.csv") From a4c8fbec47b7dbb07f0fe0050ede9096a04a2601 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 17 Mar 2025 15:42:21 +0100 Subject: [PATCH 2/7] Making all standard reporters plugin aware --- .../viper/silver/frontend/SilFrontend.scala | 4 ++ .../viper/silver/reporter/Reporter.scala | 47 ++++++++++++------- 2 files changed, 34 insertions(+), 17 deletions(-) diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index 5de692857..47ef8c23b 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala @@ -75,6 +75,10 @@ trait SilFrontend extends DefaultFrontend { None } _plugins = SilverPluginManager(pluginsArg)(reporter, logger, _config, fp) + reporter match { + case par: PluginAwareReporter => par.setPluginManager(Some(_plugins)) + case _ => + } } /** diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index bf15d0475..c8104161f 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -23,27 +23,38 @@ object NoopReporter extends Reporter { def report(msg: Message): Unit = () } -case class PluginAwareReporter(plugins: SilverPluginManager, reporter: Reporter) extends Reporter { - - val name = reporter.name - override def report(msg: Message): Unit = msg match { - case esm: EntitySuccessMessage => - val newResult = plugins.mapEntityVerificationResult(esm.concerning, Success) - reporter.report(VerificationResultMessage(esm.verifier, esm.concerning, esm.verificationTime, newResult)) - case efm: EntityFailureMessage => - val newResult = plugins.mapEntityVerificationResult(efm.concerning, efm.result) - reporter.report(VerificationResultMessage(efm.verifier, efm.concerning, efm.verificationTime, newResult)) - case m => reporter.report(m) +trait PluginAwareReporter extends Reporter { + + var plugins: Option[SilverPluginManager] = None + + def setPluginManager(pm: Option[SilverPluginManager]): Unit = { + plugins = pm } + + override def report(msg: Message): Unit = { + if (plugins.isEmpty) + return doReport(msg) + msg match { + case esm: EntitySuccessMessage => + val newResult = plugins.get.mapEntityVerificationResult(esm.concerning, Success) + doReport(VerificationResultMessage(esm.verifier, esm.concerning, esm.verificationTime, newResult)) + case efm: EntityFailureMessage => + val newResult = plugins.get.mapEntityVerificationResult(efm.concerning, efm.result) + doReport(VerificationResultMessage(efm.verifier, efm.concerning, efm.verificationTime, newResult)) + case m => doReport(m) + } + } + + def doReport(msg: Message): Unit } -case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv") extends Reporter { +case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv") extends PluginAwareReporter { def this() = this("csv_reporter", "report.csv") val csv_file = new FileWriter(path, true) - def report(msg: Message): Unit = { + def doReport(msg: Message): Unit = { msg match { case AstConstructionFailureMessage(time, _) => csv_file.write(s"AstConstructionFailureMessage,${time}\n") @@ -99,7 +110,7 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv } } -case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = true) extends Reporter { +case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = true) extends PluginAwareReporter { var counter = 0 @@ -110,7 +121,7 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t private def bulletFmt(num_items: Int): String = s"%${num_items.toString.length}d" - def report(msg: Message): Unit = { + def doReport(msg: Message): Unit = { msg match { case AstConstructionFailureMessage(t, res) => val num_errors = res.errors.length @@ -194,7 +205,9 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t // These get reported without being transformed by any plugins, it would be an issue if we printed them to STDOUT. case EntitySuccessMessage(_, _, _, _) => // FIXME Currently, we only print overall verification results to STDOUT. + println(msg) case EntityFailureMessage(_, _, _, _, _) => // FIXME Currently, we only print overall verification results to STDOUT. + println(msg) case BranchFailureMessage(_, _, _, _) => // FIXME Currently, we only print overall verification results to STDOUT. case ConfigurationConfirmation(_) => // TODO use for progress reporting //println( s"Configuration confirmation: $text" ) @@ -212,11 +225,11 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t } } -case class PollingReporter(name: String = "polling_reporter", pass_through_reporter: Reporter) extends Reporter { +case class PollingReporter(name: String = "polling_reporter", pass_through_reporter: Reporter) extends PluginAwareReporter { // this reporter stores the messages it receives and reports them upon polling var messages: Queue[Message] = Queue() - def report(msg: Message): Unit = this.synchronized { + def doReport(msg: Message): Unit = this.synchronized { messages = messages.enqueue(msg) pass_through_reporter.report(msg) } From bd6fee2b331c86e9d9f28a34a72c0f5dfe12a5ba Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 17 Mar 2025 20:30:36 +0100 Subject: [PATCH 3/7] Removed debug printlns --- src/main/scala/viper/silver/reporter/Reporter.scala | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index c8104161f..c75a486ff 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -205,9 +205,7 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t // These get reported without being transformed by any plugins, it would be an issue if we printed them to STDOUT. case EntitySuccessMessage(_, _, _, _) => // FIXME Currently, we only print overall verification results to STDOUT. - println(msg) case EntityFailureMessage(_, _, _, _, _) => // FIXME Currently, we only print overall verification results to STDOUT. - println(msg) case BranchFailureMessage(_, _, _, _) => // FIXME Currently, we only print overall verification results to STDOUT. case ConfigurationConfirmation(_) => // TODO use for progress reporting //println( s"Configuration confirmation: $text" ) From 96f2fca2fbbd8f8d7b51c90b67f4fcb78fdd2fae Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 18 Mar 2025 15:09:49 +0100 Subject: [PATCH 4/7] Update src/main/scala/viper/silver/reporter/Reporter.scala Co-authored-by: Linard Arquint --- src/main/scala/viper/silver/reporter/Reporter.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index c75a486ff..2b380a593 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -31,7 +31,7 @@ trait PluginAwareReporter extends Reporter { plugins = pm } - override def report(msg: Message): Unit = { + final override def report(msg: Message): Unit = { if (plugins.isEmpty) return doReport(msg) msg match { From 9d01939ae5de66e95eac0b95a9a8fdd7df701d41 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 18 Mar 2025 15:09:55 +0100 Subject: [PATCH 5/7] Update src/main/scala/viper/silver/reporter/Reporter.scala Co-authored-by: Linard Arquint --- src/main/scala/viper/silver/reporter/Reporter.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index 2b380a593..d4ad9b176 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -25,7 +25,7 @@ object NoopReporter extends Reporter { trait PluginAwareReporter extends Reporter { - var plugins: Option[SilverPluginManager] = None + protected var plugins: Option[SilverPluginManager] = None def setPluginManager(pm: Option[SilverPluginManager]): Unit = { plugins = pm From ada63dc4f80463d83a9b3b082eb2b3e0354c783b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 18 Mar 2025 15:10:02 +0100 Subject: [PATCH 6/7] Update src/main/scala/viper/silver/reporter/Reporter.scala Co-authored-by: Linard Arquint --- .../viper/silver/reporter/Reporter.scala | 23 +++++++++++-------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index d4ad9b176..a2bb1c1ff 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -32,16 +32,19 @@ trait PluginAwareReporter extends Reporter { } final override def report(msg: Message): Unit = { - if (plugins.isEmpty) - return doReport(msg) - msg match { - case esm: EntitySuccessMessage => - val newResult = plugins.get.mapEntityVerificationResult(esm.concerning, Success) - doReport(VerificationResultMessage(esm.verifier, esm.concerning, esm.verificationTime, newResult)) - case efm: EntityFailureMessage => - val newResult = plugins.get.mapEntityVerificationResult(efm.concerning, efm.result) - doReport(VerificationResultMessage(efm.verifier, efm.concerning, efm.verificationTime, newResult)) - case m => doReport(m) + plugins match { + case None => doReport(msg) + case Some(plgns) => + val transformed = msg match { + case esm: EntitySuccessMessage => + val newResult = plgns.mapEntityVerificationResult(esm.concerning, Success) + doReport(VerificationResultMessage(esm.verifier, esm.concerning, esm.verificationTime, newResult)) + case efm: EntityFailureMessage => + val newResult = plgns.mapEntityVerificationResult(efm.concerning, efm.result) + doReport(VerificationResultMessage(efm.verifier, efm.concerning, efm.verificationTime, newResult)) + case m => doReport(m) + } + } } } From 32d33448c54eb144af5275d5a34fed88f6e34d03 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Tue, 18 Mar 2025 15:17:02 +0100 Subject: [PATCH 7/7] Cleanup and added comment --- src/main/scala/viper/silver/reporter/Reporter.scala | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index a2bb1c1ff..3043af2fb 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -35,7 +35,10 @@ trait PluginAwareReporter extends Reporter { plugins match { case None => doReport(msg) case Some(plgns) => - val transformed = msg match { + msg match { + // We transform only EntrySuccessMessage and EntityFailureMessage, not OverallSuccessMessage and + // OverallFailureMessage here, since the overall verification results are already transformed by the verifier + // *before* reporting the corresponding message. case esm: EntitySuccessMessage => val newResult = plgns.mapEntityVerificationResult(esm.concerning, Success) doReport(VerificationResultMessage(esm.verifier, esm.concerning, esm.verificationTime, newResult)) @@ -45,7 +48,6 @@ trait PluginAwareReporter extends Reporter { case m => doReport(m) } } - } } def doReport(msg: Message): Unit