GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/interactive_shell.cpp Lines: 59 88 67.0 %
Date: 2021-03-23 Branches: 105 299 35.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file interactive_shell.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Christopher L. Conway, Andrew V. Jones
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 Interactive shell for CVC4
13
 **
14
 ** This file is the implementation for the CVC4 interactive shell.
15
 ** The shell supports the editline library.
16
 **/
17
#include "main/interactive_shell.h"
18
19
#include <algorithm>
20
#include <cstdlib>
21
#include <iostream>
22
#include <set>
23
#include <string.h>
24
#include <string>
25
#include <utility>
26
#include <vector>
27
28
// This must go before HAVE_LIBEDITLINE.
29
#include "cvc4autoconfig.h"
30
31
#if HAVE_LIBEDITLINE
32
#include <editline/readline.h>
33
#  if HAVE_EXT_STDIO_FILEBUF_H
34
#    include <ext/stdio_filebuf.h>
35
#  endif /* HAVE_EXT_STDIO_FILEBUF_H */
36
#endif   /* HAVE_LIBEDITLINE */
37
38
#include "api/cvc4cpp.h"
39
#include "base/check.h"
40
#include "base/output.h"
41
#include "expr/symbol_manager.h"
42
#include "options/language.h"
43
#include "options/options.h"
44
#include "parser/input.h"
45
#include "parser/parser.h"
46
#include "parser/parser_builder.h"
47
#include "smt/command.h"
48
#include "theory/logic_info.h"
49
50
using namespace std;
51
52
namespace CVC4 {
53
54
using namespace parser;
55
using namespace language;
56
57
8889
const string InteractiveShell::INPUT_FILENAME = "<shell>";
58
59
#if HAVE_LIBEDITLINE
60
61
#if HAVE_EXT_STDIO_FILEBUF_H
62
using __gnu_cxx::stdio_filebuf;
63
#endif /* HAVE_EXT_STDIO_FILEBUF_H */
64
65
char** commandCompletion(const char* text, int start, int end);
66
char* commandGenerator(const char* text, int state);
67
68
static const std::string cvc_commands[] = {
69
#include "main/cvc_tokens.h"
70
};/* cvc_commands */
71
72
static const std::string smt2_commands[] = {
73
#include "main/smt2_tokens.h"
74
};/* smt2_commands */
75
76
static const std::string tptp_commands[] = {
77
#include "main/tptp_tokens.h"
78
};/* tptp_commands */
79
80
static const std::string* commandsBegin;
81
static const std::string* commandsEnd;
82
83
static set<string> s_declarations;
84
85
#endif /* HAVE_LIBEDITLINE */
86
87
12
InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
88
12
    : d_options(solver->getOptions()),
89
12
      d_in(*d_options.getIn()),
90
12
      d_out(*d_options.getOutConst()),
91
36
      d_quit(false)
92
{
93
24
  ParserBuilder parserBuilder(solver, sm, INPUT_FILENAME, d_options);
94
  /* Create parser with bogus input. */
95
12
  d_parser = parserBuilder.withStringInput("").build();
96
12
  if(d_options.wasSetByUserForceLogicString()) {
97
    LogicInfo tmp(d_options.getForceLogicString());
98
    d_parser->forceLogic(tmp.getLogicString());
99
  }
100
101
#if HAVE_LIBEDITLINE
102
  if(&d_in == &cin) {
103
    ::rl_readline_name = const_cast<char*>("CVC4");
104
#if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP
105
    ::rl_completion_entry_function = commandGenerator;
106
#else /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
107
    ::rl_completion_entry_function = (int (*)(const char*, int)) commandGenerator;
108
#endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
109
    ::using_history();
110
111
    OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
112
    switch(lang) {
113
    case output::LANG_CVC4:
114
      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
115
      commandsBegin = cvc_commands;
116
      commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
117
      break;
118
    case output::LANG_TPTP:
119
      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
120
      commandsBegin = tptp_commands;
121
      commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
122
      break;
123
    default:
124
      if (language::isOutputLang_smt2(lang))
125
      {
126
        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
127
        commandsBegin = smt2_commands;
128
        commandsEnd =
129
            smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
130
      }
131
      else
132
      {
133
        std::stringstream ss;
134
        ss << "internal error: unhandled language " << lang;
135
        throw Exception(ss.str());
136
      }
137
    }
138
    d_usingEditline = true;
139
    int err = ::read_history(d_historyFilename.c_str());
140
    ::stifle_history(s_historyLimit);
141
    if(Notice.isOn()) {
142
      if(err == 0) {
143
        Notice() << "Read " << ::history_length << " lines of history from "
144
                 << d_historyFilename << std::endl;
145
      } else {
146
        Notice() << "Could not read history from " << d_historyFilename
147
                 << ": " << strerror(err) << std::endl;
148
      }
149
    }
150
  } else {
151
    d_usingEditline = false;
152
  }
153
#else  /* HAVE_LIBEDITLINE */
154
12
  d_usingEditline = false;
155
#endif /* HAVE_LIBEDITLINE */
156
12
}/* InteractiveShell::InteractiveShell() */
157
158
24
InteractiveShell::~InteractiveShell() {
159
#if HAVE_LIBEDITLINE
160
  int err = ::write_history(d_historyFilename.c_str());
161
  if(err == 0) {
162
    Notice() << "Wrote " << ::history_length << " lines of history to "
163
             << d_historyFilename << std::endl;
164
  } else {
165
    Notice() << "Could not write history to " << d_historyFilename
166
             << ": " << strerror(err) << std::endl;
167
  }
168
#endif /* HAVE_LIBEDITLINE */
169
12
  delete d_parser;
170
12
}
171
172
28
Command* InteractiveShell::readCommand()
173
{
174
28
  char* lineBuf = NULL;
175
56
  string line = "";
176
177
28
restart:
178
179
  /* Don't do anything if the input is closed or if we've seen a
180
   * QuitCommand. */
181
28
  if(d_in.eof() || d_quit) {
182
    d_out << endl;
183
    return NULL;
184
  }
185
186
  /* If something's wrong with the input, there's nothing we can do. */
187
28
  if( !d_in.good() ) {
188
    throw ParserException("Interactive input broken.");
189
  }
190
191
  /* Prompt the user for input. */
192
28
  if (d_usingEditline)
193
  {
194
#if HAVE_LIBEDITLINE
195
    lineBuf = ::readline(d_options.getInteractivePrompt()
196
                         ? (line == "" ? "CVC4> " : "... > ") : "");
197
    if(lineBuf != NULL && lineBuf[0] != '\0') {
198
      ::add_history(lineBuf);
199
    }
200
    line += lineBuf == NULL ? "" : lineBuf;
201
    free(lineBuf);
202
#endif /* HAVE_LIBEDITLINE */
203
  }
204
  else
205
  {
206
28
    if(d_options.getInteractivePrompt()) {
207
28
      if(line == "") {
208
28
        d_out << "CVC4> " << flush;
209
      } else {
210
        d_out << "... > " << flush;
211
      }
212
    }
213
214
    /* Read a line */
215
56
    stringbuf sb;
216
28
    d_in.get(sb);
217
28
    line += sb.str();
218
  }
219
220
28
  string input = "";
221
  while(true) {
222
56
    Debug("interactive") << "Input now '" << input << line << "'" << endl
223
28
                         << flush;
224
225
28
    Assert(!(d_in.fail() && !d_in.eof()) || line.empty());
226
227
    /* Check for failure. */
228
28
    if(d_in.fail() && !d_in.eof()) {
229
      /* This should only happen if the input line was empty. */
230
6
      Assert(line.empty());
231
6
      d_in.clear();
232
    }
233
234
    /* Strip trailing whitespace. */
235
28
    int n = line.length() - 1;
236
28
    while( !line.empty() && isspace(line[n]) ) {
237
      line.erase(n,1);
238
      n--;
239
    }
240
241
    /* If we hit EOF, we're done. */
242
84
    if ((!d_usingEditline && d_in.eof())
243
44
        || (d_usingEditline && lineBuf == NULL))
244
    {
245
12
      input += line;
246
247
12
      if(input.empty()) {
248
        /* Nothing left to parse. */
249
12
        d_out << endl;
250
12
        return NULL;
251
      }
252
253
      /* Some input left to parse, but nothing left to read.
254
         Jump out of input loop. */
255
      d_out << endl;
256
      input = line = "";
257
      d_in.clear();
258
      goto restart;
259
    }
260
261
16
    if (!d_usingEditline)
262
    {
263
      /* Extract the newline delimiter from the stream too */
264
16
      int c CVC4_UNUSED = d_in.get();
265
16
      Assert(c == '\n');
266
32
      Debug("interactive") << "Next char is '" << (char)c << "'" << endl
267
16
                           << flush;
268
    }
269
270
16
    input += line;
271
272
    /* If the last char was a backslash, continue on the next line. */
273
16
    n = input.length() - 1;
274
16
    if( !line.empty() && input[n] == '\\' ) {
275
      input[n] = '\n';
276
      if (d_usingEditline)
277
      {
278
#if HAVE_LIBEDITLINE
279
        lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
280
        if(lineBuf != NULL && lineBuf[0] != '\0') {
281
          ::add_history(lineBuf);
282
        }
283
        line = lineBuf == NULL ? "" : lineBuf;
284
        free(lineBuf);
285
#endif /* HAVE_LIBEDITLINE */
286
      }
287
      else
288
      {
289
        if(d_options.getInteractivePrompt()) {
290
          d_out << "... > " << flush;
291
        }
292
293
        /* Read a line */
294
        stringbuf sb;
295
        d_in.get(sb);
296
        line = sb.str();
297
      }
298
    } else {
299
      /* No continuation, we're done. */
300
16
      Debug("interactive") << "Leaving input loop." << endl << flush;
301
16
      break;
302
    }
303
  }
304
305
16
  d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
306
                                           input, INPUT_FILENAME));
