From b2455e3606311f05088e4ddfb8f517b2a9d7af43 Mon Sep 17 00:00:00 2001
From: Pieter Bos <p.h.bos@utwente.nl>
Date: Wed, 25 Oct 2023 12:51:49 +0200
Subject: [PATCH] make systemerrors use context by default, and turn non-fatal
 exceptions into systemerrors

---
 src/col/vct/col/ast/node/NodeImpl.scala       |  2 +-
 src/col/vct/col/ast/node/ProgramImpl.scala    |  4 +-
 .../vct/col/ast/statement/StatementImpl.scala |  4 +-
 .../ast/statement/composite/BlockImpl.scala   |  3 +-
 .../ast/statement/composite/LoopImpl.scala    | 29 +++++++++------
 .../ast/statement/composite/ScopeImpl.scala   | 12 +++---
 .../ast/statement/composite/SwitchImpl.scala  | 26 +------------
 .../statement/terminal/FramedProofImpl.scala  |  2 +-
 .../ast/statement/terminal/LabelImpl.scala    | 19 +++++-----
 .../vct/col/rewrite/NonLatchingRewriter.scala |  4 +-
 .../util/ConstructingSuccessorOfContext.scala | 10 ++++-
 .../col/util/CurrentCheckNodeContext.scala    | 10 ++++-
 .../col/util/CurrentCheckProgramContext.scala | 12 ++++++
 .../col/util/CurrentProgramCheckContext.scala |  6 ---
 .../util/CurrentProgramRewriteContext.scala   |  6 ---
 .../col/util/CurrentRewriteNodeContext.scala  | 14 +++++++
 .../util/CurrentRewriteProgramContext.scala   | 12 ++++++
 src/col/vct/col/util/FrozenScopes.scala       |  2 +-
 src/col/vct/col/util/Scopes.scala             | 30 ++++++---------
 src/colhelper/ColDefs.scala                   |  2 +
 src/colhelper/ColHelperRewriteHelpers.scala   |  2 +-
 src/hre/hre/io/CollectString.scala            | 13 +++++++
 src/hre/vct/result/VerificationError.scala    | 37 ++++++++++++++++---
 src/main/vct/main/modes/Verify.scala          |  7 +++-
 24 files changed, 166 insertions(+), 102 deletions(-)
 create mode 100644 src/col/vct/col/util/CurrentCheckProgramContext.scala
 delete mode 100644 src/col/vct/col/util/CurrentProgramCheckContext.scala
 delete mode 100644 src/col/vct/col/util/CurrentProgramRewriteContext.scala
 create mode 100644 src/col/vct/col/util/CurrentRewriteNodeContext.scala
 create mode 100644 src/col/vct/col/util/CurrentRewriteProgramContext.scala
 create mode 100644 src/hre/hre/io/CollectString.scala

