ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cadical_file.cpp
Go to the documentation of this file.
1#include "global.h"
2
3#include "internal.hpp"
4
5/*------------------------------------------------------------------------*/
6
7// Some more low-level 'C' headers.
8
9extern "C" {
10#include <errno.h>
11#include <fcntl.h>
12#include <stdlib.h>
13#include <string.h>
14#include <sys/stat.h>
15#include <sys/types.h>
16}
17
18#ifdef WIN32
19
20#include <windows.h>
21#include <io.h>
22#include <cstdio>
23
24#define access _access
25#define popen _popen
26#define pclose _pclose
27#define R_OK 4
28#define W_OK 2
29#define S_IFIFO _S_IFIFO
30#define S_ISFIFO(mode) (((mode) & S_IFMT) == S_IFIFO)
31#define S_ISDIR(mode) (((mode) & S_IFMT) == S_IFDIR)
32
33#else
34
35extern "C" {
36#include <sys/wait.h>
37#include <unistd.h>
38}
39
40#endif
41
42#if defined(__APPLE__) || defined(__MACH__)
43
44extern "C" {
45#include <libproc.h>
46#include <sys/proc_info.h>
47}
48
49#include <mutex>
50
51#endif
52
54
55/*------------------------------------------------------------------------*/
56
57namespace CaDiCaL {
58
59/*------------------------------------------------------------------------*/
60
61// Private constructor.
62
63File::File (Internal *i, bool w, int c, int p, FILE *f, const char *n)
64 : internal (i),
65#if !defined(CADICAL_QUIET) || !defined(CADICAL_NDEBUG)
66 writing (w),
67#endif
68 close_file (c), child_pid (p), file (f), _name (strdup (n)),
69 _lineno (1), _bytes (0) {
70 (void) w;
72}
73
74/*------------------------------------------------------------------------*/
75
76bool File::exists (const char *path) {
77 struct stat buf;
78 if (stat (path, &buf))
79 return false;
80 if (access (path, R_OK))
81 return false;
82 return true;
83}
84
85bool File::writable (const char *path) {
86 int res;
87 if (!path)
88 res = 1;
89 else if (!strcmp (path, "/dev/null"))
90 res = 0;
91 else {
92 if (!*path)
93 res = 2;
94 else {
95 struct stat buf;
96 const char *p = strrchr (path, '/');
97 if (!p) {
98 if (stat (path, &buf))
99 res = ((errno == ENOENT) ? 0 : -2);
100 else if (S_ISDIR (buf.st_mode))
101 res = 3;
102 else
103 res = (access (path, W_OK) ? 4 : 0);
104 } else if (!p[1])
105 res = 5;
106 else {
107 size_t len = p - path;
108 char *dirname = new char[len + 1];
109 strncpy (dirname, path, len);
110 dirname[len] = 0;
111 if (stat (dirname, &buf))
112 res = 6;
113 else if (!S_ISDIR (buf.st_mode))
114 res = 7;
115 else if (access (dirname, W_OK))
116 res = 8;
117 else if (stat (path, &buf))
118 res = (errno == ENOENT) ? 0 : -3;
119 else
120 res = access (path, W_OK) ? 9 : 0;
121 delete[] dirname;
122 }
123 }
124 }
125 return !res;
126}
127
129 struct stat stat;
130 int fd = fileno (file);
131 if (fstat (fd, &stat))
132 return true;
133 return S_ISFIFO (stat.st_mode);
134}
135
136// These are signatures for supported compressed file types. In 2018 the
137// SAT Competition was running on StarExec and used internally 'bzip2'
138// compressed files, but gave them uncompressed to the solver using exactly
139// the same path (with '.bz2' suffix). Then 'CaDiCaL' tried to read that
140// actually uncompressed file through 'bzip2', which of course failed. Now
141// we double check and fall back to reading the file as is, if the signature
142// does not match after issuing a warning.
143
144static int xzsig[] = {0xFD, 0x37, 0x7A, 0x58, 0x5A, 0x00, 0x00, EOF};
145static int bz2sig[] = {0x42, 0x5A, 0x68, EOF};
146static int gzsig[] = {0x1F, 0x8B, EOF};
147static int sig7z[] = {0x37, 0x7A, 0xBC, 0xAF, 0x27, 0x1C, EOF};
148static int lzmasig[] = {0x5D, EOF};
149
150bool File::match (Internal *internal, const char *path, const int *sig) {
151 CADICAL_assert (path);
152 FILE *tmp = fopen (path, "r");
153 if (!tmp) {
154 WARNING ("failed to open '%s' to check signature", path);
155 return false;
156 }
157 bool res = true;
158 for (const int *p = sig; res && (*p != EOF); p++)
159 res = (cadical_getc_unlocked (tmp) == *p);
160 fclose (tmp);
161 if (!res)
162 WARNING ("file type signature check for '%s' failed", path);
163 return res;
164}
165
166size_t File::size (const char *path) {
167 struct stat buf;
168 if (stat (path, &buf))
169 return 0;
170 return (size_t) buf.st_size;
171}
172
173// Check that 'prg' is in the 'PATH' and thus can be found if executed
174// through 'popen' or 'exec'.
175
176char *File::find_program (const char *prg) {
177 size_t prglen = strlen (prg);
178 const char *c = getenv ("PATH");
179 if (!c)
180 return 0;
181 size_t len = strlen (c);
182 char *e = new char[len + 1];
183 strcpy (e, c);
184 char *res = 0;
185 for (char *p = e, *q; !res && p < e + len; p = q) {
186 for (q = p; *q && *q != ':'; q++)
187 ;
188 *q++ = 0;
189 size_t pathlen = (q - p) + prglen;
190 char *path = new char[pathlen + 1];
191 snprintf (path, pathlen + 1, "%s/%s", p, prg);
192 CADICAL_assert (strlen (path) == pathlen);
193 if (exists (path))
194 res = path;
195 else
196 delete[] path;
197 }
198 delete[] e;
199 return res;
200}
201
202/*------------------------------------------------------------------------*/
203
204FILE *File::open_file (Internal *internal, const char *path,
205 const char *mode) {
206 (void) internal;
207 return fopen (path, mode);
208}
209
210FILE *File::read_file (Internal *internal, const char *path) {
211 MSG ("opening file to read '%s'", path);
212 return open_file (internal, path, "r");
213}
214
215FILE *File::write_file (Internal *internal, const char *path) {
216 MSG ("opening file to write '%s'", path);
217 return open_file (internal, path, "wb");
218}
219
220/*------------------------------------------------------------------------*/
221
222void File::split_str (const char *command, std::vector<char *> &argv) {
223 const char *c = command;
224 while (*c && *c == ' ')
225 c++;
226 while (*c) {
227 const char *p = c;
228 while (*p && *p != ' ')
229 p++;
230 const size_t bytes = p - c;
231 char *arg = new char[bytes + 1];
232 (void) strncpy (arg, c, bytes);
233 arg[bytes] = 0;
234 argv.push_back (arg);
235 while (*p && *p == ' ')
236 p++;
237 c = p;
238 }
239}
240
241void File::delete_str_vector (std::vector<char *> &argv) {
242 for (auto str : argv)
243 delete[] str;
244}
245
246FILE *File::open_pipe (Internal *internal, const char *fmt,
247 const char *path, const char *mode) {
248#ifdef CADICAL_QUIET
249 (void) internal;
250#endif
251 size_t prglen = 0;
252 while (fmt[prglen] && fmt[prglen] != ' ')
253 prglen++;
254 char *prg = new char[prglen + 1];
255 strncpy (prg, fmt, prglen);
256 prg[prglen] = 0;
257 char *found = find_program (prg);
258 if (found)
259 MSG ("found '%s' in path for '%s'", found, prg);
260 if (!found)
261 MSG ("did not find '%s' in path", prg);
262 delete[] prg;
263 if (!found)
264 return 0;
265 delete[] found;
266 size_t cmd_size = strlen (fmt) + strlen (path);
267 char *cmd = new char[cmd_size];
268 snprintf (cmd, cmd_size, fmt, path);
269 FILE *res = popen (cmd, mode);
270 delete[] cmd;
271 return res;
272}
273
274FILE *File::read_pipe (Internal *internal, const char *fmt, const int *sig,
275 const char *path) {
276 if (!File::exists (path)) {
277 LOG ("file '%s' does not exist", path);
278 return 0;
279 }
280 LOG ("file '%s' exists", path);
281 if (sig && !File::match (internal, path, sig))
282 return 0;
283 LOG ("file '%s' matches signature for '%s'", path, fmt);
284 MSG ("opening pipe to read '%s'", path);
285 return open_pipe (internal, fmt, path, "r");
286}
287
288#ifndef _WIN32
289
290#if defined(__APPLE__) || defined(__MACH__)
291static std::mutex compressed_file_writing_mutex;
292#endif
293
294FILE *File::write_pipe (Internal *internal, const char *command,
295 const char *path, int &child_pid) {
296 CADICAL_assert (command[0] && command[0] != ' ');
297 MSG ("writing through command '%s' to '%s'", command, path);
298#ifdef CADICAL_QUIET
299 (void) internal;
300#endif
301 std::vector<char *> args;
302 split_str (command, args);
303 CADICAL_assert (!args.empty ());
304 args.push_back (0);
305 char **argv = args.data ();
306 char *absolute_command_path = find_program (argv[0]);
307 int pipe_fds[2], out;
308 FILE *res = 0;
309#if defined(__APPLE__) || defined(__MACH__)
310 compressed_file_writing_mutex.lock ();
311#endif
312 if (!absolute_command_path)
313 MSG ("could not find '%s' in 'PATH' environment variable", argv[0]);
314 else if (::pipe (pipe_fds) < 0)
315 MSG ("could not generate pipe to '%s' command", command);
316 else if ((out = ::open (path, O_CREAT | O_TRUNC | O_WRONLY, 0644)) < 0)
317 MSG ("could not open '%s' for writing", path);
318 else if ((child_pid = ::fork ()) < 0) {
319 MSG ("could not fork process to execute '%s' command", command);
320 ::close (out);
321 } else if (child_pid) {
322 ::close (pipe_fds[0]);
323 res = ::fdopen (pipe_fds[1], "wb");
324 } else {
325
326 // Connect stdin and stdout in child
327
328 ::dup2 (pipe_fds[0], 0);
329 ::dup2 (out, 1);
330
331 // Make sure to close all non-required fds to not cause hangs.
332 // This is handled now by closefrom and remains for documentation
333 // purposes:
334 //
335 // ::close (pipe_fds[0]);
336 // ::close (pipe_fds[1]);
337 // ::close (out);
338
339 // Surpress '7z' verbose output on 'stderr'.
340
341 if (command[0] == '7') {
342 ::close (2);
343 }
344
345 // Before the fork another thread could have created more fds. These
346 // fds are cloned into the child process. As this inhibits pipes to
347 // be closed by the parent process we have to close all of the
348 // erroneously cloned fds here.
349
350#ifndef CADICAL_NCLOSEFROM
351 ::closefrom (3);
352#else
353 // Simplistic replacement on Unix without 'closefrom'.
354 for (int fd = 3; fd != FD_SETSIZE; fd++)
355 ::close (fd);
356#endif
357 execv (absolute_command_path, argv);
358 _exit (1);
359 }
360 if (absolute_command_path)
361 delete[] absolute_command_path;
362 delete_str_vector (args);
363#ifdef CADICAL_QUIET
364 (void) internal;
365#endif
366#if defined(__APPLE__) || defined(__MACH__)
367 if (!res)
368 compressed_file_writing_mutex.unlock ();
369#endif
370 return res;
371}
372
373#endif
374
375/*------------------------------------------------------------------------*/
376
377File *File::read (Internal *internal, FILE *f, const char *n) {
378 return new File (internal, false, 0, 0, f, n);
379}
380
381File *File::write (Internal *internal, FILE *f, const char *n) {
382 return new File (internal, true, 0, 0, f, n);
383}
384
385File *File::read (Internal *internal, const char *path) {
386 FILE *file;
387 int close_input = 2;
388 if (has_suffix (path, ".xz")) {
389 file = read_pipe (internal, "xz -c -d %s", xzsig, path);
390 if (!file)
391 goto READ_FILE;
392 } else if (has_suffix (path, ".lzma")) {
393 file = read_pipe (internal, "lzma -c -d %s", lzmasig, path);
394 if (!file)
395 goto READ_FILE;
396 } else if (has_suffix (path, ".bz2")) {
397 file = read_pipe (internal, "bzip2 -c -d %s", bz2sig, path);
398 if (!file)
399 goto READ_FILE;
400 } else if (has_suffix (path, ".gz")) {
401 file = read_pipe (internal, "gzip -c -d %s", gzsig, path);
402 if (!file)
403 goto READ_FILE;
404 } else if (has_suffix (path, ".7z")) {
405 file = read_pipe (internal, "7z x -so %s 2>/dev/null", sig7z, path);
406 if (!file)
407 goto READ_FILE;
408 } else {
409 READ_FILE:
410 file = read_file (internal, path);
411 close_input = 1;
412 }
413
414 if (!file)
415 return 0;
416
417 return new File (internal, false, close_input, 0, file, path);
418}
419
420File *File::write (Internal *internal, const char *path) {
421 FILE *file;
422 int close_output = 3, child_pid = 0;
423#ifndef _WIN32
424 if (has_suffix (path, ".xz"))
425 file = write_pipe (internal, "xz -c", path, child_pid);
426 else if (has_suffix (path, ".bz2"))
427 file = write_pipe (internal, "bzip2 -c", path, child_pid);
428 else if (has_suffix (path, ".gz"))
429 file = write_pipe (internal, "gzip -c", path, child_pid);
430 else if (has_suffix (path, ".7z"))
431 file = write_pipe (internal, "7z a -an -txz -si -so", path, child_pid);
432 else
433#endif
434 file = write_file (internal, path), close_output = 1;
435
436 if (!file)
437 return 0;
438
439 return new File (internal, true, close_output, child_pid, file, path);
440}
441
442void File::close (bool print) {
443 CADICAL_assert (file);
444#ifndef CADICAL_QUIET
445 if (internal->opts.quiet)
446 print = false;
447 else if (internal->opts.verbose > 0)
448 print = true;
449#endif
450 if (close_file == 0) {
451 if (print)
452 MSG ("disconnecting from '%s'", name ());
453 }
454 if (close_file == 1) {
455 if (print)
456 MSG ("closing file '%s'", name ());
457 fclose (file);
458 }
459 if (close_file == 2) {
460 if (print)
461 MSG ("closing input pipe to read '%s'", name ());
462 pclose (file);
463 }
464#ifndef _WIN32
465 if (close_file == 3) {
466 if (print)
467 MSG ("closing output pipe to write '%s'", name ());
468 fclose (file);
469 waitpid (child_pid, 0, 0);
470#if defined(__APPLE__) || defined(__MACH__)
471 compressed_file_writing_mutex.unlock ();
472#endif
473 }
474#endif
475 file = 0; // mark as closed
476
477 // TODO what about error checking for 'fclose', 'pclose' or 'waitpid'?
478
479#ifndef CADICAL_QUIET
480 if (print) {
481 if (writing) {
482 uint64_t written_bytes = bytes ();
483 double written_mb = written_bytes / (double) (1 << 20);
484 MSG ("after writing %" PRIu64 " bytes %.1f MB", written_bytes,
485 written_mb);
486 if (close_file == 3) {
487 size_t actual_bytes = size (name ());
488 if (actual_bytes) {
489 double actual_mb = actual_bytes / (double) (1 << 20);
490 MSG ("deflated to %zd bytes %.1f MB", actual_bytes, actual_mb);
491 MSG ("factor %.2f (%.2f%% compression)",
492 relative (written_bytes, actual_bytes),
493 percent (actual_bytes, written_bytes));
494 } else
495 MSG ("but could not determine actual size of written file");
496 }
497 } else {
498 uint64_t read_bytes = bytes ();
499 double read_mb = read_bytes / (double) (1 << 20);
500 MSG ("after reading %" PRIu64 " bytes %.1f MB", read_bytes, read_mb);
501 if (close_file == 2) {
502 size_t actual_bytes = size (name ());
503 double actual_mb = actual_bytes / (double) (1 << 20);
504 MSG ("inflated from %zd bytes %.1f MB", actual_bytes, actual_mb);
505 MSG ("factor %.2f (%.2f%% compression)",
506 relative (read_bytes, actual_bytes),
507 percent (actual_bytes, read_bytes));
508 }
509 }
510 }
511#endif
512}
513
514void File::flush () {
515 CADICAL_assert (file);
516 fflush (file);
517}
518
520 if (file)
521 close ();
522 free (_name);
523}
524
525} // namespace CaDiCaL
526
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define CADICAL_assert(ignore)
Definition global.h:14
#define CADICAL_QUIET
Definition global.h:8
#define CADICAL_NDEBUG
Definition global.h:5
#define LOG(...)
const char * name() const
Definition file.hpp:206
static bool match(Internal *, const char *path, const int *sig)
uint64_t bytes() const
Definition file.hpp:208
static char * find_program(const char *prg)
void close(bool print=false)
static bool exists(const char *path)
static File * write(Internal *, FILE *, const char *name)
static File * read(Internal *, FILE *f, const char *name)
static size_t size(const char *path)
static bool writable(const char *path)
Cube * p
Definition exorList.c:222
struct file file
Definition file.h:21
#define cadical_getc_unlocked
Definition file.hpp:23
#define MSG(...)
Definition message.hpp:49
#define WARNING(...)
Definition message.hpp:65
bool has_suffix(const char *str, const char *suffix)
double relative(double a, double b)
Definition util.hpp:20
double percent(double a, double b)
Definition util.hpp:21
else if(last->value< newval)
Definition sparse_int.h:41
Definition mode.h:11
int pclose()
char * strrchr()
int strlen()
char * strncpy()
int strcmp()
char * strcpy()
VOID_HACK free()
char * getenv()
FILE * popen()