Merge pull request #1749 from informalsystems/th/typecheck-exitcode

Introduce dedicated exit codes

UNRELEASED.md

@@ -10,3 +10,12 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Breaking changes
+
+ * Introduce dedicated exit codes for type-checking errors, parser errors, and
+   evaluation errors (e.g., due to unsupported language constructs or
+   operators), see #1749
+
+### Features
+
+ * Support sound records (over rows) in the model checker, see #1717

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

@@ -0,0 +1,62 @@
+package at.forsyte.apalache.infra
+
+import tlc2.output.EC
+
+/**
+ * Exit codes that are reported by `Tool`.
+ *
+ * We maintain compatibility with TLC on a small subset of its exit codes, believing that exit codes should not replace
+ * richer error explanations.
+ *
+ * TLC currently specifies exit codes
+ *   - 0 for success,
+ *   - 10–14 for (various kinds of) property violations,
+ *   - 75–77 for "failures" (e.g., properties that are tautologies, or primed variables in invariants), and
+ *   - 150–153 and 255 for syntax errors and system-level errors, respectively.
+ *
+ * Apalache uses exit codes
+ *   - 0 for success,
+ *   - 12 for all kinds of property violations,
+ *   - 75 for semantic failures to evaluate a specification,
+ *   - 120 for type-checking errors,
+ *   - 150 for syntactic errors, and
+ *   - 255 for general system-level errors.
+ *
+ * @author
+ *   Igor Konnov, Thomas Pani
+ */
+object ExitCodes {
+  type TExitCode = Int
+
+  /**
+   * No error in the specification.
+   */
+  val OK: TExitCode = EC.ExitStatus.SUCCESS // = 0
+
+  /**
+   * The model checker has found a counterexample. We do not distinguish between different kinds of counterexamples and
+   * always report VIOLATION_SAFETY.
+   */
+  val ERROR_COUNTEREXAMPLE: TExitCode = EC.ExitStatus.VIOLATION_SAFETY // = 12
+
+  /**
+   * Semantic failure to evaluate a specification, e.g. due to unsupported language constructs and operators, or those
+   * that introduce infinite structures.
+   */
+  val FAILURE_SPEC_EVAL: TExitCode = EC.ExitStatus.FAILURE_SPEC_EVAL // = 75
+
+  /**
+   * Type-checking error.
+   */
+  val ERROR_TYPECHECK: TExitCode = 120
+
+  /**
+   * Syntactic error when parsing the spec.
+   */
+  val ERROR_SPEC_PARSE: TExitCode = EC.ExitStatus.ERROR_SPEC_PARSE // = 150
+
+  /**
+   * All other kinds of errors, e.g., runtime errors.
+   */
+  val ERROR: TExitCode = EC.ExitStatus.ERROR // 255
+}

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

@@ -1,5 +1,7 @@
 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}
 
 /**
@@ -46,7 +48,7 @@ trait Pass {
    * @return
    *   the transformed module, if the pass was successful
    */
