Basic format of the configuration description

[hajduakos]

Currently, the portfolio (scripts/gazer_starter.py) is hardcoded to 3 analyses. It would be a really nice feature to have a generic portfolio executor that can read the components of the portfolio from a configuration file (e.g. yml). For example, the current hardcoded analysis could be described something like this:

- bmc
  - timeout: 150
  - flags: "--inline all", "--bound 1000000"
  - harness: true
- theta
  - timeout: 100
  - flags: "--domain EXPL", "--search ERR", ...
  - harness: true
- theta
  - flags: "--domain PRED", "--inline all", ...
  - harness: true

The syntax can of course be improved, but you get the main idea. This tells the portfolio engine to start with a BMC with 150s timeout and the given flags, and in the end, also validate the harness. Then, if the result is inconclusive, run Theta with 100s timeout, and so on.

CPAchecker can also be a good example to look at.

[AdamZsofi]

Started working on it on the branch configurable-portfolio. Currently it is not functional (almost empty), as I just started refactoring the old python portfolio as a bash script, but an example of what I think the (yaml) config file should look like can be found in the scripts directory.

[AdamZsofi]

Example config file with comments here

• It's in YAML
• It isn't definitely final (although I don't think the current options will change much) and it will be extended with further options as I work on it