Merge pull request #1648 from informalsystems/ik/features1647

Add the option `--features`
apalache-mc · Apr 26, 2022 · 2ef78c2 · 2ef78c2
2 parents b96c73a + 20c8b55
commit 2ef78c2
Show file tree

Hide file tree

Showing 6 changed files with 170 additions and 50 deletions.
diff --git a/UNRELEASED.md b/UNRELEASED.md
@@ -10,7 +10,10 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Features
+
+* Add the option `--features` to enable experimental features, see #1648
 
 ### Bug fixes
 
- * Not failing when assignment and `UNCHANGED` appear in invariants, see #1664
+* Not failing when assignment and `UNCHANGED` appear in invariants, see #1664
diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
@@ -28,7 +28,6 @@ import util.ExecutionStatisticsCollector.Selection
 
 import scala.collection.JavaConverters._
 import scala.util.Random
-import at.forsyte.apalache.io.ApalacheConfig
 import at.forsyte.apalache.io.ConfigManager
 import at.forsyte.apalache.tla.bmcmt.rules.vmt.TlaExToVMTWriter
 
@@ -53,20 +52,23 @@ object Tool extends LazyLogging {
     System.exit(run(args))
   }
 
-  private def outputAndLogConfig(cmd: General, cfg: ApalacheConfig): Unit = {
-    OutputManager.configure(cfg)
-    // We currently use dummy files for some commands, so we skip here on non-existing files
-    if (cmd.file.getName.endsWith(".tla") && cmd.file.exists()) {
-      OutputManager.initSourceLines(cmd.file)
+  // Returns `Left(errmsg)` in case of configuration errors
+  private def outputAndLogConfig(cmd: General): Either[String, Unit] = {
+    ConfigManager(cmd).map { cfg =>
+      OutputManager.configure(cfg)
+      // We currently use dummy files for some commands, so we skip here on non-existing files
+      if (cmd.file.getName.endsWith(".tla") && cmd.file.exists()) {
+        OutputManager.initSourceLines(cmd.file)
+      }
+      println(s"Output directory: ${OutputManager.runDir.normalize()}")
+      OutputManager.withWriterInRunDir(OutputManager.Names.RunFile)(
+          _.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
+      )
+      // force our programmatic logback configuration, as the autoconfiguration works unpredictably
+      new LogbackConfigurator(OutputManager.runDirPathOpt, OutputManager.customRunDirPathOpt).configureDefaultContext()
+      // TODO: update workers when the multicore branch is integrated
+      submitStatisticsIfEnabled(Map("tool" -> "apalache", "mode" -> cmd.label, "workers" -> "1"))
     }
-    println(s"Output directory: ${OutputManager.runDir.normalize()}")
-    OutputManager.withWriterInRunDir(OutputManager.Names.RunFile)(
-        _.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
-    )
-    // force our programmatic logback configuration, as the autoconfiguration works unpredictably
-    new LogbackConfigurator(OutputManager.runDirPathOpt, OutputManager.customRunDirPathOpt).configureDefaultContext()
-    // TODO: update workers when the multicore branch is integrated
-    submitStatisticsIfEnabled(Map("tool" -> "apalache", "mode" -> cmd.label, "workers" -> "1"))
   }
 
   /**
@@ -96,42 +98,46 @@ object Tool extends LazyLogging {
     cli match {
       // A standard option, e.g., --version or --help. No header, no timer, no noise
       case None => OK_EXIT_CODE
+      // One of our commands.
       case Some(cmd) => {
 
         printHeaderAndStatsConfig()
 
-        // One of our commands. Print the header and measure time
-        val startTime = LocalDateTime.now()
-
-        outputAndLogConfig(cmd, ConfigManager(cmd))
-
-        val exitcode =
-          try {
-            cmd match {
-              case parse: ParseCmd =>
-                runForModule(runParse, new ParserModule, parse)
+        val exitcode = outputAndLogConfig(cmd) match {
+          case Left(configurationErrorMessage) => {
+            logger.error(s"Configuration error: ${configurationErrorMessage}")
+            ExitCodes.ERROR
+          }
+          case Right(()) => {
+            val startTime = LocalDateTime.now()
+            try {
+              cmd match {
+                case parse: ParseCmd =>
+                  runForModule(runParse, new ParserModule, parse)
 
-              case check: CheckCmd =>
-                runForModule(runCheck, new CheckerModule, check)
+                case check: CheckCmd =>
+                  runForModule(runCheck, new CheckerModule, check)
 
-              case test: TestCmd =>
-                runForModule(runTest, new CheckerModule, test)
+                case test: TestCmd =>
+                  runForModule(runTest, new CheckerModule, test)
 
-              case typecheck: TypeCheckCmd =>
-                runForModule(runTypeCheck, new TypeCheckerModule, typecheck)
+                case typecheck: TypeCheckCmd =>
+                  runForModule(runTypeCheck, new TypeCheckerModule, typecheck)
 
-              case server: ServerCmd =>
-                runForModule(runServer, new CheckerModule, server)
+                case server: ServerCmd =>
+                  runForModule(runServer, new CheckerModule, server)
 
-              case constrain: TranspileCmd =>
-                runForModule(runConstrain, new ReTLAToVMTModule, constrain)
+                case constrain: TranspileCmd =>
+                  runForModule(runConstrain, new ReTLAToVMTModule, constrain)
 
-              case config: ConfigCmd =>
-                configure(config)
+                case config: ConfigCmd =>
+                  configure(config)
+              }
+            } finally {
+              printTimeDiff(startTime)
             }
-          } finally {
-            printTimeDiff(startTime)
           }
+        }
 
         if (exitcode == OK_EXIT_CODE) {
           Console.out.println("EXITCODE: OK")
@@ -157,6 +163,8 @@ object Tool extends LazyLogging {
   private def setCommonOptions(cli: General, options: WriteablePassOptions): Unit = {
     options.set("general.debug", cli.debug)
     options.set("smt.prof", cli.smtprof)
+    options.set("general.features", cli.features)
+
     // TODO: Remove pass option, and just rely on OutputManager config
     options.set("io.outdir", OutputManager.outDir)
   }

diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala
@@ -1,9 +1,11 @@
 package at.forsyte.apalache.tla.tooling.opt
 
 import at.forsyte.apalache.io.CliConfig
+import at.forsyte.apalache.tla.lir.Feature
 
 import java.io.File
 import org.backuity.clist._
+import org.backuity.clist.util.Read
 
 /**
  * The general commands.
@@ -32,10 +34,31 @@ trait General extends Command with CliConfig {
   var writeIntermediate = opt[Option[Boolean]](description =
         "write intermediate output files to `out-dir`, default: false (overrides envvar WRITE_INTERMEDIATE)",
       useEnv = true)
+  var features = opt[Seq[Feature]](default = Seq(),
+      description = {
+        val featureDescriptions = Feature.all.map(f => s"  ${f.name}: ${f.description}")
+        ("a comma-separated list of experimental features:" :: featureDescriptions).mkString("\n")
+      })
 
   private var _invocation = ""
   private var _env = ""
 
+  // A comma separated name of supported features
+  private val featureList = Feature.all.map(_.name).mkString(", ")
+
+  // Parse a feature
+  implicit def featureRead: Read[Feature] = {
+    Read.reads[Feature](s"a feature: ${featureList}") { str =>
+      Feature.fromString(str).getOrElse(throw new IllegalArgumentException(s"Unexpected feature: ${str}"))
+    }
+  }
+
+  implicit def featureSeqRead: Read[Seq[Feature]] = {
+    Read.reads[Seq[Feature]](expecting = s"a comma-separated list of features: ${featureList}") { str =>
+      str.split(",").map(featureRead.reads)
+    }
+  }
+
   private def getOptionEnvVar(option: CliOption[_]): Option[String] = {
     val envVar = option.name.replace("-", "_").toUpperCase()
     sys.env.get(envVar).map(value => s"${envVar}=${value}")

diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -181,6 +181,29 @@ EXITCODE: ERROR (255)
 
 This command parses a TLA+ specification with the SANY parser.
 
+### parse Empty succeeds
+
+```sh
+$ apalache-mc parse Empty.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
+### parse Empty with --features=rows succeeds
+
+```sh
+$ apalache-mc parse --features=rows Empty.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
+### parse Empty with an unsupported feature fails
+
+```sh
+$ apalache-mc parse --features=feature.unsupported Empty.tla 2>&1 | grep 'Failed to parse'
+Failed to parse command parse: Incorrect value for option features, got 'feature.unsupported', expected a feature: rows
+```
+
 ### parse LocalDefClash576 succeeds
 
 ```sh
@@ -2108,6 +2131,22 @@ EXITCODE: OK
 
 ## running the typecheck command
 
+### typecheck Empty.tla reports no error
+
+```sh
+$ apalache-mc typecheck Empty.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
+### typecheck Empty.tla reports no error when rows enabled
+
+```sh
+$ apalache-mc typecheck --features=rows Empty.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
 ### typecheck ExistTuple476.tla reports no error: regression for issues 476 and 482
 
 ```sh
@@ -2869,6 +2908,17 @@ $ test -d ./run-dir
 $ rm -rf ./run-dir ./.apalache.cfg
 ```
 
+### configuration management: invalid features are rejected with error
+
+```sh
+$ echo "features: [ invalid-feature ]" > .apalache.cfg
+$ apalache-mc check --length=0 Counter.tla | grep -o -e "Configuration error: at 'features.0'" -e "Cannot convert 'invalid-feature' to at.forsyte.apalache.tla.lir.Feature"
+...
+Configuration error: at 'features.0'
+Cannot convert 'invalid-feature' to at.forsyte.apalache.tla.lir.Feature
+$ rm -rf ./.apalache.cfg
+```
+
 ## module lookup
 
 ### module lookup: looks up dummy module from standard library

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala
@@ -4,6 +4,7 @@ import pureconfig._
 import pureconfig.generic.auto._
 import java.io.File
 import java.nio.file.{Files, Path, Paths}
+import at.forsyte.apalache.tla.lir.Feature
 
 // Provides implicit conversions used when deserializing into configurable values.
 private object Converters {
@@ -13,15 +14,21 @@ private object Converters {
     Paths.get(if (s.startsWith("~")) s.replaceFirst("~", System.getProperty("user.home")) else s)
   }
 
-  // Briniging these implicits in scope lets us override the existing File and
+  // Bringing these implicits in scope lets us override the existing File and
   // Path deserialization behavior, so we get path expansion in all configured
   // paths.
   // See https://pureconfig.github.io/docs/overriding-behavior-for-types.html
   implicit val overridePathReader = ConfigReader.fromString[Path](catchReadError(expandedFilePath))
   implicit val overrideFileReader = ConfigReader.fromString[File](catchReadError(expandedFilePath(_).toFile()))
+  // PureConfig's optF will convert None values to appropriate configuration errors
+  implicit val featureReader = ConfigReader.fromString[Feature](optF(Feature.fromString))
 }
 
-/** The configuration values that can be overriden based on CLI arguments */
+/**
+ * The configuration values that can be overriden based on CLI arguments
+ *
+ * For documentation on the use and meaning of these fields, see [[at.forsyte.apalache.tla.tooling.opt.General]].
+ */
 trait CliConfig {
 
   /** Input file */
@@ -31,6 +38,7 @@ trait CliConfig {
   def writeIntermediate: Option[Boolean]
   def profiling: Option[Boolean]
   def configFile: Option[File]
+  def features: Seq[Feature]
 }
 
 /** The application's configurable values, along with their base defaults */
@@ -40,7 +48,8 @@ case class ApalacheConfig(
     runDir: Option[File] = None,
     configFile: Option[File] = None,
     writeIntermediate: Boolean = false,
-    profiling: Boolean = false)
+    profiling: Boolean = false,
+    features: Seq[Feature] = Seq())
 
 case class ConfigManager(cmd: CliConfig) {
   private val TLA_PLUS_DIR = ".tlaplus"
@@ -76,7 +85,7 @@ case class ConfigManager(cmd: CliConfig) {
     val home = System.getProperty("user.home")
     val globalConfig = ConfigSource.file(Paths.get(home, TLA_PLUS_DIR, APALACHE_CFG))
 
-    localConfig
+    localConfig()
       .getOrElse(ConfigSource.empty)
       // `withFallback` supplies configuration sources that only apply if the preceding configs aren't set
       .withFallback(globalConfig.optional)
@@ -90,17 +99,14 @@ case class ConfigManager(cmd: CliConfig) {
             configFile = cmd.configFile.orElse(cfg.configFile),
             writeIntermediate = cmd.writeIntermediate.getOrElse(cfg.writeIntermediate),
             profiling = cmd.profiling.getOrElse(cfg.profiling),
+            features = if (cmd.features.nonEmpty) cmd.features else cfg.features,
         ))
   }
 }
 
 object ConfigManager {
 
-  /** Load the application configuration, or raise a configuration error */
-  def apply(cmd: CliConfig): ApalacheConfig = {
-    new ConfigManager(cmd).load() match {
-      case Left(err)  => throw new ConfigurationError(err.toString())
-      case Right(cfg) => cfg
-    }
-  }
+  /** Load the application configuration, converting any configuration error into a pretty printed message */
+  def apply(cmd: CliConfig): Either[String, ApalacheConfig] =
+    new ConfigManager(cmd).load().left.map(_.prettyPrint())
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
@@ -0,0 +1,30 @@
+package at.forsyte.apalache.tla.lir
+
+/**
+ * An experimental feature.
+ */
+sealed trait Feature {
+  val name: String
+  val description: String
+}
+
+/**
+ * Enable rows, new records, and variants, as described in <a
+ * href="https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md">ADR-014</a>.
+ */
+case class RowsFeature(
+    name: String = "rows",
+    description: String = "enable row typing as explained in ADR-014")
+    extends Feature
+
+object Feature {
+
+  /**
+   * A list of all supported features.
+   *
+   * This provides the source of truth for all valid feature names and descriptions.
+   */
+  val all = List(RowsFeature())
+
+  val fromString: String => Option[Feature] = str => all.find(_.name == str)
+}