finish parsers

src/col/vct/col/ast/Node.scala

@@ -82,7 +82,7 @@ import vct.result.VerificationError.Unreachable
 
 sealed trait NodeFamily[G] extends Node[G] with NodeFamilyImpl[G]
 
-final case class Verification[G](tasks: Seq[VerificationContext[G]], expectedErrors: Seq[ExpectedError])(implicit val o: Origin) extends NodeFamily[G] with VerificationImpl[G]
+final case class Verification[G](tasks: Seq[VerificationContext[G]])(implicit val o: Origin) extends NodeFamily[G] with VerificationImpl[G]
 final case class VerificationContext[G](program: Program[G])(implicit val o: Origin) extends NodeFamily[G] with VerificationContextImpl[G]
 final case class Program[G](declarations: Seq[GlobalDeclaration[G]], blame: Blame1[G])(implicit val o: Origin) extends NodeFamily[G] with ProgramImpl[G]
 
@@ -154,7 +154,8 @@ case class BlameSplitTerminationMeasure[G](terminationMeasure: BlameTrafo[G], ot
 case class BlameSplitContextEverywhere[G](contextEverywhere: BlameTrafo[G], otherwise: BlameTrafo[G])(implicit val o: Origin) extends BlameTrafo[G]
 case class BlameSplitSignals[G](signals: BlameTrafo[G], otherwise: BlameTrafo[G])(implicit val o: Origin) extends BlameTrafo[G]
 
-class CancellativeFailureGrouping[G]()(implicit val o: Origin) extends GlobalDeclaration[G]
+final class CancellativeFailureGrouping[G](val filterCode: Option[String], val filterFailureCount: Option[Int])(implicit val o: Origin) extends GlobalDeclaration[G]
+final class ExpectedError[G](val blame: Blame1[G])(implicit val o: Origin) extends GlobalDeclaration[G] with ExpectedErrorImpl[G]
 case class Blame1[G](trafo: BlameTrafo[G], cancellativeGroupings: Seq[Ref[G, CancellativeFailureGrouping[G]]])(implicit val o: Origin) extends NodeFamily[G]
 
 sealed trait Type[G] extends NodeFamily[G] with TypeImpl[G]

src/col/vct/col/ast/declaration/global/ExpectedErrorImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.declaration.global
+
+import vct.col.ast.ExpectedError
+import vct.col.print.{Ctx, Doc, Empty}
+
+trait ExpectedErrorImpl[G] { this: ExpectedError[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Empty
+}

src/col/vct/col/origin/Blame.scala

@@ -103,6 +103,7 @@ trait WithContractFailure extends VerificationFailure {
     inlineDescWithSource(node.o.inlineContext, failure.inlineDescCompletion)
 }
 
+/*
 sealed trait ExpectedErrorFailure extends VerificationFailure {
   def err: ExpectedError
 }
@@ -120,6 +121,7 @@ case class ExpectedErrorNotTripped(err: ExpectedError) extends ExpectedErrorFail
   override def desc: String = err.errorRegion.messageInContext(s"The expected error with code `${err.errorCode}` was not encountered." + errUrl)
   override def inlineDesc: String = s"The expected error with code `${err.errorCode}` was not encountered."
 }
+*/
 
 case class AssignFailed(node: SilverFieldAssign[_]) extends NodeVerificationFailure {
   override def code: String = "assignFieldFailed"
@@ -716,6 +718,7 @@ trait Blame[-T <: VerificationFailure] {
   def blame(error: T): Unit
 }
 
+/*
 case class FilterExpectedErrorBlame(otherwise: Blame[VerificationFailure], expectedError: ExpectedError) extends Blame[VerificationFailure] {
   override def blame(error: VerificationFailure): Unit =
     if(expectedError.errorCode.r.matches(error.code)) {
@@ -724,6 +727,7 @@ case class FilterExpectedErrorBlame(otherwise: Blame[VerificationFailure], expec
       otherwise.blame(error)
     }
 }
+*/
 
 case object BlamePathError extends SystemError {
   override def text: String = "The accounting for a pre- or postcondition is wrong: the path is empty before the layered blames are resolved, or an empty path was expected but it is not."

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -1744,8 +1744,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
 
   def coerce(node: Verification[Pre]): Verification[Pre] = {
     implicit val o: Origin = node.o
-    val Verification(tasks, expectedErrors) = node
-    Verification(tasks, expectedErrors)
+    val Verification(tasks) = node
+    Verification(tasks)
   }
 
   def coerce(node: VerificationContext[Pre]): VerificationContext[Pre] = {

src/colhelper/ColDefs.scala

@@ -17,7 +17,6 @@ object ColDefs {
     q"import vct.col.origin._",
     q"import vct.col.ref.Ref",
     q"import vct.col.resolve.ctx.Referrable",
-    q"import vct.col.origin.ExpectedError",
     q"import hre.data.BitString",
   )
 

src/colhelper/ColDescription.scala

@@ -134,7 +134,7 @@ class ColDescription {
       else
         q"rewriter.porcelainRefSucc[$decl[Post]]($term).getOrElse(rewriter.anySucc[${Type.Name(tDecl)}[Post]]($term.decl))"
     case Type.Name("Int") | Type.Name("String") | Type.Name("Boolean") | Type.Name("BigInt") | Type.Name("BigDecimal") |
-         Type.Name("BitString") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") =>
+         Type.Name("BitString") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) =>
       term
     case Type.Apply(Type.Name("Either"), List(t1, t2)) =>
       q"$term.left.map(l => ${rewriteDefault(q"l", t1)}).map(r => ${rewriteDefault(q"r", t2)})"

src/colhelper/ColHelperComparator.scala

@@ -10,7 +10,7 @@ case class ColHelperComparator(info: ColDescription) extends ColHelperMaker {
     case Type.Apply(Type.Name("Ref"), _) => q"true"
 
     case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") |
-         Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") | Type.Name("BitString") =>
+         Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("BitString") =>
       q"$left == $right"
 
     case Type.Apply(Type.Name("Seq"), List(inner)) =>
@@ -45,7 +45,7 @@ case class ColHelperComparator(info: ColDescription) extends ColHelperMaker {
 
     case Type.Apply(Type.Name(name), List(Type.Name("G"))) if info.supports("Node")(name) => q"LazyList.empty"
     case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") |
-         Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") | Type.Name("BitString") =>
+         Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("BitString") =>
       q"LazyList.empty"
 
     case Type.Apply(Type.Name("Seq"), List(inner)) =>
@@ -78,7 +78,7 @@ case class ColHelperComparator(info: ColDescription) extends ColHelperMaker {
 
     case Type.Apply(Type.Name("Ref"), _) => q"LazyList.empty"
     case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") |
-         Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") | Type.Name("BitString") =>
+         Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("BitString") =>
       q"LazyList.empty"
 
     case Type.Apply(Type.Name("Seq"), List(inner)) =>

src/colhelper/ColHelperDeserialize.scala

@@ -33,8 +33,6 @@ case class ColHelperDeserialize(info: ColDescription, proto: ColProto) extends C
 
   def deserializeTerm(term: Term, typ: proto.Typ, scalaTyp: Type): Term =
     proto.primitivize(typ) match {
-      case proto.TName("ExpectedErrors") => q"Nil"
-
       case proto.TBool => term
       case r @ proto.TRef() => q"ref[${lastTypeArg(scalaTyp)}]($term.index)"
       case proto.TInt => term

src/colhelper/ColHelperSerialize.scala

@@ -37,8 +37,6 @@ case class ColHelperSerialize(info: ColDescription, proto: ColProto) extends Col
 
   def serializeTerm(term: Term, typ: proto.Typ): Term =
     proto.primitivize(typ) match {
-      case proto.TName("ExpectedErrors") => q"ser.ExpectedErrors()"
-
       case proto.TBool => term
       case proto.TRef() => q"ser.Ref(decls($term.decl))"
       case proto.TInt => term

src/colhelper/ColHelperSubnodes.scala

@@ -26,8 +26,7 @@ case class ColHelperSubnodes(info: ColDescription) extends ColHelperMaker {
       case Type.Apply(Type.Name(typ), List(Type.Name("G"))) if info.supports("NodeFamily")(typ) || info.supports("Declaration")(typ) =>
         Some(node => q"Seq($node)")
       case Type.Name("Int") | Type.Name("String") | Type.Name("Boolean") | Type.Name("BigInt") | Type.Name("BigDecimal") |
-           Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Apply(Type.Name("Ref"), _) |
-           Type.Name("ExpectedError") | Type.Name("BitString") =>
+           Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Apply(Type.Name("Ref"), _) | Type.Name("BitString") =>
         None
       case Type.Apply(Type.Name("Either"), List(t1, t2)) =>
         val f1 = subnodePatternByType(t1).getOrElse((elem: Term) => q"Nil")

src/colhelper/ColProto.scala

@@ -72,8 +72,6 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) =
   case class TTuple(ts: Seq[Typ])(val scalaArg: Seq[SType]) extends Typ
 
   def getType(t: SType): Typ = t match {
-    case SType.Apply(SType.Name("Seq"), List(SType.Name("ExpectedError"))) => TName("ExpectedErrors")
-
     case SType.Apply(SType.Name("Seq"), List(arg)) => TSeq(getType(arg))(arg)
     case SType.Apply(SType.Name("Option"), List(arg)) => TOption(getType(arg))(arg)
     case SType.Apply(SType.Name("Set"), List(arg)) => TSet(getType(arg))(arg)
@@ -180,8 +178,6 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) =
     message("Ref")
       .addField(field("index").setType(PType.TYPE_INT64))
       .build(),
-    message("ExpectedErrors")
-      .build(),
   )
 
   def declarationKinds(): Seq[DescriptorProto] =

src/parsers/vct/parsers/ColIParser.scala

@@ -14,13 +14,13 @@ case class ColIParser(override val originProvider: OriginProvider, override val
       val parser = new CParser(tokens)
 
       val (errors, tree) = noErrorsOrThrow(parser, lexer, originProvider) {
-        val errors = expectedErrors(tokens, LangCLexer.EXPECTED_ERROR_CHANNEL, LangCLexer.VAL_EXPECT_ERROR_OPEN, LangCLexer.VAL_EXPECT_ERROR_CLOSE)
+        val errors = expectedErrors[G](tokens, LangCLexer.EXPECTED_ERROR_CHANNEL, LangCLexer.VAL_EXPECT_ERROR_OPEN, LangCLexer.VAL_EXPECT_ERROR_CLOSE)
         val tree = parser.compilationUnit()
         (errors, tree)
       }
 
-      val decls = CToCol[G](originProvider, blameProvider, errors).convert(tree)
-      ParseResult(decls, errors.map(_._3))
+      val decls = CToCol[G](originProvider, errors._2).convert(tree)
+      ParseResult(errors._2.map(_._3) ++ errors._1 ++ decls)
     } catch {
       case m: MatchError =>
         throw ParseMatchError(m.getMessage())

src/parsers/vct/parsers/ColJavaParser.scala

@@ -3,7 +3,6 @@ package vct.parsers
 import org.antlr.v4.runtime.{CharStream, CommonTokenStream}
 import vct.antlr4.generated._
 import vct.col.ast.GlobalDeclaration
-import vct.col.origin.ExpectedError
 import vct.parsers.transform.{BlameProvider, JavaToCol, OriginProvider}
 
 import scala.jdk.CollectionConverters.CollectionHasAsScala
@@ -24,35 +23,43 @@ case class ColJavaParser(override val originProvider: OriginProvider, override v
       }
 
       val (errors, tree) = noErrorsOrThrow(parser, lexer, originProvider) {
-        val errors = expectedErrors(tokens, LangJavaLexer.EXPECTED_ERROR_CHANNEL, LangJavaLexer.VAL_EXPECT_ERROR_OPEN, LangJavaLexer.VAL_EXPECT_ERROR_CLOSE)
+        val errors = expectedErrors[G](tokens, LangJavaLexer.EXPECTED_ERROR_CHANNEL, LangJavaLexer.VAL_EXPECT_ERROR_OPEN, LangJavaLexer.VAL_EXPECT_ERROR_CLOSE)
         val tree = parser.compilationUnit()
         (errors, tree)
       }
 
-      val decls = JavaToCol[G](originProvider, blameProvider, errors).convert(tree)
-      ParseResult(decls, errors.map(_._3))
+      val decls = JavaToCol[G](originProvider, errors._2).convert(tree)
+      ParseResult(errors._2.map(_._3) ++ errors._1 ++ decls)
     } catch {
       case m: MatchError =>
         throw ParseMatchError(m.getMessage())
     }
   }
 
-  def parseExpr[G](stream: CharStream, specCommentsNeeded: Boolean): (vct.col.ast.Expr[G], Seq[ExpectedError]) = {
+  def parseExpr[G](stream: CharStream, specCommentsNeeded: Boolean): vct.col.ast.Expr[G] = {
     try {
       val lexer = new LangJavaLexer(stream)
       val tokens = new CommonTokenStream(lexer)
       originProvider.setTokenStream(tokens)
-      val errors = expectedErrors(tokens, LangJavaLexer.EXPECTED_ERROR_CHANNEL, LangJavaLexer.VAL_EXPECT_ERROR_OPEN, LangJavaLexer.VAL_EXPECT_ERROR_CLOSE)
       val parser = new JavaParser(tokens)
       if (!specCommentsNeeded) {
         parser.specLevel = 1
       }
 
-      val tree = noErrorsOrThrow(parser, lexer, originProvider) {
-        parser.expr()
+      val (errors, tree) = noErrorsOrThrow(parser, lexer, originProvider) {
+        val errors = expectedErrors[G](tokens, LangJavaLexer.EXPECTED_ERROR_CHANNEL, LangJavaLexer.VAL_EXPECT_ERROR_OPEN, LangJavaLexer.VAL_EXPECT_ERROR_CLOSE)
+        val tree = parser.expr()
+        (errors, tree)
+      }
+
+      val expr = JavaToCol[G](originProvider, errors._2).convert(tree)
+
+      if(errors._2.nonEmpty) {
+        val (start, stop, _) = errors._2.head
+        throw ParseError(originProvider(start, stop), "Expected errors in recursively parsed embedded expressions are currently not supported.")
       }
-      val decls = JavaToCol[G](originProvider, blameProvider, errors).convert(tree)
-      (decls, errors.map(_._3))
+
+      expr
     } catch {
       case m: MatchError =>
         throw ParseMatchError(m.getMessage())

src/parsers/vct/parsers/ColLLVMParser.scala

@@ -35,7 +35,7 @@ case class ColLLVMParser(override val originProvider: OriginProvider, override v
     }
     val protoProgram = Program.parseFrom(process.getInputStream)
     val COLProgram = Deserialize.deserialize[G](protoProgram)
-    ParseResult(COLProgram.declarations, Seq.empty)
+    ParseResult(COLProgram.declarations)
   }
 
 }

src/parsers/vct/parsers/ColPVLParser.scala

@@ -14,13 +14,13 @@ case class ColPVLParser(override val originProvider: OriginProvider, override va
       val parser = new PVLParser(tokens)
 
       val (errors, tree) = noErrorsOrThrow(parser, lexer, originProvider) {
-        val errors = expectedErrors(tokens, LangPVLLexer.EXPECTED_ERROR_CHANNEL, LangPVLLexer.VAL_EXPECT_ERROR_OPEN, LangPVLLexer.VAL_EXPECT_ERROR_CLOSE)
+        val errors = expectedErrors[G](tokens, LangPVLLexer.EXPECTED_ERROR_CHANNEL, LangPVLLexer.VAL_EXPECT_ERROR_OPEN, LangPVLLexer.VAL_EXPECT_ERROR_CLOSE)
         val tree = parser.program()
         (errors, tree)
       }
 
-      val decls = PVLToCol[G](originProvider, blameProvider, errors).convert(tree)
-      ParseResult(decls, errors.map(_._3))
+      val decls = PVLToCol[G](originProvider, errors._2).convert(tree)
+      ParseResult(errors._2.map(_._3) ++ errors._1 ++ decls)
     } catch {
       case m: MatchError =>
         throw ParseMatchError(m.getMessage())

src/parsers/vct/parsers/ParseResult.scala

@@ -1,14 +1,13 @@
 package vct.parsers
 
 import vct.col.ast.{GlobalDeclaration, VerificationContext}
-import vct.col.origin.ExpectedError
 
 case object ParseResult {
   def reduce[G](parses: Seq[ParseResult[G]]): ParseResult[G] =
     parses.reduceOption((l, r) => (l, r) match {
-      case (ParseResult(declsLeft, expectedLeft), ParseResult(declsRight, expectedRight)) =>
-        ParseResult(declsLeft ++ declsRight, expectedLeft ++ expectedRight)
-    }).getOrElse(ParseResult(Nil, Nil))
+      case (ParseResult(declsLeft), ParseResult(declsRight)) =>
+        ParseResult(declsLeft ++ declsRight)
+    }).getOrElse(ParseResult(Nil))
 }
 
-case class ParseResult[G](decls: Seq[GlobalDeclaration[G]], expectedErrors: Seq[ExpectedError])
+case class ParseResult[G](decls: Seq[GlobalDeclaration[G]])

src/parsers/vct/parsers/Parser.scala

@@ -3,9 +3,10 @@ package vct.parsers
 import hre.io.Readable
 import org.antlr.v4.runtime
 import org.antlr.v4.runtime.{BailErrorStrategy, CharStreams, CommonTokenStream, Token}
-import vct.col.origin.ExpectedError
 import vct.parsers.transform.{BlameProvider, OriginProvider}
 import vct.result.VerificationError.UserError
+import vct.col.ast._
+import vct.col.origin.Origin
 
 import java.io.FileNotFoundException
 import scala.jdk.CollectionConverters._
@@ -16,10 +17,11 @@ abstract class Parser(val originProvider: OriginProvider, val blameProvider: Bla
     override def text: String = "There is no scope to close here."
   }
 
-  def expectedErrors(lexer: CommonTokenStream, channel: Int, startToken: Int, endToken: Int): Seq[(Token, Token, ExpectedError)] = {
+  def expectedErrors[G](lexer: CommonTokenStream, channel: Int, startToken: Int, endToken: Int): (Seq[ExpectedError[G]], Seq[(Token, Token, CancellativeFailureGrouping[G])]) = {
     lexer.fill()
     var startStack: Seq[(String, Token)] = Nil
-    var errors = Seq.empty[(Token, Token, ExpectedError)]
+    var errors = Seq.empty[ExpectedError[G]]
+    var groupings = Seq.empty[(Token, Token, CancellativeFailureGrouping[G])]
 
     for(token <- lexer.getTokens.asScala.filter(_.getChannel == channel)) {
       if(token.getType == startToken) {
@@ -36,12 +38,15 @@ abstract class Parser(val originProvider: OriginProvider, val blameProvider: Bla
         if(startStack.isEmpty) throw UnbalancedExpectedError(token)
         val (code, start) = startStack.last
         startStack = startStack.init
-        val err = ExpectedError(code, originProvider(start, token), blameProvider(start, token))
-        errors :+= (start, token, err)
+        implicit val o: Origin = originProvider(start, token)
+        val grouping = new CancellativeFailureGrouping[G](Some(code), Some(2))
+        val err = new ExpectedError[G](Blame1(BlameInput(), Seq(grouping.ref)))
+        errors :+= err
+        groupings :+= ((start, token, grouping))
       }
     }
 
-    errors.sortBy(_._1.getTokenIndex)
+    (errors, groupings.sortBy(_._1.getTokenIndex))
   }
 
   protected def getErrorsFor[T](parser: runtime.Parser, lexer: runtime.Lexer, originProvider: OriginProvider)(f: => T): Either[Seq[ParseError], T] = {