cprover
piped_process.h
Go to the documentation of this file.
1 
5 #ifndef CPROVER_UTIL_PIPED_PROCESS_H
6 #define CPROVER_UTIL_PIPED_PROCESS_H
7 
8 #ifdef _WIN32
9 # include <memory>
10 // The below are forward declarations for Windows APIs
11 struct _PROCESS_INFORMATION; // NOLINT
12 typedef struct _PROCESS_INFORMATION PROCESS_INFORMATION; // NOLINT
13 typedef void *HANDLE; // NOLINT
14 #endif
15 
16 #include "optional.h"
17 #include <vector>
18 
19 #define PIPED_PROCESS_INFINITE_TIMEOUT \
20  optionalt<std::size_t> \
21  { \
22  }
23 
25 {
26 public:
28  enum class statet
29  {
30  RUNNING,
31  ERRORED
32  };
33 
35  enum class send_responset
36  {
37  SUCCEEDED,
38  FAILED,
39  ERRORED
40  };
41 
45  send_responset send(const std::string &message);
48  std::string receive();
52  std::string wait_receive();
53 
57 
64  bool can_receive(optionalt<std::size_t> wait_time);
65 
69  bool can_receive();
70 
75  // of can_receive(0)
76  void wait_receivable(int wait_time);
77 
81  explicit piped_processt(const std::vector<std::string> &commandvec);
82 
83  // Deleted due to declaring an explicit destructor and not wanting copy
84  // constructors to be implemented.
85  piped_processt(const piped_processt &) = delete;
88 
89 protected:
90 #ifdef _WIN32
91  // Process information handle for Windows
92  std::unique_ptr<PROCESS_INFORMATION> proc_info;
93  // Handles for communication with child process
94  HANDLE child_std_IN_Rd;
95  HANDLE child_std_IN_Wr;
96  HANDLE child_std_OUT_Rd;
97  HANDLE child_std_OUT_Wr;
98 #else
99  // Child process ID.
102  // The member fields below are so named from the perspective of the
103  // parent -> child process. So `pipe_input` is where we are feeding
104  // commands to the child process, and `pipe_output` is where we read
105  // the results of execution from.
106  int pipe_input[2];
107  int pipe_output[2];
108 #endif
110 };
111 
112 #endif // endifndef CPROVER_UTIL_PIPED_PROCESS_H
piped_processt::statet
statet
Enumeration to keep track of child process state.
Definition: piped_process.h:29
piped_processt::send_responset::FAILED
@ FAILED
optional.h
piped_processt::can_receive
bool can_receive()
See if this process can receive data from the other process.
Definition: piped_process.cpp:468
piped_processt::statet::ERRORED
@ ERRORED
piped_processt::operator=
piped_processt & operator=(const piped_processt &)=delete
piped_processt::pipe_input
int pipe_input[2]
Definition: piped_process.h:106
piped_processt::~piped_processt
~piped_processt()
Definition: piped_process.cpp:314
piped_processt::wait_receivable
void wait_receivable(int wait_time)
Wait for the pipe to be ready, waiting specified time between checks.
Definition: piped_process.cpp:473
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
piped_processt::send_responset
send_responset
Enumeration for send response.
Definition: piped_process.h:36
piped_processt
Definition: piped_process.h:25
piped_processt::child_process_id
pid_t child_process_id
Definition: piped_process.h:100
piped_processt::process_state
statet process_state
Definition: piped_process.h:109
piped_processt::command_stream
FILE * command_stream
Definition: piped_process.h:101
piped_processt::send
send_responset send(const std::string &message)
Send a string message (command) to the child process.
Definition: piped_process.cpp:338
piped_processt::statet::RUNNING
@ RUNNING
piped_processt::piped_processt
piped_processt(const std::vector< std::string > &commandvec)
Initiate a new subprocess with pipes supporting communication between the parent (this process) and t...
Definition: piped_process.cpp:123
piped_processt::receive
std::string receive()
Read a string from the child process' output.
Definition: piped_process.cpp:363
piped_processt::send_responset::SUCCEEDED
@ SUCCEEDED
piped_processt::wait_receive
std::string wait_receive()
Wait until a string is available and read a string from the child process' output.
Definition: piped_process.cpp:399
piped_processt::get_status
statet get_status()
Get child process status.
Definition: piped_process.cpp:407
piped_processt::piped_processt
piped_processt(const piped_processt &)=delete
piped_processt::pipe_output
int pipe_output[2]
Definition: piped_process.h:107
piped_processt::send_responset::ERRORED
@ ERRORED
statet
unsigned int statet
Definition: trace_automaton.h:24