Return failure data from pass chain executions (#2186)

Co-authored-by: Igor Konnov <igor@informal.systems>

.unreleased/features/2186-rpc-data.md

@@ -0,0 +1,2 @@
+Return JSON with success or failure data from RPC calls to the CmdExecutor
+service (see #2186).

build.sbt

@@ -136,7 +136,9 @@ lazy val infra = (project in file("mod-infra"))
   .settings(
       testSettings,
       libraryDependencies ++= Seq(
-          Deps.commonsIo
+          Deps.commonsIo,
+          Deps.ujson,
+          Deps.upickle,
       ),
   )
 

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/Pass.scala

@@ -2,7 +2,10 @@ package at.forsyte.apalache.infra.passes
 
 import at.forsyte.apalache.infra.ExitCodes.TExitCode
 import at.forsyte.apalache.infra.passes.Pass.PassResult
-import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
+import at.forsyte.apalache.tla.lir.ModuleProperty
+import at.forsyte.apalache.tla.lir.TlaModule
+import upickle.default.Writer
+import upickle.default.writeJs
 
 /**
  * <p>An analysis or transformation pass. Instead of explicitly setting a pass' input and output, we interconnect passes
@@ -16,6 +19,8 @@ import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
  *
  * @author
  *   Igor Konnov
+ * @author
+ *   Shon Feder
  */
 trait Pass {
 
@@ -69,8 +74,51 @@ trait Pass {
    */
   def transformations: Set[ModuleProperty.Value]
 
+  /**
+   * Construct a failing pass result
+   *
+   * To be called to construct a failing `PassResult` in the event that a pass fails.
+   *
+   * @param errorData
+   *   Data providing insights into the reasons for the failure.
+   * @param exitCode
+   *   The exit code to be used when terminating the program.
+   * @param f
+   *   An implicit upickle writer than can convert the `errorData` into json. You can import `upickle.default._` to get
+   *   implicits for common datatypes. For an example of defining a custom writer, see
+   *   `at.forsyte.apalache.tla.bmcmt.Counterexample`.
+   */
+  def passFailure[E](errorData: E, exitCode: TExitCode)(implicit f: Writer[E]): PassResult =
+    Left(Pass.PassFailure(name, writeJs(errorData), exitCode))
 }
 
 object Pass {
-  type PassResult = Either[TExitCode, TlaModule]
+
+  import upickle.implicits.key
+
+  /**
+   * Represents a failing pass
+   *
+   * @param passName
+   *   The name of the pass which has failed.
+   * @param errorData
+   *   Data providing insights into the reasons for the failure.
+   * @param exitCode
+   *   The exit code to be used when terminating the program.
+   */
+  case class PassFailure(
+      @key("pass_name") passName: String,
+      @key("error_data") errorData: ujson.Value,
+      @key("exit_code") exitCode: TExitCode) {}
+
+  /** Implicit conversions for [[PassFailure]] */
+  object PassFailure {
+    import upickle.default.{macroRW, writeJs, ReadWriter}
+
+    implicit val upickleReadWriter: ReadWriter[PassFailure] = macroRW
+
+    implicit val ujsonView: PassFailure => ujson.Value = writeJs
+  }
+
+  type PassResult = Either[PassFailure, TlaModule]
 }

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/PassChainExecutor.scala

@@ -1,6 +1,5 @@
 package at.forsyte.apalache.infra.passes
 
-import at.forsyte.apalache.infra.ExitCodes.TExitCode
 import at.forsyte.apalache.infra.passes.Pass.PassResult
 import com.typesafe.scalalogging.LazyLogging
 import at.forsyte.apalache.tla.lir.{MissingTransformationError, TlaModule, TlaModuleProperties}
@@ -22,7 +21,7 @@ import at.forsyte.apalache.infra.AdaptedException
  */
 object PassChainExecutor extends LazyLogging {
 
-  type PassResultModule = Either[TExitCode, TlaModule with TlaModuleProperties]
+  type PassResultModule = Either[Pass.PassFailure, TlaModule with TlaModuleProperties]
 
   def run[O <: OptionGroup](toolModule: ToolModule[O]): PassResult = {
 

mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala

@@ -17,7 +17,7 @@ class TestPassChainExecutor extends AnyFunSuite {
       if (result) {
         Right(TlaModule("TestModule", Seq()))
       } else {
-        Left(ExitCodes.ERROR)
+        passFailure(None, ExitCodes.ERROR)
       }
     }
     override def dependencies = deps

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -124,8 +124,8 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     PassChainExecutor.run(new CheckerModule(options)) match {
-      case Right(_)   => Right(s"Checker reports no error up to computation length ${options.checker.length}")
-      case Left(code) => Left(code, "Checker has found an error")
+      case Right(_)      => Right(s"Checker reports no error up to computation length ${options.checker.length}")
+      case Left(failure) => Left(failure.exitCode, "Checker has found an error")
     }
   }
 

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ParseCmd.scala

@@ -36,7 +36,7 @@ class ParseCmd
 
     PassChainExecutor.run(new ParserModule(options)) match {
       case Right(m) => Right(s"Parsed successfully\nRoot module: ${m.name} with ${m.declarations.length} declarations.")
-      case Left(code) => Left(code, "Parser has failed")
+      case Left(failure) => Left(failure.exitCode, "Parser has failed")
     }
   }
 }

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala

@@ -73,8 +73,8 @@ class TestCmd
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     PassChainExecutor.run(new CheckerModule(options)) match {
-      case Right(_)   => Right("No example found")
-      case Left(code) => Left(code, "Found a violation of the postcondition. Check violation.tla.")
+      case Right(_)      => Right("No example found")
+      case Left(failure) => Left(failure.exitCode, "Found a violation of the postcondition. Check violation.tla.")
     }
 
   }

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TranspileCmd.scala

@@ -26,8 +26,8 @@ class TranspileCmd extends AbstractCheckerCmd(name = "transpile", description =
       .getOrElse(TlaExToVMTWriter.outFileName)
 
     PassChainExecutor.run(new ReTLAToVMTModule(options)) match {
-      case Right(_)   => Right(s"VMT constraints successfully generated at\n$outFilePath")
-      case Left(code) => Left(code, "Failed to generate constraints")
+      case Right(_)      => Right(s"VMT constraints successfully generated at\n$outFilePath")
+      case Left(failure) => Left(failure.exitCode, "Failed to generate constraints")
     }
   }
 }

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TypeCheckCmd.scala

