|
| 1 | +/// \file Subprocess communication with pipes |
| 2 | +/// |
| 3 | +/// \author Diffblue Ltd. |
| 4 | + |
1 | 5 | #ifdef _WIN32
|
2 | 6 | // Windows includes go here
|
3 | 7 | #else
|
4 |
| -#include <cstring> |
5 |
| -#include <iostream> |
6 |
| -#include <unistd.h> |
7 |
| -#include <errno.h> |
8 |
| -#include <fcntl.h> // library for fcntl function |
| 8 | +# include <cstring> |
| 9 | +# include <errno.h> |
| 10 | +# include <fcntl.h> // library for fcntl function |
| 11 | +# include <iostream> |
| 12 | +# include <unistd.h> |
9 | 13 | #endif
|
10 | 14 |
|
11 | 15 | #include "invariant.h"
|
12 | 16 | #include "piped_process.h"
|
13 | 17 |
|
14 |
| - |
15 | 18 | piped_processt::piped_processt(const std::string &command)
|
16 | 19 | {
|
17 |
| - #ifdef _WIN32 |
18 |
| - // This should use the new error state from PR #6131 once that is done |
19 |
| - INVARIANT(false, "New SMT2 backend WIP: Windows piped_process constructor."); |
20 |
| - #else |
21 |
| - |
22 |
| - if (pipe(pipe_input) == -1) { |
23 |
| - throw std::runtime_error("Input pipe creation failed"); |
24 |
| - } |
25 |
| - |
26 |
| - if (pipe(pipe_output) == -1) { |
27 |
| - throw std::runtime_error("Output pipe creation failed"); |
28 |
| - } |
29 |
| - |
30 |
| - // Default state |
31 |
| - process_state = process_statet::NOT_CREATED; |
32 |
| - |
33 |
| - if (fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0) { |
34 |
| - throw std::runtime_error("Setting pipe non-blocking failed"); |
35 |
| - } |
| 20 | +#ifdef _WIN32 |
| 21 | + // This should use the new error state from PR #6131 once that is done |
| 22 | + INVARIANT(false, "New SMT2 backend WIP: Windows piped_process constructor."); |
| 23 | +#else |
36 | 24 |
|
37 |
| - // Create a new process for the child that will execute the |
38 |
| - // command and receive information via pipes. |
39 |
| - pid_t pid = fork(); |
40 |
| - if (pid == 0) { |
41 |
| - // child process here |
42 |
| - |
43 |
| - // Close pipes that will be used by the parent so we do |
44 |
| - // not have our own copies and conflicts. |
45 |
| - close(pipe_input[1]); |
46 |
| - close(pipe_output[0]); |
47 |
| - |
48 |
| - // Duplicate pipes so we have the ones we need. |
49 |
| - dup2(pipe_input[0], STDIN_FILENO); |
50 |
| - dup2(pipe_output[1], STDOUT_FILENO); |
51 |
| - dup2(pipe_output[1], STDERR_FILENO); |
52 |
| - |
53 |
| - // Create the arguments to execvp from the construction string |
54 |
| - char **args = split_command_args(command); |
55 |
| - // Execute the command |
56 |
| - execvp(args[0], args); |
57 |
| - // Only reachable if execvp failed |
58 |
| - throw std::runtime_error("Launching \"" + command + |
59 |
| - "\" failed with error: " + strerror(errno)); |
60 |
| - } else { |
61 |
| - // parent process here |
62 |
| - // Close pipes to be used by the child process |
63 |
| - close(pipe_input[0]); |
64 |
| - close(pipe_output[1]); |
65 |
| - |
66 |
| - // Get stream for sending to the child process |
67 |
| - command_stream = fdopen(pipe_input[1], "w"); |
68 |
| - process_state = process_statet::CREATED; |
69 |
| - } |
70 |
| - #endif |
| 25 | + if(pipe(pipe_input) == -1) |
| 26 | + { |
| 27 | + throw std::runtime_error("Input pipe creation failed"); |
| 28 | + } |
| 29 | + |
| 30 | + if(pipe(pipe_output) == -1) |
| 31 | + { |
| 32 | + throw std::runtime_error("Output pipe creation failed"); |
| 33 | + } |
| 34 | + |
| 35 | + // Default state |
| 36 | + process_state = process_statet::NOT_CREATED; |
| 37 | + |
| 38 | + if(fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0) |
| 39 | + { |
| 40 | + throw std::runtime_error("Setting pipe non-blocking failed"); |
| 41 | + } |
| 42 | + |
| 43 | + // Create a new process for the child that will execute the |
| 44 | + // command and receive information via pipes. |
| 45 | + pid_t pid = fork(); |
| 46 | + if(pid == 0) |
| 47 | + { |
| 48 | + // child process here |
| 49 | + |
| 50 | + // Close pipes that will be used by the parent so we do |
| 51 | + // not have our own copies and conflicts. |
| 52 | + close(pipe_input[1]); |
| 53 | + close(pipe_output[0]); |
| 54 | + |
| 55 | + // Duplicate pipes so we have the ones we need. |
| 56 | + dup2(pipe_input[0], STDIN_FILENO); |
| 57 | + dup2(pipe_output[1], STDOUT_FILENO); |
| 58 | + dup2(pipe_output[1], STDERR_FILENO); |
| 59 | + |
| 60 | + // Create the arguments to execvp from the construction string |
| 61 | + char **args = split_command_args(command); |
| 62 | + // Execute the command |
| 63 | + execvp(args[0], args); |
| 64 | + // Only reachable if execvp failed |
| 65 | + throw std::runtime_error( |
| 66 | + "Launching \"" + command + "\" failed with error: " + strerror(errno)); |
| 67 | + } |
| 68 | + else |
| 69 | + { |
| 70 | + // parent process here |
| 71 | + // Close pipes to be used by the child process |
| 72 | + close(pipe_input[0]); |
| 73 | + close(pipe_output[1]); |
| 74 | + |
| 75 | + // Get stream for sending to the child process |
| 76 | + command_stream = fdopen(pipe_input[1], "w"); |
| 77 | + process_state = process_statet::CREATED; |
| 78 | + } |
| 79 | +#endif |
71 | 80 | }
|
72 | 81 |
|
73 | 82 | bool piped_processt::send(const std::string &message)
|
74 | 83 | {
|
75 |
| - #ifdef _WIN32 |
76 |
| - // This should use the new error state from PR #6131 once that is done |
77 |
| - INVARIANT(false, "New SMT2 backend WIP: Windows piped_processt::send."); |
78 |
| - #else |
79 |
| - |
80 |
| - if(process_state != process_statet::CREATED) |
81 |
| - { |
82 |
| - return false; |
83 |
| - } |
84 |
| - |
85 |
| - // send message to solver process |
86 |
| - int send_status = fputs(message.c_str(), command_stream); |
87 |
| - fflush(command_stream); |
88 |
| - |
89 |
| - if(send_status == EOF) |
90 |
| - { |
91 |
| - // Some kind of error occured, maybe we should update the |
92 |
| - // solver status here? |
93 |
| - return false; |
94 |
| - } |
| 84 | +#ifdef _WIN32 |
| 85 | + // This should use the new error state from PR #6131 once that is done |
| 86 | + INVARIANT(false, "New SMT2 backend WIP: Windows piped_processt::send."); |
| 87 | +#else |
95 | 88 |
|
96 |
| - return true; |
97 |
| - #endif |
| 89 | + if(process_state != process_statet::CREATED) |
| 90 | + { |
| 91 | + return false; |
| 92 | + } |
| 93 | + |
| 94 | + // send message to solver process |
| 95 | + int send_status = fputs(message.c_str(), command_stream); |
| 96 | + fflush(command_stream); |
| 97 | + |
| 98 | + if(send_status == EOF) |
| 99 | + { |
| 100 | + // Some kind of error occured, maybe we should update the |
| 101 | + // solver status here? |
| 102 | + return false; |
| 103 | + } |
| 104 | + |
| 105 | + return true; |
| 106 | +#endif |
98 | 107 | }
|
99 | 108 |
|
100 | 109 | std::string piped_processt::receive()
|
101 | 110 | {
|
102 |
| - #ifdef _WIN32 |
103 |
| - // This should use the new error state from PR #6131 once that is done |
104 |
| - INVARIANT(false, "New SMT2 backend WIP: Windows piped_processt::receive."); |
105 |
| - #else |
106 |
| - |
107 |
| - if(process_state != process_statet::CREATED) |
108 |
| - return NULL; |
109 |
| - |
110 |
| - std::string response = std::string(""); |
111 |
| - int nbytes; |
112 |
| - char buff[BUFSIZE]; |
113 |
| - |
114 |
| - while (true) |
115 |
| - { |
116 |
| - nbytes = read(pipe_output[0], buff, BUFSIZE); |
117 |
| - switch (nbytes) { |
118 |
| - case -1: |
119 |
| - // Nothing more to read in the pipe |
120 |
| - return response; |
121 |
| - case 0: |
122 |
| - // Pipe is closed. |
123 |
| - process_state = process_statet::STOPPED; |
124 |
| - if (response == std::string("")) { |
125 |
| - return NULL; |
126 |
| - } |
127 |
| - return response; |
128 |
| - default: |
129 |
| - // Read some bytes, append them to the response and continue |
130 |
| - response.append(buff, nbytes); |
131 |
| - } |
132 |
| - } |
133 |
| - |
134 |
| - UNREACHABLE; |
135 |
| - #endif |
136 |
| -} |
| 111 | +#ifdef _WIN32 |
| 112 | + // This should use the new error state from PR #6131 once that is done |
| 113 | + INVARIANT(false, "New SMT2 backend WIP: Windows piped_processt::receive."); |
| 114 | +#else |
137 | 115 |
|
| 116 | + if(process_state != process_statet::CREATED) |
| 117 | + return NULL; |
138 | 118 |
|
139 |
| -char ** piped_processt::split_command_args(const std::string &command) |
140 |
| -{ |
141 |
| - char ** res = NULL; |
142 |
| - int n_spaces = 0; |
143 |
| - char *p = strtok(strdup(command.c_str()), " "); |
| 119 | + std::string response = std::string(""); |
| 120 | + int nbytes; |
| 121 | + char buff[BUFSIZE]; |
144 | 122 |
|
145 |
| - while(p) |
| 123 | + while(true) |
| 124 | + { |
| 125 | + nbytes = read(pipe_output[0], buff, BUFSIZE); |
| 126 | + switch(nbytes) |
146 | 127 | {
|
147 |
| - res = (char **)realloc(res, sizeof (char*) * ++n_spaces); |
148 |
| - if (res == NULL) |
149 |
| - exit (-1); /* memory allocation failed */ |
150 |
| - res[n_spaces-1] = p; |
151 |
| - p = strtok (NULL, " "); |
| 128 | + case -1: |
| 129 | + // Nothing more to read in the pipe |
| 130 | + return response; |
| 131 | + case 0: |
| 132 | + // Pipe is closed. |
| 133 | + process_state = process_statet::STOPPED; |
| 134 | + if(response == std::string("")) |
| 135 | + { |
| 136 | + return NULL; |
| 137 | + } |
| 138 | + return response; |
| 139 | + default: |
| 140 | + // Read some bytes, append them to the response and continue |
| 141 | + response.append(buff, nbytes); |
152 | 142 | }
|
| 143 | + } |
153 | 144 |
|
154 |
| - res = (char **)realloc (res, sizeof (char*) * (n_spaces+1)); |
155 |
| - res[n_spaces] = 0; |
156 |
| - return res; |
| 145 | + UNREACHABLE; |
| 146 | +#endif |
| 147 | +} |
| 148 | + |
| 149 | +char **piped_processt::split_command_args(const std::string &command) |
| 150 | +{ |
| 151 | + char **res = NULL; |
| 152 | + int n_spaces = 0; |
| 153 | + char *p = strtok(strdup(command.c_str()), " "); |
| 154 | + |
| 155 | + while(p) |
| 156 | + { |
| 157 | + res = reinterpret_cast<char **>(realloc(res, sizeof(char *) * ++n_spaces)); |
| 158 | + if(res == NULL) |
| 159 | + exit(-1); /* memory allocation failed */ |
| 160 | + res[n_spaces - 1] = p; |
| 161 | + p = strtok(NULL, " "); |
| 162 | + } |
| 163 | + |
| 164 | + res = |
| 165 | + reinterpret_cast<char **>(realloc(res, sizeof(char *) * (n_spaces + 1))); |
| 166 | + res[n_spaces] = 0; |
| 167 | + return res; |
157 | 168 | }
|
0 commit comments