Add patcher as a mode, and not as a run script

build.sc

@@ -578,7 +578,6 @@ object vercors extends Module {
       "carbon" -> "viper.carbon.Carbon",
       "silicon" -> "viper.silicon.SiliconRunner",
       "bashOptions" -> "vct.options.BashCompletion",
-      "patcher" -> "hre.util.Patch",
     ) }
     override def packedResources = T.sources()
     override def bareResourcePaths = T {

src/main/vct/main/Main.scala

@@ -12,7 +12,7 @@ import org.slf4j.LoggerFactory
 import scopt.OParser
 import vct.col.ast.Node
 import vct.debug.CrashReport
-import vct.main.modes.{CFG, Compile, VeSUV, Verify, VeyMont}
+import vct.main.modes.{CFG, Compile, Patcher, VeSUV, Verify, VeyMont}
 import vct.main.stages.Transformation
 import vct.options.Options
 import vct.options.types.Mode
@@ -103,7 +103,7 @@ case object Main extends LazyLogging {
   }
 
   def runMode(mode: Mode, options: Options): Int =
-    options.mode match {
+    mode match {
       case Mode.Verify => Verify.runOptions(options)
       case Mode.HelpVerifyPasses =>
         logger.info("Available passes:")
@@ -120,5 +120,6 @@ case object Main extends LazyLogging {
         logger.info("Starting control flow graph transformation")
         CFG.runOptions(options)
       case Mode.Compile => Compile.runOptions(options)
+      case Mode.Patcher => Patcher.runOptions(options)
     }
 }

src/main/vct/main/modes/Compile.scala

@@ -14,7 +14,7 @@ import java.nio.file.Paths
 case object Compile extends LazyLogging {
   def runOptions(options: Options): Int = {
     if (options.inputs.isEmpty) {
-      logger.warn("No inputs found, not compiling anything")
+      logger.warn("No inputs given, not compiling anything")
     }
 
     val collector = BlameCollector()

src/main/vct/main/modes/Patcher.scala

@@ -0,0 +1,61 @@
+package vct.main.modes
+
+import com.typesafe.scalalogging.LazyLogging
+import hre.util.Patch
+import hre.util.Patch.NoPatchException
+import vct.main.Main.{EXIT_CODE_ERROR, EXIT_CODE_SUCCESS}
+import vct.options.Options
+import vct.options.types.PathOrStd
+
+import java.nio.file.{FileAlreadyExistsException, Files, Paths}
+
+case object Patcher extends LazyLogging {
+  def runOptions(options: Options): Int = {
+    val patches =
+      try { Patch.fromFile(options.patchFile) }
+      catch {
+        case NoPatchException =>
+          logger.warn("Patch file is empty, not patching anything")
+          Seq()
+      }
+
+    options.inputs match {
+      case Seq() =>
+        logger.warn("No inputs given, not patching anything")
+        EXIT_CODE_SUCCESS
+      case Seq(in) =>
+        logger.info(
+          s"Applying patch `${options.patchFile}` to `${in.underlyingFile
+              .getOrElse("stdin")}`. Writing result to `${options.patchOutput}`"
+        )
+        Files.writeString(
+          options.patchOutput,
+          Patch.applyAll(patches, in.readToCompletion()),
+        )
+        EXIT_CODE_SUCCESS
+      case inputs =>
+        try { Files.createDirectories(options.patchOutput) }
+        catch {
+          case _: FileAlreadyExistsException =>
+            logger.error("Output directory already exists as file")
+            return EXIT_CODE_ERROR
+        }
+        for (input <- inputs) {
+          val outputPath =
+            input match {
+              case PathOrStd.Path(path) => options.patchOutput.resolve(path)
+              case PathOrStd.StdInOrOut => options.patchOutput.resolve("stdin")
+            }
+          logger.info(
+            s"Applying patch `${options.patchFile}` to `${input.underlyingFile
+                .getOrElse("stdin")}`. Writing result to `${outputPath}`"
+          )
+          Files.writeString(
+            outputPath,
+            Patch.applyAll(patches, input.readToCompletion()),
+          )
+        }
+        EXIT_CODE_SUCCESS
+    }
+  }
+}

src/main/vct/options/Options.scala

@@ -388,6 +388,22 @@ case object Options {
           .text("Output Java file")
       ),
       note(""),
+      note("Patcher mode"),
+      opt[Unit]("patcher").action((_, c) => c.copy(mode = Mode.Patcher)).text(
+        "Patches a file given a patch in the custom VerCors patch format."
+      ).children(
+        opt[Path]("patch-file").valueName("<path>").required()
+          .action((path, c) => c.copy(patchFile = path))
+          .text("Path to patch file to apply"),
+        opt[Path]("patch-output").valueName("<path>").required().action(
+          (path, c) => c.copy(patchOutput = path)
+        ).text(
+          "Output path. If the patcher is given only one input, this is interpeted as a file destination." +
+            " " +
+            "If the patcher is given multiple inputs, this is interpreted as a directory path."
+        ),
+      ),
+      note(""),
       note(""),
       arg[PathOrStd]("<path>...").unbounded().optional()
         .action((path, c) => c.copy(inputs = c.inputs :+ path))
@@ -501,6 +517,10 @@ case class Options(
 
     // Compile options
     compileOutput: Option[Path] = None,
+
+    // Patch options
+    patchFile: Path = null,
+    patchOutput: Path = null,
 ) {
   def getParserDebugOptions: vct.parsers.debug.DebugOptions =
     vct.parsers.debug.DebugOptions(

src/main/vct/options/types/Mode.scala

@@ -10,4 +10,5 @@ case object Mode {
   case object VeSUV extends Mode
   case object CFG extends Mode
   case object Compile extends Mode
+  case object Patcher extends Mode
 }