-  def execute(module: TlaModule): Option[TlaModule]
+  def execute(module: TlaModule): PassResult
 
   /**
    * List the dependencies of the pass. These are properties the module has to have in order to be processed by the
@@ -68,3 +70,7 @@ trait Pass {
   def transformations: Set[ModuleProperty.Value]
 
 }
+
+object Pass {
+  type PassResult = Either[TExitCode, TlaModule]
+}

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

@@ -1,5 +1,7 @@
 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}
 
@@ -15,12 +17,11 @@ import at.forsyte.apalache.tla.lir.{MissingTransformationError, TlaModule, TlaMo
  */
 
 class PassChainExecutor(val options: WriteablePassOptions, passes: Seq[Pass]) extends LazyLogging {
-
-  def run(): Option[TlaModule] = {
-    def exec(seqNo: Int, passToRun: Pass, module: TlaModule): Option[TlaModule] = {
+  def run(): PassResult = {
+    def exec(seqNo: Int, passToRun: Pass, module: TlaModule): PassResult = {
       logger.info("PASS #%d: %s".format(seqNo, passToRun.name))
       val result = passToRun.execute(module)
-      val outcome = if (result.isDefined) "[OK]" else "[FAIL]"
+      val outcome = result.fold(_ => "[FAIL]", _ => "[OK]")
       // TODO: As part of #858, PassWithOutputs.writeOut should be called here.
       logger.debug("PASS #%d: %s %s".format(seqNo, passToRun.name, outcome))
       result
@@ -34,21 +35,21 @@ class PassChainExecutor(val options: WriteablePassOptions, passes: Seq[Pass]) ex
       }
     }
 
-    passes.zipWithIndex
-      .foldLeft(Option[TlaModule with TlaModuleProperties](new TlaModule("empty", Seq()) with TlaModuleProperties)) {
-        case (moduleOpt, (pass, index)) =>
-          // Raise error if the pass dependencies aren't satisfied
-          moduleOpt.map { m => checkDependencies(m, pass) }
+    val emptyModuleWithProperties: TlaModule with TlaModuleProperties = new TlaModule("empty", Seq())
+      with TlaModuleProperties
+    val startValue: Either[TExitCode, TlaModule with TlaModuleProperties] = Right(emptyModuleWithProperties)
+    passes.zipWithIndex.foldLeft(startValue) { case (moduleOpt, (pass, index)) =>
+      // Raise error if the pass dependencies aren't satisfied
+      moduleOpt.map { m => checkDependencies(m, pass) }
 
-          for {
-            module <- moduleOpt
-            transformedModule <- exec(index, pass, module)
-          } yield {
-            val newModule = new TlaModule(transformedModule.name, transformedModule.declarations)
-              with TlaModuleProperties
-            newModule.properties = module.properties ++ pass.transformations
-            newModule
-          }
+      for {
+        module <- moduleOpt
+        transformedModule <- exec(index, pass, module)
+      } yield {
+        val newModule = new TlaModule(transformedModule.name, transformedModule.declarations) with TlaModuleProperties
+        newModule.properties = module.properties ++ pass.transformations
+        newModule
       }
+    }
   }
 }

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

@@ -1,5 +1,7 @@
 package at.forsyte.apalache.infra.passes
 
+import at.forsyte.apalache.infra.ExitCodes
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import org.junit.runner.RunWith
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatestplus.junit.JUnitRunner
@@ -11,11 +13,11 @@ class TestPassChainExecutor extends AnyFunSuite {
   class ParametrizedPass(result: Boolean, deps: Set[ModuleProperty.Value], transfs: Set[ModuleProperty.Value])
       extends Pass {
     override def name = "TestPass"
-    override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+    override def execute(tlaModule: TlaModule): PassResult = {
       if (result) {
-        Some(new TlaModule("TestModule", Seq()))
+        Right(TlaModule("TestModule", Seq()))
       } else {
-        None
+        Left(ExitCodes.ERROR)
       }
     }
     override def dependencies = deps
@@ -30,7 +32,7 @@ class TestPassChainExecutor extends AnyFunSuite {
 
     val executor = new PassChainExecutor(options, Seq(pass1, pass2))
     val result = executor.run()
-    assert(result.isDefined)
+    assert(result.isRight)
   }
 
   test("""Throws error on a bad ordered chain""") {
@@ -54,6 +56,6 @@ class TestPassChainExecutor extends AnyFunSuite {
     val executor = new PassChainExecutor(options, Seq(pass1, pass2))
 
     val result = executor.run()
-    assert(result.isEmpty)
+    assert(result.isLeft)
   }
 }

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -2,15 +2,14 @@ package at.forsyte.apalache.tla
 
 // Generated from the build.sbt file by the buildInfo plugin
 import apalache.BuildInfo
+import at.forsyte.apalache.infra._
 import at.forsyte.apalache.infra.log.LogbackConfigurator
 import at.forsyte.apalache.infra.passes.{PassChainExecutor, ToolModule, WriteablePassOptions}
-import at.forsyte.apalache.infra.{ExceptionAdapter, FailureMessage, NormalErrorMessage, PassOptionException}
 import at.forsyte.apalache.io.{ConfigManager, ConfigurationError, OutputManager, ReportGenerator}
 import at.forsyte.apalache.tla.bmcmt.config.{CheckerModule, ReTLAToVMTModule}
 import at.forsyte.apalache.tla.bmcmt.rules.vmt.TlaExToVMTWriter
 import at.forsyte.apalache.tla.imp.passes.ParserModule
 import at.forsyte.apalache.tla.lir.TlaModule
-import at.forsyte.apalache.tla.tooling.ExitCodes
 import at.forsyte.apalache.tla.tooling.opt._
 import at.forsyte.apalache.tla.typecheck.passes.TypeCheckerModule
 import com.google.inject.{Guice, Injector}
@@ -37,8 +36,8 @@ object Tool extends LazyLogging {
   lazy val ISSUES_LINK: String = "[https://github.com/informalsystems/apalache/issues]"
 
   /**
-   * Run the tool in the standalone mode with the provided arguments. This method calls System.exit with the computed
-   * exit code. If you like to call the tool without System.exit, use the the Tool#run.
+   * Run the tool in the standalone mode with the provided arguments. This method calls [[System.exit]] with the
+   * computed exit code. To call the tool without System.exit, use [[run]].
    *
    * @param args
    *   the command line arguments
@@ -184,15 +183,15 @@ object Tool extends LazyLogging {
   private def runAndExit(
       executor: PassChainExecutor,
       msgIfOk: TlaModule => String,
-      msgIfFail: String,
-      errCode: Int = ExitCodes.ERROR): Int = {
+      msgIfFail: String): ExitCodes.TExitCode = {
     val result = executor.run()
-    if (result.isDefined) {
-      logger.info(msgIfOk(result.get))
-      ExitCodes.OK
-    } else {
-      logger.info(msgIfFail)
-      errCode
+    result match {
+      case Left(errorCode) =>
+        logger.info(msgIfFail)
+        errorCode
+      case Right(module) =>
+        logger.info(msgIfOk(module))
+        ExitCodes.OK
     }
   }
 
@@ -265,7 +264,6 @@ object Tool extends LazyLogging {
         executor,
         _ => "Checker reports no error up to computation length " + check.length,
         "Checker has found an error",
-        ExitCodes.ERROR_COUNTEREXAMPLE,
     )
   }
 
@@ -308,7 +306,6 @@ object Tool extends LazyLogging {
         executor,
         _ => "No example found",
         "Checker has found an example. Check counterexample.tla.",
-        ExitCodes.ERROR_COUNTEREXAMPLE,
     )
   }