diff options
Diffstat (limited to 'src/options/options_template.cpp')
| -rw-r--r-- | src/options/options_template.cpp | 471 |
1 files changed, 471 insertions, 0 deletions
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp new file mode 100644 index 000000000..2df69b5d3 --- /dev/null +++ b/src/options/options_template.cpp @@ -0,0 +1,471 @@ +/********************* */ +/*! \file options_template.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains code for handling command-line options. + ** + ** Contains code for handling command-line options + **/ + +#include <cstdio> +#include <cstdlib> +#include <new> +#include <string> +#include <sstream> +#include <limits> +#include <unistd.h> +#include <string.h> +#include <stdint.h> +#include <time.h> + +#include <getopt.h> + +#include "expr/expr.h" +#include "util/configuration.h" +#include "util/exception.h" +#include "util/language.h" + +${include_all_option_headers} + +#line 40 "${template}" + +#include "util/output.h" +#include "options/options_holder.h" +#include "cvc4autoconfig.h" +#include "options/base_options_handlers.h" + +${option_handler_includes} + +#line 49 "${template}" + +using namespace CVC4; +using namespace CVC4::options; + +namespace CVC4 { + +CVC4_THREADLOCAL(Options*) Options::s_current = NULL; + +/** + * This is a default handler for options of built-in C++ type. This + * template is really just a helper for the handleOption() template, + * below. Variants of this template handle numeric and non-numeric, + * integral and non-integral, signed and unsigned C++ types. + * handleOption() makes sure to instantiate the right one. + * + * This implements default behavior when e.g. an option is + * unsigned but the user specifies a negative argument; etc. + */ +template <class T, bool is_numeric, bool is_integer> +struct OptionHandler { + static T handle(std::string option, std::string optarg); +};/* struct OptionHandler<> */ + +/** Variant for integral C++ types */ +template <class T> +struct OptionHandler<T, true, true> { + static T handle(std::string option, std::string optarg) { + try { + Integer i(optarg, 0); + + if(! std::numeric_limits<T>::is_signed && i < 0) { + // unsigned type but user gave negative argument + throw OptionException(option + " requires a nonnegative argument"); + } else if(i < std::numeric_limits<T>::min()) { + // negative overflow for type + std::stringstream ss; + ss << option << " requires an argument >= " << std::numeric_limits<T>::min(); + throw OptionException(ss.str()); + } else if(i > std::numeric_limits<T>::max()) { + // positive overflow for type + std::stringstream ss; + ss << option << " requires an argument <= " << std::numeric_limits<T>::max(); + throw OptionException(ss.str()); + } + + if(std::numeric_limits<T>::is_signed) { + return T(i.getLong()); + } else { + return T(i.getUnsignedLong()); + } + } catch(std::invalid_argument&) { + // user gave something other than an integer + throw OptionException(option + " requires an integer argument"); + } + } +};/* struct OptionHandler<T, true, true> */ + +/** Variant for numeric but non-integral C++ types */ +template <class T> +struct OptionHandler<T, true, false> { + static T handle(std::string option, std::string optarg) { + std::stringstream in(optarg); + long double r; + in >> r; + if(! in.eof()) { + // we didn't consume the whole string (junk at end) + throw OptionException(option + " requires a numeric argument"); + } + + if(! std::numeric_limits<T>::is_signed && r < 0.0) { + // unsigned type but user gave negative value + throw OptionException(option + " requires a nonnegative argument"); + } else if(r < -std::numeric_limits<T>::max()) { + // negative overflow for type + std::stringstream ss; + ss << option << " requires an argument >= " << -std::numeric_limits<T>::max(); + throw OptionException(ss.str()); + } else if(r > std::numeric_limits<T>::max()) { + // positive overflow for type + std::stringstream ss; + ss << option << " requires an argument <= " << std::numeric_limits<T>::max(); + throw OptionException(ss.str()); + } + + return T(r); + } +};/* struct OptionHandler<T, true, false> */ + +/** Variant for non-numeric C++ types */ +template <class T> +struct OptionHandler<T, false, false> { + static T handle(std::string option, std::string optarg) { + T::unsupported_handleOption_call___please_write_me; + // The above line causes a compiler error if this version of the template + // is ever instantiated (meaning that a specialization is missing). So + // don't worry about the segfault in the next line, the "return" is only + // there to keep the compiler from giving additional, distracting errors + // and warnings. + return *(T*)0; + } +};/* struct OptionHandler<T, false, false> */ + +/** Handle an option of type T in the default way. */ +template <class T> +T handleOption(std::string option, std::string optarg) { + return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optarg); +} + +/** Handle an option of type std::string in the default way. */ +template <> +std::string handleOption<std::string>(std::string option, std::string optarg) { + return optarg; +} + +/** + * Run handler, and any user-given predicates, for option T. + * If a user specifies a :handler or :predicates, it overrides this. + */ +template <class T> +typename T::type runHandlerAndPredicates(T, std::string option, std::string optarg, SmtEngine* smt) { + // By default, parse the option argument in a way appropriate for its type. + // E.g., for "unsigned int" options, ensure that the provided argument is + // a nonnegative integer that fits in the unsigned int type. + + return handleOption<typename T::type>(option, optarg); +} + +template <class T> +void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) { + // By default, nothing to do for bool. Users add things with + // :predicate in options files to provide custom checking routines + // that can throw exceptions. +} + +${all_custom_handlers} + +#line 186 "${template}" + +#ifdef CVC4_DEBUG +# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true +#else /* CVC4_DEBUG */ +# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false +#endif /* CVC4_DEBUG */ + +#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE) +# define DO_SEMANTIC_CHECKS_BY_DEFAULT false +#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */ +# define DO_SEMANTIC_CHECKS_BY_DEFAULT true +#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */ + +Options::Options() : + d_holder(new options::OptionsHolder()) { +} + +Options::Options(const Options& options) : + d_holder(new options::OptionsHolder(*options.d_holder)) { +} + +Options::~Options() { + delete d_holder; +} + +options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} +{ +} + +#line 216 "${template}" + +static const std::string mostCommonOptionsDescription = "\ +Most commonly-used CVC4 options:${common_documentation}"; + +#line 221 "${template}" + +static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ +\n\ +Additional CVC4 options:${remaining_documentation}"; + +#line 227 "${template}" + +static const std::string languageDescription = "\ +Languages currently supported as arguments to the -L / --lang option:\n\ + auto attempt to automatically determine the input language\n\ + pl | cvc4 CVC4 presentation language\n\ + smt | smtlib SMT-LIB format 1.2\n\ + smt2 | smtlib2 SMT-LIB format 2.0\n\ + tptp TPTP format (cnf and fof)\n\ +\n\ +Languages currently supported as arguments to the --output-lang option:\n\ + auto match the output language to the input language\n\ + pl | cvc4 CVC4 presentation language\n\ + smt | smtlib SMT-LIB format 1.2\n\ + smt2 | smtlib2 SMT-LIB format 2.0\n\ + tptp TPTP format\n\ + ast internal format (simple syntax-tree language)\n\ +"; + +std::string Options::getDescription() const { + return optionsDescription; +} + +void Options::printUsage(const std::string msg, std::ostream& out) { + out << msg << optionsDescription << std::endl << std::flush; +} + +void Options::printShortUsage(const std::string msg, std::ostream& out) { + out << msg << mostCommonOptionsDescription << std::endl << std::endl + << "For full usage, please use --help." << std::endl << std::flush; +} + +void Options::printLanguageHelp(std::ostream& out) { + out << languageDescription << std::flush; +} + +/** + * This is a table of long options. By policy, each short option + * should have an equivalent long option (but the reverse isn't the + * case), so this table should thus contain all command-line options. + * + * Each option in this array has four elements: + * + * 1. the long option string + * 2. argument behavior for the option: + * no_argument - no argument permitted + * 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 + * 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) + * + * If you add something here, you should add it in src/main/usage.h + * also, to document it. + * + * If you add something that has a short option equivalent, you should + * add it to the getopt_long() call in parseOptions(). + */ +static struct option cmdlineOptions[] = {${all_modules_long_options} + { NULL, no_argument, NULL, '\0' } +};/* cmdlineOptions */ + +#line 291 "${template}" + +static void preemptGetopt(int& argc, char**& argv, const char* opt) { + const size_t maxoptlen = 128; + + Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl; + + AlwaysAssert(opt != NULL && *opt != '\0'); + AlwaysAssert(strlen(opt) <= maxoptlen); + + ++argc; + unsigned i = 1; + while(argv[i] != NULL && argv[i][0] != '\0') { + ++i; + } + + if(argv[i] == NULL) { + argv = (char**) realloc(argv, (i + 6) * sizeof(char*)); + for(unsigned j = i; j < i + 5; ++j) { + argv[j] = (char*) malloc(sizeof(char) * maxoptlen); + argv[j][0] = '\0'; + } + argv[i + 5] = NULL; + } + + strncpy(argv[i], opt, maxoptlen - 1); + argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow +} + +namespace options { + +/** Set a given Options* as "current" just for a particular scope. */ +class OptionsGuard { + Options** d_field; + Options* d_old; +public: + OptionsGuard(Options** field, Options* opts) : + d_field(field), + d_old(*field) { + *field = opts; + } + ~OptionsGuard() { + *d_field = d_old; + } +};/* class OptionsGuard */ + +}/* CVC4::options namespace */ + +/** Parse argc/argv and put the result into a CVC4::Options. */ +int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { + options::OptionsGuard guard(&s_current, this); + + const char *progName = main_argv[0]; + SmtEngine* const smt = NULL; + + // 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 also need this +#endif /* HAVE_DECL_OPTRESET */ + + // 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); + + int extra_argc = 1; + char **extra_argv = (char**) malloc(2 * sizeof(char*)); + extra_argv[0] = NULL; + extra_argv[1] = NULL; + + int extra_optind = 0, main_optind = 0; + int old_optind; + + char** argv = main_argv; + + for(;;) { + int c = -1; + 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 + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + old_optind = optind = extra_optind; + argv = extra_argv; + Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl; + 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(optind >= extra_argc) { + Debug("preemptGetopt") << "-- no more preempt args" << std::endl; + unsigned i = 0; + 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; + } + } + if(c == -1) { +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + old_optind = optind = main_optind; + argv = main_argv; + c = getopt_long(argc, main_argv, + ":${all_modules_short_options}", + cmdlineOptions, NULL); + main_optind = optind; + if(c == -1) { + break; + } + } + + Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "')" << std::endl; + + switch(c) { +${all_modules_option_handlers} + +#line 418 "${template}" + + case ':': + // This can be a long or short option, and the way to get at the + // name of it is different. + if(optopt == 0 || + ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { + // was a long option + throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); + } else { + // was a short option + throw OptionException(std::string("option `-") + char(optopt) + "' missing its required argument"); + } + + case '?': + default: + if(optopt == 0 && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 && + isdigit(argv[optind - 1][8])) { + std::vector<std::string>& threadArgv = d_holder->threadArgv; + int tnum = atoi(argv[optind - 1] + 8); + threadArgv.resize(tnum + 1); + if(threadArgv[tnum] != "") { + threadArgv[tnum] += " "; + } + const char* p = strchr(argv[optind - 1] + 9, '='); + if(p == NULL) { // e.g., we have --thread0 "foo" + threadArgv[tnum] += argv[optind++]; + } else { // e.g., we have --thread0="foo" + threadArgv[tnum] += p + 1; + } + break; + } + + // This can be a long or short option, and the way to get at the name of it is different. + if(optopt == 0) { // was a long option + throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'"); + } else { // was a short option + throw OptionException(std::string("can't understand option `-") + char(optopt) + "'"); + } + } + } + + if((*this)[options::incrementalSolving] && (*this)[options::proof]) { + throw OptionException(std::string("The use of --incremental with --proof is not yet supported")); + } + + return optind; +} + +#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT +#undef DO_SEMANTIC_CHECKS_BY_DEFAULT + +}/* CVC4 namespace */ |