apalache icon indicating copy to clipboard operation
apalache copied to clipboard

Replace untyped option maps with statically typed configuration objects

Open shonfeder opened this issue 2 years ago • 0 comments

We are currently using a Map[String, Any] to store most of the application configuration. E.g., see

https://github.com/informalsystems/apalache/blob/98306abe0b7d2ffb913b50e9fd5dacd772712f10/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/WriteablePassOptions.scala#L23-L24

When values are fetched from the map, we need to do a runtime cast, which has also required carrying around typing information which could otherwise be erased:

https://github.com/informalsystems/apalache/blob/98306abe0b7d2ffb913b50e9fd5dacd772712f10/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/WriteablePassOptions.scala#L38-L57

This makes the application configuration significantly more brittle than it needs to be, as it it subject to runtime errors due to illtyped configuration values or missing keys.

Afaict, we should be able to replace the untyped map with a class that provides static guarantees for the correct typing of the configuration values, and that any components that depend on configuration receive all values they need.

If we push all such configuration to the ConfigManager added in #1160, we'll also get the added benefit of being able to load and dump the full application configuration programmatically. The former should support automation, and the latter reproducibility, benchmarking, and debugging (e.g., the bug reports we generate could report a dump of the entire application configuration, which could then be loaded up trivially in regression tests).


We need to thread the statically specified options through our DI framework Guice. Here's the plan:

  • [x] #2038 after which the class ApalacheConfig will be used specify the values that can be be supplied to the options from the various configuration sources.
  • [ ] #2040
  • [ ] #2050
  • [ ] #2066
  • [ ] Options classes FooOptions will be defined as a subclasses ConfigurableOptions extended with mixins for each additional option class needed for the given mode of execution, drawing from the already defined infra.options traits.
  • [ ] A Provider[FooOptions] will be implemented to allow the options object to be constructed.
  • [ ] For each pass, we will bind a Provider[FooOptions] the Guice module -- this will replace the current uniform binding of WriteableOptions to PassOptions.
  • [ ] After creating the executor in the run method of each *Cmd, we will call options.configure(this)

shonfeder avatar Dec 14 '21 18:12 shonfeder