it finally compiles, but there is a None.get error, which was somewha…

…t expected
utwente-fmt · Oct 12, 2023 · 54d8deb · 54d8deb
1 parent 89b7132
commit 54d8deb
Show file tree

Hide file tree

Showing 12 changed files with 36 additions and 28 deletions.
diff --git a/src/main/vct/importer/JavaLibraryLoader.scala b/src/main/vct/importer/JavaLibraryLoader.scala
@@ -2,8 +2,9 @@ package vct.importer
 
 import hre.io.RWFile
 import vct.col.ast.JavaNamespace
+import vct.col.origin.Origin
 import vct.col.resolve.ExternalJavaLoader
-import vct.parsers.transform.{BlameProvider, ReadableOriginProvider}
+import vct.parsers.transform.BlameProvider
 import vct.parsers.{ColJavaParser, FileNotFound}
 
 import java.io.File
@@ -12,7 +13,7 @@ import java.nio.file.Path
 case class JavaLibraryLoader(blameProvider: BlameProvider) extends ExternalJavaLoader {
   override def load[G](base: Path, name: Seq[String]): Option[JavaNamespace[G]] = try {
     val f = RWFile(base.resolve((name.init :+ name.last + ".java").mkString(File.separator)).toFile)
-    ColJavaParser(ReadableOriginProvider(f), blameProvider).parse[G](f).decls match {
+    ColJavaParser(Origin(Seq()).addReadableOrigin(f), blameProvider).parse[G](f).decls match {
       case Seq(ns: JavaNamespace[G]) => Some(ns)
       case _ => None
     }

diff --git a/src/main/vct/importer/Util.scala b/src/main/vct/importer/Util.scala
@@ -2,11 +2,11 @@ package vct.importer
 
 import hre.io.Readable
 import vct.col.ast.{JavaClass, JavaNamespace, Program}
-import vct.col.origin.{Blame, ReadableOrigin, VerificationFailure}
+import vct.col.origin.{Blame, Origin, ReadableOrigin, VerificationFailure}
 import vct.col.rewrite.Disambiguate
 import vct.main.stages.Resolution
 import vct.parsers.{ColJavaParser, ColPVLParser}
-import vct.parsers.transform.{ConstantBlameProvider, ReadableOriginProvider}
+import vct.parsers.transform.ConstantBlameProvider
 import vct.result.VerificationError.UserError
 
 case object Util {
@@ -22,7 +22,7 @@ case object Util {
   }
 
   def loadPVLLibraryFile[G](readable: Readable): Program[G] = {
-    val res = ColPVLParser(ReadableOriginProvider(readable), ConstantBlameProvider(LibraryFileBlame)).parse(readable)
+    val res = ColPVLParser(Origin(Seq(ReadableOrigin(readable))), ConstantBlameProvider(LibraryFileBlame)).parse(readable)
     val context = Resolution(ConstantBlameProvider(LibraryFileBlame)).run(res)
     val unambiguousProgram: Program[_] = Disambiguate().dispatch(context.tasks.head.program)
     unambiguousProgram.asInstanceOf[Program[G]]
@@ -35,7 +35,7 @@ case object Util {
   }
 
   def loadJavaClass[G](readable: Readable): JavaClass[G] =
-    ColJavaParser(ReadableOriginProvider(readable), ConstantBlameProvider(LibraryFileBlame)).parse(readable).decls match {
+    ColJavaParser(Origin(Seq(ReadableOrigin(readable))), ConstantBlameProvider(LibraryFileBlame)).parse(readable).decls match {
       case Seq(javaNamespace: JavaNamespace[G]) => javaNamespace.declarations match {
         case Seq(javaClass: JavaClass[G]) => javaClass
         case seq => throw JavaLoadError("Expected to load exactly one Java class but found " + seq.size)

diff --git a/src/main/vct/main/stages/Parsing.scala b/src/main/vct/main/stages/Parsing.scala
@@ -2,11 +2,12 @@ package vct.main.stages
 
 import hre.io.Readable
 import hre.stages.Stage
+import vct.col.origin.{Origin, ReadableOrigin}
 import vct.col.rewrite.Generation
 import vct.main.stages.Parsing.{Language, UnknownFileExtension}
 import vct.options.Options
 import vct.parsers._
-import vct.parsers.transform.{BlameProvider, ReadableOriginProvider}
+import vct.parsers.transform.BlameProvider
 import vct.resources.Resources
 import vct.result.VerificationError.UserError
 import viper.api.transform.ColSilverParser
@@ -80,7 +81,7 @@ case class Parsing[G <: Generation]
         .orElse(Language.fromFilename(readable.fileName))
         .getOrElse(throw UnknownFileExtension(readable.fileName))
 
-      val origin = ReadableOriginProvider(readable)
+      val origin = Origin(Seq(ReadableOrigin(readable)))
 
       val parser = language match {
         case Language.C => ColCParser(origin, blameProvider, cc, cSystemInclude, cOtherIncludes, cDefines)

diff --git a/src/main/vct/main/stages/Resolution.scala b/src/main/vct/main/stages/Resolution.scala
@@ -6,7 +6,7 @@ import vct.col.ast.{AddrOf, ApplicableContract, CGlobalDeclaration, Expr, Global
 import org.antlr.v4.runtime.CharStreams
 import vct.col.ast._
 import vct.col.check.CheckError
-import vct.col.origin.{FileSpanningOrigin, Origin, OriginFilename}
+import vct.col.origin.{FileSpanningOrigin, Origin, OriginFilename, ReadableOrigin}
 import vct.col.resolve.{Resolve, ResolveReferences, ResolveTypes}
 import vct.col.rewrite.Generation
 import vct.col.rewrite.bip.IsolateBipGlue
@@ -15,7 +15,7 @@ import vct.importer.JavaLibraryLoader
 import vct.main.stages.Resolution.InputResolutionError
 import vct.options.Options
 import vct.options.types.ClassPathEntry
-import vct.parsers.transform.{BlameProvider, ReadableOriginProvider, RedirectOriginProvider}
+import vct.parsers.transform.BlameProvider
 import vct.parsers.{ColJavaParser, ColLLVMParser, FileNotFound, ParseResult}
 import vct.resources.Resources
 import vct.result.VerificationError.UserError
@@ -72,20 +72,20 @@ case class MyLocalJavaParser(blameProvider: BlameProvider) extends Resolve.SpecE
 
 case class MyLocalLLVMSpecParser(blameProvider: BlameProvider) extends Resolve.SpecContractParser {
   override def parse[G](input: LlvmFunctionContract[G], o: Origin): ApplicableContract[G] = {
-    val originProvider = ReadableOriginProvider(input.o.getFilename match {
+    val originProvider = Origin(Seq(ReadableOrigin(input.o.getFilename match {
       case Some(OriginFilename(filename)) => StringReadable(input.value, filename)
       case _ => StringReadable(input.value)
-    })
+    })))
     val charStream = CharStreams.fromString(input.value)
     ColLLVMParser(originProvider, blameProvider)
       .parseFunctionContract[G](charStream)._1
   }
 
   override def parse[G](input: LlvmGlobal[G], o: Origin): GlobalDeclaration[G] = {
-    val originProvider = ReadableOriginProvider(input.o.getFilename match {
+    val originProvider = Origin(Seq(ReadableOrigin(input.o.getFilename match {
       case Some(OriginFilename(filename)) => StringReadable(input.value, filename)
       case _ => StringReadable(input.value)
-    })
+    })))
     val charStream = CharStreams.fromString(input.value)
     ColLLVMParser(originProvider, blameProvider)
       .parseGlobal(charStream)._1

diff --git a/src/parsers/vct/parsers/ColIParser.scala b/src/parsers/vct/parsers/ColIParser.scala
@@ -19,7 +19,7 @@ case class ColIParser(override val origin: Origin, override val blameProvider: B
         (errors, tree)
       }
 
-      val decls = CToCol[G](blameProvider, errors).convert(tree)
+      val decls = CToCol[G](origin, blameProvider, errors).convert(tree)
       ParseResult(decls, errors.map(_._3))
     } catch {
       case m: MatchError =>

diff --git a/src/parsers/vct/parsers/ColJavaParser.scala b/src/parsers/vct/parsers/ColJavaParser.scala
@@ -29,7 +29,7 @@ case class ColJavaParser(override val origin: Origin,
         (errors, tree)
       }
 
-      val decls = JavaToCol[G](blameProvider, errors).convert(tree)
+      val decls = JavaToCol[G](origin, blameProvider, errors).convert(tree)
       ParseResult(decls, errors.map(_._3))
     } catch {
       case m: MatchError =>
@@ -50,7 +50,7 @@ case class ColJavaParser(override val origin: Origin,
       val tree = noErrorsOrThrow(origin, parser, lexer) {
         parser.expr()
       }
-      val decls = JavaToCol[G](blameProvider, errors).convert(tree)
+      val decls = JavaToCol[G](origin, blameProvider, errors).convert(tree)
       (decls, errors.map(_._3))
     } catch {
       case m: MatchError =>

diff --git a/src/parsers/vct/parsers/ColLLVMParser.scala b/src/parsers/vct/parsers/ColLLVMParser.scala
@@ -55,7 +55,7 @@ case class ColLLVMParser(override val origin: Origin, override val blameProvider
       val tree = parser.valEmbedContract()
       (errors, tree)
     }
-    val contract = LLVMContractToCol[G](blameProvider, errors).convert(tree)
+    val contract = LLVMContractToCol[G](origin, blameProvider, errors).convert(tree)
     (contract, errors.map(_._3))
   }
 
@@ -71,7 +71,7 @@ case class ColLLVMParser(override val origin: Origin, override val blameProvider
       val tree = parser.valGlobalDeclaration()
       (errors, tree)
     }
-    val global = LLVMContractToCol[G](blameProvider, errors).convert(tree)
+    val global = LLVMContractToCol[G](origin, blameProvider, errors).convert(tree)
     (global, errors.map(_._3))
   }
 }
diff --git a/src/parsers/vct/parsers/ColPVLParser.scala b/src/parsers/vct/parsers/ColPVLParser.scala
@@ -21,7 +21,7 @@ case class ColPVLParser(override val origin: Origin,
         (errors, tree)
       }
 
-      val decls = PVLToCol[G](blameProvider, errors).convert(tree)
+      val decls = PVLToCol[G](origin, blameProvider, errors).convert(tree)
       ParseResult(decls, errors.map(_._3))
     } catch {
       case m: MatchError =>

diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala
@@ -16,8 +16,9 @@ import scala.annotation.nowarn
 import scala.collection.mutable
 
 @nowarn("msg=match may not be exhaustive&msg=Some\\(")
-case class CToCol[G](override val blameProvider: BlameProvider, override val errors: Seq[(Token, Token, ExpectedError)])
-  extends ToCol(blameProvider, errors) {
+case class CToCol[G](override val baseOrigin: Origin,
+                     override val blameProvider: BlameProvider, override val errors: Seq[(Token, Token, ExpectedError)])
+  extends ToCol(baseOrigin, blameProvider, errors) {
   def convert(unit: CompilationUnitContext): Seq[GlobalDeclaration[G]] = unit match {
     case CompilationUnit0(translationUnit, _) =>
       translationUnit.toSeq.map(convert(_))

diff --git a/src/parsers/vct/parsers/transform/JavaToCol.scala b/src/parsers/vct/parsers/transform/JavaToCol.scala
@@ -18,8 +18,10 @@ import scala.annotation.nowarn
 import scala.collection.mutable
 
 @nowarn("msg=match may not be exhaustive&msg=Some\\(")
-case class JavaToCol[G](override val blameProvider: BlameProvider, override val errors: Seq[(Token, Token, ExpectedError)])
-  extends ToCol[G](blameProvider, errors) with LazyLogging {
+case class JavaToCol[G](override val baseOrigin: Origin,
+                        override val blameProvider: BlameProvider,
+                        override val errors: Seq[(Token, Token, ExpectedError)])
+  extends ToCol[G](baseOrigin, blameProvider, errors) with LazyLogging {
   def convert(implicit unit: CompilationUnitContext): Seq[GlobalDeclaration[G]] = unit match {
     case CompilationUnit0(pkg, imports, decls, _) =>
       Seq(new JavaNamespace(pkg.map(convert(_)), imports.map(convert(_)), decls.flatMap(convert(_))))

diff --git a/src/parsers/vct/parsers/transform/LLVMContractToCol.scala b/src/parsers/vct/parsers/transform/LLVMContractToCol.scala
@@ -15,9 +15,10 @@ import scala.collection.immutable.{AbstractSeq, LinearSeq}
 import scala.collection.mutable
 
 @nowarn("msg=match may not be exhaustive&msg=Some\\(")
-case class LLVMContractToCol[G](override val blameProvider: BlameProvider,
+case class LLVMContractToCol[G](override val baseOrigin: Origin,
+                                override val blameProvider: BlameProvider,
                                 override val errors: Seq[(Token, Token, ExpectedError)])
-  extends ToCol(blameProvider, errors) {
+  extends ToCol(baseOrigin, blameProvider, errors) {
 
   def local(ctx: ParserRuleContext, name: String): Expr[G] =
     LlvmLocal(name)(blame(ctx))(origin(ctx))

diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala
@@ -17,8 +17,10 @@ import scala.annotation.nowarn
 import scala.collection.mutable
 
 @nowarn("msg=match may not be exhaustive&msg=Some\\(")
-case class PVLToCol[G](override val blameProvider: BlameProvider, override val errors: Seq[(Token, Token, ExpectedError)])
-  extends ToCol[G](blameProvider, errors) {
+case class PVLToCol[G](override val baseOrigin: Origin,
+                       override val blameProvider: BlameProvider,
+                       override val errors: Seq[(Token, Token, ExpectedError)])
+  extends ToCol[G](baseOrigin, blameProvider, errors) {
   def convert(implicit program: ProgramContext): Seq[GlobalDeclaration[G]] = program match {
     case Program0(decls, _, _) => decls.flatMap(convert(_))
   }