GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/driver_unified.cpp Lines: 85 250 34.0 %
Date: 2021-03-22 Branches: 119 662 18.0 %

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