LCOV - code coverage report
Current view: top level - smt/source - child_process.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 66 0.0 %
Date: 2020-10-20 00:45:57 Functions: 0 8 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Thomas Neele
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file child_process.cpp
      10             : 
      11             : #include "mcrl2/smt/child_process.h"
      12             : #include "mcrl2/utilities/exception.h"
      13             : #include "mcrl2/utilities/platform.h"
      14             : 
      15             : #ifdef MCRL2_PLATFORM_WINDOWS
      16             :   #include <windows.h>
      17             :   #include <tchar.h>
      18             :   #include <cstdio>
      19             :   #include <strsafe.h>
      20             : #else
      21             :   #include <unistd.h>
      22             :   #include <sys/select.h>
      23             :   #include <sys/wait.h>
      24             : #endif // MCRL2_PLATFORM_WINDOWS
      25             : 
      26             : #include <cstring>
      27             : #include <csignal>
      28             : #include <cerrno>
      29             : 
      30             : 
      31             : namespace mcrl2
      32             : {
      33             : namespace smt
      34             : {
      35             : 
      36             : #ifdef MCRL2_PLATFORM_WINDOWS
      37             : 
      38             : struct child_process::platform_impl
      39             : {
      40             :   HANDLE g_hChildStd_IN_Rd = NULL;
      41             :   HANDLE g_hChildStd_IN_Wr = NULL;
      42             :   HANDLE g_hChildStd_OUT_Rd = NULL;
      43             :   HANDLE g_hChildStd_OUT_Wr = NULL;
      44             : };
      45             : 
      46             : void child_process::write(const std::string& command) const
      47             : {
      48             :   DWORD dwWritten;
      49             :   BOOL bSuccess = FALSE;
      50             : 
      51             :   bSuccess = WriteFile(m_pimpl->g_hChildStd_IN_Wr, command.c_str(), static_cast<DWORD>(command.size()), &dwWritten, NULL);
      52             :   if(!bSuccess || dwWritten != command.size())
      53             :   {
      54             :     throw mcrl2::runtime_error("Failed to write SMT problem to the solver.\n" + command);
      55             :   }
      56             : }
      57             : 
      58             : 
      59             : std::string child_process::read() const
      60             : {
      61             :   DWORD dwRead, totalRead;
      62             :   CHAR output[512];
      63             :   BOOL bSuccess = FALSE;
      64             : 
      65             :   totalRead = 0;
      66             :   do
      67             :   {
      68             :     bSuccess = ReadFile( m_pimpl->g_hChildStd_OUT_Rd, output + totalRead, 512 - totalRead, &dwRead, NULL);
      69             :     totalRead += dwRead;
      70             :   } while(bSuccess && output[totalRead-1] != '\n');
      71             :   if(!bSuccess || totalRead == 0 )
      72             :   {
      73             :     throw mcrl2::runtime_error("Reading from child process " + m_name + " failed.");
      74             :   }
      75             :   return std::string(output, totalRead);
      76             : }
      77             : 
      78             : std::string child_process::read(const std::chrono::microseconds& timeout) const
      79             : {
      80             :   // Not implemented on Windows
      81             :   return read();
      82             : }
      83             : 
      84             : void child_process::send_sigint() const
      85             : {
      86             :   // Not implemented on Windows
      87             : }
      88             : 
      89             : void child_process::initialize()
      90             : {
      91             :   m_pimpl = std::make_shared<child_process::platform_impl>();
      92             :   SECURITY_ATTRIBUTES saAttr;
      93             :   // Set the bInheritHandle flag so pipe handles are inherited.
      94             :   saAttr.nLength = sizeof(SECURITY_ATTRIBUTES);
      95             :   saAttr.bInheritHandle = TRUE;
      96             :   saAttr.lpSecurityDescriptor = NULL;
      97             : 
      98             :   // Create a pipe for the child process's STDOUT.
      99             :   if (!CreatePipe(&m_pimpl->g_hChildStd_OUT_Rd, &m_pimpl->g_hChildStd_OUT_Wr, &saAttr, 0))
     100             :   {
     101             :     throw mcrl2::runtime_error("Could not connect to SMT solver: failed to create pipe Stdout");
     102             :   }
     103             :   // Ensure the read handle to the pipe for STDOUT is not inherited.
     104             :   if(!SetHandleInformation(m_pimpl->g_hChildStd_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
     105             :   {
     106             :     throw mcrl2::runtime_error("Could not modify SMT solver handle: SetHandleInformation Stdout");
     107             :   }
     108             :   // Create a pipe for the child process's STDIN.
     109             :   if(!CreatePipe(&m_pimpl->g_hChildStd_IN_Rd, &m_pimpl->g_hChildStd_IN_Wr, &saAttr, 0))
     110             :   {
     111             :     throw mcrl2::runtime_error("Could not connect to SMT solver: failed to create pipe Stdin");
     112             :   }
     113             :   // Ensure the write handle to the pipe for STDIN is not inherited.
     114             :   if(!SetHandleInformation(m_pimpl->g_hChildStd_IN_Wr, HANDLE_FLAG_INHERIT, 0))
     115             :   {
     116             :     throw mcrl2::runtime_error("Could not modify SMT solver handle: SetHandleInformation Stdin");
     117             :   }
     118             :   // Create the child process.
     119             :   TCHAR szCmdline[] = TEXT("z3.exe -smt2 -in");
     120             :   PROCESS_INFORMATION piProcInfo;
     121             :   STARTUPINFO siStartInfo;
     122             :   BOOL bSuccess = FALSE;
     123             : 
     124             :   // Set up members of the PROCESS_INFORMATION structure.
     125             :   ZeroMemory(&piProcInfo, sizeof(PROCESS_INFORMATION));
     126             : 
     127             :   // Set up members of the STARTUPINFO structure.
     128             :   // This structure specifies the STDIN and STDOUT handles for redirection.
     129             :   ZeroMemory(&siStartInfo, sizeof(STARTUPINFO));
     130             :   siStartInfo.cb = sizeof(STARTUPINFO);
     131             :   siStartInfo.hStdError = m_pimpl->g_hChildStd_OUT_Wr;
     132             :   siStartInfo.hStdOutput = m_pimpl->g_hChildStd_OUT_Wr;
     133             :   siStartInfo.hStdInput = m_pimpl->g_hChildStd_IN_Rd;
     134             :   siStartInfo.dwFlags |= STARTF_USESTDHANDLES;
     135             : 
     136             :   // Create the child process.
     137             :   bSuccess = CreateProcess(NULL,
     138             :     szCmdline,     // command line
     139             :     NULL,          // process security attributes
     140             :     NULL,          // primary thread security attributes
     141             :     TRUE,          // handles are inherited
     142             :     0,             // creation flags
     143             :     NULL,          // use parent's environment
     144             :     NULL,          // use parent's current directory
     145             :     &siStartInfo,  // STARTUPINFO pointer
     146             :     &piProcInfo);  // receives PROCESS_INFORMATION
     147             : 
     148             :   // If an error occurs, exit the application.
     149             :   if(!bSuccess)
     150             :   {
     151             :     throw mcrl2::runtime_error("Problem occurred while creating SMT solver process.\nIs " + m_name + " in your path?");
     152             :   }
     153             :   else
     154             :   {
     155             :     // Close handles to the child process and its primary thread.
     156             :     // Some applications might keep these handles to monitor the status
     157             :     // of the child process, for example.
     158             :     CloseHandle(piProcInfo.hProcess);
     159             :     CloseHandle(piProcInfo.hThread);
     160             :   }
     161             : }
     162             : 
     163             : child_process::~child_process()
     164             : {
     165             :   // Clean up the child process
     166             :   // It terminates when we close its stdin
     167             :   CloseHandle(m_pimpl->g_hChildStd_IN_Wr);
     168             : }
     169             : 
     170             : 
     171             : #else // MCRL2_PLATFORM_WINDOWS
     172             : 
     173             : struct child_process::platform_impl
     174             : {
     175             :   pid_t child_pid;
     176             :   int pipe_stdin[2];
     177             :   int pipe_stdout[2];
     178             :   int pipe_stderr[2];
     179             : };
     180             : 
     181           0 : void child_process::write(const std::string& command) const
     182             : {
     183           0 :   if(::write(m_pimpl->pipe_stdin[1], command.c_str(), command.size()) < 0)
     184             :   {
     185           0 :     throw mcrl2::runtime_error("Failed to write to " + m_name + ".\n" + command);
     186             :   }
     187           0 : }
     188             : 
     189           0 : std::string child_process::read() const
     190             : {
     191             :   char output[512];
     192             :   // check return value
     193           0 :   int count = ::read(m_pimpl->pipe_stdout[0], output, 512);
     194           0 :   if(count > 0)
     195             :   {
     196           0 :     return std::string(output, count);
     197             :   }
     198             :   else
     199             :   {
     200           0 :     std::string message;
     201             : 
     202           0 :     while(int i = ::read(m_pimpl->pipe_stderr[0], output, 512))
     203             :     {
     204           0 :       message.append(output, 0, i);
     205           0 :     }
     206             : 
     207           0 :     throw mcrl2::runtime_error("Reading from child process " + m_name + " failed: " + message);
     208             :   }
     209             : }
     210             : 
     211           0 : std::string child_process::read(const std::chrono::microseconds& timeout) const
     212             : {
     213             :   struct timeval tv;
     214           0 :   tv.tv_sec = 0;
     215           0 :   tv.tv_usec = timeout.count();
     216             : 
     217             :   fd_set readfds;
     218           0 :   FD_ZERO(&readfds);
     219           0 :   FD_SET(m_pimpl->pipe_stdout[0], &readfds);
     220             : 
     221           0 :   int result = ::select(m_pimpl->pipe_stdout[0] + 1, &readfds, NULL, NULL, &tv);
     222             : 
     223           0 :   if(result == -1)
     224             :   {
     225           0 :     throw mcrl2::runtime_error("Error while waiting for input from " + m_name);
     226             :   }
     227           0 :   else if(result == 0)
     228             :   {
     229           0 :     send_sigint();
     230             :   }
     231           0 :   return read();
     232             : }
     233             : 
     234           0 : void child_process::send_sigint() const
     235             : {
     236           0 :   ::kill(m_pimpl->child_pid, SIGINT);
     237           0 : }
     238             : 
     239           0 : void child_process::initialize()
     240             : {
     241           0 :   signal(SIGPIPE, SIG_IGN);
     242           0 :   m_pimpl = std::make_shared<child_process::platform_impl>();
     243             :   // Create pipes (two pairs r/w)
     244           0 :   if (::pipe(&m_pimpl->pipe_stdin[0]) < 0)
     245             :   {
     246           0 :     throw mcrl2::runtime_error("failed to create pipe");
     247             :   }
     248             : 
     249           0 :   if (::pipe(&m_pimpl->pipe_stdout[0]) < 0)
     250             :   {
     251           0 :     throw mcrl2::runtime_error("failed to create pipe");
     252             :   }
     253             : 
     254           0 :   if (::pipe(&m_pimpl->pipe_stderr[0]) < 0)
     255             :   {
     256           0 :     throw mcrl2::runtime_error("failed to create pipe");
     257             :   }
     258             : 
     259             :   // fork process
     260           0 :   pid_t pid = ::fork();
     261           0 :   if (pid == 0)
     262             :   {
     263             :     // Forked process keeps waiting for input
     264           0 :     ::dup2(m_pimpl->pipe_stdin[0], STDIN_FILENO);
     265           0 :     ::dup2(m_pimpl->pipe_stdout[1], STDOUT_FILENO);
     266           0 :     ::dup2(m_pimpl->pipe_stderr[1], STDERR_FILENO);
     267             : 
     268           0 :     ::close(m_pimpl->pipe_stdin[1]);
     269           0 :     ::close(m_pimpl->pipe_stdout[0]);
     270           0 :     ::close(m_pimpl->pipe_stderr[0]);
     271             : 
     272           0 :     ::execlp("z3", "z3", "-smt2", "-in", (char*) nullptr);
     273             : 
     274           0 :     ::_exit(errno);
     275             :   }
     276           0 :   else if (pid < 0)
     277             :   {
     278           0 :     ::close(m_pimpl->pipe_stdin[0]);
     279           0 :     ::close(m_pimpl->pipe_stdin[1]);
     280           0 :     ::close(m_pimpl->pipe_stdout[0]);
     281           0 :     ::close(m_pimpl->pipe_stdout[1]);
     282           0 :     ::close(m_pimpl->pipe_stderr[0]);
     283           0 :     ::close(m_pimpl->pipe_stderr[1]);
     284             : 
     285           0 :     throw mcrl2::runtime_error("Problem occurred while forking SMT solver process: " + std::string(strerror(errno)) + ".\nIs " + m_name + " in your path?");
     286             :   }
     287             :   else
     288             :   {
     289           0 :     m_pimpl->child_pid = pid;
     290           0 :     ::close(m_pimpl->pipe_stdin[0]);
     291           0 :     ::close(m_pimpl->pipe_stdout[1]);
     292           0 :     ::close(m_pimpl->pipe_stderr[1]);
     293             :   }
     294           0 : }
     295             : 
     296           0 : child_process::~child_process()
     297             : {
     298             :   // Clean up the child process
     299             :   // It terminates when we close its stdin
     300           0 :   ::close(m_pimpl->pipe_stdin[1]);
     301           0 :   ::close(m_pimpl->pipe_stdout[0]);
     302           0 :   ::close(m_pimpl->pipe_stderr[0]);
     303             : 
     304             :   int return_status;
     305           0 :   ::wait(&return_status);
     306           0 : }
     307             : 
     308             : #endif // MCRL2_PLATFORM_WINDOWS
     309             : 
     310             : 
     311             : } // namespace smt
     312           0 : } // namespace mcrl2

Generated by: LCOV version 1.13