Expose output configuration via CLI arguments

- Followup to #1025 - Required for #1059 This plumbs configuration of the OutputManager's settings for the out-dir and write-intermediate fields through to the CLI. This is needed for us to control the location and kind of output for the benchmark tests, and was planned in #1025
apalache-mc · Oct 26, 2021 · 0076cf0 · 0076cf0
1 parent 4ff18e1
commit 0076cf0
Show file tree

Hide file tree

Showing 4 changed files with 172 additions and 55 deletions.
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
@@ -23,6 +23,7 @@ import util.ExecutionStatisticsCollector.Selection
 
 import scala.collection.JavaConverters._
 import scala.util.Random
+import at.forsyte.apalache.infra.passes.WriteablePassOptions
 
 /**
  * Command line access to the APALACHE tools.
@@ -51,21 +52,19 @@ object Tool extends LazyLogging {
     System.exit(exitcode)
   }
 
-  def mkRunFile(cmd: General): Unit = OutputManager.runDirPathOpt.foreach { runDir =>
-    println(s"Output directory: ${runDir.toFile}")
-    val outFile = new File(runDir.toFile, OutputManager.Names.RunFile)
-    val writer = new PrintWriter(new FileWriter(outFile, false))
-    try {
-      writer.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
-    } finally {
-      writer.close()
-    }
-  }
-
   private def outputAndLogConfig(runDirNamePrefix: String, cmd: General): Unit = {
-    OutputManager.syncFromGlobalConfig()
+    OutputManager.configure(cmd)
     OutputManager.createRunDirectory(runDirNamePrefix)
-    mkRunFile(cmd)
+    OutputManager.runDirPathOpt.foreach{ runDir =>
+      println(s"Output directory: ${runDir.toFile}")
+      val outFile = new File(runDir.toFile, OutputManager.Names.RunFile)
+      val writer = new PrintWriter(new FileWriter(outFile, false))
+      try {
+        writer.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
+      } finally {
+        writer.close()
+      }
+    }
     // force our programmatic logback configuration, as the autoconfiguration works unpredictably
     new LogbackConfigurator(OutputManager.runDirPathOpt).configureDefaultContext()
     // TODO: update workers when the multicore branch is integrated
@@ -137,6 +136,13 @@ object Tool extends LazyLogging {
           .format(ChronoUnit.SECONDS.between(startTime, endTime), ChronoUnit.MILLIS.between(startTime, endTime) % 1000))
   }
 
+  // Set the pass options from the cli configs shared between all commands
+  private def setCommonOptions(cli: General, options: WriteablePassOptions): Unit = {
+    options.set("general.debug", cli.debug)
+    options.set("smt.prof", cli.smtprof)
+    OutputManager.syncWithOptions(options)
+  }
+
   private def runParse(injector: => Injector, parse: ParseCmd): Int = {
     // here, we implement a terminal pass to get the parse results
     val executor = injector.getInstance(classOf[PassChainExecutor])
@@ -148,7 +154,10 @@ object Tool extends LazyLogging {
     executor.options.set("parser.filename", parse.file.getAbsolutePath)
     executor.options.set("parser.output", parse.output)
 
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(parse, executor.options)
+
     val result = executor.run()
     if (result.isDefined) {
       logger.info("Parsed successfully")
@@ -175,8 +184,6 @@ object Tool extends LazyLogging {
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     executor.options.set("general.tuning", tuning)
-    executor.options.set("general.debug", check.debug)
-    executor.options.set("smt.prof", check.smtprof)
     executor.options.set("parser.filename", check.file.getAbsolutePath)
     if (check.config != "")
       executor.options.set("checker.config", check.config)
@@ -199,7 +206,9 @@ object Tool extends LazyLogging {
       executor.options.set("checker.view", check.view)
     // for now, enable polymorphic types. We probably want to disable this option for the type checker
     executor.options.set("typechecker.inferPoly", true)
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(check, executor.options)
 
     val result = executor.run()
     if (result.isDefined) {
@@ -228,8 +237,6 @@ object Tool extends LazyLogging {
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     executor.options.set("general.tuning", tuning)
-    executor.options.set("general.debug", test.debug)
-    executor.options.set("smt.prof", test.smtprof)
     executor.options.set("parser.filename", test.file.getAbsolutePath)
     executor.options.set("checker.init", test.before)
     executor.options.set("checker.next", test.action)
@@ -247,7 +254,9 @@ object Tool extends LazyLogging {
     executor.options.set("checker.algo", "offline")
     // for now, enable polymorphic types. We probably want to disable this option for the type checker
     executor.options.set("typechecker.inferPoly", true)
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(test, executor.options)
 
     val result = executor.run()
     if (result.isDefined) {
@@ -269,7 +278,10 @@ object Tool extends LazyLogging {
     executor.options.set("parser.filename", typecheck.file.getAbsolutePath)
     executor.options.set("typechecker.inferPoly", typecheck.inferPoly)
 
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(typecheck, executor.options)
+
     executor.run() match {
       case None =>
         logger.info("Type checker [FAILED]")
@@ -322,11 +334,6 @@ object Tool extends LazyLogging {
     props ++ hereProps
   }
 
-  private def createOutputDir(options: PassOptions): Path = {
-    OutputManager.syncFromOptions(options)
-    OutputManager.runDirPathOpt.get
-  }
-
   private def injectorFactory(cmd: Command): Injector = {
     cmd match {
       case _: ParseCmd     => Guice.createInjector(new ParserModule)

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,6 +1,11 @@
 package at.forsyte.apalache.tla.tooling.opt
 
+import at.forsyte.apalache.io.{OutputManagerConfig, OutputManager}
+
+
+import java.io.File
 import org.backuity.clist._
+import at.forsyte.apalache.io.OutputManager
 
 /**
  * The general commands.
@@ -9,9 +14,11 @@ import org.backuity.clist._
  *
  * @author Igor Konnov
  */
