Silicon progress tracing

col/src/main/java/vct/col/print/Printer.scala

@@ -1279,7 +1279,7 @@ case class Printer(out: Appendable,
     say(node.names.mkString("."))
 
   def printLocation(loc: Location[_]): Unit = loc match {
-//    case FieldLocation(obj, field) =>
+    case FieldLocation(obj, field) => say(expr(obj)._1, ".", field.decl.o.preferredName)
 //    case ModelLocation(obj, field) =>
 //    case SilverFieldLocation(obj, field) =>
     case ArrayLocation(array, subscript) => (phrase(assoc(100, array), "[", subscript, "]"), 100)
@@ -1288,7 +1288,7 @@ case class Printer(out: Appendable,
 //    case InstancePredicateLocation(predicate, obj, args) =>
     case AmbiguousLocation(expr) => say(expr)
     case x =>
-      say(s"Unknown node type in Printer.scala: ${x.getClass.getCanonicalName}")
+      say(s"Unknown location type in Printer.scala: ${x.getClass.getCanonicalName}")
   }
 
   def printVerification(node: Verification[_]): Unit = {

hre/src/main/java/hre/progress/Progress.scala

@@ -1,7 +1,7 @@
 package hre.progress
 
 import hre.platform.Platform
-import org.fusesource.jansi.{AnsiConsole, AnsiType}
+import org.fusesource.jansi.{Ansi, AnsiConsole, AnsiType}
 
 import scala.collection.parallel.CollectionConverters.IterableIsParallelizable
 
@@ -137,9 +137,18 @@ case object Progress {
     override def weightDone: Int = position
   }
 
+  case class OriginFocusFrame(var contexts: Seq[String]) extends Frame {
+    override def position: Int = 0
+    override def currentWeight: Int = 1
+    override def currentMessage: String = "XXX"
+    override def count: Int = 0
+    override def totalWeight: Int = 1
+    override def weightDone: Int = 1
+  }
+
   private var frames: Seq[Frame] = Nil
 
-  private def withFrame[T](frame: Frame)(f: => T): T = {
+  /* private */ def withFrame[T](frame: Frame)(f: => T): T = {
     frames :+= frame
     update()
     try {
@@ -221,4 +230,38 @@ case object Progress {
 
       update()
     }
+
+  def nextOrigin(os: Seq[String]): Unit = {
+    this.synchronized {
+      frames.last match {
+        case frame: OriginFocusFrame =>
+          val oldCtxs = frame.contexts
+          frame.contexts = os
+          if (oldCtxs != os) {
+            paintContexts()
+            update()
+          }
+        case _ => ???
+      }
+    }
+  }
+
+  def paintContexts(): Unit = {
+    frames.last match {
+      case OriginFocusFrame(ctxs) =>
+        val ansi = Ansi.ansi()
+        ansi.eraseScreen()
+          .saveCursorPosition()
+          .cursor(1, 1)
+        if (ctxs.nonEmpty) {
+          ansi.append(ctxs.head)
+        }
+        if (ctxs.length > 1) {
+          ansi.append(ctxs.last)
+        }
+        ansi.restoreCursorPosition()
+        System.out.print(ansi.toString)
+      case _ => ???
+    }
+  }
 }

rewrite/src/main/java/vct/col/rewrite/InlineApplicables.scala

@@ -92,7 +92,7 @@ case object InlineApplicables extends RewriterBuilder {
     def expr(e: Expr[Pre])(implicit o: Origin): Expr[Pre] = {
       val replaced = Substitute[Pre](replacements.map(r => r.replacing -> r.withVariable.get).toMap).dispatch(e)
       replacements.foldRight(replaced) {
-        case (replacement, e) => Let(replacement.withVariable, replacement.binding, e)
+        case (replacement, e) => Let(replacement.withVariable, replacement.binding, e)(e.o)
       }
     }
 

rewrite/src/main/java/vct/col/rewrite/ParBlockEncoder.scala

@@ -128,7 +128,7 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] {
           // Scale the body if it contains permissions
           nonQuantVars.foldLeft(body)((body, iter) => {
             val scale = to(iter) - from(iter)
-            Scale(scale, body)(PanicBlame("Par block was checked to be non-empty"))
+            Scale(scale, body)(PanicBlame("Par block was checked to be non-empty"))(body.o)
           })
         } else {
           body
@@ -140,7 +140,7 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] {
             Seq(variables.dispatch(v)),
             Nil,
             (from(iter) <= Local[Post](succ(v)) && Local[Post](succ(v)) < to(iter)) ==> body
-          )(ParBlockNotInjective(block, e))
+          )(ParBlockNotInjective(block, e))(body.o)
         })
       }
     )

rewrite/src/main/java/vct/col/rewrite/SimplifyNestedQuantifiers.scala

@@ -518,6 +518,8 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre]
 
   case class Pointer[G](index: Expr[G], subnodes: Seq[Node[G]], array: Expr[G]) extends Subscript[G]
 
+  case class Sequence[G](index: Expr[G], subnodes: Seq[Node[G]], array: Expr[G]) extends Subscript[G]
+
     class FindLinearArrayAccesses(quantifierData: RewriteQuantifierData){
 
       // Search for linear array expressions
@@ -527,6 +529,8 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre]
             testSubscript(Array(e.subscript, e.subnodes, e.array))
           case e @ ArraySubscript(_, _)  =>
             testSubscript(Array(e.index, e.subnodes, e.arr))
