[RFC] Refactor command line options #4404

peterschrammel · 2019-03-18T14:20:47Z

Before I go ahead with this rather big refactoring, I'd like to collect some feedback and additional requirements that you might think of.

a1496e0 is to showcase some of the capabilities.
CI is expected to fail.

Currently, I have the following requirements:

export machine-readable commandline options output (JSON/XML) for downstream consumption
export information on deprecated options for downstream consumption
a step further towards making plain/json/xml output clean (there's no help/usage output in JSON/XML at the moment)
make sure plain help text is always properly formatted and wrapped
prepare for unifying cmdlinet->optionst parsing code

Checklist:

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

LAJW · 2019-03-20T14:13:57Z

Looks decent, though I had something like this in mind: https://www.npmjs.com/package/commander where each command could have its own parser. But it requires std::any (or a polyfill).

peterschrammel · 2019-03-21T15:37:30Z

where each command could have its own parser.

I don't think that we have an issue with the raw parsing. Most of the mess comes from duplicating the translation into a configuration object (optionst) across all driver programs. My vague plans for the second step there are to associate these translations with a cmdline_definitiont/cmdline_optiont. That will factor out all the verbose cmdline->options code. In third step we could then transition to more structured configuration objects.

A structured way of defining command line options.

martin-cs · 2019-03-21T19:37:40Z

These sound like reasonable goals. Bringing some sanity to the option handling of goto-instrument and goto-analyzer and not having to manually duplicate and parallel maintain their command options would make me very happy. If we could also do a rationalisation / orthogonalisation on the options that would also be great. One of the selling points of CBMC used to be that it didn't have an insane number of options.

I'm not sure that I understand from the patch how the new system is supposed to work; perhaps you could write a little bit describing it? The main value(?) of separating cmdlinet and optionst is in giving sane defaults and flagging combinations that don't work. As long as we can do that I think it could be a big improvement.

One point of pedantry; can we call the combined thing something more like options or parameters rather than command line because it would be nice to believe in a world where that config might come from somewhere else.

[ Inflammatory, unhelpful suggestion -- maybe we could also include configt in this refactor ... ]

martin-cs · 2019-03-21T19:38:15Z

Oh yes; for keeping things in sync, there is also the question of the Java tools.

tautschnig

Thank you for starting to work on this! Yet I am surprised that #1521 isn't referenced here. Maybe this PR can even go all the way and eventually close that issue?

tautschnig · 2019-03-22T08:18:12Z

src/cbmc/cbmc_parse_options.h

-  OPT_VALIDATE \
-  OPT_ANSI_C_LANGUAGE \
-  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+const cmdline_definitiont ui_options


A rather unrelated comment: does anyone know why this ever needed to go in the header file? I.e., not just the changes in this PR, but also the current CBMC_OPTIONS?

tautschnig · 2019-03-22T08:20:31Z

src/util/cmdline_definition.h

+    optionalt<argumentt> argument,
+    std::string help_text,
+    std::string option_group,
+    optionalt<deprecatedt> deprecated);


Wouldn't it make for a very easy (and IMHO) nice extension to have a second constructor that takes a std::function for argument parsing (possibly achieving what @LAJW suggested)?

That requires a bit more thinking as many options are not independent... I have a few ideas...

Speaking of dependent options: it would actually be nice if one had a way to specify implied options (e.g., --z3 implies --smt2). But I suppose the wish-list is unbounded (what about conflicting options...) 😇

tautschnig · 2019-03-22T08:21:08Z

src/util/cmdline_definition.h

+
+  cmdline_optiont(
+    std::string name,
+    optionalt<argumentt> argument,


I don't think we should use optionalt here (or below, for deprecated), just have multiple constructors with varying numbers of parameters. The optionalt class members of course still remain in place.

Yes, although {} flows quite intuitively in the initialiser list...

tautschnig · 2019-03-22T08:27:04Z

src/util/cmdline_definition.h

+  optionalt<argumentt> argument;
+  std::string help_text;
+  std::string option_group;
+  optionalt<deprecatedt> deprecated;


I would like to propose one more member: hidden. At the moment, we have a number of command-line options that are intentionally undocumented, because either we consider them harmful (such as --no-propagation) or because they used to be supported and we just don't want to break scripts or other tooling still using them (such as --floatbv).

tautschnig · 2019-03-22T08:41:39Z

Maybe we should actually have a class hierarchy under cmdline_optiont, including cmdline_option_with_argumentt, deprecated_cmdline_optiont, hidden_cmdline_optiont? cmdline_optiont would just provide some virtual functions so that printing and reading any set values can be achieved. But I guess for a start multiple constructors with a single class make things easier.

peterschrammel added do not merge RFC Request for comment labels Mar 18, 2019

peterschrammel requested review from kroening, pkesseli, smowton and tautschnig as code owners March 18, 2019 14:20

peterschrammel assigned smowton, thk123, tautschnig, kroening, martin-cs, allredj and chrisr-diffblue Mar 18, 2019

peterschrammel added 2 commits March 21, 2019 15:40

Add cmdline_definitiont

f93e0e6

A structured way of defining command line options.

[Do not merge] Use cmdline_definition in CBMC

a1496e0

peterschrammel force-pushed the refactor-parse-options branch from 6ecae31 to a1496e0 Compare March 21, 2019 15:43

tautschnig reviewed Mar 22, 2019

View reviewed changes

peterschrammel assigned peterschrammel and unassigned smowton, thk123, tautschnig, kroening, martin-cs, allredj and chrisr-diffblue Mar 23, 2019

peterschrammel mentioned this pull request Apr 17, 2019

Symex-driven lazy loading uses goto-checker [blocks: #2212] #4541

Merged

6 tasks

peterschrammel mentioned this pull request Oct 24, 2022

new help formatter and console API #7141

Merged

6 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[RFC] Refactor command line options #4404

[RFC] Refactor command line options #4404

peterschrammel commented Mar 18, 2019 •

edited

Loading

LAJW commented Mar 20, 2019

peterschrammel commented Mar 21, 2019 •

edited

Loading

martin-cs commented Mar 21, 2019

martin-cs commented Mar 21, 2019

tautschnig left a comment

tautschnig Mar 22, 2019

peterschrammel Mar 22, 2019

tautschnig Mar 22, 2019

peterschrammel Mar 22, 2019

tautschnig Mar 23, 2019

tautschnig Mar 22, 2019

peterschrammel Mar 22, 2019

tautschnig Mar 22, 2019

tautschnig commented Mar 22, 2019

[RFC] Refactor command line options #4404

Are you sure you want to change the base?

[RFC] Refactor command line options #4404

Conversation

peterschrammel commented Mar 18, 2019 • edited Loading

LAJW commented Mar 20, 2019

peterschrammel commented Mar 21, 2019 • edited Loading

martin-cs commented Mar 21, 2019

martin-cs commented Mar 21, 2019

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Mar 22, 2019

peterschrammel commented Mar 18, 2019 •

edited

Loading

peterschrammel commented Mar 21, 2019 •

edited

Loading