Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/main/driver_unified.cpp	Lines:	74	137	54.0 %
Date:	2021-09-21	Branches:	138	458	30.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Liana Hadarean, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Driver for cvc5 executable (cvc5).
 */

#include <stdio.h>
#include <unistd.h>

#include <cstdlib>
#include <cstring>
#include <fstream>
#include <iostream>
#include <memory>
#include <new>

#include "api/cpp/cvc5.h"
#include "base/configuration.h"
#include "base/cvc5config.h"
#include "base/output.h"
#include "main/command_executor.h"
#include "main/interactive_shell.h"
#include "main/main.h"
#include "main/options.h"
#include "main/signal_handlers.h"
#include "main/time_limit.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
#include "smt/smt_engine.h"
#include "util/result.h"

using namespace std;
using namespace cvc5;
using namespace cvc5::parser;
using namespace cvc5::main;

namespace cvc5 {
namespace main {

/** Full argv[0] */
const char* progPath;

/** Just the basename component of argv[0] */
std::string progName;

/** A pointer to the CommandExecutor (the signal handlers need it) */
std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;

}  // namespace main
}  // namespace cvc5

    void printUsage(const api::DriverOptions& dopts, bool full)
    {
      std::stringstream ss;
      ss << "usage: " << progName << " [options] [input-file]" << std::endl
         << std::endl
         << "Without an input file, or with `-', cvc5 reads from standard "
            "input."
         << std::endl
         << std::endl
         << "cvc5 options:" << std::endl;
      if (full)
      {
        main::printUsage(ss.str(), dopts.out());
      }
      else
      {
        main::printShortUsage(ss.str(), dopts.out());
      }
    }

int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
{
  // Initialize the signal handlers
  signal_handlers::install();

  progPath = argv[0];

  // Create the command executor to execute the parsed commands
  pExecutor = std::make_unique<CommandExecutor>(solver);
  api::DriverOptions dopts = solver->getDriverOptions();

  // Parse the options
  std::vector<string> filenames = main::parse(*solver, argc, argv, progName);

  auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue());

  if (solver->getOptionInfo("help").boolValue())
  {
    printUsage(dopts, true);
    exit(1);
  }
  else if (solver->getOptionInfo("language-help").boolValue())
  {
    main::printLanguageHelp(dopts.out());
    exit(1);
  }
  else if (solver->getOptionInfo("version").boolValue())
  {
    dopts.out() << Configuration::about().c_str() << flush;
    exit(0);
  }

  segvSpin = solver->getOptionInfo("segv-spin").boolValue();

  // If in competition mode, set output stream option to flush immediately
#ifdef CVC5_COMPETITION_MODE
  dopts.out() << unitbuf;