diff --git a/src/col/vct/col/ast/node/NodeImpl.scala b/src/col/vct/col/ast/node/NodeImpl.scala
index e156a69c34..9a67d8ed65 100644
--- a/src/col/vct/col/ast/node/NodeImpl.scala
+++ b/src/col/vct/col/ast/node/NodeImpl.scala
@@ -52,7 +52,7 @@ trait NodeImpl[G] extends Show { this: Node[G] =>
     if(childrenErrors.nonEmpty) {
       childrenErrors
     } else {
-      VerificationError.context(CurrentCheckNodeContext(this)) {
+      VerificationError.withContext(CurrentCheckNodeContext(this)) {
         check(context)
       }
     }
diff --git a/src/col/vct/col/ast/node/ProgramImpl.scala b/src/col/vct/col/ast/node/ProgramImpl.scala
index 124dbf87e7..4ff48978af 100644
--- a/src/col/vct/col/ast/node/ProgramImpl.scala
+++ b/src/col/vct/col/ast/node/ProgramImpl.scala
@@ -4,14 +4,14 @@ import vct.col.ast.{Node, Program}
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
 import vct.col.print.{Ctx, Doc}
-import vct.col.util.CurrentProgramCheckContext
+import vct.col.util.CurrentCheckProgramContext
 import vct.result.VerificationError
 
 trait ProgramImpl[G] extends Declarator[G] { this: Program[G] =>
   def check: Seq[CheckError] = checkTrans(CheckContext())
 
   override def checkContextRecursor[T](context: CheckContext[G], f: (CheckContext[G], Node[G]) => T): Seq[T] =
-    VerificationError.context(CurrentProgramCheckContext(this)) {
+    VerificationError.withContext(CurrentCheckProgramContext(this)) {
       super.checkContextRecursor(context, f)
     }
 
diff --git a/src/col/vct/col/ast/statement/StatementImpl.scala b/src/col/vct/col/ast/statement/StatementImpl.scala
index a332b02628..3a5caf423d 100644
--- a/src/col/vct/col/ast/statement/StatementImpl.scala
+++ b/src/col/vct/col/ast/statement/StatementImpl.scala
@@ -6,7 +6,7 @@ import vct.col.print._
 
 trait StatementImpl[G] extends NodeFamilyImpl[G] { this: Statement[G] =>
   def layoutAsBlock(implicit ctx: Ctx): Doc =
-    Text("{") <>> Doc.stack(blockElementsForLayout) <+/> "}"
+    Text("{") <>> foldBlock(_ <+/> _) <+/> "}"
 
-  def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] = Seq(this)
+  def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = show
 }
diff --git a/src/col/vct/col/ast/statement/composite/BlockImpl.scala b/src/col/vct/col/ast/statement/composite/BlockImpl.scala
index c31e80c986..1c9da4595d 100644
--- a/src/col/vct/col/ast/statement/composite/BlockImpl.scala
+++ b/src/col/vct/col/ast/statement/composite/BlockImpl.scala
@@ -5,6 +5,5 @@ import vct.col.print._
 
 trait BlockImpl[G] { this: Block[G] =>
   override def layout(implicit ctx: Ctx): Doc = layoutAsBlock
-  override def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] =
-    statements.flatMap(_.blockElementsForLayout)
+  override def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = NodeDoc(this, Doc.fold(statements.map(_.foldBlock(f)))(f))
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/statement/composite/LoopImpl.scala b/src/col/vct/col/ast/statement/composite/LoopImpl.scala
index 882e621ccd..a49b404417 100644
--- a/src/col/vct/col/ast/statement/composite/LoopImpl.scala
+++ b/src/col/vct/col/ast/statement/composite/LoopImpl.scala
@@ -77,19 +77,26 @@ trait LoopImpl[G] { this: Loop[G] =>
       Group(Text("while") <+> "(" <> Doc.arg(cond) <> ")") <+> body.layoutAsBlock
     ))
 
-  def layoutControlElement(e: Show)(implicit ctx: Ctx): Option[Show] = Some(e match {
-    case Eval(e) => e.show
-    case a: Assign[G] => a.layoutAsExpr
-    case e: VeyMontAssignExpression[G] => return layoutControlElement(e.assign)
-    case e: VeyMontCommExpression[G] => return layoutControlElement(e.assign)
-    case LocalDecl(local) => local.show
-    case JavaLocalDeclarationStatement(local) => local.show
-
-    case _ => return None
-  })
+  def simpleControlElements(stat: Statement[G])(implicit ctx: Ctx): Option[Doc] = stat match {
+    case Eval(e) => Some(e.show)
+    case a: Assign[G] => Some(a.layoutAsExpr)
+    case e: VeyMontAssignExpression[G] => simpleControlElements(e.assign)
+    case e: VeyMontCommExpression[G] => simpleControlElements(e.assign)
+    case LocalDecl(local) => Some(local.show)
+    case JavaLocalDeclarationStatement(local) => Some(local.show)
+
+    case Block(stats) =>
+      stats
+        .map(simpleControlElements(_))
+        .foldLeft[Option[Seq[Doc]]](Some(Nil)) {
+          case (Some(acc), Some(more)) => Some(acc :+ more)
+          case (_, _) => None
+        }
+        .map(elems => NodeDoc(stat, Doc.fold(elems)(_ <> "," <+/> _)))
+  }
 
   def layoutControl(stat: Statement[G])(implicit ctx: Ctx): Doc =
-    Group(Doc.args(stat.blockElementsForLayout.map(layoutControlElement(_).getOrElse(return stat.show))))
+    simpleControlElements(stat).map(doc => Group(Doc.arg(doc))).getOrElse(stat.show)
 
   def layoutGenericFor(implicit ctx: Ctx): Doc =
     Doc.stack(Seq(
diff --git a/src/col/vct/col/ast/statement/composite/ScopeImpl.scala b/src/col/vct/col/ast/statement/composite/ScopeImpl.scala
index 4b317a91ca..05e00f5546 100644
--- a/src/col/vct/col/ast/statement/composite/ScopeImpl.scala
+++ b/src/col/vct/col/ast/statement/composite/ScopeImpl.scala
@@ -11,9 +11,11 @@ trait ScopeImpl[G] {
     context.withScope(locals, toScan = Seq(body))
 
   override def layout(implicit ctx: Ctx): Doc = layoutAsBlock
-  override def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] =
-    locals.map(local => ctx.syntax match {
-      case Ctx.Silver => Text("var") <+> local
-      case _ => local.show <> ";"
-    }) ++ body.blockElementsForLayout
+  override def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc =
+    NodeDoc(this,
+      Doc.fold(locals.map(local => ctx.syntax match {
+        case Ctx.Silver => Text("var") <+> local
+        case _ => local.show <> ";"
+      }) :+ body.foldBlock(f))(f)
+    )
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/statement/composite/SwitchImpl.scala b/src/col/vct/col/ast/statement/composite/SwitchImpl.scala
index 8c30881664..29b51dca28 100644
--- a/src/col/vct/col/ast/statement/composite/SwitchImpl.scala
+++ b/src/col/vct/col/ast/statement/composite/SwitchImpl.scala
@@ -13,30 +13,6 @@ trait SwitchImpl[G] { this: Switch[G] =>
 
   def isNotCase(s: Show): Boolean = !isCase(s)
 
-  @tailrec
-  private def layoutContentWithCaseLabel(content: Seq[Show], acc: Show)(implicit ctx: Ctx): Show = {
-    if(content.isEmpty) acc
-    else {
-      val label = content.head
-      val more = content.tail
-      val (uncased, casePrefix) = more.span(isNotCase)
-      val newAcc = acc.show <+/> label <> Nest(Line <> Doc.stack(uncased))
-      layoutContentWithCaseLabel(casePrefix, newAcc)
-    }
-  }
-
-  def layoutContent(implicit ctx: Ctx): Doc = {
-    val elements = body.blockElementsForLayout
-    val (uncased, casePrefix) = elements.span(isNotCase)
-
-    if(casePrefix.isEmpty) {
-      // PB: very weird switch, or we just can't peek through blocks
-      Line <> Doc.stack(uncased)
-    } else {
-      Nest(Line <> Doc.stack(uncased)) <> layoutContentWithCaseLabel(casePrefix, Empty)
-    }
-  }
-
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("switch") <+> "(" <> Doc.arg(expr) <> ")") <+> "{" <> Nest(layoutContent) <+/> "}"
+    Group(Text("switch") <+> "(" <> Doc.arg(expr) <> ")") <+> "{" <>> body.foldBlock(_ <+/> _) <+/> "}"
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/statement/terminal/FramedProofImpl.scala b/src/col/vct/col/ast/statement/terminal/FramedProofImpl.scala
index aacaa4f048..8473c908e4 100644
--- a/src/col/vct/col/ast/statement/terminal/FramedProofImpl.scala
+++ b/src/col/vct/col/ast/statement/terminal/FramedProofImpl.scala
@@ -13,7 +13,7 @@ trait FramedProofImpl[G] { this: FramedProof[G] =>
     ))
 
   def layoutWithSpec(implicit ctx: Ctx): Doc =
-    Doc.spec(Show.lazily(frameHeader(_))) <+/> Doc.stack(body.blockElementsForLayout) <+/> Doc.inlineSpec(Text("}"))
+    Doc.spec(Show.lazily(frameHeader(_))) <+/> body.foldBlock(_ <+/> _) <+/> Doc.inlineSpec(Text("}"))
 
   def layoutNative(implicit ctx: Ctx): Doc =
     Doc.stack(Seq(
diff --git a/src/col/vct/col/ast/statement/terminal/LabelImpl.scala b/src/col/vct/col/ast/statement/terminal/LabelImpl.scala
index 2bb7699518..8d9b8b27a4 100644
--- a/src/col/vct/col/ast/statement/terminal/LabelImpl.scala
+++ b/src/col/vct/col/ast/statement/terminal/LabelImpl.scala
@@ -1,23 +1,22 @@
 package vct.col.ast.statement.terminal
 
 import vct.col.ast.Label
-import vct.col.print.{Ctx, Doc, Show, Text}
+import vct.col.print.{Ctx, Doc, NodeDoc, Show, Text}
 
 trait LabelImpl[G] { this: Label[G] =>
-  override def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] = ctx.syntax match {
-    case Ctx.PVL => Seq(layoutLabel) ++ stat.blockElementsForLayout
-    case Ctx.Silver => Seq(layoutLabel) ++ stat.blockElementsForLayout
-    case Ctx.Java => Seq(this)
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Seq(layoutLabel) ++ stat.blockElementsForLayout
+  override def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = ctx.syntax match {
+    case Ctx.PVL => f(layoutLabel, stat.foldBlock(f))
+    case Ctx.Silver => f(layoutLabel, stat.foldBlock(f))
+    case Ctx.Java => layoutLabel <+> stat.show
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => f(layoutLabel, stat.foldBlock(f))
   }
 
-  def layoutLabel(implicit ctx: Ctx): Doc = ctx.syntax match {
+  def layoutLabel(implicit ctx: Ctx): Doc = NodeDoc(this, ctx.syntax match {
     case Ctx.PVL => Text("label") <+> ctx.name(decl) <> ";"
     case Ctx.Silver => Text("label") <+> ctx.name(decl)
     case Ctx.Java => Text(ctx.name(decl)) <> ":"
     case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Text(ctx.name(decl)) <> ":"
-  }
+  })
 
-  override def layout(implicit ctx: Ctx): Doc =
-    Doc.stack(blockElementsForLayout)
+  override def layout(implicit ctx: Ctx): Doc = foldBlock(_ <+/> _)
 }
\ No newline at end of file
diff --git a/src/col/vct/col/rewrite/NonLatchingRewriter.scala b/src/col/vct/col/rewrite/NonLatchingRewriter.scala
index 33c1f7d3d9..21c7484073 100644
--- a/src/col/vct/col/rewrite/NonLatchingRewriter.scala
+++ b/src/col/vct/col/rewrite/NonLatchingRewriter.scala
@@ -1,14 +1,14 @@
 package vct.col.rewrite
 
 import vct.col.ast._
-import vct.col.util.CurrentProgramRewriteContext
+import vct.col.util.CurrentRewriteProgramContext
 import vct.result.VerificationError
 
 class NonLatchingRewriter[Pre, Post]() extends AbstractRewriter[Pre, Post] {
   override def dispatch(context: Verification[Pre]): Verification[Post] = rewriteDefault(context)
   override def dispatch(context: VerificationContext[Pre]): VerificationContext[Post] = rewriteDefault(context)
   override def dispatch(program: Program[Pre]): Program[Post] =
-    VerificationError.context(CurrentProgramRewriteContext(program)) {
+    VerificationError.withContext(CurrentRewriteProgramContext(program)) {
       rewriteDefault(program)
     }
 
diff --git a/src/col/vct/col/util/ConstructingSuccessorOfContext.scala b/src/col/vct/col/util/ConstructingSuccessorOfContext.scala
index 17882491a0..f3367061a4 100644
--- a/src/col/vct/col/util/ConstructingSuccessorOfContext.scala
+++ b/src/col/vct/col/util/ConstructingSuccessorOfContext.scala
@@ -1,6 +1,14 @@
 package vct.col.util
 
 import vct.col.ast.Declaration
+import vct.col.print.Doc
 import vct.result.VerificationError
 
-case class ConstructingSuccessorOfContext(decl: Declaration[_]) extends VerificationError.Context
+case class ConstructingSuccessorOfContext(decl: Declaration[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    err.context[CurrentRewriteProgramContext].map { ctx =>
+      Doc.messagesInContext(Seq(
+        (ctx.program, decl, message)
+      ))
+    }
+}
diff --git a/src/col/vct/col/util/CurrentCheckNodeContext.scala b/src/col/vct/col/util/CurrentCheckNodeContext.scala
index ffa6eeafa3..a9ccff344b 100644
--- a/src/col/vct/col/util/CurrentCheckNodeContext.scala
+++ b/src/col/vct/col/util/CurrentCheckNodeContext.scala
@@ -1,6 +1,14 @@
 package vct.col.util
 
 import vct.col.ast.Node
+import vct.col.print.Doc
 import vct.result.VerificationError
 
-case class CurrentCheckNodeContext(node: Node[_]) extends VerificationError.Context
+case class CurrentCheckNodeContext(node: Node[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    err.context[CurrentCheckProgramContext].map { ctx =>
+      Doc.messagesInContext(Seq(
+        (ctx.program, node, message)
+      ))
+    }
+}
diff --git a/src/col/vct/col/util/CurrentCheckProgramContext.scala b/src/col/vct/col/util/CurrentCheckProgramContext.scala
new file mode 100644
index 0000000000..8f2107f084
--- /dev/null
+++ b/src/col/vct/col/util/CurrentCheckProgramContext.scala
@@ -0,0 +1,12 @@
+package vct.col.util
+
+import vct.col.ast.Program
+import vct.col.print.Doc
+import vct.result.VerificationError
+
+case class CurrentCheckProgramContext(program: Program[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    Some(Doc.messagesInContext(Seq(
+      (program, program, message)
+    )))
+}
diff --git a/src/col/vct/col/util/CurrentProgramCheckContext.scala b/src/col/vct/col/util/CurrentProgramCheckContext.scala
deleted file mode 100644
index 06d0c1c8c4..0000000000
--- a/src/col/vct/col/util/CurrentProgramCheckContext.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-package vct.col.util
-
-import vct.col.ast.Node
-import vct.result.VerificationError
-
-case class CurrentProgramCheckContext(node: Node[_]) extends VerificationError.Context
diff --git a/src/col/vct/col/util/CurrentProgramRewriteContext.scala b/src/col/vct/col/util/CurrentProgramRewriteContext.scala
deleted file mode 100644
index 83c31da05d..0000000000
--- a/src/col/vct/col/util/CurrentProgramRewriteContext.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-package vct.col.util
-
-import vct.col.ast.Program
-import vct.result.VerificationError
-
-case class CurrentProgramRewriteContext(program: Program[_]) extends VerificationError.Context
diff --git a/src/col/vct/col/util/CurrentRewriteNodeContext.scala b/src/col/vct/col/util/CurrentRewriteNodeContext.scala
new file mode 100644
index 0000000000..ac830a0bdd
--- /dev/null
+++ b/src/col/vct/col/util/CurrentRewriteNodeContext.scala
@@ -0,0 +1,14 @@
+package vct.col.util
+
+import vct.col.ast.Node
+import vct.col.print.Doc
+import vct.result.VerificationError
+
+case class CurrentRewriteNodeContext(node: Node[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    err.context[CurrentRewriteProgramContext].map { ctx =>
+      Doc.messagesInContext(Seq(
+        (ctx.program, node, message)
+      ))
+    }
+}
diff --git a/src/col/vct/col/util/CurrentRewriteProgramContext.scala b/src/col/vct/col/util/CurrentRewriteProgramContext.scala
new file mode 100644
index 0000000000..25be84f4ca
--- /dev/null
+++ b/src/col/vct/col/util/CurrentRewriteProgramContext.scala
@@ -0,0 +1,12 @@
+package vct.col.util
+
+import vct.col.ast.Program
+import vct.col.print.Doc
+import vct.result.VerificationError
+
+case class CurrentRewriteProgramContext(program: Program[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    Some(Doc.messagesInContext(Seq(
+      (program, program, message)
+    )))
+}
diff --git a/src/col/vct/col/util/FrozenScopes.scala b/src/col/vct/col/util/FrozenScopes.scala
index 95e1a9abf6..8f99752558 100644
--- a/src/col/vct/col/util/FrozenScopes.scala
+++ b/src/col/vct/col/util/FrozenScopes.scala
@@ -22,7 +22,7 @@ class FrozenScopes[Pre, Post, PreDecl <: Declaration[Pre], PostDecl <: Declarati
   override def computeSucc(decl: PreDecl): Option[PostDecl] = scopes.collectFirst { case m if m.contains(decl) => m(decl) }
 
   override def succ[RefDecl <: Declaration[Post]](decl: PreDecl)(implicit tag: ClassTag[RefDecl]): Ref[Post, RefDecl] =
-    VerificationError.context(ConstructingSuccessorOfContext(decl)) {
+    VerificationError.withContext(ConstructingSuccessorOfContext(decl)) {
       TimeTravel.cause { causeIdx =>
         new LazyRef(computeSucc(decl).getOrElse(TimeTravel.badEffect(causeIdx, throw Scopes.NoSuccessor(decl))), Some(EqualityMeasure(this, decl)))
       }
diff --git a/src/col/vct/col/util/Scopes.scala b/src/col/vct/col/util/Scopes.scala
index 35f074ddde..8467c5ef6c 100644
--- a/src/col/vct/col/util/Scopes.scala
+++ b/src/col/vct/col/util/Scopes.scala
@@ -13,6 +13,7 @@ import vct.result.VerificationError.SystemError
 import scala.collection.mutable
 import scala.collection.mutable.ArrayBuffer
 import scala.reflect.ClassTag
+import scala.util.Try
 
 object Scopes {
   case class WrongDeclarationCount(kind: ClassTag[_], count: Int) extends SystemError {
@@ -36,25 +37,18 @@ object Scopes {
 
   case class NoSuccessor(pre: Declaration[_]) extends SystemError {
     override def text: String = {
-      (
-        getContext[CurrentProgramCheckContext],
-        getContext[CurrentCheckNodeContext],
-        getContext[CurrentProgramRewriteContext],
-        getContext[ConstructingSuccessorOfContext],
-      ) match {
-        case (
-          Some(CurrentProgramCheckContext(useProgram)),
-          Some(CurrentCheckNodeContext(useNode)),
-          Some(CurrentProgramRewriteContext(predProgram)),
-          Some(ConstructingSuccessorOfContext(predDecl)),
-        ) =>
-          Doc.messagesInContext(Seq(
-            (predProgram, predDecl, "A reference to the successor of this declaration was made, ..."),
-            (useProgram, useNode, "... but it has no successor in this position.")
-          ))
-        case _ => pre.o.messageInContext("A reference to the successor of this declaration was made, but it has no successor.")
+      Try {
+        val useProgram = getContext[CurrentCheckProgramContext].program
+        val useNode = getContext[CurrentCheckNodeContext].node
+        val predProgram = getContext[CurrentRewriteProgramContext].program
+        val predDecl = getContext[ConstructingSuccessorOfContext].decl
+        Doc.messagesInContext(Seq(
+          (predProgram, predDecl, "A reference to the successor of this declaration was made, ..."),
+          (useProgram, useNode, "... but it has no successor in this position.")
+        ))
+      } getOrElse {
+        pre.o.messageInContext("A reference to the successor of this declaration was made, but it has no successor.")
       }
-
     }
   }
 }
diff --git a/src/colhelper/ColDefs.scala b/src/colhelper/ColDefs.scala
index 4f49d7a739..e52b8b3871 100644
--- a/src/colhelper/ColDefs.scala
+++ b/src/colhelper/ColDefs.scala
@@ -17,6 +17,8 @@ object ColDefs {
     q"import vct.col.ref.Ref",
     q"import vct.col.resolve.ctx.Referrable",
     q"import vct.col.origin.ExpectedError",
+    q"import vct.result.VerificationError",
+    q"import vct.col.util.CurrentRewriteNodeContext",
     q"import hre.data.BitString",
   )
 
diff --git a/src/colhelper/ColHelperRewriteHelpers.scala b/src/colhelper/ColHelperRewriteHelpers.scala
index 829b137228..264148d1c1 100644
--- a/src/colhelper/ColHelperRewriteHelpers.scala
+++ b/src/colhelper/ColHelperRewriteHelpers.scala
@@ -15,7 +15,7 @@ case class ColHelperRewriteHelpers(info: ColDescription) extends ColHelperMaker
 
       def rewrite(..${cls.params.map(rewriteHelperParam) ++
         cls.blameType.toSeq.map(t => Term.Param(Nil, q"blame", Some(t), Some(q"rewriter.dispatch(subject.blame)"))) :+
-        Term.Param(List(), q"o", Some(t"Origin"), Some(q"rewriter.dispatch(subject.o)"))}): ${cls.typ}[Post] = {
+        Term.Param(List(), q"o", Some(t"Origin"), Some(q"rewriter.dispatch(subject.o)"))}): ${cls.typ}[Post] = VerificationError.withContext(CurrentRewriteNodeContext(subject)) {
         ${ColDefs.DECLARATION_NAMESPACE.foldLeft(
           cls.make(cls.params.map(p => Term.Name(p.name.value)), q"blame", q"o")
         ){
diff --git a/src/hre/hre/io/CollectString.scala b/src/hre/hre/io/CollectString.scala
new file mode 100644
index 0000000000..31225b1306
--- /dev/null
+++ b/src/hre/hre/io/CollectString.scala
@@ -0,0 +1,13 @@
+package hre.io
+
+import java.io.{ByteArrayOutputStream, PrintStream}
+import java.nio.charset.StandardCharsets
+
+object CollectString {
+  def apply(f: PrintStream => Unit): String = {
+    val bytes = new ByteArrayOutputStream
+    val print = new PrintStream(bytes)
+    f(print)
+    new String(bytes.toByteArray, StandardCharsets.UTF_8)
+  }
+}
diff --git a/src/hre/vct/result/VerificationError.scala b/src/hre/vct/result/VerificationError.scala
index cba416ea29..8811276f66 100644
--- a/src/hre/vct/result/VerificationError.scala
+++ b/src/hre/vct/result/VerificationError.scala
@@ -2,6 +2,7 @@ package vct.result
 
 import scala.collection.mutable.ArrayBuffer
 import scala.reflect.ClassTag
+import scala.util.control.NonFatal
 
 sealed abstract class VerificationError extends RuntimeException {
   def text: String
@@ -10,12 +11,22 @@ sealed abstract class VerificationError extends RuntimeException {
 
   val contexts: ArrayBuffer[VerificationError.Context] = ArrayBuffer()
 
-  def getContext[T](implicit tag: ClassTag[T]): Option[T] = {
-    contexts.collectFirst{
+  def context[T](implicit tag: ClassTag[T]): Option[T] = {
+    contexts.collectFirst {
       case x : T =>
         x
     }
   }
+
+  def getContext[T](implicit tag: ClassTag[T]): T = context[T].get
+
+  def messageContext(message: String, backupContext: String => String = identity): String =
+    // PB: note: the innermost context is added to contexts first, so we end up trying to use the most specific context
+    // for rendering the message context first, which is what we want.
+    contexts.foldLeft[Option[String]](None) {
+      case (Some(messageInContext), _) => Some(messageInContext)
+      case (None, ctx) => ctx.tryMessageContext(message, this)
+    } getOrElse backupContext(message)
 }
 
 object VerificationError {
@@ -28,17 +39,33 @@ object VerificationError {
    * should be a (documented) UserError. */
   abstract class SystemError extends VerificationError
 
-  case class Unreachable(text: String) extends SystemError
+  case class Unreachable(reason: String) extends SystemError {
+    override def text: String = messageContext(reason)
+  }
+
+  case class Crash(cause: Throwable) extends SystemError {
+    initCause(cause)
 
-  trait Context
+    override def text: String =
+      messageContext("VerCors crashed near this position. Cause follows:")
+  }
+
+  trait Context {
+    def tryMessageContext(message: String, err: VerificationError): Option[String] = None
+  }
 
-  def context[T](ctx: Context)(f: => T): T = {
+  def withContext[T](ctx: Context)(f: => T): T = {
     try {
       f
     } catch {
       case e : VerificationError =>
         e.contexts += ctx
         throw e
+      case NonFatal(e) =>
+        // PB: if you clicked here, scoll down to the exception cause :)
+        val crash = Crash(e)
+        crash.contexts += ctx
+        throw crash
     }
   }
 }
\ No newline at end of file
diff --git a/src/main/vct/main/modes/Verify.scala b/src/main/vct/main/modes/Verify.scala
index f16c47a5d4..15c50e8443 100644
--- a/src/main/vct/main/modes/Verify.scala
+++ b/src/main/vct/main/modes/Verify.scala
@@ -2,7 +2,7 @@ package vct.main.modes
 
 import com.typesafe.scalalogging.LazyLogging
 import vct.options.Options
-import hre.io.Readable
+import hre.io.{CollectString, Readable}
 import sun.misc.{Signal, SignalHandler}
 import vct.col.origin.{BlameCollector, TableEntry, VerificationFailure}
 import vct.col.rewrite.bip.BIP
@@ -72,9 +72,12 @@ case object Verify extends LazyLogging {
     }
 
     verifyWithOptions(options, options.inputs) match {
-      case Left(err) =>
+      case Left(err: VerificationError.UserError) =>
         logger.error(err.text)
         EXIT_CODE_ERROR
+      case Left(err: VerificationError.SystemError) =>
+        logger.error(CollectString(s => err.printStackTrace(s)))
+        EXIT_CODE_ERROR
       case Right((Nil, report)) =>
         logger.info("Verification completed successfully.")
         friendlyHandleBipReport(report, options.bipReportFile)