Merge pull request #1858 from informalsystems/1114/refactor-cli-pipeline

Refactor CLI pipeline

mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala

@@ -5,21 +5,25 @@ import com.typesafe.scalalogging.LazyLogging
 /**
  * An abstract error message.
  */
-sealed abstract class ErrorMessage
+sealed abstract class ErrorMessage {
+
+  /** The concrete content of a message */
+  val msg: String
+}
 
 /**
  * A normal error that does not require a stack trace.
  * @param msg
  *   the message text
  */
-case class NormalErrorMessage(msg: String) extends ErrorMessage
+case class NormalErrorMessage(val msg: String) extends ErrorMessage
 
 /**
  * A failure message that should be printed along with a stack trace.
  * @param msg
  *   the message text
  */
-case class FailureMessage(msg: String) extends ErrorMessage
+case class FailureMessage(val msg: String) extends ErrorMessage
 
 /**
  * ExceptionAdapter allows us to convert an exception into a message string. The purpose of the adapter is to push the

mod-infra/src/main/scala/at/forsyte/apalache/infra/Executor.scala

@@ -0,0 +1,41 @@
+package at.forsyte.apalache.infra
+
+import at.forsyte.apalache.infra.passes.{Pass, PassChainExecutor, ToolModule, WriteablePassOptions}
+import com.google.inject.Guice
+
+/**
+ * This Executor abstracts the dependency injection and execution logic required for executing a PassChainExecutor
+ *
+ * @param toolModule
+ *   The [[ToolModule]] that specifies the sequence of passes
+ * @throws [[AdaptedException]]
+ *   if any exceptions are caught by the configured [[ExceptionAdapter]]
+ * @author
+ *   Shon Feder
+ */
+case class Executor(val toolModule: ToolModule) {
+  private val injector = Guice.createInjector(toolModule)
+
+  /** Exposes mutable access to options configuring the behavior of the [passChainExecutor] */
+  val passOptions = injector.getInstance(classOf[WriteablePassOptions])
+
+  private val exceptionAdapter = injector.getInstance(classOf[ExceptionAdapter])
+
+  private val passChainExecutor = {
+    val passes = toolModule.passes.zipWithIndex.map { case (p, i) =>
+      injector.getInstance(p).withNumber(i)
+    }
+    new PassChainExecutor(passOptions, passes)
+  }
+
+  /** Run the underlying PassChainExecutor, adapting exceptions as needed, and returning a `PassResult` */
+  def run(): Pass.PassResult = {
+    try {
+      passChainExecutor.run()
+    } catch {
+      case e: Throwable if exceptionAdapter.toMessage.isDefinedAt(e) =>
+        throw new AdaptedException(exceptionAdapter.toMessage(e))
+    }
+  }
+
+}

mod-infra/src/main/scala/at/forsyte/apalache/infra/exceptions.scala

@@ -14,3 +14,10 @@ class PassExecException(message: String) extends Exception(message)
  *   an error message
  */
 class PassOptionException(message: String) extends Exception(message)
+
+/**
+ * An error that has been adapted by the [[ExceptionAdaptor]]
+ * @param err
+ *   the [[ErrorMessage]] into which the originating error was adapted
+ */
+class AdaptedException(val err: ErrorMessage) extends Exception(err.msg)