Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace untyped option maps with statically typed configuration objects #1174

Closed
5 tasks done
Tracked by #2015
shonfeder opened this issue Dec 14, 2021 · 1 comment
Closed
5 tasks done
Tracked by #2015
Assignees
Labels
new New issue to be triaged. refactoring

Comments

@shonfeder
Copy link
Contributor

shonfeder commented Dec 14, 2021

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

class WriteablePassOptions extends PassOptions {
private val store: mutable.Map[String, Any] = mutable.HashMap[String, Any]()

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:

/**
* Get a pass option
* @param passName a pass name, or any other convenient name
* @param optionName an option name
* @return the option value, normally, an Integer or String
*/
def get[T: ClassTag](passName: String, optionName: String): Option[T] = {
// The ClassTag prevents the type of `T` from being erased at runtime
// See https://stackoverflow.com/a/18136667/1187277
store.get(passName + "." + optionName) match {
// Since we have added the ClassTag, we are able to match on its value here
case Some(value: T) =>
Some(value)
case Some(value) =>
throw new IllegalArgumentException(s"Option $optionName has unexpected type: " + value.getClass)
case None => None
}
}

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:

@shonfeder shonfeder added new New issue to be triaged. refactoring labels Dec 14, 2021
@shonfeder shonfeder mentioned this issue Jun 10, 2022
1 task
@shonfeder shonfeder self-assigned this Jul 26, 2022
shonfeder pushed a commit that referenced this issue Jul 26, 2022
This is required for #1174, since we'll need the SMTEncoding type for
the pass options declarations, but we cannot introduce a dependency from
infra -> bmcmt, as there is already a dependency going the other way.

Along the way, I also made some small cleanups to

- the naming the way the case class was declared (to use a more
- idiomatic pattern, following examples like, inter alia,
  https://nrinaudo.github.io/scala-best-practices/definitions/adt.html)
- remove the unneeded literal identifiers ``
- move string conversion into the class (keeping the closely related
  logic together)
shonfeder pushed a commit that referenced this issue Jul 27, 2022
* Create `infra.passes.options` object

This object is mimicking a package currently (see
https://docs.scala-lang.org/style/naming-conventions.html#objects). We
may move this stuff into a package if it gets too large.

This package will collect all the statically declared options parameters
we use to configure Apalache.

* Move SMTEncoding into `infra.passes.options`

This is required for #1174, since we'll need the SMTEncoding type for
the pass options declarations, but we cannot introduce a dependency from
infra -> bmcmt, as there is already a dependency going the other way.

Along the way, I also made some small cleanups to

- the naming the way the case class was declared (to use a more
- idiomatic pattern, following examples like, inter alia,
  https://nrinaudo.github.io/scala-best-practices/definitions/adt.html)
- remove the unneeded literal identifiers ``
- move string conversion into the class (keeping the closely related
  logic together)
shonfeder pushed a commit that referenced this issue Jul 28, 2022
Just a simple code organization change consistent with #2018 and the
ongoinig work on #1174.
shonfeder pushed a commit that referenced this issue Jul 28, 2022
Contributes towards #1174

This adds traits with values to represent all the options that we are
currently setting in the `at.forsyte.apalache.tla.tooling.opt.Cmd*`
classes. None of those options are actually transferred over here.
Instead, this changeset just prepares the representation of the options,
with the aim of obtaining feedback on the presentation.
shonfeder pushed a commit that referenced this issue Jul 29, 2022
Just a simple code organization change consistent with #2018 and the
ongoinig work on #1174.
shonfeder pushed a commit that referenced this issue Jul 29, 2022
Just a simple code organization change consistent with #2018 and the
ongoinig work on #1174.
shonfeder pushed a commit that referenced this issue Jul 29, 2022
Contributes towards #1174

This adds traits with values to represent all the options that we are
currently setting in the `at.forsyte.apalache.tla.tooling.opt.Cmd*`
classes. None of those options are actually transferred over here.
Instead, this changeset just prepares the representation of the options,
with the aim of obtaining feedback on the presentation.
shonfeder pushed a commit that referenced this issue Jul 29, 2022
Contributes towards #1174

This adds traits with values to represent all the options that we are
currently setting in the `at.forsyte.apalache.tla.tooling.opt.Cmd*`
classes. None of those options are actually transferred over here.
Instead, this changeset just prepares the representation of the options,
with the aim of obtaining feedback on the presentation.
@shonfeder
Copy link
Contributor Author

Closed by #2074

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
new New issue to be triaged. refactoring
Projects
None yet
Development

No branches or pull requests

1 participant