307
308
  /* There may be more than one command in the input. Build up a
309
     sequence. */
310
16
  CommandSequence *cmd_seq = new CommandSequence();
311
  Command *cmd;
312
313
  try
314
  {
315
40
    while ((cmd = d_parser->nextCommand()))
316
    {
317
12
      cmd_seq->addCommand(cmd);
318
12
      if (dynamic_cast<QuitCommand*>(cmd) != NULL)
319
      {
320
        d_quit = true;
321
        break;
322
      }
323
      else
324
      {
325
#if HAVE_LIBEDITLINE
326
        if (dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL)
327
        {
328
          s_declarations.insert(
329
              dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
330
        }
331
        else if (dynamic_cast<DefineFunctionCommand*>(cmd) != NULL)
332
        {
333
          s_declarations.insert(
334
              dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
335
        }
336
        else if (dynamic_cast<DeclareSortCommand*>(cmd) != NULL)
337
        {
338
          s_declarations.insert(
339
              dynamic_cast<DeclareSortCommand*>(cmd)->getSymbol());
340
        }
341
        else if (dynamic_cast<DefineSortCommand*>(cmd) != NULL)
342
        {
343
          s_declarations.insert(
344
              dynamic_cast<DefineSortCommand*>(cmd)->getSymbol());
345
        }
346
#endif /* HAVE_LIBEDITLINE */
347
      }
348
    }
349
  }
350
  catch (ParserEndOfFileException& pe)
351
  {
352
    line += "\n";
353
    goto restart;
354
  }
355
  catch (ParserException& pe)
356
  {
357
    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
358
    {
359
      d_out << "(error \"" << pe << "\")" << endl;
360
    }
361
    else
362
    {
363
      d_out << pe << endl;
364
    }
365
    // We can't really clear out the sequence and abort the current line,
366
    // because the parse error might be for the second command on the
367
    // line.  The first ones haven't yet been executed by the SmtEngine,
368
    // but the parser state has already made the variables and the mappings
369
    // in the symbol table.  So unfortunately, either we exit CVC4 entirely,
370
    // or we commit to the current line up to the command with the parse
371
    // error.
372
    //
373
    // FIXME: does that mean e.g. that a pushed LET scope might not yet have
374
    // been popped?!
375
    //
376
    // delete cmd_seq;
377
    // cmd_seq = new CommandSequence();
378
  }
379
380
16
  return cmd_seq;
381
}/* InteractiveShell::readCommand() */
382
383
#if HAVE_LIBEDITLINE
384
385
char** commandCompletion(const char* text, int start, int end) {
386
  Debug("rl") << "text: " << text << endl;
387
  Debug("rl") << "start: " << start << " end: " << end << endl;
388
  return rl_completion_matches(text, commandGenerator);
389
}
390
391
// Our peculiar versions of "less than" for strings
392
struct StringPrefix1Less {
393
  bool operator()(const std::string& s1, const std::string& s2) {
394
    size_t l1 = s1.length(), l2 = s2.length();
395
    size_t l = l1 <= l2 ? l1 : l2;
396
    return s1.compare(0, l1, s2, 0, l) < 0;
397
  }
398
};/* struct StringPrefix1Less */
399
struct StringPrefix2Less {
400
  bool operator()(const std::string& s1, const std::string& s2) {
401
    size_t l1 = s1.length(), l2 = s2.length();
402
    size_t l = l1 <= l2 ? l1 : l2;
403
    return s1.compare(0, l, s2, 0, l2) < 0;
404
  }
405
};/* struct StringPrefix2Less */
406
407
char* commandGenerator(const char* text, int state) {
408
  static thread_local const std::string* rlCommand;
409
  static thread_local set<string>::const_iterator* rlDeclaration;
410
411
  const std::string* i = lower_bound(commandsBegin, commandsEnd, text, StringPrefix2Less());
412
  const std::string* j = upper_bound(commandsBegin, commandsEnd, text, StringPrefix1Less());
413
414
  set<string>::const_iterator ii = lower_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix2Less());
415
  set<string>::const_iterator jj = upper_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix1Less());
416
417
  if(rlDeclaration == NULL) {
418
    rlDeclaration = new set<string>::const_iterator();
419
  }
420
421
  if(state == 0) {
422
    rlCommand = i;
423
    *rlDeclaration = ii;
424
  }
425
426
  if(rlCommand != j) {
427
    return strdup((*rlCommand++).c_str());
428
  }
429
430
  return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
431
}
432
433
#endif /* HAVE_LIBEDITLINE */
434
435
26667
}/* CVC4 namespace */