diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e205944bc27..94b594c614f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -83,7 +84,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "xml_interface.h" cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) - : parse_options_baset(CBMC_OPTIONS, argc, argv, ui_message_handler), + : parse_options_baset(cbmc_options.to_option_string(), argc, argv, ui_message_handler), xml_interfacet(cmdline), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) @@ -93,9 +94,9 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) ::cbmc_parse_optionst::cbmc_parse_optionst( int argc, const char **argv, - const std::string &extra_options) + const cmdline_definitiont &extra_options) : parse_options_baset( - CBMC_OPTIONS + extra_options, + (cbmc_options + extra_options).to_option_string(), argc, argv, ui_message_handler), @@ -915,121 +916,35 @@ bool cbmc_parse_optionst::process_goto_program( /// display command line help void cbmc_parse_optionst::help() { - // clang-format off - std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n' - << align_center_with_border("Copyright (C) 2001-2018") << '\n' - << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*) - << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*) - << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*) - << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*) - << - "\n" - "Usage: Purpose:\n" - "\n" - " cbmc [-?] [-h] [--help] show help\n" - " cbmc file.c ... source file names\n" - "\n" - "Analysis options:\n" - HELP_SHOW_PROPERTIES - " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) - " --property id only check one specific property\n" - " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) - " --trace give a counterexample trace for failed properties\n" //NOLINT(*) - "\n" - "C/C++ frontend options:\n" - " -I path set include path (C/C++)\n" - " -D macro define preprocessor macro (C/C++)\n" - " --preprocess stop after preprocessing\n" - " --16, --32, --64 set width of int\n" - " --LP64, --ILP64, --LLP64,\n" - " --ILP32, --LP32 set width of int, long and pointers\n" - " --little-endian allow little-endian word-byte conversions\n" - " --big-endian allow big-endian word-byte conversions\n" - " --unsigned-char make \"char\" unsigned by default\n" - " --mm model set memory model (default: sc)\n" - " --arch set architecture (default: " - << configt::this_architecture() << ")\n" - " --os set operating system (default: " - << configt::this_operating_system() << ")\n" - " --c89/99/11 set C language standard (default: " - << (configt::ansi_ct::default_c_standard()== - configt::ansi_ct::c_standardt::C89?"c89": - configt::ansi_ct::default_c_standard()== - configt::ansi_ct::c_standardt::C99?"c99": - configt::ansi_ct::default_c_standard()== - configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*) - " --cpp98/03/11 set C++ language standard (default: " - << (configt::cppt::default_cpp_standard()== - configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*) - configt::cppt::default_cpp_standard()== - configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*) - configt::cppt::default_cpp_standard()== - configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*) - #ifdef _WIN32 - " --gcc use GCC as preprocessor\n" - #endif - " --no-arch don't set up an architecture\n" - " --no-library disable built-in abstract C library\n" - " --round-to-nearest rounding towards nearest even (default)\n" - " --round-to-plus-inf rounding towards plus infinity\n" - " --round-to-minus-inf rounding towards minus infinity\n" - " --round-to-zero rounding towards zero\n" - HELP_ANSI_C_LANGUAGE - HELP_FUNCTIONS - "\n" - "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" - HELP_SHOW_GOTO_FUNCTIONS - "\n" - "Program instrumentation options:\n" - HELP_GOTO_CHECK - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - " --error-label label check that label is unreachable\n" - " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) - " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) - HELP_REACHABILITY_SLICER - HELP_REACHABILITY_SLICER_FB - " --full-slice run full slicer (experimental)\n" // NOLINT(*) - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) - "\n" - "Semantic transformations:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" - "\n" - "BMC options:\n" - HELP_BMC - "\n" - "Backend options:\n" - " --object-bits n number of bits used for object addresses\n" - " --dimacs generate CNF in DIMACS format\n" - " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*) - " --localize-faults localize faults (experimental)\n" - " --smt2 use default SMT2 solver (Z3)\n" - " --boolector use Boolector\n" - " --cprover-smt2 use CPROVER SMT2 solver\n" - " --cvc4 use CVC4\n" - " --mathsat use MathSAT\n" - " --yices use Yices\n" - " --z3 use Z3\n" - " --refine use refinement procedure (experimental)\n" - HELP_STRING_REFINEMENT_CBMC - " --outfile filename output formula to given file\n" - " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) - " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) - "\n" - "Other options:\n" - " --version show version and exit\n" - " --xml-ui use XML-formatted output\n" - " --xml-interface bi-directional XML interface\n" - " --json-ui use JSON-formatted output\n" - // NOLINTNEXTLINE(whitespace/line_length) - HELP_VALIDATE - HELP_GOTO_TRACE - HELP_FLUSH - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; - // clang-format on + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + // clang-format off + log.result() + << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2001-2018") << '\n' + << align_center_with_border("Daniel Kroening, Edmund Clarke") + << '\n' // NOLINT(*) + << align_center_with_border( + "Carnegie Mellon University, Computer Science Department") + << '\n' // NOLINT(*) + << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*) + << align_center_with_border("Protected in part by U.S. patent 7,225,417") + << '\n' // NOLINT(*) + << + "\n" + "Usage: Purpose:\n" + "\n" + " cbmc [-?] [-h] [--help] show help\n" + " cbmc file.c ... source file names\n" + << cbmc_options.to_help_text(30, 80) << messaget::eom; + // clang-format on + break; + case ui_message_handlert::uit::JSON_UI: + ui_message_handler.get_json_stream().push_back(cbmc_options.to_json()); + break; + case ui_message_handlert::uit::XML_UI: + log.result() << cbmc_options.to_xml(); + break; + } } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index f3d63499913..c23990398c9 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -38,49 +39,45 @@ class goto_functionst; class optionst; // clang-format off -#define CBMC_OPTIONS \ - OPT_BMC \ - "(preprocess)(slice-by-trace):" \ - OPT_FUNCTIONS \ - "(no-simplify)(full-slice)" \ - OPT_REACHABILITY_SLICER \ - "(debug-level):(no-propagation)(no-simplify-if)" \ - "(document-subgoals)(outfile):(test-preprocessor)" \ - "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \ - "(object-bits):" \ - OPT_GOTO_CHECK \ - "(no-assertions)(no-assumptions)" \ - "(xml-ui)(xml-interface)(json-ui)" \ - "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ - "(cprover-smt2)" \ - "(no-sat-preprocessor)" \ - "(beautify)" \ - "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ - OPT_STRING_REFINEMENT_CBMC \ - "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ - "(little-endian)(big-endian)" \ - OPT_SHOW_GOTO_FUNCTIONS \ - OPT_SHOW_PROPERTIES \ - "(show-symbol-table)(show-parse-tree)" \ - "(drop-unused-functions)" \ - "(property):(stop-on-fail)(trace)" \ - "(error-label):(verbosity):(no-library)" \ - "(nondet-static)" \ - "(version)" \ - "(cover):(symex-coverage-report):" \ - "(mm):" \ - OPT_TIMESTAMP \ - "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ - "(ppc-macos)(unsigned-char)" \ - "(arrays-uf-always)(arrays-uf-never)" \ - "(string-abstraction)(no-arch)(arch):" \ - "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ - OPT_FLUSH \ - "(localize-faults)" \ - OPT_GOTO_TRACE \ - 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 +{ + { + "json-ui", + {}, + "use JSON-formatted output", + "Other options", + {} + }, + { + "xml-ui", + {}, + "use XML-formatted output", + "Other options", + {} + } +}; + +const cmdline_definitiont cbmc_options( + ui_options + + cmdline_definitiont{ + { + "preprocess", + {}, + "stop after preprocessing. " + "This is a veeeeeeeeeeeeeeeeery long help text. " + "This is a veeeeeeeeeeeeeeeeery long help text.", + "C/C++ frontend options", + {} + }, + { + "slice-by-trace", + cmdline_optiont::argumentt{"f", "string"}, + "", + "", + cmdline_optiont::deprecatedt("-slice-by-trace has been removed") + } + } + + ui_options); // clang-format on class cbmc_parse_optionst: @@ -96,7 +93,7 @@ class cbmc_parse_optionst: cbmc_parse_optionst( int argc, const char **argv, - const std::string &extra_options); + const cmdline_definitiont &extra_options); /// \brief Set the options that have default values /// diff --git a/src/util/Makefile b/src/util/Makefile index 8c4c6b5beb4..42b6bcac60c 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -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 \ diff --git a/src/util/cmdline_definition.cpp b/src/util/cmdline_definition.cpp new file mode 100644 index 00000000000..f3e0a801d3e --- /dev/null +++ b/src/util/cmdline_definition.cpp @@ -0,0 +1,158 @@ +/*******************************************************************\ + +Module: Command line parsing + +Author: Peter Schrammel + +\*******************************************************************/ + +// \file Command line options definition + +#include "cmdline_definition.h" + +#include + +#include +#include +#include + +cmdline_optiont::cmdline_optiont( + std::string name, + optionalt argument, + std::string help_text, + std::string option_group, + optionalt 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 &&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; +} diff --git a/src/util/cmdline_definition.h b/src/util/cmdline_definition.h new file mode 100644 index 00000000000..d2929504fe1 --- /dev/null +++ b/src/util/cmdline_definition.h @@ -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 +#include +#include + +#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 argument, + std::string help_text, + std::string option_group, + optionalt deprecated); + + std::string name; + optionalt argument; + std::string help_text; + std::string option_group; + optionalt deprecated; +}; + +class cmdline_definitiont +{ +public: + explicit cmdline_definitiont( + std::initializer_list &&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_options; +}; + +cmdline_definitiont +operator+(cmdline_definitiont first, const cmdline_definitiont &second); + +#endif // CPROVER_UTIL_CMDLINE_DEFINITION_H