src/options/options_template.cpp

   1 /*********************                                                        */
   2 /*! \file options_template.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Contains code for handling command-line options.
  13  **
  14  ** Contains code for handling command-line options
  15  **/
  16
  17 #if !defined(_BSD_SOURCE) && (defined(__MINGW32__) || defined(__MINGW64__))
  18 // force use of optreset; mingw croaks on argv-switching otherwise
  19 #  include "cvc4autoconfig.h"
  20 #  define _BSD_SOURCE
  21 #  undef HAVE_DECL_OPTRESET
  22 #  define HAVE_DECL_OPTRESET 1
  23 #  define CVC4_IS_NOT_REALLY_BSD
  24 #endif /* !_BSD_SOURCE && (__MINGW32__ || __MINGW64__) */
  25
  26 #include <getopt.h>
  27
  28 // clean up
  29 #ifdef CVC4_IS_NOT_REALLY_BSD
  30 #  undef _BSD_SOURCE
  31 #endif /* CVC4_IS_NOT_REALLY_BSD */
  32
  33 #include <cstdio>
  34 #include <cstdlib>
  35 #include <new>
  36 #include <string>
  37 #include <sstream>
  38 #include <limits>
  39 #include <unistd.h>
  40 #include <string.h>
  41 #include <stdint.h>
  42 #include <time.h>
  43
  44 #include "expr/expr.h"
  45 #include "util/configuration.h"
  46 #include "util/exception.h"
  47 #include "util/language.h"
  48 #include "util/tls.h"
  49
  50 ${include_all_option_headers}
  51
  52 #line 57 "${template}"
  53
  54 #include "util/output.h"
  55 #include "options/options_holder.h"
  56 #include "cvc4autoconfig.h"
  57 #include "options/base_options_handlers.h"
  58
  59 ${option_handler_includes}
  60
  61 #line 66 "${template}"
  62
  63 using namespace CVC4;
  64 using namespace CVC4::options;
  65
  66 namespace CVC4 {
  67
  68 CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
  69
  70 /**
  71  * This is a default handler for options of built-in C++ type.  This
  72  * template is really just a helper for the handleOption() template,
  73  * below.  Variants of this template handle numeric and non-numeric,
  74  * integral and non-integral, signed and unsigned C++ types.
  75  * handleOption() makes sure to instantiate the right one.
  76  *
  77  * This implements default behavior when e.g. an option is
  78  * unsigned but the user specifies a negative argument; etc.
  79  */
  80 template <class T, bool is_numeric, bool is_integer>
  81 struct OptionHandler {
  82   static T handle(std::string option, std::string optionarg);
  83 };/* struct OptionHandler<> */
  84
  85 /** Variant for integral C++ types */
  86 template <class T>
  87 struct OptionHandler<T, true, true> {
  88   static T handle(std::string option, std::string optionarg) {
  89     try {
  90       Integer i(optionarg, 10);
  91
  92       if(! std::numeric_limits<T>::is_signed && i < 0) {
  93         // unsigned type but user gave negative argument
  94         throw OptionException(option + " requires a nonnegative argument");
  95       } else if(i < std::numeric_limits<T>::min()) {
  96         // negative overflow for type
  97         std::stringstream ss;
  98         ss << option << " requires an argument >= " << std::numeric_limits<T>::min();
  99         throw OptionException(ss.str());
 100       } else if(i > std::numeric_limits<T>::max()) {
 101         // positive overflow for type
 102         std::stringstream ss;
 103         ss << option << " requires an argument <= " << std::numeric_limits<T>::max();
 104         throw OptionException(ss.str());
 105       }
 106
 107       if(std::numeric_limits<T>::is_signed) {
 108         return T(i.getLong());
 109       } else {
 110         return T(i.getUnsignedLong());
 111       }
 112     } catch(std::invalid_argument&) {
 113       // user gave something other than an integer
 114       throw OptionException(option + " requires an integer argument");
 115     }
 116   }
 117 };/* struct OptionHandler<T, true, true> */
 118
 119 /** Variant for numeric but non-integral C++ types */
 120 template <class T>
 121 struct OptionHandler<T, true, false> {
 122   static T handle(std::string option, std::string optionarg) {
 123     std::stringstream in(optionarg);
 124     long double r;
 125     in >> r;
 126     if(! in.eof()) {
 127       // we didn't consume the whole string (junk at end)
 128       throw OptionException(option + " requires a numeric argument");
 129     }
 130
 131     if(! std::numeric_limits<T>::is_signed && r < 0.0) {
 132       // unsigned type but user gave negative value
 133       throw OptionException(option + " requires a nonnegative argument");
 134     } else if(r < -std::numeric_limits<T>::max()) {
 135       // negative overflow for type
 136       std::stringstream ss;
 137       ss << option << " requires an argument >= " << -std::numeric_limits<T>::max();
 138       throw OptionException(ss.str());
 139     } else if(r > std::numeric_limits<T>::max()) {
 140       // positive overflow for type
 141       std::stringstream ss;
 142       ss << option << " requires an argument <= " << std::numeric_limits<T>::max();
 143       throw OptionException(ss.str());
 144     }
 145
 146     return T(r);
 147   }
 148 };/* struct OptionHandler<T, true, false> */
 149
 150 /** Variant for non-numeric C++ types */
 151 template <class T>
 152 struct OptionHandler<T, false, false> {
 153   static T handle(std::string option, std::string optionarg) {
 154     T::unsupported_handleOption_call___please_write_me;
 155     // The above line causes a compiler error if this version of the template
 156     // is ever instantiated (meaning that a specialization is missing).  So
 157     // don't worry about the segfault in the next line, the "return" is only
 158     // there to keep the compiler from giving additional, distracting errors
 159     // and warnings.
 160     return *(T*)0;
 161   }
 162 };/* struct OptionHandler<T, false, false> */
 163
 164 /** Handle an option of type T in the default way. */
 165 template <class T>
 166 T handleOption(std::string option, std::string optionarg) {
 167   return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
 168 }
 169
 170 /** Handle an option of type std::string in the default way. */
 171 template <>
 172 std::string handleOption<std::string>(std::string option, std::string optionarg) {
 173   return optionarg;
 174 }
 175
 176 /**
 177  * Run handler, and any user-given predicates, for option T.
 178  * If a user specifies a :handler or :predicates, it overrides this.
 179  */
 180 template <class T>
 181 typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, SmtEngine* smt) {
 182   // By default, parse the option argument in a way appropriate for its type.
 183   // E.g., for "unsigned int" options, ensure that the provided argument is
 184   // a nonnegative integer that fits in the unsigned int type.
 185
 186   return handleOption<typename T::type>(option, optionarg);
 187 }
 188
 189 template <class T>
 190 void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
 191   // By default, nothing to do for bool.  Users add things with
 192   // :predicate in options files to provide custom checking routines
 193   // that can throw exceptions.
 194 }
 195
 196 ${all_custom_handlers}
 197
 198 #line 203 "${template}"
 199
 200 #ifdef CVC4_DEBUG
 201 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
 202 #else /* CVC4_DEBUG */
 203 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
 204 #endif /* CVC4_DEBUG */
 205
 206 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
 207 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
 208 #else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 209 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
 210 #endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 211
 212 Options::Options() :
 213   d_holder(new options::OptionsHolder()) {
 214 }
 215
 216 Options::Options(const Options& options) :
 217   d_holder(new options::OptionsHolder(*options.d_holder)) {
 218 }
 219
 220 Options::~Options() {
 221   delete d_holder;
 222 }
 223
 224 options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 225 {
 226 }
 227
 228 #line 233 "${template}"
 229
 230 static const std::string mostCommonOptionsDescription = "\
 231 Most commonly-used CVC4 options:${common_documentation}";
 232
 233 #line 238 "${template}"
 234
 235 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 236 \n\
 237 Additional CVC4 options:${remaining_documentation}";
 238
 239 #line 244 "${template}"
 240
 241 static const std::string optionsFootnote = "\n\
 242 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
 243     sense of the option.\n\
 244 ";
 245
 246 static const std::string languageDescription = "\
 247 Languages currently supported as arguments to the -L / --lang option:\n\
 248   auto                           attempt to automatically determine language\n\
 249   cvc4 | presentation | pl       CVC4 presentation language\n\
 250   smt1 | smtlib1                 SMT-LIB format 1.2\n\
 251   smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
 252   tptp                           TPTP format (cnf and fof)\n\
 253 \n\
 254 Languages currently supported as arguments to the --output-lang option:\n\
 255   auto                           match output language to input language\n\
 256   cvc4 | presentation | pl       CVC4 presentation language\n\
 257   smt1 | smtlib1                 SMT-LIB format 1.2\n\
 258   smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
 259   tptp                           TPTP format\n\
 260   ast                            internal format (simple syntax trees)\n\
 261 ";
 262
 263 std::string Options::getDescription() const {
 264   return optionsDescription;
 265 }
 266
 267 void Options::printUsage(const std::string msg, std::ostream& out) {
 268   out << msg << optionsDescription << std::endl
 269       << optionsFootnote << std::endl << std::flush;
 270 }
 271
 272 void Options::printShortUsage(const std::string msg, std::ostream& out) {
 273   out << msg << mostCommonOptionsDescription << std::endl
 274       << optionsFootnote << std::endl
 275       << "For full usage, please use --help." << std::endl << std::endl << std::flush;
 276 }
 277
 278 void Options::printLanguageHelp(std::ostream& out) {
 279   out << languageDescription << std::flush;
 280 }
 281
 282 /**
 283  * This is a table of long options.  By policy, each short option
 284  * should have an equivalent long option (but the reverse isn't the
 285  * case), so this table should thus contain all command-line options.
 286  *
 287  * Each option in this array has four elements:
 288  *
 289  * 1. the long option string
 290  * 2. argument behavior for the option:
 291  *    no_argument - no argument permitted
 292  *    required_argument - an argument is expected
 293  *    optional_argument - an argument is permitted but not required
 294  * 3. this is a pointer to an int which is set to the 4th entry of the
 295  *    array if the option is present; or NULL, in which case
 296  *    getopt_long() returns the 4th entry
 297  * 4. the return value for getopt_long() when this long option (or the
 298  *    value to set the 3rd entry to; see #3)
 299  *
 300  * If you add something here, you should add it in src/main/usage.h
 301  * also, to document it.
 302  *
 303  * If you add something that has a short option equivalent, you should
 304  * add it to the getopt_long() call in parseOptions().
 305  */
 306 static struct option cmdlineOptions[] = {${all_modules_long_options}
 307   { NULL, no_argument, NULL, '\0' }
 308 };/* cmdlineOptions */
 309
 310 #line 315 "${template}"
 311
 312 static void preemptGetopt(int& argc, char**& argv, const char* opt) {
 313   const size_t maxoptlen = 128;
 314
 315   Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
 316
 317   AlwaysAssert(opt != NULL && *opt != '\0');
 318   AlwaysAssert(strlen(opt) <= maxoptlen);
 319
 320   ++argc;
 321   unsigned i = 1;
 322   while(argv[i] != NULL && argv[i][0] != '\0') {
 323     ++i;
 324   }
 325
 326   if(argv[i] == NULL) {
 327     argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
 328     for(unsigned j = i; j < i + 5; ++j) {
 329       argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
 330       argv[j][0] = '\0';
 331     }
 332     argv[i + 5] = NULL;
 333   }
 334
 335   strncpy(argv[i], opt, maxoptlen - 1);
 336   argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
 337 }
 338
 339 namespace options {
 340
 341 /** Set a given Options* as "current" just for a particular scope. */
 342 class OptionsGuard {
 343   CVC4_THREADLOCAL_TYPE(Options*)* d_field;
 344   Options* d_old;
 345 public:
 346   OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) :
 347     d_field(field),
 348     d_old(*field) {
 349     *field = opts;
 350   }
 351   ~OptionsGuard() {
 352     *d_field = d_old;
 353   }
 354 };/* class OptionsGuard */
 355
 356 }/* CVC4::options namespace */
 357
 358 /**
 359  * Parse argc/argv and put the result into a CVC4::Options.
 360  * The return value is what's left of the command line (that is, the
 361  * non-option arguments).
 362  */
 363 std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
 364   options::OptionsGuard guard(&s_current, this);
 365
 366   const char *progName = main_argv[0];
 367   SmtEngine* const smt = NULL;
 368
 369   Debug("options") << "main_argv == " << main_argv << std::endl;
 370
 371   // Reset getopt(), in the case of multiple calls to parseOptions().
 372   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
 373   optind = 0;
 374 #if HAVE_DECL_OPTRESET
 375   optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 376 #endif /* HAVE_DECL_OPTRESET */
 377
 378   // find the base name of the program
 379   const char *x = strrchr(progName, '/');
 380   if(x != NULL) {
 381     progName = x + 1;
 382   }
 383   d_holder->binary_name = std::string(progName);
 384
 385   int extra_argc = 1;
 386   char **extra_argv = (char**) malloc(2 * sizeof(char*));
 387   extra_argv[0] = NULL;
 388   extra_argv[1] = NULL;
 389
 390   int extra_optind = 0, main_optind = 0;
 391   int old_optind;
 392   int *optind_ref = &main_optind;
 393
 394   char** argv = main_argv;
 395
 396   std::vector<std::string> nonOptions;
 397
 398   for(;;) {
 399     int c = -1;
 400     optopt = 0;
 401     std::string option, optionarg;
 402     Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl;
 403     if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
 404 #if HAVE_DECL_OPTRESET
 405       if(optind_ref != &extra_optind) {
 406         optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 407       }
 408 #endif /* HAVE_DECL_OPTRESET */
 409       old_optind = optind = extra_optind;
 410       optind_ref = &extra_optind;
 411       argv = extra_argv;
 412       Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl;
 413       if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') {
 414         InternalError("preempted args cannot give non-options command-line args (found `%s')", extra_argv[extra_optind == 0 ? 1 : extra_optind]);
 415       }
 416       c = getopt_long(extra_argc, extra_argv,
 417                       "+:${all_modules_short_options}",
 418                       cmdlineOptions, NULL);
 419       Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl;
 420       if(optopt == 0 ||
 421          ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
 422         // long option
 423         option = argv[old_optind == 0 ? 1 : old_optind];
 424         optionarg = (optarg == NULL) ? "" : optarg;
 425       } else {
 426         // short option
 427         option = std::string("-") + char(optopt);
 428         optionarg = (optarg == NULL) ? "" : optarg;
 429       }
 430       if(optind >= extra_argc) {
 431         Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
 432         unsigned i = 1;
 433         while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') {
 434           extra_argv[i][0] = '\0';
 435           ++i;
 436         }
 437         extra_argc = 1;
 438         extra_optind = 0;
 439       } else {
 440         Debug("preemptGetopt") << "-- more preempt args" << std::endl;
 441         extra_optind = optind;
 442       }
 443     }
 444     if(c == -1) {
 445 #if HAVE_DECL_OPTRESET
 446       if(optind_ref != &main_optind) {
 447         optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 448       }
 449 #endif /* HAVE_DECL_OPTRESET */
 450       old_optind = optind = main_optind;
 451       optind_ref = &main_optind;
 452       argv = main_argv;
 453       if(main_optind < argc && main_argv[main_optind][0] != '-') {
 454         do {
 455           if(main_optind != 0) {
 456             nonOptions.push_back(main_argv[main_optind]);
 457           }
 458           ++main_optind;
 459         } while(main_optind < argc && main_argv[main_optind][0] != '-');
 460         continue;
 461       }
 462       Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
 463 #if defined(__MINGW32__) || defined(__MINGW64__)
 464       if(optreset == 1 && optind > 1) {
 465         // on mingw, optreset will reset the optind, so we have to
 466         // manually advance argc, argv
 467         main_argv[optind - 1] = main_argv[0];
 468         argv = main_argv += optind - 1;
 469         argc -= optind - 1;
 470         old_optind = optind = main_optind = 1;
 471         if(argc > 0) {
 472           Debug("options") << "looking at : " << argv[0] << std::endl;
 473         }
 474         /*c = getopt_long(argc, main_argv,
 475                         "+:${all_modules_short_options}",
 476                         cmdlineOptions, NULL);
 477         Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl;
 478         Debug("options") << "optind was reset to " << optind << std::endl;
 479         optind = main_optind;
 480         Debug("options") << "I restored optind to " << optind << std::endl;*/
 481       }
 482 #endif /* __MINGW32__ || __MINGW64__ */
 483       Debug("options") << "[ argc == " << argc << ", main_argv == " << main_argv << " ]" << std::endl;
 484       c = getopt_long(argc, main_argv,
 485                       "+:${all_modules_short_options}",
 486                       cmdlineOptions, NULL);
 487       main_optind = optind;
 488       Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" << std::endl;
 489       Debug("options") << "[ next option will be at pos: " << optind << " ]" << std::endl;
 490       if(c == -1) {
 491         Debug("options") << "done with option parsing" << std::endl;
 492         break;
 493       }
 494       option = argv[old_optind == 0 ? 1 : old_optind];
 495       optionarg = (optarg == NULL) ? "" : optarg;
 496     }
 497
 498     Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl;
 499
 500     switch(c) {
 501 ${all_modules_option_handlers}
 502
 503 #line 508 "${template}"
 504
 505     case ':':
 506       // This can be a long or short option, and the way to get at the
 507       // name of it is different.
 508       throw OptionException(std::string("option `") + option + "' missing its required argument");
 509
 510     case '?':
 511     default:
 512       if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) &&
 513           !strncmp(argv[optind - 1], "--thread", 8) &&
 514           strlen(argv[optind - 1]) > 8 ) {
 515         if(! isdigit(argv[optind - 1][8])) {
 516           throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
 517         }
 518         std::vector<std::string>& threadArgv = d_holder->threadArgv;
 519         char *end;
 520         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
 521         if(tnum < 0 || (*end != '\0' && *end != '=')) {
 522           throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
 523         }
 524         if(threadArgv.size() <= size_t(tnum)) {
 525           threadArgv.resize(tnum + 1);
 526         }
 527         if(threadArgv[tnum] != "") {
 528           threadArgv[tnum] += " ";
 529         }
 530         if(*end == '\0') { // e.g., we have --thread0 "foo"
 531           if(argc <= optind) {
 532             throw OptionException(std::string("option `") + option + "' missing its required argument");
 533           }
 534           Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl;
 535           threadArgv[tnum] += argv[(*optind_ref)++];
 536         } else { // e.g., we have --thread0="foo"
 537           if(end[1] == '\0') {
 538             throw OptionException(std::string("option `") + option + "' missing its required argument");
 539           }
 540           Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl;
 541           threadArgv[tnum] += end + 1;
 542         }
 543         Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] << std::endl;
 544         break;
 545       }
 546
 547       throw OptionException(std::string("can't understand option `") + option + "'");
 548     }
 549   }
 550
 551   if((*this)[options::incrementalSolving] && (*this)[options::proof]) {
 552     throw OptionException(std::string("The use of --incremental with --proof is not yet supported"));
 553   }
 554
 555   Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
 556
 557   return nonOptions;
 558 }
 559
 560 std::vector<std::string> Options::suggestCommandLineOptions(const std::string& optionName) throw() {
 561   std::vector<std::string> suggestions;
 562
 563   const char* opt;
 564   for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
 565     if(std::strstr(opt, optionName.c_str()) != NULL) {
 566       suggestions.push_back(opt);
 567     }
 568   }
 569
 570   return suggestions;
 571 }
 572
 573 static const char* smtOptions[] = {
 574   ${all_modules_smt_options},
 575 #line 590 "${template}"
 576   NULL
 577 };/* smtOptions[] */
 578
 579 std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
 580   std::vector<std::string> suggestions;
 581
 582   const char* opt;
 583   for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
 584     if(std::strstr(opt, optionName.c_str()) != NULL) {
 585       suggestions.push_back(opt);
 586     }
 587   }
 588
 589   return suggestions;
 590 }
 591
 592 SExpr Options::getOptions() const throw() {
 593   std::vector<SExpr> opts;
 594
 595   ${all_modules_get_options}
 596
 597 #line 612 "${template}"
 598
 599   return SExpr(opts);
 600 }
 601
 602 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 603 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 604
 605 }/* CVC4 namespace */