#endif /* CVC5_COMPETITION_MODE */

  // We only accept one input file
  if(filenames.size() > 1) {
    throw Exception("Too many input files specified.");
  }

  // If no file supplied we will read from standard input
  const bool inputFromStdin = filenames.empty() || filenames[0] == "-";

  // if we're reading from stdin on a TTY, default to interactive mode
  if (!solver->getOptionInfo("interactive").setByUser)
  {
    solver->setOption("interactive", (inputFromStdin && isatty(fileno(stdin))) ? "true" : "false");
  }

  // Auto-detect input language by filename extension
  std::string filenameStr("<stdin>");
  if (!inputFromStdin) {
    filenameStr = std::move(filenames[0]);
  }
  const char* filename = filenameStr.c_str();

  if (solver->getOption("input-language") == "LANG_AUTO")
  {
    if( inputFromStdin ) {
      // We can't do any fancy detection on stdin
      solver->setOption("input-language", "cvc");
    } else {
      size_t len = filenameStr.size();
      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
        solver->setOption("input-language", "smt2");
      } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
        solver->setOption("input-language", "tptp");
      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
        solver->setOption("input-language", "cvc");
      } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
        // version 2 sygus is the default
        solver->setOption("input-language", "sygus2");
      }
    }
  }

  if (solver->getOption("output-language") == "LANG_AUTO")
  {
    solver->setOption("output-language", solver->getOption("input-language"));
  }
  pExecutor->storeOptionsAsOriginal();

  // Determine which messages to show based on smtcomp_mode and verbosity
  if(Configuration::isMuzzledBuild()) {
    DebugChannel.setStream(&cvc5::null_os);
    TraceChannel.setStream(&cvc5::null_os);
    NoticeChannel.setStream(&cvc5::null_os);
    ChatChannel.setStream(&cvc5::null_os);
    MessageChannel.setStream(&cvc5::null_os);
    WarningChannel.setStream(&cvc5::null_os);
  }

  int returnValue = 0;
  {
    solver->setInfo("filename", filenameStr);

    // Parse and execute commands until we are done
    std::unique_ptr<Command> cmd;
    bool status = true;
    if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin)
    {
      if (!solver->getOptionInfo("incremental").setByUser)
      {
        cmd.reset(new SetOptionCommand("incremental", "true"));
        cmd->setMuted(true);
        pExecutor->doCommand(cmd);
      }
      InteractiveShell shell(pExecutor->getSolver(),
                             pExecutor->getSymbolManager(),
                             dopts.in(),
                             dopts.out());

      CVC5Message() << Configuration::getPackageName() << " "
                    << Configuration::getVersionString();
      if (Configuration::isGitBuild())
      {
        CVC5Message() << " [" << Configuration::getGitId() << "]";
      }
      CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
                    << " assertions:"
                    << (Configuration::isAssertionBuild() ? "on" : "off")
                    << endl
                    << endl;
      CVC5Message() << Configuration::copyright() << endl;

      while(true) {
        try {
          cmd.reset(shell.readCommand());
        } catch(UnsafeInterruptException& e) {
          dopts.out() << CommandInterrupted();
          break;
        }
        if (cmd == nullptr)
          break;
        status = pExecutor->doCommand(cmd) && status;
        if (cmd->interrupted()) {
          break;
        }
      }
    }
    else
    {
      if (!solver->getOptionInfo("incremental").setByUser)
      {
        cmd.reset(new SetOptionCommand("incremental", "false"));
        cmd->setMuted(true);
        pExecutor->doCommand(cmd);
      }

      ParserBuilder parserBuilder(
          pExecutor->getSolver(), pExecutor->getSymbolManager(), true);
      std::unique_ptr<Parser> parser(parserBuilder.build());
      if( inputFromStdin ) {
        parser->setInput(Input::newStreamInput(
            solver->getOption("input-language"), cin, filename));
      }
      else
      {
        parser->setInput(
            Input::newFileInput(solver->getOption("input-language"),
                                filename,
                                solver->getOptionInfo("mmap").boolValue()));
      }

      bool interrupted = false;
      while (status)
      {
        if (interrupted) {
          dopts.out() << CommandInterrupted();
          pExecutor->reset();
          break;
        }
        try {
          cmd.reset(parser->nextCommand());
          if (cmd == nullptr) break;
        } catch (UnsafeInterruptException& e) {
          interrupted = true;
          continue;
        }

        status = pExecutor->doCommand(cmd);
        if (cmd->interrupted() && status == 0) {
          interrupted = true;
          break;
        }

        if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
          break;
        }
      }
    }

    api::Result result;
    if(status) {
      result = pExecutor->getResult();
      returnValue = 0;
    } else {
      // there was some kind of error
      returnValue = 1;
    }

#ifdef CVC5_COMPETITION_MODE
    dopts.out() << std::flush;
    // exit, don't return (don't want destructors to run)
    // _exit() from unistd.h doesn't run global destructors
    // or other on_exit/atexit stuff.
    _exit(returnValue);
#endif /* CVC5_COMPETITION_MODE */

    pExecutor->flushOutputStreams();

#ifdef CVC5_DEBUG
    {
      auto info = solver->getOptionInfo("early-exit");
      if (info.boolValue() && info.setByUser)
      {
        _exit(returnValue);
      }
    }
#else  /* CVC5_DEBUG */
    if (solver->getOptionInfo("early-exit").boolValue())
    {
      _exit(returnValue);
    }
