Description
This has come up in reviewing a number of PRs recently and I thought it might be good to have a documented consensus on this. To achieve one, we possibly need a discussion. So this is my understanding of the current state-of-affairs / how things are (but not necessarily how I, or anyone else) thinks they should be.
-
There has been a long-term goal of minimising the number of command-line options and making sure that the default options Do The Right Thing. Verification systems seems to grow vast numbers of options, for comparison, another system I have worked with has over 300 flags, another requires a sophisticated config file (it has it's own include system!) and comes with around 75 sample configuration. In these cases it is easy for configuration to become a skill in itself, creating a steep barrier to entry and meaning the majority of users do not use the majority of the functionality of the system. There is also the obvious QA and testing nightmare.
-
There have always been undocumented options. These are experimental features, features that only work / help in restricted / limited use-cases, features for specific customers, etc. This is not really an ideal state of affairs but it allows some functionality to be maintained centrally but only really used by some users.
-
The command line gets transferred to a cmdlinet object owned by the appropriate child of parse_options_baset (which contains the fantastic "doit" method, the entry point to our binaries). This is the unfiltered, lightly parsed command-line and shouldn't (there are exceptions but there probably shouldn't be new exceptions) really be used apart from parsing to options.
-
The parse_options methods should include code that checks cmdlinet, validates that the (combination of) flags make sense and sets values (including defaults, if applicable) in an optionst. This tends to be a local variable of a top-level method and is passed (as a const reference) to parts of the system that need config information. This should, preferably, but not necessarily exclusively be in the directory associated with the relevant binary.
-
Then there is configt. This holds details of the language and platform for which the code is being verified. It is auto-detected or loaded from the goto-program where possible but can be over-ridden from the command-line (and example of where a cmdline is used for something other than building options). This structure is global because many of these options are used all over the place in weird corners. It should only really contain options which are about the language / platform being analyzed.
So to add an option, one should:
A. Work out if it is needed and if so, which tool(s) needs it. Is there any sane way of automatically configuring this information?
B. Add it to the ($BINARY)_OPTIONS macro in $BINARY/$BINARY_parse_options.h. Things that are used by multiple tools should probably get a macro to reduce duplication. See OPT_GOTO_CHECK. If it is going to be fully / properly supported then add it to the help text at the end of $BINARY/$BINARY_parse_options.cpp , again, macros to reduce duplication.
C. If it is an option for what language version / platform we are emulating, then it should get the appropriate field in configt and be parsed from the command line by configt::set.
D. If not then code should be added to $BINARY/$BINARY_parse_options.cpp to recognise the flag and set the correct values in the optionst, including default values.
E. Ideally, somewhere in $BINARY/* , we should make use of the optionst entry to set-up the relevant objects. The API on objects should be sufficient to do this. If you find yourself threading individual arguments or const optionst & through a series of interfaces then there is probably something wrong and there is probably an easier way.
@kroening @tautschnig @peterschrammel Does this match your view of the intention behind the design.
@smowton You were running into issues with some of this in the CEGIS code; what should we improve?
Everyone : Questions, thoughts, opinions? Particularly backed with examples of things we have to do / have done.