From: Gereon Kremer Date: Mon, 13 Sep 2021 15:54:55 +0000 (+0200) Subject: Refactor options parsing (#7143) X-Git-Tag: cvc5-1.0.0~1229 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02088737d2845ea00714b6ba6fed8c20485a9645;p=cvc5.git Refactor options parsing (#7143) This PR refactors the code for options parsing. --- diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp index dfd93843e..a7a4429e3 100644 --- a/src/main/options_template.cpp +++ b/src/main/options_template.cpp @@ -82,19 +82,25 @@ Languages currently supported as arguments to the --output-lang option:\n\ "; // clang-format on -void printUsage(const std::string& msg, std::ostream& os) { - os << msg << "\n" << commonOptionsDescription << "\n\n" << additionalOptionsDescription << std::endl - << optionsFootnote << std::endl << std::flush; +void printUsage(const std::string& msg, std::ostream& os) +{ + os << msg << "\n" + << commonOptionsDescription << "\n\n" + << additionalOptionsDescription << std::endl + << optionsFootnote << std::endl; } -void printShortUsage(const std::string& msg, std::ostream& os) { - os << msg << "\n" << commonOptionsDescription << std::endl - << optionsFootnote << std::endl - << "For full usage, please use --help." - << std::endl << std::endl << std::flush; +void printShortUsage(const std::string& msg, std::ostream& os) +{ + os << msg << "\n" + << commonOptionsDescription << std::endl + << optionsFootnote << std::endl + << "For full usage, please use --help." << std::endl + << std::endl; } -void printLanguageHelp(std::ostream& os) { +void printLanguageHelp(std::ostream& os) +{ os << languageDescription << std::flush; } @@ -111,40 +117,45 @@ void printLanguageHelp(std::ostream& os) { * required_argument - an argument is expected * optional_argument - an argument is permitted but not required * 3. this is a pointer to an int which is set to the 4th entry of the - * array if the option is present; or NULL, in which case + * array if the option is present; or nullptr, in which case * getopt_long() returns the 4th entry * 4. the return value for getopt_long() when this long option (or the * value to set the 3rd entry to; see #3) */ -// clang-format off static struct option cmdlineOptions[] = { - ${cmdline_options}$ +// clang-format off + ${cmdoptions_long}$ +// clang-format on {nullptr, no_argument, nullptr, '\0'} }; -// clang-format on std::string suggestCommandLineOptions(const std::string& optionName) { DidYouMean didYouMean; const char* opt; - for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { + for (size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) + { didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); } - return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); + return didYouMean.getMatchAsString( + optionName.substr(0, optionName.find('='))); } -void parseInternal(api::Solver& solver, int argc, - char* argv[], - std::vector& nonoptions) +void parseInternal(api::Solver& solver, + int argc, + char* argv[], + std::vector& nonoptions) { Assert(argv != nullptr); - if(Debug.isOn("options")) { - Debug("options") << "starting a new parseInternal with " - << argc << " arguments" << std::endl; - for( int i = 0; i < argc ; i++ ){ - Assert(argv[i] != NULL); + if (Debug.isOn("options")) + { + Debug("options") << "starting a new parseInternal with " << argc + << " arguments" << std::endl; + for (int i = 0; i < argc; ++i) + { + Assert(argv[i] != nullptr); Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; } } @@ -161,8 +172,8 @@ void parseInternal(api::Solver& solver, int argc, int main_optind = 0; int old_optind; - - while(true) { // Repeat Forever + while (true) + { // Repeat Forever optopt = 0; @@ -172,8 +183,8 @@ void parseInternal(api::Solver& solver, int argc, // If we encounter an element that is not at zero and does not start // with a "-", this is a non-option. We consume this element as a // non-option. - if (main_optind > 0 && main_optind < argc && - argv[main_optind][0] != '-') { + if (main_optind > 0 && main_optind < argc && argv[main_optind][0] != '-') + { Debug("options") << "enqueueing " << argv[main_optind] << " as a non-option." << std::endl; nonoptions.push_back(argv[main_optind]); @@ -181,7 +192,6 @@ void parseInternal(api::Solver& solver, int argc, continue; } - Debug("options") << "[ before, main_optind == " << main_optind << " ]" << std::endl; Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; @@ -189,8 +199,8 @@ void parseInternal(api::Solver& solver, int argc, << std::endl; // clang-format off int c = getopt_long(argc, argv, - "+:${options_short}$", - cmdlineOptions, NULL); + "+:${cmdoptions_short}$", + cmdlineOptions, nullptr); // clang-format on main_optind = optind; @@ -202,15 +212,19 @@ void parseInternal(api::Solver& solver, int argc, // The initial getopt_long call should always determine that argv[0] // is not an option and returns -1. We always manually advance beyond // this element. - if ( old_optind == 0 && c == -1 ) { + if (old_optind == 0 && c == -1) + { Assert(main_optind > 0); continue; } - if ( c == -1 ) { - if(Debug.isOn("options")) { + if (c == -1) + { + if (Debug.isOn("options")) + { Debug("options") << "done with option parsing" << std::endl; - for(int index = optind; index < argc; ++index) { + for (int index = optind; index < argc; ++index) + { Debug("options") << "remaining " << argv[index] << std::endl; } } @@ -220,30 +234,29 @@ void parseInternal(api::Solver& solver, int argc, std::string option = argv[old_optind == 0 ? 1 : old_optind]; std::string optionarg = (optarg == nullptr) ? "" : optarg; - Debug("preemptGetopt") << "processing option " << c - << " (`" << char(c) << "'), " << option << std::endl; + Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) + << "'), " << option << std::endl; - // clang-format off - switch(c) + switch (c) { - ${options_handler}$ +// clang-format off + ${parseinternal_impl}$ +// clang-format on - case ':' : + case ':' : // This can be a long or short option, and the way to get at the // name of it is different. throw OptionException(std::string("option `") + option + "' missing its required argument"); - - case '?': - default: + case '?': + default: throw OptionException(std::string("can't understand option `") + option + "'" + suggestCommandLineOptions(option)); } } - // clang-format on - Debug("options") << "got " << nonoptions.size() - << " non-option arguments." << std::endl; + Debug("options") << "got " << nonoptions.size() << " non-option arguments." + << std::endl; } /** @@ -253,31 +266,36 @@ void parseInternal(api::Solver& solver, int argc, * * Throws OptionException on failures. */ -std::vector parse( - api::Solver& solver, int argc, char* argv[], std::string& binaryName) +std::vector parse(api::Solver& solver, + int argc, + char* argv[], + std::string& binaryName) { Assert(argv != nullptr); - const char *progName = argv[0]; + const char* progName = argv[0]; // To debug options parsing, you may prefer to simply uncomment this // and recompile. Debug flags have not been parsed yet so these have // not been set. - //DebugChannel.on("options"); + // DebugChannel.on("options"); Debug("options") << "argv == " << argv << std::endl; // Find the base name of the program. - const char *x = strrchr(progName, '/'); - if(x != nullptr) { + const char* x = strrchr(progName, '/'); + if (x != nullptr) + { progName = x + 1; } binaryName = std::string(progName); std::vector nonoptions; parseInternal(solver, argc, argv, nonoptions); - if (Debug.isOn("options")){ - for (const auto& no: nonoptions){ + if (Debug.isOn("options")) + { + for (const auto& no : nonoptions) + { Debug("options") << "nonoptions " << no << std::endl; } } diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index f277a1967..67ba635a3 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -422,6 +422,82 @@ def generate_holder_mem_copy(modules): # stuff for main/options.cpp +def _add_cmdoption(option, name, opts, next_id): + fmt = { + 'name': name, + 'arg': 'no' if option.type in ['bool', 'void'] else 'required', + 'next_id': next_id + } + opts.append( + '{{ "{name}", {arg}_argument, nullptr, {next_id} }},'.format(**fmt)) + + +def generate_parsing(modules): + """Generates the implementation for main::parseInternal() and matching + options definitions suitable for getopt_long(). Returns a tuple with: + - short options description (passed as third argument to getopt_long) + - long options description (passed as fourth argument to getopt_long) + - handler code that turns getopt_long return value to a setOption call + """ + short = "" + opts = [] + code = [] + next_id = 256 + for _, option in all_options(modules, False): + needs_impl = False + if option.short: # short option + needs_impl = True + code.append("case '{0}': // -{0}".format(option.short)) + short += option.short + if option.type not in ['bool', 'void']: + short += ':' + if option.long: # long option + needs_impl = True + _add_cmdoption(option, option.long_name, opts, next_id) + code.append('case {}: // --{}'.format(next_id, option.long_name)) + next_id += 1 + if option.alias: # long option aliases + needs_impl = True + for alias in option.alias: + _add_cmdoption(option, alias, opts, next_id) + code.append('case {}: // --{}'.format(next_id, alias)) + next_id += 1 + + if needs_impl: + # there is some way to call it, add call to solver.setOption() + if option.type == 'bool': + code.append(' solver.setOption("{}", "true"); break;'.format( + option.long_name)) + elif option.type == 'void': + code.append(' solver.setOption("{}", ""); break;'.format( + option.long_name)) + else: + code.append( + ' solver.setOption("{}", optionarg); break;'.format( + option.long_name)) + + if option.alternate: + assert option.type == 'bool' + # bool option that wants a --no-* + needs_impl = False + if option.long: # long option + needs_impl = True + _add_cmdoption(option, 'no-' + option.long_name, opts, next_id) + code.append('case {}: // --no-{}'.format( + next_id, option.long_name)) + next_id += 1 + if option.alias: # long option aliases + needs_impl = True + for alias in option.alias: + _add_cmdoption(option, 'no-' + alias, opts, next_id) + code.append('case {}: // --no-{}'.format(next_id, alias)) + next_id += 1 + code.append(' solver.setOption("{}", "false"); break;'.format( + option.long_name)) + + return short, '\n '.join(opts), '\n '.join(code) + + def _cli_help_format_options(option): """ Format short and long options for the cmdline documentation @@ -809,28 +885,13 @@ def codegen_module(module, dst_dir, tpls): write_file(dst_dir, filename, tpl['content'].format(**data)) -def add_getopt_long(long_name, argument_req, getopt_long): - """ - For each long option we need to add an instance of the option struct in - order to parse long options (command-line) with getopt_long. Each long - option is associated with a number that gets incremented by one each time - we add a new long option. - """ - value = g_getopt_long_start + len(getopt_long) - getopt_long.append( - TPL_GETOPT_LONG.format( - long_get_option(long_name), - 'required' if argument_req else 'no', value)) - - def codegen_all_modules(modules, build_dir, dst_dir, tpls): """Generate code for all option modules.""" headers_module = [] # generated *_options.h header includes - getopt_short = [] # short options for getopt_long - getopt_long = [] # long options for getopt_long options_get_info = [] # code for getOptionInfo() - options_handler = [] # option handler calls + help_common = [] # help text for all common options + help_others = [] # help text for all non-common options sphinxgen = SphinxGenerator() @@ -846,46 +907,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): sphinxgen.add(module, option) - # Generate options_handler and getopt_long - cases = [] - if option.short: - cases.append("case '{0}': // -{0}".format(option.short)) - - getopt_short.append(option.short) - if argument_req: - getopt_short.append(':') - - if option.long: - cases.append( - 'case {}: // --{}'.format( - g_getopt_long_start + len(getopt_long), - option.long)) - add_getopt_long(option.long, argument_req, getopt_long) - if option.alias: - for alias in option.alias: - cases.append( - 'case {}: // --{}'.format( - g_getopt_long_start + len(getopt_long), - alias)) - add_getopt_long(alias, argument_req, getopt_long) - - if cases: - if option.type == 'bool': - cases.append( - ' solver.setOption("{}", "true");'.format(option.long_name) - ) - elif option.type == 'void': - cases.append( - ' solver.setOption("{}", "");'.format(option.long_name)) - else: - cases.append( - ' solver.setOption("{}", optionarg);'.format(option.long_name)) - - cases.append(' break;') - - options_handler.extend(cases) - - # Generate handlers for setOption/getOption if option.long: # Make long and alias names available via set/get-option @@ -927,30 +948,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): else: options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, false, OptionInfo::VoidInfo{{}}}};'.format(cond, long_get_option(option.long), alias=alias)) - # Add --no- alternative options for boolean options - if option.long and option.alternate: - cases = [] - cases.append( - 'case {}: // --no-{}'.format( - g_getopt_long_start + len(getopt_long), - option.long)) - - add_getopt_long('no-{}'.format(option.long), argument_req, - getopt_long) - if option.alias: - for alias in option.alias: - cases.append( - 'case {}: // --no-{}'.format( - g_getopt_long_start + len(getopt_long), - alias)) - add_getopt_long('no-{}'.format(alias), argument_req, - getopt_long) - - cases.append( - ' solver.setOption("{}", "false");'.format(option.long_name) - ) - cases.append(' break;') - options_handler.extend(cases) + short, cmdline_opts, parseinternal = generate_parsing(modules) help_common, help_others = generate_cli_help(modules) @@ -969,12 +967,13 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): 'getnames_impl': generate_getnames_impl(modules), 'get_impl': generate_get_impl(modules), 'set_impl': generate_set_impl(modules), - 'cmdline_options': '\n '.join(getopt_long), 'help_common': help_common, 'help_others': help_others, - 'options_handler': '\n '.join(options_handler), - 'options_short': ''.join(getopt_short), 'options_get_info': '\n '.join(sorted(options_get_info)), + # main/options.cpp + 'cmdoptions_long': cmdline_opts, + 'cmdoptions_short': short, + 'parseinternal_impl': parseinternal, } for tpl in tpls: write_file(dst_dir, tpl['output'], tpl['content'].format(**data))