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 index 2391025b18..9652560d7b 100644 --- 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 index 3432bca6c5..63a5d37e7e 100644 --- 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,10 @@ 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 +13,13 @@ 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 index 14760e23c9..0683e6fed0 100644 --- 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 index 0f40987586..e5cfce0659 100644 --- 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,6 +1,6 @@ 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} @@ -8,6 +8,12 @@ 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,35 @@ 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 +79,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 +104,41 @@ object OutputManager { } } // If `OutdirNameInCfg` is not specified, default to making rundir = /_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 +152,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) } }