+          case e@SeqSubscript(seq, index) =>
+            testSubscript(Sequence(index, e.subnodes, seq))
           case e @ PointerSubscript(_, _)  =>
             testSubscript(Pointer(e.index, e.subnodes, e.pointer))
           case e @ PointerAdd(_, _) =>
@@ -738,6 +742,10 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre]
               Seq(Seq(ArraySubscript(newGen(arrayIndex.array), x_new_var)(PanicBlame("Only used as trigger, not as access"))),
                // Seq(ArrayLocation(newGen(arrayIndex.array), x_new_var)(PanicBlame("Only used as trigger, not as access")))
               )
+            case sequenceIndex: Sequence[Pre] =>
+              Seq(Seq(SeqSubscript(newGen(sequenceIndex.array), x_new_var)(PanicBlame("Only used as trigger, not as access"))),
+                // Seq(ArrayLocation(newGen(arrayIndex.array), x_new_var)(PanicBlame("Only used as trigger, not as access")))
+              )
             case arrayIndex: Pointer[Pre] =>
               Seq(Seq(PointerSubscript(newGen(arrayIndex.array), x_new_var)(PanicBlame("Only used as trigger, not as access"))),
                 Seq(PointerAdd(newGen(arrayIndex.array), x_new_var)(PanicBlame("Only used as trigger, not as access"))))

viper/src/main/java/viper/api/backend/SilverBackend.scala

@@ -2,6 +2,8 @@ package viper.api.backend
 
 import com.typesafe.scalalogging.LazyLogging
 import hre.io.RWFile
+import hre.progress.Progress
+import hre.progress.Progress.OriginFocusFrame
 import vct.col.origin.AccountedDirection
 import vct.col.{ast => col, origin => blame}
 import vct.result.VerificationError.SystemError
@@ -99,15 +101,18 @@ trait SilverBackend extends Backend with LazyLogging {
       case None => throw PluginErrors(plugins.errors)
     }
 
-    val backendVerifies = // tracker.withEntities(transformedProgram) {
-      plugins.mapVerificationResult(verifier.verify(transformedProgram)) match {
-        case Success => true
-        case Failure(errors) =>
-          logger.debug(errors.toString())
-          logger.whenDebugEnabled()
-          errors.foreach(processError)
-          false
-      }
+    val backendVerifies = { // tracker.withEntities(transformedProgram) {
+      Progress.withFrame(OriginFocusFrame(Seq()))(
+        plugins.mapVerificationResult(verifier.verify(transformedProgram)) match {
+          case Success => true
+          case Failure(errors) =>
+            logger.debug(errors.toString())
+            logger.whenDebugEnabled()
+            errors.foreach(processError)
+            false
+        }
+      )
+    }
     // }
 
     stopVerifier(verifier)

viper/src/main/java/viper/api/backend/silicon/SiliconLogListener.scala

@@ -1,6 +1,7 @@
 package viper.api.backend.silicon
 
 import com.typesafe.scalalogging.LazyLogging
+import hre.progress.Progress
 import vct.col.ast.Neq
 import viper.api.transform.NodeInfo
 import viper.silicon.decider.PathConditionStack
@@ -77,6 +78,11 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
     case _ => None
   }
 
+  def which(node: Node): Option[vct.col.ast.Node[_]] = node match {
+    case node: Infoed => node.info.getUniqueInfo[NodeInfo[vct.col.ast.Node[_]]].map(_.node)
+    case _ => None
+  }
+
   def printRecords(records: mutable.Map[Int, DataRecord], excludedBy: Map[Int, Int]): Unit = {
     for(record <- records.values.toSeq.sortBy(_.id)) {
       val at = record match {
@@ -159,6 +165,7 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
   override def appendDataRecord(r: DataRecord): Unit = {
     progress()
     openScopeFrames.head(r.id) = r
+    updateAsciiProgress()
   }
 
   override def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = {
@@ -175,6 +182,7 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
         }
       case _: OpenScopeRecord => // This is just done from datarecord; safe to ignore.
     }
+    updateAsciiProgress()
   }
 
   override def appendBranchingRecord(r: BranchingRecord): Unit = {
@@ -195,6 +203,7 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
     }
 
     updateBranch("->")
+    updateAsciiProgress()
   }
 
   def invert(term: Term): Term = term match {
@@ -222,10 +231,14 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
     advanceBranch()
 
     updateBranch("->")
+
+    updateAsciiProgress()
   }
 
   override def markBranchReachable(uidBranchPoint: Int): Unit = {
     progress()
+
+    updateAsciiProgress()
   }
 
   override def doEndBranchPoint(uidBranchPoint: Int): Unit = {
@@ -242,5 +255,22 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
 
     branchScopeCloseRecords = branchScopeCloseRecords.tail
     branchConditions = branchConditions.tail
+
+    updateAsciiProgress()
+  }
+
+  def updateAsciiProgress(): Unit = {
+    val nodes: Seq[vct.col.ast.Node[_]] = (for (records <- openScopeFrames.reverse; record <- records.values.toSeq.sortBy(_.id))
+      yield {
+        record match {
+          case member: MemberRecord => which(member.value)
+          case exec: ExecuteRecord => which(exec.value)
+          case produce: ProduceRecord => which(produce.value)
+          case consume: ConsumeRecord => which(consume.value)
+          case _ => None
+        }
+      }).collect { case Some(n) => n }
+
+    Progress.nextOrigin(nodes.map { n: vct.col.ast.Node[_] => n.o.context })
   }
 }