@@ -40,8 +40,8 @@ class TypeCheckCmd
     logger.info("Type checking " + file)
 
     PassChainExecutor.run(new TypeCheckerModule(options)) match {
-      case Right(_)   => Right("Type checker [OK]")
-      case Left(code) => Left(code, "Type checker [FAILED]")
+      case Right(_)      => Right("Type checker [OK]")
+      case Left(failure) => Left(failure.exitCode, "Type checker [FAILED]")
     }
   }
 }

project/Dependencies.scala

@@ -35,6 +35,7 @@ object Dependencies {
     val shapeless = "com.chuusai" %% "shapeless" % "2.3.10"
     val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT"
     val ujson = "com.lihaoyi" %% "ujson" % "2.0.0"
+    val upickle = "com.lihaoyi" %% "upickle" % "2.0.0"
     val z3 = "tools.aqua" % "z3-turnkey" % "4.11.2"
     val zio = "dev.zio" %% "zio" % zioVersion
     // Keep up to sync with version in plugins.sbt

shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala

@@ -1,25 +1,20 @@
 package at.forsyte.apalache.shai.v1
 
+import scala.util.Try
+
 import com.typesafe.scalalogging.Logger
 import io.grpc.Status
-import scala.util.Failure
-import scala.util.Success
-import zio.ZIO
 import zio.ZEnv
+import zio.ZIO
 
-import at.forsyte.apalache.infra.passes.PassChainExecutor
 import at.forsyte.apalache.infra.passes.options.OptionGroup
+import at.forsyte.apalache.infra.passes.{Pass, PassChainExecutor}
 import at.forsyte.apalache.io.ConfigManager
 import at.forsyte.apalache.io.json.impl.TlaToUJson
-import at.forsyte.apalache.io.lir.TlaType1PrinterPredefs.printer // Required as implicit parameter to JsonTlaWRiter
-import at.forsyte.apalache.shai.v1.cmdExecutor.Cmd
-import at.forsyte.apalache.shai.v1.cmdExecutor.{CmdRequest, CmdResponse, ZioCmdExecutor}
+import at.forsyte.apalache.shai.v1.cmdExecutor.{Cmd, CmdRequest, CmdResponse, ZioCmdExecutor}
 import at.forsyte.apalache.tla.bmcmt.config.CheckerModule
 import at.forsyte.apalache.tla.imp.passes.ParserModule
-import at.forsyte.apalache.tla.lir.TlaModule
 import at.forsyte.apalache.tla.typecheck.passes.TypeCheckerModule
-import scala.util.Try
-import at.forsyte.apalache.infra.passes.options.Config
 
 /**
  * Provides the [[CmdExecutorService]]
@@ -43,17 +38,31 @@ class CmdExecutorService(logger: Logger) extends ZioCmdExecutor.ZCmdExecutor[ZEn
   def run(req: CmdRequest): Result[CmdResponse] = for {
     cmd <- validateCmd(req.cmd)
     resp <- executeCmd(cmd, req.config) match {
-      case Right(r)  => ZIO.succeed(CmdResponse.Result.Success(r))
-      case Left(err) => ZIO.succeed(CmdResponse.Result.Failure(err))
+      case Right(r)  => ZIO.succeed(CmdResponse.Result.Success(r.toString()))
+      case Left(err) => ZIO.succeed(CmdResponse.Result.Failure(err.toString()))
     }
   } yield CmdResponse(resp)
 
-  private def executeCmd(cmd: Cmd, cfgStr: String): Either[String, String] = {
-    // Convert a Try into an `Either` with `Left` the message from a possible `Failure`.
-    def convErr[O](v: Try[O]) = v.toEither.left.map(e => e.getMessage())
+  // Convert pass error results into the JSON representation
+  private object Converters {
+    import ujson._
+
+    def passErr(err: Pass.PassFailure): ujson.Value = {
+      Obj("error_type" -> "pass_failure", "data" -> err)
+    }
+
+    def throwableErr(err: Throwable): ujson.Value =
+      Obj("error_type" -> "unexpected",
+          "data" -> Obj("msg" -> err.getMessage(), "stack_trace" -> err.getStackTrace().map(_.toString()).toList))
+
+    def convErr[O](v: Try[O]): Either[ujson.Value, O] = v.toEither.left.map(throwableErr)
+  }
+
+  import Converters._
+  private def executeCmd(cmd: Cmd, cfgStr: String): Either[ujson.Value, ujson.Value] = {
 
     for {
-      cfg <- parseConfig(cfgStr)
+      cfg <- convErr(ConfigManager(cfgStr)).map(cfg => cfg.copy(common = cfg.common.copy(command = Some("server"))))
 
       toolModule <- {
         import OptionGroup._
@@ -67,13 +76,11 @@ class CmdExecutorService(logger: Logger) extends ZioCmdExecutor.ZCmdExecutor[ZEn
       }
 
       tlaModule <-
-        try { PassChainExecutor.run(toolModule).left.map(errCode => s"Command failed with error code: ${errCode}") }
+        try { PassChainExecutor.run(toolModule).left.map(passErr) }
         catch {
-          case e: Throwable => Left(s"Command failed with exception: ${e.getMessage()}")
+          case err: Throwable => Left(throwableErr(err))
         }
-
-      json = jsonOfModule(tlaModule)
-    } yield s"Command succeeded ${json}"
+    } yield TlaToUJson(tlaModule)
   }
 
   // Allows us to handle invalid protobuf messages on the ZIO level, before
@@ -84,15 +91,4 @@ class CmdExecutorService(logger: Logger) extends ZioCmdExecutor.ZCmdExecutor[ZEn
       ZIO.fail(Status.INVALID_ARGUMENT.withDescription(msg))
     case cmd => ZIO.succeed(cmd)
   }
-
-  private def parseConfig(data: String): Either[String, Config.ApalacheConfig] = {
-    ConfigManager(data) match {
-      case Success(cfg) => Right(cfg.copy(common = cfg.common.copy(command = Some("server"))))
-      case Failure(err) => Left(s"Invalid configuration data given to command: ${err.getMessage()}")
-    }
-  }
-
-  private def jsonOfModule(module: TlaModule): String = {
-    new TlaToUJson(None).makeRoot(Seq(module)).toString
-  }
 }

shai/src/test/scala/at/forsyte/apalache/shai/v1/TestCmdExecutorService.scala

@@ -80,27 +80,35 @@ object TestCmdExecutorService extends DefaultRunnableSpec {
           resp <- s.run(runCmd(Cmd.CHECK, checkableSpec))
         } yield assert(resp.result.isSuccess)(isTrue)
       },
-      testM("running check on spec with vioalted invariant fails") {
+      testM("running check on spec with violated invariant fails") {
         for {
           s <- ZIO.service[CmdExecutorService]
           config = Config.ApalacheConfig(checker = Config.Checker(inv = Some(List("Inv"))))
           resp <- s.run(runCmd(Cmd.CHECK, checkableSpec, cfg = config))
-          // error code 12 indicates counterexamples found
-        } yield assert(resp.result.failure.get)(containsString("Command failed with error code: 12"))
+          json = ujson.read(resp.result.failure.get)
+        } yield {
+          assert(json("error_type").str)(equalTo("pass_failure"))
+          assert(json("data")("pass_name").str)(equalTo("BoundedChecker"))
+          assert(json("data")("error_data")("checking_result").str)(equalTo("violation"))
+          assert(json("data")("error_data")("counterexamples").arr)(isNonEmpty)
+        }
       },
       testM("typechecking well-typed spec succeeds") {
         for {
           s <- ZIO.service[CmdExecutorService]
           resp <- s.run(runCmd(Cmd.TYPECHECK, trivialSpec))
-          // error code 12 indicates counterexamples found
         } yield assert(resp.result.isSuccess)(isTrue)
       },
       testM("typechecking ill-typed spec returns an error") {
         for {
           s <- ZIO.service[CmdExecutorService]
           resp <- s.run(runCmd(Cmd.TYPECHECK, illTypedSpec))
-          // error code 120 indicates a typechecking error
-        } yield assert(resp.result.failure.get)(containsString("Command failed with error code: 120"))
+          json = ujson.read(resp.result.failure.get)
+        } yield {
+          assert(json("error_type").str)(equalTo("pass_failure"))
+          assert(json("data")("pass_name").str)(equalTo("TypeCheckerSnowcat"))
+          assert(json("data")("error_data").arr)(isNonEmpty)
+        }
       },
   )
     // Create the single shared service for use in our tests, allowing us to run

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala

@@ -13,13 +13,30 @@ object Checker {
     val isOk: Boolean
   }
 
+  object CheckerResult {
+
+    import upickle.default.{writer, Writer}
+    import ujson._
+
+    implicit val ujsonView: CheckerResult => ujson.Value = {
+      case Error(nerrors, counterexamples) =>
+        Obj("checking_result" -> "Error", "counterexamples" -> counterexamples, "nerrors" -> nerrors)
+      case Deadlock(counterexample) =>
+        Obj("checking_result" -> "Deadlock", "counterexample" -> counterexample)
+      case other =>
+        Obj("checking_result" -> other.toString())
+    }
+
+    implicit val upickleWriter: Writer[CheckerResult] = writer[ujson.Value].comap(ujsonView)
+  }
+
   case class NoError() extends CheckerResult {
     override def toString: String = "NoError"
 
     override val isOk: Boolean = true
   }
 
-  case class Error(nerrors: Int) extends CheckerResult {
+  case class Error(nerrors: Int, counterexamples: Seq[Counterexample]) extends CheckerResult {
     override def toString: String = s"Error"
 
     override val isOk: Boolean = false
@@ -28,7 +45,7 @@ object Checker {
   /**
    * An execution cannot be extended. We interpret it as a deadlock.
    */
-  case class Deadlock() extends CheckerResult {
+  case class Deadlock(counterexample: Option[Counterexample]) extends CheckerResult {
     override def toString: String = "Deadlock"
 
     override val isOk: Boolean = false

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/CollectCounterexamplesModelCheckerListener.scala

@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt
 
 import at.forsyte.apalache.tla.bmcmt.trex.DecodedExecution
-import at.forsyte.apalache.tla.lir.{TlaEx, TlaModule}
+import at.forsyte.apalache.tla.lir.TlaModule
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.collection.mutable.ListBuffer
@@ -12,18 +12,16 @@ import scala.collection.mutable.ListBuffer
 class CollectCounterexamplesModelCheckerListener extends ModelCheckerListener with LazyLogging {
 
   override def onCounterexample(
-      rootModule: TlaModule,
-      trace: DecodedExecution,
-      invViolated: TlaEx,
+      counterexample: Counterexample,
       errorIndex: Int): Unit = {
-    _counterExamples += trace
+    _counterExamples += counterexample
   }
 
   override def onExample(rootModule: TlaModule, trace: DecodedExecution, exampleIndex: Int): Unit = {
     // ignore the examples
   }
 
-  private val _counterExamples = ListBuffer.empty[DecodedExecution]
+  private val _counterExamples = ListBuffer.empty[Counterexample]
 
-  def counterExamples: Seq[DecodedExecution] = _counterExamples.toSeq
+  def counterExamples: Seq[Counterexample] = _counterExamples.toSeq
 }