src/main/driver_unified.cpp

   1 /*********************                                                        */
   2 /*! \file driver_unified.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Liana Hadarean, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Driver for CVC4 executable (cvc4)
  13  **/
  14
  15 #include <stdio.h>
  16 #include <unistd.h>
  17
  18 #include <cstdlib>
  19 #include <cstring>
  20 #include <fstream>
  21 #include <iostream>
  22 #include <memory>
  23 #include <new>
  24
  25 #include "cvc4autoconfig.h"
  26
  27 #include "api/cvc4cpp.h"
  28 #include "base/configuration.h"
  29 #include "base/output.h"
  30 #include "main/command_executor.h"
  31 #include "main/interactive_shell.h"
  32 #include "main/main.h"
  33 #include "main/signal_handlers.h"
  34 #include "main/time_limit.h"
  35 #include "options/options.h"
  36 #include "options/set_language.h"
  37 #include "parser/parser.h"
  38 #include "parser/parser_builder.h"
  39 #include "parser/parser_exception.h"
  40 #include "smt/command.h"
  41 #include "util/result.h"
  42 #include "util/statistics_registry.h"
  43
  44 using namespace std;
  45 using namespace CVC4;
  46 using namespace CVC4::parser;
  47 using namespace CVC4::main;
  48
  49 namespace CVC4 {
  50   namespace main {
  51     /** Global options variable */
  52     thread_local Options* pOptions;
  53
  54     /** Full argv[0] */
  55     const char *progPath;
  56
  57     /** Just the basename component of argv[0] */
  58     const std::string *progName;
  59
  60     /** A pointer to the CommandExecutor (the signal handlers need it) */
  61     CVC4::main::CommandExecutor* pExecutor = nullptr;
  62
  63     /** A pointer to the totalTime driver stat (the signal handlers need it) */
  64     CVC4::TimerStat* pTotalTime = nullptr;
  65
  66   }/* CVC4::main namespace */
  67 }/* CVC4 namespace */
  68
  69
  70 void printUsage(Options& opts, bool full) {
  71   stringstream ss;
  72   ss << "usage: " << opts.getBinaryName() << " [options] [input-file]"
  73      << endl << endl
  74      << "Without an input file, or with `-', CVC4 reads from standard input."
  75      << endl << endl
  76      << "CVC4 options:" << endl;
  77   if(full) {
  78     Options::printUsage( ss.str(), *(opts.getOut()) );
  79   } else {
  80     Options::printShortUsage( ss.str(), *(opts.getOut()) );
  81   }
  82 }
  83
  84 int runCvc4(int argc, char* argv[], Options& opts) {
  85
  86   // Timer statistic
  87   pTotalTime = new TimerStat("totalTime");
  88   pTotalTime->start();
  89
  90   // For the signal handlers' benefit
  91   pOptions = &opts;
  92
  93   // Initialize the signal handlers
  94   signal_handlers::install();
  95
  96   progPath = argv[0];
  97
  98   // Parse the options
  99   vector<string> filenames = Options::parseOptions(&opts, argc, argv);
 100
 101   auto limit = install_time_limit(opts);
 102
 103   string progNameStr = opts.getBinaryName();
 104   progName = &progNameStr;
 105
 106   if( opts.getHelp() ) {
 107     printUsage(opts, true);
 108     exit(1);
 109   } else if( opts.getLanguageHelp() ) {
 110     Options::printLanguageHelp(*(opts.getOut()));
 111     exit(1);
 112   } else if( opts.getVersion() ) {
 113     *(opts.getOut()) << Configuration::about().c_str() << flush;
 114     exit(0);
 115   }
 116
 117   segvSpin = opts.getSegvSpin();
 118
 119   // If in competition mode, set output stream option to flush immediately
 120 #ifdef CVC4_COMPETITION_MODE
 121   *(opts.getOut()) << unitbuf;
 122 #endif /* CVC4_COMPETITION_MODE */
 123
 124   // We only accept one input file
 125   if(filenames.size() > 1) {
 126     throw Exception("Too many input files specified.");
 127   }
 128
 129   // If no file supplied we will read from standard input
 130   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 131
 132   // if we're reading from stdin on a TTY, default to interactive mode
 133   if(!opts.wasSetByUserInteractive()) {
 134     opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
 135   }
 136
 137   // Auto-detect input language by filename extension
 138   std::string filenameStr("<stdin>");
 139   if (!inputFromStdin) {
 140     // Use swap to avoid copying the string
 141     // TODO: use std::move() when switching to c++11
 142     filenameStr.swap(filenames[0]);
 143   }
 144   const char* filename = filenameStr.c_str();
 145
 146   if(opts.getInputLanguage() == language::input::LANG_AUTO) {
 147     if( inputFromStdin ) {
 148       // We can't do any fancy detection on stdin
 149       opts.setInputLanguage(language::input::LANG_CVC4);
 150     } else {
 151       unsigned len = filenameStr.size();
 152       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 153         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
 154       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 155                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 156         opts.setInputLanguage(language::input::LANG_TPTP);
 157       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 158                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 159         opts.setInputLanguage(language::input::LANG_CVC4);
 160       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 161                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 162         // version 2 sygus is the default
 163         opts.setInputLanguage(language::input::LANG_SYGUS_V2);
 164       }
 165     }
 166   }
 167
 168   if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
 169     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
 170   }
 171
 172   // Determine which messages to show based on smtcomp_mode and verbosity
 173   if(Configuration::isMuzzledBuild()) {
 174     DebugChannel.setStream(&CVC4::null_os);
 175     TraceChannel.setStream(&CVC4::null_os);
 176     NoticeChannel.setStream(&CVC4::null_os);
 177     ChatChannel.setStream(&CVC4::null_os);
 178     MessageChannel.setStream(&CVC4::null_os);
 179     WarningChannel.setStream(&CVC4::null_os);
 180   }
 181
 182   // important even for muzzled builds (to get result output right)
 183   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 184
 185   // Create the command executor to execute the parsed commands
 186   pExecutor = new CommandExecutor(opts);
 187
 188   int returnValue = 0;
 189   {
 190     // Timer statistic
 191     RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(),
 192                                     pTotalTime);
 193
 194     // Filename statistics
 195     ReferenceStat<std::string> s_statFilename("filename", filenameStr);
 196     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
 197                                       &s_statFilename);
 198     // notify SmtEngine that we are starting to parse
 199     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 200
 201     // Parse and execute commands until we are done
 202     std::unique_ptr<Command> cmd;
 203     bool status = true;
 204     if(opts.getInteractive() && inputFromStdin) {
 205       if(opts.getTearDownIncremental() > 0) {
 206         throw OptionException(
 207             "--tear-down-incremental doesn't work in interactive mode");
 208       }
 209       if(!opts.wasSetByUserIncrementalSolving()) {
 210         cmd.reset(new SetOptionCommand("incremental", "true"));
 211         cmd->setMuted(true);
 212         pExecutor->doCommand(cmd);
 213       }
 214       InteractiveShell shell(pExecutor->getSolver(),
 215                              pExecutor->getSymbolManager());
 216       if(opts.getInteractivePrompt()) {
 217         CVC4Message() << Configuration::getPackageName() << " "
 218                       << Configuration::getVersionString();
 219         if(Configuration::isGitBuild()) {
 220           CVC4Message() << " [" << Configuration::getGitId() << "]";
 221         }
 222         CVC4Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 223                       << " assertions:"
 224                       << (Configuration::isAssertionBuild() ? "on" : "off")
 225                       << endl
 226                       << endl;
 227         CVC4Message() << Configuration::copyright() << endl;
 228       }
 229
 230       while(true) {
 231         try {
 232           cmd.reset(shell.readCommand());
 233         } catch(UnsafeInterruptException& e) {
 234           (*opts.getOut()) << CommandInterrupted();
 235           break;
 236         }
 237         if (cmd == nullptr)
 238           break;
 239         status = pExecutor->doCommand(cmd) && status;
 240         if (cmd->interrupted()) {
 241           break;
 242         }
 243       }
 244     } else if( opts.getTearDownIncremental() > 0) {
 245       if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
 246         // For tear-down-incremental values greater than 1, need incremental
 247         // on too.
 248         cmd.reset(new SetOptionCommand("incremental", "true"));
 249         cmd->setMuted(true);
 250         pExecutor->doCommand(cmd);
 251         // if(opts.wasSetByUserIncrementalSolving()) {
 252         //   throw OptionException(
 253         //     "--tear-down-incremental incompatible with --incremental");
 254         // }
 255
 256         // cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
 257         // cmd->setMuted(true);
 258         // pExecutor->doCommand(cmd);
 259       }
 260
 261       ParserBuilder parserBuilder(pExecutor->getSolver(),
 262                                   pExecutor->getSymbolManager(),
 263                                   filename,
 264                                   opts);
 265
 266       if( inputFromStdin ) {
 267 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 268         parserBuilder.withStreamInput(cin);
 269 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 270         parserBuilder.withLineBufferedStreamInput(cin);
 271 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 272       }
 273
 274       vector< vector<Command*> > allCommands;
 275       allCommands.push_back(vector<Command*>());
 276       std::unique_ptr<Parser> parser(parserBuilder.build());
 277       int needReset = 0;
 278       // true if one of the commands was interrupted
 279       bool interrupted = false;
 280       while (status)
 281       {
 282         if (interrupted) {
 283           (*opts.getOut()) << CommandInterrupted();
 284           break;
 285         }
 286
 287         try {
 288           cmd.reset(parser->nextCommand());
 289           if (cmd == nullptr) break;
 290         } catch (UnsafeInterruptException& e) {
 291           interrupted = true;
 292           continue;
 293         }
 294
 295         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
 296           if(needReset >= opts.getTearDownIncremental()) {
 297             pExecutor->reset();
 298             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 299               if (interrupted) break;
 300               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 301               {
 302                 Command* ccmd = allCommands[i][j]->clone();
 303                 ccmd->setMuted(true);
 304                 pExecutor->doCommand(ccmd);
 305                 if (ccmd->interrupted())
 306                 {
 307                   interrupted = true;
 308                 }
 309                 delete ccmd;
 310               }
 311             }
 312             needReset = 0;
 313           }
 314           allCommands.push_back(vector<Command*>());
 315           Command* copy = cmd->clone();
 316           allCommands.back().push_back(copy);
 317           status = pExecutor->doCommand(cmd);
 318           if(cmd->interrupted()) {
 319             interrupted = true;
 320             continue;
 321           }
 322         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
 323           allCommands.pop_back(); // fixme leaks cmds here
 324           if (needReset >= opts.getTearDownIncremental()) {
 325             pExecutor->reset();
 326             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 327               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 328               {
 329                 std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
 330                 ccmd->setMuted(true);
 331                 pExecutor->doCommand(ccmd);
 332                 if (ccmd->interrupted())
 333                 {
 334                   interrupted = true;
 335                 }
 336               }
 337             }
 338             if (interrupted) continue;
 339             (*opts.getOut()) << CommandSuccess();
 340             needReset = 0;
 341           } else {
 342             status = pExecutor->doCommand(cmd);
 343             if(cmd->interrupted()) {
 344               interrupted = true;
 345               continue;
 346             }
 347           }
 348         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
 349                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
 350           if(needReset >= opts.getTearDownIncremental()) {
 351             pExecutor->reset();
 352             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 353               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 354               {
 355                 Command* ccmd = allCommands[i][j]->clone();
 356                 ccmd->setMuted(true);
 357                 pExecutor->doCommand(ccmd);
 358                 if (ccmd->interrupted())
 359                 {
 360                   interrupted = true;
 361                 }
 362                 delete ccmd;
 363               }
 364             }
 365             needReset = 0;
 366           } else {
 367             ++needReset;
 368           }
 369           if (interrupted) {
 370             continue;
 371           }
 372
 373           status = pExecutor->doCommand(cmd);
 374           if(cmd->interrupted()) {
 375             interrupted = true;
 376             continue;
 377           }
 378         } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
 379           pExecutor->doCommand(cmd);
 380           allCommands.clear();
 381           allCommands.push_back(vector<Command*>());
 382         } else {
 383           // We shouldn't copy certain commands, because they can cause
 384           // an error on replay since there's no associated sat/unsat check
 385           // preceding them.
 386           if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
 387              dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
 388              dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
 389              dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
 390              dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
 391              dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
 392              dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
 393              dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
 394              dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
 395              dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
 396             Command* copy = cmd->clone();
 397             allCommands.back().push_back(copy);
 398           }
 399           status = pExecutor->doCommand(cmd);
 400           if(cmd->interrupted()) {
 401             interrupted = true;
 402             continue;
 403           }
 404
 405           if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 406             break;
 407           }
 408         }
 409       }
 410     } else {
 411       if(!opts.wasSetByUserIncrementalSolving()) {
 412         cmd.reset(new SetOptionCommand("incremental", "false"));
 413         cmd->setMuted(true);
 414         pExecutor->doCommand(cmd);
 415       }
 416
 417       ParserBuilder parserBuilder(pExecutor->getSolver(),
 418                                   pExecutor->getSymbolManager(),
 419                                   filename,
 420                                   opts);
 421
 422       if( inputFromStdin ) {
 423 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 424         parserBuilder.withStreamInput(cin);
 425 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 426         parserBuilder.withLineBufferedStreamInput(cin);
 427 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 428       }
 429
 430       std::unique_ptr<Parser> parser(parserBuilder.build());
 431       bool interrupted = false;
 432       while (status)
 433       {
 434         if (interrupted) {
 435           (*opts.getOut()) << CommandInterrupted();
 436           pExecutor->reset();
 437           break;
 438         }
 439         try {
 440           cmd.reset(parser->nextCommand());
 441           if (cmd == nullptr) break;
 442         } catch (UnsafeInterruptException& e) {
 443           interrupted = true;
 444           continue;
 445         }
 446
 447         status = pExecutor->doCommand(cmd);
 448         if (cmd->interrupted() && status == 0) {
 449           interrupted = true;
 450           break;
 451         }
 452
 453         if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 454           break;
 455         }
 456       }
 457     }
 458
 459     api::Result result;
 460     if(status) {
 461       result = pExecutor->getResult();
 462       returnValue = 0;
 463     } else {
 464       // there was some kind of error
 465       returnValue = 1;
 466     }
 467
 468 #ifdef CVC4_COMPETITION_MODE
 469     opts.flushOut();
 470     // exit, don't return (don't want destructors to run)
 471     // _exit() from unistd.h doesn't run global destructors
 472     // or other on_exit/atexit stuff.
 473     _exit(returnValue);
 474 #endif /* CVC4_COMPETITION_MODE */
 475
 476     ReferenceStat<api::Result> s_statSatResult("sat/unsat", result);
 477     RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
 478                                        &s_statSatResult);
 479
 480     pTotalTime->stop();
 481
 482     // Tim: I think that following comment is out of date?
 483     // Set the global executor pointer to nullptr first.  If we get a
 484     // signal while dumping statistics, we don't want to try again.
 485     pExecutor->flushOutputStreams();
 486
 487 #ifdef CVC4_DEBUG
 488     if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
 489       _exit(returnValue);
 490     }
 491 #else /* CVC4_DEBUG */
 492     if(opts.getEarlyExit()) {
 493       _exit(returnValue);
 494     }
 495 #endif /* CVC4_DEBUG */
 496   }
 497
 498   // On exceptional exit, these are leaked, but that's okay... they
 499   // need to be around in that case for main() to print statistics.
 500   delete pTotalTime;
 501   delete pExecutor;
 502
 503   pTotalTime = nullptr;
 504   pExecutor = nullptr;
 505
 506   signal_handlers::cleanup();
 507
 508   return returnValue;
 509 }