Skip to content

[RFC] Refactor command line options #4404

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

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/util/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ SRC = allocate_objects.cpp \
byte_operators.cpp \
c_types.cpp \
cmdline.cpp \
cmdline_definition.cpp \
config.cpp \
cout_message.cpp \
decision_procedure.cpp \
Expand Down
158 changes: 158 additions & 0 deletions src/util/cmdline_definition.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
/*******************************************************************\

Module: Command line parsing

Author: Peter Schrammel

\*******************************************************************/

// \file Command line options definition

#include "cmdline_definition.h"

#include <sstream>

#include <util/invariant.h>
#include <util/json.h>
#include <util/xml.h>

cmdline_optiont::cmdline_optiont(
std::string name,
optionalt<argumentt> argument,
std::string help_text,
std::string option_group,
optionalt<std::string> deprecated)
: name(name),
argument(argument),
help_text(help_text),
option_group(option_group),
deprecated(deprecated)
{
}

cmdline_optiont::argumentt::argumentt(std::string name, std::string type)
: name(name), type(type)
{
}

cmdline_definitiont::cmdline_definitiont(
std::initializer_list<cmdline_optiont> &&initializer_list)
: cmdline_options(initializer_list)
{
}

void cmdline_definitiont::concat(const cmdline_definitiont &other)
{
cmdline_options.insert(
cmdline_options.end(),
other.cmdline_options.begin(),
other.cmdline_options.end());
}

std::string cmdline_definitiont::to_help_text(
std::size_t option_width,
std::size_t total_width) const
{
std::ostringstream os;
std::string option_group;
for(const auto &option : cmdline_options)
{
// do not print deprecated options
if(option.deprecated.has_value())
continue;

// print option group at the start of a new grouop
if(option.option_group != option_group)
{
option_group = option.option_group;
os << '\n' << option_group << ":\n";
}

// print option with optional argument and auto-wrap help text
std::string option_text = option.name;
if(option.name.size() == 1)
option_text = " -" + option_text;
else
option_text = " --" + option_text;
if(option.argument.has_value())
option_text += " " + option.argument->name;
os << option_text;
std::size_t padding = option_width;
if(option_text.size() < option_width)
padding = option_width - (option_text.size());
else
os << '\n';
std::size_t index = 0;
do
{
os << std::string(padding, ' ')
<< option.help_text.substr(index, total_width - option_width)
<< '\n';
padding = option_width;
index += total_width - option_width;
} while(index < option.help_text.size() - 1);
}
return os.str();
}

std::string cmdline_definitiont::to_option_string() const
{
std::ostringstream os;
for(const auto &option : cmdline_options)
os << "(" + option.name + ")" + (option.argument.has_value() ? ":" : "");
return os.str();
}

json_arrayt cmdline_definitiont::to_json() const
{
json_arrayt json_array;
for(const auto &option : cmdline_options)
{
json_objectt json_option;
json_option["name"] = json_stringt(option.name);
json_option["helpText"] = json_stringt(option.help_text);
json_option["optionGroup"] = json_stringt(option.option_group);
if(option.argument.has_value())
{
json_objectt &json_argument = json_option["argument"].make_object();
json_argument["name"] = json_stringt(option.argument->name);
json_argument["type"] = json_stringt(option.argument->type);
}
if(option.deprecated.has_value())
{
json_option["deprecated"] = json_stringt(*option.deprecated);
}
json_array.push_back(std::move(json_option));
}
return json_array;
}

xmlt cmdline_definitiont::to_xml() const
{
xmlt xml_cmdline("commandline");
for(const auto &option : cmdline_options)
{
xmlt &xml_option = xml_cmdline.new_element("option");
xml_option.set_attribute("name", option.name);
xml_option.new_element("help_text").data = option.help_text;
xml_option.new_element("option_group").data = option.option_group;
if(option.argument.has_value())
{
xmlt &xml_argument = xml_option.new_element("argument");
xml_argument.set_attribute("name", option.argument->name);
xml_argument.set_attribute("type", option.argument->type);
}
if(option.deprecated.has_value())
{
xml_option.new_element("deprecated").data = *option.deprecated;
}
}
return xml_cmdline;
}

cmdline_definitiont
operator+(cmdline_definitiont first, const cmdline_definitiont &second)
{
first.concat(second);
return first;
}
70 changes: 70 additions & 0 deletions src/util/cmdline_definition.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
/*******************************************************************\

Module: Command line parsing

Author: Peter Schrammel

\*******************************************************************/

// \file Command line options definition

#ifndef CPROVER_UTIL_CMDLINE_DEFINITION_H
#define CPROVER_UTIL_CMDLINE_DEFINITION_H

#include <list>
#include <string>
#include <vector>

#include "optional.h"

class json_arrayt;
class xmlt;

struct cmdline_optiont
{
struct argumentt
{
argumentt(std::string name, std::string type);

std::string name;
std::string type;
};

typedef std::string deprecatedt;

cmdline_optiont(
std::string name,
optionalt<argumentt> argument,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

std::string help_text,
std::string option_group,
optionalt<deprecatedt> deprecated);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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...) 😇


std::string name;
optionalt<argumentt> argument;
std::string help_text;
std::string option_group;
optionalt<deprecatedt> deprecated;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

};

class cmdline_definitiont
{
public:
explicit cmdline_definitiont(
std::initializer_list<cmdline_optiont> &&initializer_list);

void concat(const cmdline_definitiont &other);

std::string
to_help_text(std::size_t option_width, std::size_t total_width) const;
std::string to_option_string() const;
json_arrayt to_json() const;
xmlt to_xml() const;

private:
std::vector<cmdline_optiont> cmdline_options;
};

cmdline_definitiont
operator+(cmdline_definitiont first, const cmdline_definitiont &second);

#endif // CPROVER_UTIL_CMDLINE_DEFINITION_H