piped_process.h

Go to the documentation of this file.

 
#ifndef CPROVER_UTIL_PIPED_PROCESS_H
#define CPROVER_UTIL_PIPED_PROCESS_H
 
#ifdef _WIN32
#  include <memory>
// The below are forward declarations for Windows APIs
struct _PROCESS_INFORMATION;                             // NOLINT
typedef struct _PROCESS_INFORMATION PROCESS_INFORMATION; // NOLINT
typedef void *HANDLE;                                    // NOLINT
#endif
 
#include "message.h"
#include "nodiscard.h"
#include "optional.h"
 
#include <vector>
 
#define PIPED_PROCESS_INFINITE_TIMEOUT                                         \
  optionalt<std::size_t>                                                       \
  {                                                                            \
  }
 
class piped_processt
{
public:
  enum class statet
  {
    RUNNING,
    ERRORED
  };
 
  enum class send_responset
  {
    SUCCEEDED,
    FAILED,
    ERRORED
  };
 
  NODISCARD send_responset send(const std::string &message);
  std::string receive();
  std::string wait_receive();
 
  statet get_status();
 
  bool can_receive(optionalt<std::size_t> wait_time);
 
  bool can_receive();
 
  //         of can_receive(0)
  void wait_receivable(int wait_time);
 
  explicit piped_processt(
    const std::vector<std::string> &commandvec,
    message_handlert &message_handler);
 
  // Deleted due to declaring an explicit destructor and not wanting copy
  // constructors to be implemented.
  piped_processt(const piped_processt &) = delete;
  piped_processt &operator=(const piped_processt &) = delete;
  ~piped_processt();
 
protected:
#ifdef _WIN32
  // Process information handle for Windows
  std::unique_ptr<PROCESS_INFORMATION> proc_info;
  // Handles for communication with child process
  HANDLE child_std_IN_Rd;
  HANDLE child_std_IN_Wr;
  HANDLE child_std_OUT_Rd;
  HANDLE child_std_OUT_Wr;
#else
  // Child process ID.
  pid_t child_process_id;
  FILE *command_stream;
  // The member fields below are so named from the perspective of the
  // parent -> child process. So `pipe_input` is where we are feeding
  // commands to the child process, and `pipe_output` is where we read
  // the results of execution from.
  int pipe_input[2];
  int pipe_output[2];
#endif
  statet process_state;
  messaget log;
};
 
#endif // endifndef CPROVER_UTIL_PIPED_PROCESS_H