#endif /* CVC5_DEBUG */
  }

  pExecutor.reset();

  signal_handlers::cleanup();

  return returnValue;
}


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Liana Hadarean, Tim King
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* Driver for cvc5 executable (cvc5).
14		*/
15
16		#include <stdio.h>
17		#include <unistd.h>
18
19		#include <cstdlib>
20		#include <cstring>
21		#include <fstream>
22		#include <iostream>
23		#include <memory>
24		#include <new>
25
26		#include "api/cpp/cvc5.h"
27		#include "base/configuration.h"
28		#include "base/cvc5config.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/options.h"
34		#include "main/signal_handlers.h"
35		#include "main/time_limit.h"
36		#include "parser/parser.h"
37		#include "parser/parser_builder.h"
38		#include "smt/command.h"
39		#include "smt/smt_engine.h"
40		#include "util/result.h"
41
42		using namespace std;
43		using namespace cvc5;
44		using namespace cvc5::parser;
45		using namespace cvc5::main;
46
47		namespace cvc5 {
48		namespace main {
49
50		/** Full argv[0] */
51		const char* progPath;
52
53		/** Just the basename component of argv[0] */
54	9856	std::string progName;
55
56		/** A pointer to the CommandExecutor (the signal handlers need it) */
57	9856	std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
58
59		} // namespace main
60		} // namespace cvc5
61
62		void printUsage(const api::DriverOptions& dopts, bool full)
63		{
64		std::stringstream ss;
65		ss << "usage: " << progName << " [options] [input-file]" << std::endl
66		<< std::endl
67		<< "Without an input file, or with `-', cvc5 reads from standard "
68		"input."
69		<< std::endl
70		<< std::endl
71		<< "cvc5 options:" << std::endl;
72		if (full)
73		{
74		main::printUsage(ss.str(), dopts.out());
75		}
76		else
77		{
78		main::printShortUsage(ss.str(), dopts.out());
79		}
80		}
81
82	8804	int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
83		{
84		// Initialize the signal handlers
85	8804	signal_handlers::install();
86
87	8804	progPath = argv[0];
88
89		// Create the command executor to execute the parsed commands
90	8804	pExecutor = std::make_unique<CommandExecutor>(solver);
91	8804	api::DriverOptions dopts = solver->getDriverOptions();
92
93		// Parse the options
94	14979	std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
95
96	12350	auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue());
97
98	6175	if (solver->getOptionInfo("help").boolValue())
99		{
100		printUsage(dopts, true);
101		exit(1);
102		}
103	6175	else if (solver->getOptionInfo("language-help").boolValue())
104		{
105		main::printLanguageHelp(dopts.out());
106		exit(1);
107		}
108	6175	else if (solver->getOptionInfo("version").boolValue())
109		{
110		dopts.out() << Configuration::about().c_str() << flush;
111		exit(0);
112		}
113
114	6175	segvSpin = solver->getOptionInfo("segv-spin").boolValue();
115
116		// If in competition mode, set output stream option to flush immediately
117		#ifdef CVC5_COMPETITION_MODE
118		dopts.out() << unitbuf;
119		#endif /* CVC5_COMPETITION_MODE */
120
121		// We only accept one input file
122	6175	if(filenames.size() > 1) {
123		throw Exception("Too many input files specified.");
124		}
125
126		// If no file supplied we will read from standard input
127	6175	const bool inputFromStdin = filenames.empty() \|\| filenames[0] == "-";
128
129		// if we're reading from stdin on a TTY, default to interactive mode
130	6175	if (!solver->getOptionInfo("interactive").setByUser)
131		{
132	6175	solver->setOption("interactive", (inputFromStdin && isatty(fileno(stdin))) ? "true" : "false");
133		}
134
135		// Auto-detect input language by filename extension
136	12350	std::string filenameStr("<stdin>");
137	6175	if (!inputFromStdin) {
138	6175	filenameStr = std::move(filenames[0]);
139		}
140	6175	const char* filename = filenameStr.c_str();
141
142	6175	if (solver->getOption("input-language") == "LANG_AUTO")
143		{
144	5949	if( inputFromStdin ) {
145		// We can't do any fancy detection on stdin
146		solver->setOption("input-language", "cvc");
147		} else {
148	5949	size_t len = filenameStr.size();
149	5949	if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
150	5089	solver->setOption("input-language", "smt2");
151	860	} else if((len >= 2 && !strcmp(".p", filename + len - 2))
152	819	\|\| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
153	41	solver->setOption("input-language", "tptp");
154	819	} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
155	16	\|\| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
156	803	solver->setOption("input-language", "cvc");
157	16	} else if((len >= 3 && !strcmp(".sy", filename + len - 3))
158		\|\| (len >= 3 && !strcmp(".sl", filename + len - 3))) {
159		// version 2 sygus is the default
160	16	solver->setOption("input-language", "sygus2");
161		}
162		}
163		}
164
165	6175	if (solver->getOption("output-language") == "LANG_AUTO")
166		{
167	6175	solver->setOption("output-language", solver->getOption("input-language"));
168		}
169	6175	pExecutor->storeOptionsAsOriginal();
170
171		// Determine which messages to show based on smtcomp_mode and verbosity
172	6175	if(Configuration::isMuzzledBuild()) {
173		DebugChannel.setStream(&cvc5::null_os);
174		TraceChannel.setStream(&cvc5::null_os);
175		NoticeChannel.setStream(&cvc5::null_os);
176		ChatChannel.setStream(&cvc5::null_os);
177		MessageChannel.setStream(&cvc5::null_os);
178		WarningChannel.setStream(&cvc5::null_os);
179		}
180
181	6175	int returnValue = 0;
182		{
183	6175	solver->setInfo("filename", filenameStr);
184
185		// Parse and execute commands until we are done
186	12350	std::unique_ptr<Command> cmd;
187	6175	bool status = true;
188	6175	if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin)
189		{
190		if (!solver->getOptionInfo("incremental").setByUser)
191		{
192		cmd.reset(new SetOptionCommand("incremental", "true"));
193		cmd->setMuted(true);
194		pExecutor->doCommand(cmd);
195		}
196		InteractiveShell shell(pExecutor->getSolver(),
197		pExecutor->getSymbolManager(),
198		dopts.in(),
199		dopts.out());
200
201		CVC5Message() << Configuration::getPackageName() << " "
202		<< Configuration::getVersionString();
203		if (Configuration::isGitBuild())
204		{
205		CVC5Message() << " [" << Configuration::getGitId() << "]";
206		}
207		CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
208		<< " assertions:"
209		<< (Configuration::isAssertionBuild() ? "on" : "off")
210		<< endl
211		<< endl;
212		CVC5Message() << Configuration::copyright() << endl;
213
214		while(true) {
215		try {
216		cmd.reset(shell.readCommand());
217		} catch(UnsafeInterruptException& e) {
218		dopts.out() << CommandInterrupted();
219		break;
220		}
221		if (cmd == nullptr)
222		break;
223		status = pExecutor->doCommand(cmd) && status;
224		if (cmd->interrupted()) {
225		break;
226		}
227		}
228		}
229		else
230		{
231	6175	if (!solver->getOptionInfo("incremental").setByUser)
232		{
233	5511	cmd.reset(new SetOptionCommand("incremental", "false"));
234	5511	cmd->setMuted(true);
235	5511	pExecutor->doCommand(cmd);
236		}
237
238		ParserBuilder parserBuilder(
239	12350	pExecutor->getSolver(), pExecutor->getSymbolManager(), true);
240	12350	std::unique_ptr<Parser> parser(parserBuilder.build());
241	6175	if( inputFromStdin ) {
242		parser->setInput(Input::newStreamInput(
243		solver->getOption("input-language"), cin, filename));
244		}
245		else
246		{
247	24700	parser->setInput(
248	12350	Input::newFileInput(solver->getOption("input-language"),
249		filename,
250	12350	solver->getOptionInfo("mmap").boolValue()));
251		}
252
253	6175	bool interrupted = false;
254	585283	while (status)
255		{
256	295691	if (interrupted) {
257		dopts.out() << CommandInterrupted();
258		pExecutor->reset();
259		break;
260		}
261		try {
262	295691	cmd.reset(parser->nextCommand());
263	295671	if (cmd == nullptr) break;
264		} catch (UnsafeInterruptException& e) {
265		interrupted = true;
266		continue;
267		}
268
269	290286	status = pExecutor->doCommand(cmd);
270	290286	if (cmd->interrupted() && status == 0) {
271		interrupted = true;
272		break;
273		}
274
275	290286	if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
276	732	break;
277		}
278		}
279		}
280
281	12310	api::Result result;
282	6155	if(status) {
283	6117	result = pExecutor->getResult();
284	6117	returnValue = 0;
285		} else {
286		// there was some kind of error
287	38	returnValue = 1;
288		}
289
290		#ifdef CVC5_COMPETITION_MODE
291		dopts.out() << std::flush;
292		// exit, don't return (don't want destructors to run)
293		// _exit() from unistd.h doesn't run global destructors
294		// or other on_exit/atexit stuff.
295		_exit(returnValue);
296		#endif /* CVC5_COMPETITION_MODE */
297
298	6155	pExecutor->flushOutputStreams();
299
300		#ifdef CVC5_DEBUG
301		{
302	12310	auto info = solver->getOptionInfo("early-exit");
303	6155	if (info.boolValue() && info.setByUser)
304		{
305		_exit(returnValue);
306		}
307		}
308		#else /* CVC5_DEBUG */
309		if (solver->getOptionInfo("early-exit").boolValue())
310		{
311		_exit(returnValue);
312		}
313		#endif /* CVC5_DEBUG */
314		}
315
316	6155	pExecutor.reset();
317
318	6155	signal_handlers::cleanup();
319
320	12310	return returnValue;
321	29568	}