-trait General extends Command {
+trait General extends Command with OutputManagerConfig {
   var debug = opt[Boolean](description = "extensive logging in detailed.log and log.smt, default: false")
   var smtprof = opt[Boolean](description = "profile SMT constraints in log.smt, default: false")
+  var outDir = opt[Option[File]](name = OutputManager.Names.OutdirNameInCfg, description = "where output files will be written, default: ./_apalache-out", useEnv = true)
+  var writeIntermediate = opt[Option[Boolean]](name = OutputManager.Names.IntermediateFlag, description = "write intermediate output files to `out-dir`, default: false", useEnv = true)
 
   private var _invocation = ""
   private var _env = ""

diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -1992,3 +1992,75 @@ Statistics collection is ON.
 ...
 EXITCODE: OK
 ```
+
+## configuring the output manager
+
+### set the output directory by CLI flag
+
+```sh
+$ apalache-mc check --out-dir=./test-out-dir Counter.tla > /dev/null && find ./test-out-dir -type f -exec basename {} \;
+detailed.log
+log0.smt
+run.txt
+$ rm -rf ./test-out-dir
+```
+
+### set the output directory by envvar
+
+```sh
+$ OUT_DIR=./test-out-dir apalache-mc check Counter.tla > /dev/null && find ./test-out-dir -type f -exec basename {} \;
+detailed.log
+log0.smt
+run.txt
+$ rm -rf ./test-out-dir
+```
+
+### the output directory CLI flag overrides the envvar
+
+```sh
+$ OUT_DIR=./not-here apalache-mc check --out-dir=./test-out-dir Counter.tla > /dev/null && find ./test-out-dir -type f -exec basename {} \;
+detailed.log
+log0.smt
+run.txt
+$ rm -rf ./test-out-dir
+```
+
+### write intermediate files
+
+```sh
+$ apalache-mc check --out-dir=./test-out-dir --write-intermediate=true Counter.tla > /dev/null && find ./test-out-dir -type f -exec basename {} \;
+detailed.log
+log0.smt
+11_OutAnalysis.json
+10_OutOpt.tla
+00_OutParser.tla
+03_OutDesugarer.json
+01_OutTypeCheckerSnowcat.json
+12_out-pre-PostTypeCheckerSnowcat.json
+03_OutDesugarer.tla
+12_OutPostTypeCheckerSnowcat.json
+04_OutUnroll.tla
+12_OutPostTypeCheckerSnowcat.tla
+07_OutVCGen.tla
+05_OutInline.tla
+07_OutVCGen.json
+09_OutTransition.tla
+12_out-post-PostTypeCheckerSnowcat.json
+02_OutConfig.json
+06_OutPriming.tla
+01_out-pre-TypeCheckerSnowcat.json
+08_OutPrepro.tla
+10_OutOpt.json
+11_OutAnalysis.tla
+04_OutUnroll.json
+09_OutTransition.json
+00_OutParser.json
+01_out-post-TypeCheckerSnowcat.json
+02_OutConfig.tla
+08_OutPrepro.json
+01_OutTypeCheckerSnowcat.tla
+05_OutInline.json
+06_OutPriming.json
+run.txt
+$ rm -rf ./test-out-dir
+```
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
@@ -1,13 +1,19 @@
 package at.forsyte.apalache.io
 
-import at.forsyte.apalache.infra.passes.PassOptions
+import at.forsyte.apalache.infra.passes.WriteablePassOptions
 
 import java.io.{File, FileInputStream}
 import java.nio.file.{Files, Path, Paths}
 import java.time.LocalDateTime
 import java.time.format.DateTimeFormatter
 import org.yaml.snakeyaml.Yaml
 
+trait OutputManagerConfig {
+  // TODO def debug : Boolean
+  def outDir : Option[File]
+  def writeIntermediate : Option[Boolean]
+}
+
 /**
  * The OutputManager is the central source of truth, for all IO related locations.
  * Any IO operation should request read/write target paths from this object.
@@ -24,8 +30,9 @@ object OutputManager {
     val RunFile = "run.txt"
   }
   import Names._
-  // Absolute path
-  private var outputDirPath: String = ""
+
+  // outDirOpt is stored as an expanded and absolute path
+  private var outDirOpt: Option[Path] = None
   private var runDirOpt: Option[Path] = None
   private var flags: Map[String, Boolean] =
     Map(
@@ -34,11 +41,33 @@ object OutputManager {
     )
 
   /** If this is FALSE, outputs (of any sort) cannot happen, so the tool should exit */
-  def isConfigured: Boolean = new File(outputDirPath).isDirectory
+  def isConfigured: Boolean = outDirOpt.nonEmpty
 
   /** Accessor, read-only */
   def runDirPathOpt: Option[Path] = runDirOpt
 
+  /** Accessor for the configured run directory.
+   *
+   * @throws IllegalStateException if called before OutputManager is configured this is considered an implementator error */
+  def outDir : Path = {
+    outDirOpt.getOrElse(throw new IllegalStateException("out-dir is not configured"))
+  }
+
+  private def setOutDir(f: File): Unit = {
+    if (!f.exists() && !f.mkdirs()) {
+      throw new ConfigurationError(s"Could not find or create directory: ${f.getCanonicalPath}.")
+    } else if (!f.isDirectory()) {
+      throw new ConfigurationError(s"Configured out-dir is not a directory: ${f.getCanonicalPath}.")
+    } else {
+      outDirOpt = Some(f.toPath().toAbsolutePath())
+    }
+  }
+
+  private def expandedFilePath(s: String): File = {
+    val home = System.getProperty("user.home")
+    new File(if (s.startsWith("~")) s.replaceFirst("~", home) else s)
+  }
+
   /** Loads the Apalache configuration file from HOME/.tlaplus */
   def syncFromGlobalConfig(): Unit = {
     val home = System.getProperty("user.home")
@@ -48,23 +77,10 @@ object OutputManager {
       val configYaml: java.util.Map[String, Any] = yaml.load(new FileInputStream(configFile.getCanonicalPath))
 
       configYaml.forEach { case (flagName, flagValue) =>
+        // `OutdirNameInCfg` is a special flag that governs the output directory
         if (flagName == OutdirNameInCfg) {
           flagValue match {
-            case flagValAsString: String =>
-              // `OutdirNameInCfg` is a special flag that governs the output directory
-              val replacedHome =
-                if (flagValAsString.startsWith("~")) flagValAsString.replaceFirst("~", home)
-                else flagValAsString
-              val outdir = new File(replacedHome)
-              // Try to make the dir, if it fails we skip and go to the default
-              if (!outdir.exists()) {
-                outdir.mkdir()
-              }
-              if (!outdir.exists()) {
-                throw new ConfigurationError(s"Could not find or create directory: ${outdir.getCanonicalPath}.")
-              } else {
-                outputDirPath = outdir.getCanonicalPath
-              }
+            case path: String => setOutDir(expandedFilePath(path))
             case _ =>
               throw new ConfigurationError(
                   s"Flag [$flagName] in [${configFile.getAbsolutePath}] must be a directory path string.")
@@ -86,20 +102,39 @@ object OutputManager {
       }
     }
     // If `OutdirNameInCfg` is not specified, default to making rundir = <CWD>/_apalache-out/
-    if (outputDirPath.isEmpty) {
-      outputDirPath = Paths.get(System.getProperty("user.dir"), DefaultOutdir).toString
+    if (outDirOpt.isEmpty) {
+      outDirOpt = Some(Paths.get(System.getProperty("user.dir"), DefaultOutdir))
     }
   }
 
+  /** Configure OutputManager based on supported CLI flags */
+  // TODO(shon): Perhaps we should reworking this object as a class that takes a configuration
+  // matching the specification of this trait?
+  def syncFromCli(cli: OutputManagerConfig): Unit = {
+    cli.outDir.foreach(setOutDir)
+    cli.writeIntermediate.foreach(flags += IntermediateFlag -> _)
+  }
+
+  /** Confgigure OutputManager, with cli congiruation taking precedence
+   * over the configuraiton file  */
+  def configure(cli: OutputManagerConfig): Unit = {
+    syncFromGlobalConfig()
+    syncFromCli(cli)
+  }
+
   // Flags can be passed from options too, e.g. --profile or --write-intermediate
+  // Strangly, we currently require data to flow both from the pass options
+  // to the output manager and from the manager to the pass options, this this "sync"
+  // is by directional.
   // TODO: remove this once all flag operations are moved into PassOptions
-  def syncFromOptions(opt: PassOptions): Unit = {
+  def syncWithOptions(opt: WriteablePassOptions): Unit = {
     opt.get[Boolean]("general", IntermediateFlag) foreach {
       flags += IntermediateFlag -> _
     }
     opt.get[Boolean]("general", ProfilingFlag) foreach {
       flags += ProfilingFlag -> _
     }
+    opt.set("io.outdir", outDir)
   }
 
   /** lends flags to execute `cmd` conditionally */
@@ -113,17 +148,13 @@ object OutputManager {
         }
       )
 
-  /** Inside `outputDirPath`, create a directory for an individual run */
+  /** Inside `outputDirOpt`, create a directory for an individual run */
   def createRunDirectory(specName: String): Unit =
     if (runDirOpt.isEmpty) {
       val nicedate = LocalDateTime.now().format(DateTimeFormatter.ofPattern(s"yyyy-MM-dd"))
       val nicetime = LocalDateTime.now().format(DateTimeFormatter.ofPattern(s"HH-mm-ss"))
-      val outdir = new File(outputDirPath)
-      if (!outdir.exists()) {
-        outdir.mkdir()
-      }
       // prefix for disambiguation
-      val rundir = Files.createTempDirectory(Paths.get(outdir.getAbsolutePath), s"${specName}_${nicedate}T${nicetime}_")
+      val rundir = Files.createTempDirectory(outDir, s"${specName}_${nicedate}T${nicetime}_")
       runDirOpt = Some(rundir)
     }
 }