LCOV - code coverage report
Current view: top level - data/source/detail/prover - smt_lib_solver.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1 56 1.8 %
Date: 2020-07-11 00:44:39 Functions: 2 8 25.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : #if !(defined(_MSC_VER) || defined(__MINGW32__) || defined(__CYGWIN__))
       2             : #include <cerrno>       // for errno
       3             : #include <sys/types.h>  // for pid_t
       4             : #include <sys/wait.h>   // for waitpid()
       5             : #include <sys/ioctl.h>  // for ioctl() and FIONREAD
       6             : #include "mcrl2/data/detail/prover/smt_lib_solver.h"
       7             : 
       8             : using namespace mcrl2::log;
       9             : 
      10             : namespace mcrl2
      11             : {
      12             : namespace data
      13             : {
      14             : namespace detail
      15             : {
      16             : namespace prover
      17             : {
      18             : template < typename T >
      19           0 : bool binary_smt_solver< T >::execute(std::string const& benchmark)
      20             : {
      21             :   int pipe_stdin[2];
      22             :   int pipe_stdout[2];
      23             :   int pipe_stderr[2];
      24             : 
      25             :   // Create pipes (two pairs r/w)
      26           0 :   if (::pipe(&pipe_stdin[0]) < 0)
      27             :   {
      28           0 :     throw mcrl2::runtime_error("failed to create pipe");
      29             :   }
      30             : 
      31           0 :   if (::pipe(&pipe_stdout[0]) < 0)
      32             :   {
      33           0 :     throw mcrl2::runtime_error("failed to create pipe");
      34             :   }
      35             : 
      36           0 :   if (::pipe(&pipe_stderr[0]) < 0)
      37             :   {
      38           0 :     throw mcrl2::runtime_error("failed to create pipe");
      39             :   }
      40             : 
      41             :   // fork process
      42           0 :   pid_t pid = ::fork();
      43             : 
      44           0 :   if (pid == 0)
      45             :   {
      46           0 :     ::dup2(pipe_stdin[0], STDIN_FILENO);
      47           0 :     ::dup2(pipe_stdout[1], STDOUT_FILENO);
      48           0 :     ::dup2(pipe_stderr[1], STDERR_FILENO);
      49             : 
      50           0 :     ::close(pipe_stdin[1]);
      51           0 :     ::close(pipe_stdout[0]);
      52           0 :     ::close(pipe_stderr[0]);
      53             : 
      54           0 :     T::exec();
      55             : 
      56           0 :     ::_exit(errno);
      57             :   }
      58           0 :   else if (pid < 0)
      59             :   {
      60           0 :     mCRL2log(error) << strerror(errno) << std::endl;
      61             : 
      62           0 :     ::close(pipe_stdin[0]);
      63           0 :     ::close(pipe_stdin[1]);
      64           0 :     ::close(pipe_stdout[0]);
      65           0 :     ::close(pipe_stdout[1]);
      66           0 :     ::close(pipe_stderr[0]);
      67           0 :     ::close(pipe_stderr[1]);
      68             : 
      69           0 :     return false;
      70             :   }
      71             :   else
      72             :   {
      73           0 :     if(::write(pipe_stdin[1], benchmark.c_str(), benchmark.size()) < 0)
      74             :     {
      75           0 :       throw mcrl2::runtime_error("failed to write benchmark");
      76             :     }
      77             : 
      78           0 :     ::close(pipe_stdin[0]);
      79           0 :     ::close(pipe_stdin[1]);
      80           0 :     ::close(pipe_stdout[1]);
      81           0 :     ::close(pipe_stderr[1]);
      82             : 
      83             :     char output[64];
      84             : 
      85             :     int return_status;
      86             : 
      87             :     // check return value
      88           0 :     if (0 < ::read(pipe_stdout[0], output, 8))
      89             :     {
      90           0 :       if (strncmp(output, "sat", 3) == 0)
      91             :       {
      92           0 :         mCRL2log(verbose) << "The formula is satisfiable" << std::endl;
      93             : 
      94           0 :         ::close(pipe_stdout[0]);
      95           0 :         ::close(pipe_stderr[0]);
      96             : 
      97           0 :         ::wait(&return_status);
      98             : 
      99           0 :         return true;
     100             :       }
     101           0 :       else if (strncmp(output, "unsat", 5) == 0)
     102             :       {
     103           0 :         mCRL2log(verbose) << "The formula is unsatisfiable" << std::endl;
     104             :       }
     105           0 :       else if (strncmp(output, "unknown", 7) == 0)
     106             :       {
     107           0 :         mCRL2log(verbose) << T::name() << " cannot determine whether this formula is satisfiable or not." << std::endl;
     108             :       }
     109             :     }
     110             :     else
     111             :     {
     112           0 :       std::string message;
     113             : 
     114           0 :       while (int i = ::read(pipe_stderr[0], output, 64))
     115             :       {
     116           0 :         message.append(output, 0, i);
     117             :       }
     118             : 
     119           0 :       throw mcrl2::runtime_error(std::string("The SMT prover ") + T::name() + " does not work properly. " + message );
     120             :     }
     121             : 
     122           0 :     ::close(pipe_stdout[0]);
     123           0 :     ::close(pipe_stderr[0]);
     124             : 
     125           0 :     ::wait(&return_status);
     126             :   }
     127             : 
     128           0 :   return false;
     129             : }
     130             : 
     131             : /**
     132             :  * \brief Checks the availability/usability of the prover
     133             :  **/
     134             : template < typename T >
     135           0 : bool binary_smt_solver< T >::usable()
     136             : {
     137           0 :   if (!binary_smt_solver::execute("(benchmark nameless :formula true)"))
     138             :   {
     139             :     throw mcrl2::runtime_error(std::string("The SMT solver ") + T::name() + " is not available. \n" + 
     140           0 :                      "Consult the manual of the tool you are using for instructions on how to obtain " + T::name() + ".");
     141             : 
     142             :     return false;
     143             :   }
     144             : 
     145           0 :   return true;
     146             : }
     147             : 
     148             : // instantiate for cvc prover
     149             : template class binary_smt_solver< cvc_smt_solver >;
     150             : 
     151             : // instantiate for z3 prover
     152             : template class binary_smt_solver< z3_smt_solver >;
     153             : 
     154             : // instantiate for ario prover
     155             : template class binary_smt_solver< ario_smt_solver >;
     156             : }
     157             : }
     158             : }
     159         366 : }
     160             : #endif
     161             : 

Generated by: LCOV version 1.13