Use underlyingPath where available in SilverToCol (needs proper fix)

utwente-fmt · Nov 22, 2024 · b5e997d · b5e997d
1 parent 7d8907e
commit b5e997d
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 28 deletions.
diff --git a/src/col/vct/col/serialize/SerializeOrigin.scala b/src/col/vct/col/serialize/SerializeOrigin.scala
@@ -95,9 +95,13 @@ object SerializeOrigin extends LazyLogging {
           )
         case ReadableOrigin(readable) =>
           // Not sure how to best deal with directory/filename here
-          Seq(ser.OriginContent.Content.ReadableOrigin(
-            ser.ReadableOrigin("", readable.fileName, None, None)
-          ))
+          Seq(ser.OriginContent.Content.ReadableOrigin(ser.ReadableOrigin(
+            "",
+            readable.underlyingPath.map(_.toString)
+              .getOrElse(readable.fileName),
+            None,
+            None,
+          )))
         case PositionRange(startLineIdx, endLineIdx, startEndColIdx) =>
           Seq(ser.OriginContent.Content.PositionRange(ser.PositionRange(
             startLineIdx,

diff --git a/src/main/vct/main/stages/Parsing.scala b/src/main/vct/main/stages/Parsing.scala
@@ -99,8 +99,6 @@ case class Parsing[G <: Generation](
           .orElse(Language.fromFilename(readable.fileName))
           .getOrElse(throw UnknownFileExtension(readable.fileName))
 
-        val origin = Origin(Seq(ReadableOrigin(readable)))
-
         val parser =
           language match {
             case Language.C =>
@@ -109,7 +107,7 @@ case class Parsing[G <: Generation](
                 blameProvider,
                 cc,
                 cSystemInclude,
-                Option(Paths.get(readable.fileName).getParent).toSeq ++
+                readable.underlyingPath.map(_.getParent).toSeq ++
                   cOtherIncludes,
                 cDefines,
               )
@@ -121,7 +119,7 @@ case class Parsing[G <: Generation](
                 blameProvider,
                 ccpp,
                 cppSystemInclude,
-                Option(Paths.get(readable.fileName).getParent).toSeq ++
+                readable.underlyingPath.map(_.getParent).toSeq ++
                   cppOtherIncludes,
                 cppDefines,
               )

diff --git a/src/viper/viper/api/transform/SilverParserDummyFrontend.scala b/src/viper/viper/api/transform/SilverParserDummyFrontend.scala
@@ -51,7 +51,10 @@ case class SilverParserDummyFrontend()
     parse(RWFile(path).readToCompletion(), path)
 
   def parse(readable: Readable): Either[Seq[AbstractError], Program] =
-    parse(readable.readToCompletion(), Paths.get(readable.fileName))
+    parse(
+      readable.readToCompletion(),
+      readable.underlyingPath.getOrElse(Paths.get(readable.fileName)),
+    )
 
   override def createVerifier(fullCmd: String): Verifier = noVerifier
 

diff --git a/src/viper/viper/api/transform/SilverToCol.scala b/src/viper/viper/api/transform/SilverToCol.scala
@@ -28,8 +28,6 @@ import viper.silver.plugin.standard.termination.{
 import viper.silver.verifier.AbstractError
 import viper.silver.{ast => silver}
 
-import java.nio.file.{Path, Paths}
-
 case object SilverToCol {
   private def SilverPositionOrigin(node: silver.Positioned): Origin =
     node.pos match {
@@ -66,7 +64,7 @@ case object SilverToCol {
         })
   }
 
-  case class SilverFrontendParseError(path: Path, errors: Seq[AbstractError])
+  case class SilverFrontendParseError(path: String, errors: Seq[AbstractError])
       extends UserError {
     override def code: String = "silverFrontendError"
     override def text: String =
@@ -78,36 +76,22 @@ case object SilverToCol {
   }
 
   def transform[G](
-      diagnosticPath: Path,
+      diagnosticFilename: String,
       in: Either[Seq[AbstractError], silver.Program],
       blameProvider: BlameProvider,
   ): col.Program[G] =
     in match {
       case Right(program) => SilverToCol(program, blameProvider).transform()
       case Left(errors) =>
-        throw SilverFrontendParseError(diagnosticPath, errors)
+        throw SilverFrontendParseError(diagnosticFilename, errors)
     }
 
-  def parse[G](path: Path, blameProvider: BlameProvider): col.Program[G] =
-    transform(path, SilverParserDummyFrontend().parse(path), blameProvider)
-
-  def parse[G](
-      input: String,
-      diagnosticPath: Path,
-      blameProvider: BlameProvider,
-  ): col.Program[G] =
-    transform(
-      diagnosticPath,
-      SilverParserDummyFrontend().parse(input, diagnosticPath),
-      blameProvider,
-    )
-
   def parse[G](
       readable: Readable,
       blameProvider: BlameProvider,
   ): col.Program[G] =
     transform(
-      Paths.get(readable.fileName),
+      readable.fileName,
       SilverParserDummyFrontend().parse(readable),
       blameProvider,
     )