GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/driver_unified.cpp Lines: 76 241 31.5 %
Date: 2021-03-23 Branches: 113 650 17.4 %

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