From a3488beb805ac339ce5f603b5e520d181f868992 Mon Sep 17 00:00:00 2001
From: trk <trktby@gmail.com>
Date: Fri, 15 Mar 2024 18:34:42 +0100
Subject: [PATCH] Add BlockReachedMessage and BlockProcessedMessage

Add path association data to relevant messeges

Rename BlockProcessedMessage to PathProcessedMessage

Add BlockFailureMessages to report a block level failure immediately

Add failure messages to csv reporter
---
 .gitignore                                     |  1 +
 .../scala/viper/silver/reporter/Message.scala  | 18 ++++++++++++++++++
 .../scala/viper/silver/reporter/Reporter.scala |  6 ++++++
 3 files changed, 25 insertions(+)

diff --git a/.gitignore b/.gitignore
index 2ce14fd82..623fd978e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
+.vscode
 .cache
 project/project/**
 bin/**
diff --git a/src/main/scala/viper/silver/reporter/Message.scala b/src/main/scala/viper/silver/reporter/Message.scala
index a5d725456..c12da9ff6 100644
--- a/src/main/scala/viper/silver/reporter/Message.scala
+++ b/src/main/scala/viper/silver/reporter/Message.scala
@@ -335,3 +335,21 @@ case class BenchmarkingMessage(category: String, payload: String) extends Messag
   override val name: String = "benchmarking_message"
   override val toString: String = s"Benchmarking message of type $category with payload $payload"
 }
+
+/** Reported when the block of a method CFG is reached. */
+case class BlockReachedMessage(methodName: String, label: String, pathId: Int) extends  Message {
+  override val toString: String = s"block_reached_message(methodName=$methodName, label=$label, pathId=$pathId)"
+  override val name: String = "block_reached_message"
+}
+
+/** Reported when the block of a method CFG failed to verify. */
+case class BlockFailureMessage(methodName: String, label: String, pathId: Int) extends  Message {
+  override val toString: String = s"block_failure_message(methodName=$methodName, label=$label, pathId=$pathId)"
+  override val name: String = "block_failure_message"
+}
+
+/** Reported when an execution path through the method has completed. */
+case class PathProcessedMessage(methodName: String, pathId: Int, result: String) extends  Message {
+  override val toString: String = s"path_processed_message(methodName=$methodName, pathId=$pathId, result=$result)"
+  override val name: String = "path_processed_message"
+}
diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala
index 58f06edd6..6e1f9af80 100644
--- a/src/main/scala/viper/silver/reporter/Reporter.scala
+++ b/src/main/scala/viper/silver/reporter/Reporter.scala
@@ -117,6 +117,9 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
       case q: QuantifierInstantiationsMessage => csv_file.write(s"${q.toString}\n")
       case q: QuantifierChosenTriggersMessage => csv_file.write(s"${q.toString}\n")
       case t: VerificationTerminationMessage => csv_file.write(s"${t.toString}\n")
+      case r: BlockReachedMessage => csv_file.write(s"${r.toString}\n")
+      case f: BlockFailureMessage => csv_file.write(s"${f.toString}\n")
+      case p: PathProcessedMessage => csv_file.write(s"${p.toString}\n")
       case _ =>
         println( s"Cannot properly print message of unsupported type: $msg" )
     }
@@ -235,6 +238,9 @@ case class StdIOReporter(name: String = "stdout_reporter",
         //println( sm.text )
       case _: QuantifierInstantiationsMessage => // too verbose, do not print
       case _: QuantifierChosenTriggersMessage => // too verbose, do not print
+      case _: BlockReachedMessage => // too verbose, do not print
+      case _: BlockFailureMessage =>  // too verbose, do not print
+      case _: PathProcessedMessage =>  // too verbose, do not print
       case _: VerificationTerminationMessage =>
       case _: BenchmarkingMessage =>
       case _ =>