diff options
Diffstat (limited to 'src/options/options_template.cpp')
| -rw-r--r-- | src/options/options_template.cpp | 345 |
1 files changed, 178 insertions, 167 deletions
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 51b2bea5e..f029dfd17 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file options_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Contains code for handling command-line options. ** @@ -53,13 +53,14 @@ extern int optreset; #include "base/output.h" #include "base/tls.h" #include "options/argument_extender.h" +#include "options/argument_extender_implementation.h" #include "options/didyoumean.h" #include "options/language.h" #include "options/options_handler.h" ${include_all_option_headers} -#line 63 "${template}" +#line 64 "${template}" #include "options/options_holder.h" #include "cvc4autoconfig.h" @@ -67,7 +68,7 @@ ${include_all_option_headers} ${option_handler_includes} -#line 71 "${template}" +#line 72 "${template}" using namespace CVC4; using namespace CVC4::options; @@ -389,7 +390,7 @@ Options::registerSetReplayLogFilename( ${all_custom_handlers} -#line 393 "${template}" +#line 394 "${template}" #ifdef CVC4_DEBUG # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true @@ -407,18 +408,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} { } -#line 411 "${template}" +#line 412 "${template}" static const std::string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:${common_documentation}"; -#line 416 "${template}" +#line 417 "${template}" static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ \n\ Additional CVC4 options:${remaining_documentation}"; -#line 422 "${template}" +#line 423 "${template}" static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ @@ -431,7 +432,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ cvc4 | presentation | pl CVC4 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ smt | smtlib | smt2 |\n\ - smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ + smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ tptp TPTP format (cnf and fof)\n\ sygus SyGuS format\n\ @@ -442,7 +443,7 @@ Languages currently supported as arguments to the --output-lang option:\n\ cvc3 CVC3 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ smt | smtlib | smt2 |\n\ - smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ + smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ tptp TPTP format\n\ z3str SMT-LIB 2.0 with Z3-str string constraints\n\ @@ -497,7 +498,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 501 "${template}" +#line 502 "${template}" // static void preemptGetopt(int& argc, char**& argv, const char* opt) { @@ -549,178 +550,196 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ -std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { - options::OptionsGuard guard(&s_current, this); +std::vector<std::string> Options::parseOptions(Options* options, + int argc, char* argv[]) + throw(OptionException) { - // Having this synonym simplifies the generation code in mkoptions. - options::OptionsHandler* handler = d_handler; + Assert(options != NULL); + Assert(argv != NULL); - const char *progName = main_argv[0]; + options::OptionsGuard guard(&s_current, options); - ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen); - std::vector<char*> allocated; + const char *progName = argv[0]; - Debug("options") << "main_argv == " << main_argv << std::endl; + // 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"); - // Reset getopt(), in the case of multiple calls to parseOptions(). - // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. - optind = 0; -#if HAVE_DECL_OPTRESET - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this -#endif /* HAVE_DECL_OPTRESET */ + Debug("options") << "Options::parseOptions == " << options << std::endl; + Debug("options") << "argv == " << argv << std::endl; - // find the base name of the program + // Find the base name of the program. const char *x = strrchr(progName, '/'); if(x != NULL) { progName = x + 1; } - d_holder->binary_name = std::string(progName); + options->d_holder->binary_name = std::string(progName); + + ArgumentExtender* argumentExtender = new ArgumentExtenderImplementation(); + for(int position = 1; position < argc; position++) { + argumentExtender->pushBackArgument(argv[position]); + } + + std::vector<std::string> nonoptions; + parseOptionsRecursive(options, argumentExtender, &nonoptions); + if(Debug.isOn("options")){ + for(std::vector<std::string>::const_iterator i = nonoptions.begin(), + iend = nonoptions.end(); i != iend; ++i){ + Debug("options") << "nonoptions " << *i << std::endl; + } + } + + delete argumentExtender; + return nonoptions; +} + +void Options::parseOptionsRecursive(Options* options, + ArgumentExtender* extender, + std::vector<std::string>* nonoptions) + throw(OptionException) { + + int argc; + char** argv; + + extender->movePreemptionsToArguments(); + extender->pushFrontArgument(""); + extender->getArguments(&argc, &argv); + + if(Debug.isOn("options")) { + Debug("options") << "starting a new parseOptionsRecursive with " + << argc << " arguments" << std::endl; + for( int i = 0; i < argc ; i++ ){ + Assert(argv[i] != NULL); + Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; + } + } - int extra_argc = 1; - char **extra_argv = (char**) malloc(2 * sizeof(char*)); - extra_argv[0] = NULL; - extra_argv[1] = NULL; + // Having this synonym simplifies the generation code in mkoptions. + options::OptionsHandler* handler = options->d_handler; + options::OptionsHolder* holder = options->d_holder; - int extra_optind = 0, main_optind = 0; + // Reset getopt(), in the case of multiple calls to parseOptions(). + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this +#endif /* HAVE_DECL_OPTRESET */ + + + int main_optind = 0; int old_optind; - int *optind_ref = &main_optind; - char** argv = main_argv; - std::vector<std::string> nonOptions; + while(true) { // Repeat Forever + + if(extender->hasPreemptions()){ + // Stop this round of parsing. We now parse recursively + // to start on a new character array for argv. + parseOptionsRecursive(options, extender, nonoptions); + break; + } - for(;;) { - int c = -1; optopt = 0; std::string option, optionarg; - Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind - << ", extra_argc == " << extra_argc << std::endl; - if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) { -#if HAVE_DECL_OPTRESET - if(optind_ref != &extra_optind) { - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this - } -#endif /* HAVE_DECL_OPTRESET */ - old_optind = optind = extra_optind; - optind_ref = &extra_optind; - argv = extra_argv; - Debug("preemptGetopt") << "in preempt code, next arg is " - << extra_argv[optind == 0 ? 1 : optind] - << std::endl; - if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') { - InternalError( - "preempted args cannot give non-options command-line args (found `%s')", - extra_argv[extra_optind == 0 ? 1 : extra_optind]); - } - c = getopt_long(extra_argc, extra_argv, - "+:${all_modules_short_options}", - cmdlineOptions, NULL); - Debug("preemptGetopt") << "in preempt code" - << ", c == " << c << " (`" << char(c) << "')" - << " optind == " << optind << std::endl; - if(optopt == 0 || - ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { - // long option - option = argv[old_optind == 0 ? 1 : old_optind]; - optionarg = (optarg == NULL) ? "" : optarg; - } else { - // short option - option = std::string("-") + char(optopt); - optionarg = (optarg == NULL) ? "" : optarg; - } - if(optind >= extra_argc) { - Debug("preemptGetopt") << "-- no more preempt args" << std::endl; - unsigned i = 1; - while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') { - extra_argv[i][0] = '\0'; - ++i; - } - extra_argc = 1; - extra_optind = 0; - } else { - Debug("preemptGetopt") << "-- more preempt args" << std::endl; - extra_optind = optind; - } + + optind = main_optind; + old_optind = main_optind; + //optind_ref = &main_optind; + //argv = main_argv; + + // 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] != '-') { + Debug("options") << "enqueueing " << argv[main_optind] + << " as a non-option." << std::endl; + nonoptions->push_back(argv[main_optind]); + ++main_optind; + extender->popFrontArgument(); + continue; } - if(c == -1) { -#if HAVE_DECL_OPTRESET - if(optind_ref != &main_optind) { - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this - } -#endif /* HAVE_DECL_OPTRESET */ - old_optind = optind = main_optind; - optind_ref = &main_optind; - argv = main_argv; - if(main_optind < argc && main_argv[main_optind][0] != '-') { - do { - if(main_optind != 0) { - nonOptions.push_back(main_argv[main_optind]); - } - ++main_optind; - } while(main_optind < argc && main_argv[main_optind][0] != '-'); - continue; - } - Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; -#if defined(__MINGW32__) || defined(__MINGW64__) - if(optreset == 1 && optind > 1) { - // on mingw, optreset will reset the optind, so we have to - // manually advance argc, argv - main_argv[optind - 1] = main_argv[0]; - argv = main_argv += optind - 1; - argc -= optind - 1; - old_optind = optind = main_optind = 1; - if(argc > 0) { - Debug("options") << "looking at : " << argv[0] << std::endl; - } - /*c = getopt_long(argc, main_argv, + + + Debug("options") << "[ before, main_optind == " << main_optind << " ]" + << std::endl; + Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; + Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" + << std::endl; + int c = getopt_long(argc, argv, "+:${all_modules_short_options}", cmdlineOptions, NULL); - Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl; - Debug("options") << "optind was reset to " << optind << std::endl; - optind = main_optind; - Debug("options") << "I restored optind to " << optind << std::endl;*/ - } -#endif /* __MINGW32__ || __MINGW64__ */ - Debug("options") << "[ argc == " << argc - << ", main_argv == " << main_argv << " ]" << std::endl; - c = getopt_long(argc, main_argv, - "+:${all_modules_short_options}", - cmdlineOptions, NULL); - main_optind = optind; - Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" - << std::endl; - Debug("options") << "[ next option will be at pos: " << optind << " ]" - << std::endl; - if(c == -1) { + + while(main_optind < optind) { + main_optind++; + extender->popFrontArgument(); + } + + Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" + << "[ next option will be at pos: " << optind << " ]" + << std::endl; + + // 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. + // + // We have to reinitialize optind to 0 instead of 1 as we need to support + // changing the argv array passed to getopt. + // This is needed as are using GNU extensions. + // From: http://man7.org/linux/man-pages/man3/getopt.3.html + // A program that scans multiple argument vectors, or rescans the same + // vector more than once, and wants to make use of GNU extensions such + // as '+' and '-' at the start of optstring, or changes the value of + // POSIXLY_CORRECT between scans, must reinitialize getopt() by + // resetting optind to 0, rather than the traditional value of 1. + // (Resetting to 0 forces the invocation of an internal initialization + // routine that rechecks POSIXLY_CORRECT and checks for GNU extensions + // in optstring.) + if ( old_optind == 0 && c == -1 ) { + Assert(main_optind > 0); + continue; + } + + if ( c == -1 ) { + if(Debug.isOn("options")) { Debug("options") << "done with option parsing" << std::endl; - break; + for(int index = optind; index < argc; ++index) { + Debug("options") << "remaining " << argv[index] << std::endl; + } } - option = argv[old_optind == 0 ? 1 : old_optind]; - optionarg = (optarg == NULL) ? "" : optarg; + break; } + option = argv[old_optind == 0 ? 1 : old_optind]; + optionarg = (optarg == NULL) ? "" : optarg; + Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl; switch(c) { ${all_modules_option_handlers} -#line 709 "${template}" +#line 722 "${template}" 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"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); case '?': default: - if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) && - !strncmp(argv[optind - 1], "--thread", 8) && - strlen(argv[optind - 1]) > 8 ) { + if( ( optopt == 0 || + ( optopt >= ${long_option_value_begin} && + optopt <= ${long_option_value_end} ) + ) && !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 ) + { if(! isdigit(argv[optind - 1][8])) { throw OptionException(formatThreadOptionException(option)); } - std::vector<std::string>& threadArgv = d_holder->threadArgv; + std::vector<std::string>& threadArgv = holder->threadArgv; char *end; long tnum = strtol(argv[optind - 1] + 8, &end, 10); if(tnum < 0 || (*end != '\0' && *end != '=')) { @@ -734,23 +753,24 @@ ${all_modules_option_handlers} } if(*end == '\0') { // e.g., we have --thread0 "foo" if(argc <= optind) { - throw OptionException(std::string("option `") + option - + "' missing its required argument"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); } Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl; - threadArgv[tnum] += argv[(*optind_ref)++]; + threadArgv[tnum] += argv[main_optind]; + main_optind++; } else { // e.g., we have --thread0="foo" if(end[1] == '\0') { throw OptionException(std::string("option `") + option + "' missing its required argument"); } - Debug("options") << "thread " << tnum << " gets option " << (end + 1) - << std::endl; + Debug("options") << "thread " << tnum << " gets option " + << (end + 1) << std::endl; threadArgv[tnum] += end + 1; } - Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] - << std::endl; + Debug("options") << "thread " << tnum << " now has " + << threadArgv[tnum] << std::endl; break; } @@ -759,19 +779,10 @@ ${all_modules_option_handlers} } } - Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl; - - free(extra_argv); - for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end(); - i != iend; ++i) - { - char* current = *i; - #warning "TODO: Unit tests fail if garbage collection is done here." - //free(current); - } - allocated.clear(); + Debug("options") << "got " << nonoptions->size() + << " non-option arguments." << std::endl; - return nonOptions; + free(argv); } std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() { @@ -787,7 +798,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 790 "${template}" +#line 800 "${template}" NULL };/* smtOptions[] */ @@ -809,7 +820,7 @@ std::vector< std::vector<std::string> > Options::getOptions() const throw() { ${all_modules_get_options} -#line 813 "${template}" +#line 762 "${template}" return opts; } |