Generate ASCII / DOT file client side

Author: 7i6ht

Diff for: src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -283,9 +283,9 @@ trait SilFrontend extends DefaultFrontend {
     val res = plugins.beforeFinish(tRes)
     val filteredRes = res match {
       case Success => res
-      case Failure(errors,branchTree) =>
+      case Failure(errors,exploredBranches) =>
         // Remove duplicate errors
-        Failure(errors.distinctBy(failureFilterAndGroupingCriterion),branchTree)
+        Failure(errors.distinctBy(failureFilterAndGroupingCriterion),exploredBranches)
     }
     _verificationResult = Some(filteredRes)
     filteredRes match {

Diff for: src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala

@@ -103,11 +103,11 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
   private def translateVerificationResult(input: VerificationResult): VerificationResult = {
     input match {
       case Success => input
-      case Failure(errors,branchTree) =>
+      case Failure(errors,exploredBranches) =>
         Failure(errors.map {
           case e@PreconditionInAppFalse(_, _, _) => e.transformedError()
           case e => e
-        },branchTree)
+        },exploredBranches)
     }
   }
 

Diff for: src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala

@@ -74,14 +74,14 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
     mapVerificationResultsForNode(program, input)
 
   private def mapVerificationResultsForNode(n: Node, input: VerificationResult): VerificationResult = {
-    val (refutesForWhichErrorOccurred, otherErrors, branchTree_) = input match {
+    val (refutesForWhichErrorOccurred, otherErrors, exploredBranches_) = input match {
       case Success => (Seq.empty, Seq.empty,None)
-      case Failure(errors,branchTree) =>
+      case Failure(errors,exploredBranches) =>
         val partErrs = errors.partitionMap {
         case AssertFailed(NodeWithRefuteInfo(RefuteInfo(r)), _, _) => Left((r, r.pos))
         case err => Right(err)
       }
-      (partErrs._1, partErrs._2, branchTree)
+      (partErrs._1, partErrs._2, exploredBranches)
     }
     val refutesContainedInNode = n.collect {
       case NodeWithRefuteInfo(RefuteInfo(r)) => (r, r.pos)
@@ -95,7 +95,7 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
 
     val errors = otherErrors ++ missingErrorsInNode
     if (errors.isEmpty) Success
-    else Failure(errors, branchTree_)
+    else Failure(errors, exploredBranches_)
   }
 }
 

Diff for: src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -297,10 +297,10 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
     input match {
       case Success => input
-      case Failure(errors,branchTree) => Failure(errors.map({
+      case Failure(errors,exploredBranches) => Failure(errors.map({
         case a@AssertFailed(Assert(_), _, _) => a.transformedError()
         case e => e
-      }),branchTree)
+      }),exploredBranches)
     }
   }
 

Diff for: src/main/scala/viper/silver/reporter/Message.scala

@@ -8,7 +8,7 @@ package viper.silver.reporter
 
 import viper.silver.reporter.BackendSubProcessStages.BackendSubProcessStage
 import viper.silver.verifier._
-import viper.silver.ast.{Exp, Method, QuantifiedExp, Trigger}
+import viper.silver.ast.{Method, QuantifiedExp, Trigger}
 import viper.silver.parser.PProgram
 
 /**
@@ -169,22 +169,14 @@ case class BranchFailureMessage(verifier: String, concerning: Entity,
     s"result=${result.toString}, cached=$cached)"
 }
 
-trait BranchTree {
-  val DotFilePath : String
-  var cached: Boolean = false
-  def getMethod() : Method
-  def getBeams() : Seq[BeamInfo]
-  def prettyPrint() : String
-  def toDotFile() : Unit
-}
-case class BeamInfo(e: Exp, isLeftFatal : Boolean, isRightFatal : Boolean)
-case class BranchTreeReport(tree : BranchTree)
+case class ExploredBranches(method: Method, paths: Vector[(Seq[Exp], Boolean)], var cached : Boolean = false)
+case class ExploredBranchesReport(exploredBranches : ExploredBranches)
   extends Message {
 
-  override lazy val toString: String = s"branch_tree_report(" +
-    s"method=${tree.getMethod().name}, tree=${tree.prettyPrint()}, beams=${tree.getBeams()}"
+  override lazy val toString: String = s"explored_branches_report(" +
+    s"method=${exploredBranches.method.name}, paths=${exploredBranches.paths}"
 
-  override val name = "branch_tree"
+  override val name = "explored_branches"
 }
 
 case class StatisticsReport(nOfMethods: Int, nOfFunctions: Int, nOfPredicates: Int,

Diff for: src/main/scala/viper/silver/reporter/Reporter.scala

@@ -68,8 +68,8 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
 
       case BranchFailureMessage(_, concerning, _, cached) =>
         csv_file.write(s"BranchFailureMessage,${concerning.name},${cached}\n")
-      case BranchTreeReport(tree) =>
-        csv_file.write(s"BranchTreeReport,${tree.getMethod().name},${tree.prettyPrint()}\n")
+      case ExploredBranchesReport(eb) =>
+        csv_file.write(s"ExploredBranchesReport,${eb.method.name},${eb.paths}, ${eb.cached}\n")
 
       case _: SimpleMessage | _: CopyrightReport | _: MissingDependencyReport | _: BackendSubProcessReport |
            _: InternalWarningMessage | _: ConfigurationConfirmation=> // Irrelevant for reporting
@@ -181,7 +181,7 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
       case EntitySuccessMessage(_, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
       case EntityFailureMessage(_, _, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
       case BranchFailureMessage(_, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
-      case BranchTreeReport(_) =>
+      case ExploredBranchesReport(_) =>
       case ConfigurationConfirmation(_) =>     // TODO  use for progress reporting
       //println( s"Configuration confirmation: $text" )
       case InternalWarningMessage(_) =>        // TODO  use for progress reporting

Diff for: src/main/scala/viper/silver/verifier/VerificationResult.scala

@@ -7,9 +7,10 @@
 package viper.silver.verifier
 
 import viper.silver.ast._
-import viper.silver.reporter.BranchTree
+import viper.silver.reporter.ExploredBranches
 
 import scala.annotation.unused
+import viper.silver.reporter.ExploredBranches
 
 /** Describes the outcome of a verification attempt of a Viper program.
 
@@ -28,12 +29,12 @@ object Success extends VerificationResult {
  *
  * @param errors The errors encountered during parsing, translation or verification.
  */
-case class Failure(errors: Seq[AbstractError], branchTree : Option[BranchTree] = None) extends VerificationResult {
+case class Failure(errors: Seq[AbstractError], exploredBranches : Option[ExploredBranches] = None) extends VerificationResult {
   override def toString = {
     s"Verification failed with ${errors.size} errors:\n  " +
       (errors map (e => "[" + e.fullId + "] " + e.readableMessage)).mkString("\n  ")
   }
-  override def transformedResult(): VerificationResult = Failure(errors.map(_.transformedError()), branchTree)
+  override def transformedResult(): VerificationResult = Failure(errors.map(_.transformedError()), exploredBranches)
 }
 
 /**