Add enhancements for PAAR2022

  - Quapify: Simplify command line use with more messages.
  - Quapify: Add some new printing features (see -h).
  - Quapify: Support solving without adding assumptions
  - QuAPI: Add Zero-Copy support for big formulas as compile time
    option. Enable using -DENABLE_ZEROCOPY with cmake.
  - QuAPI: Add ZLib function injection support, so that Minisat works.
  - QuAPI: Add error for when not compiling on Linux (as only
    Linux is supported currently).
  - QuAPI: Add error message for when read() injection didn't work.
  - QuAPI: Remove strict requirement for PCRE2. Builds now also work
    without the library being installed, but parsing a solver's
    stdout is disabled if PCRE2 support is not compiled in. QuAPI exits
    if one tries to use regular expressions without PCRE2.
  - General: Add some scripts for running on slurm clusters.

CMakeLists.txt

@@ -1,20 +1,25 @@
 cmake_minimum_required(VERSION 3.9.4)
 project(quapi)
 
+if(NOT ${CMAKE_SYSTEM_NAME} STREQUAL "Linux")
+    message(FATAL_ERROR "Currently, QuAPI only supports Linux! In the future, The BSDs (FreeBSD, etc) and MacOS may be supported. Windows has too little support for preloading libraries reliably. This system is ${CMAKE_SYSTEM_NAME}")
+endif()
+
 include(GenerateExportHeader)
 
 set(CMAKE_MODULE_PATH
     "${CMAKE_CURRENT_SOURCE_DIR}/cmake/"
     ${CMAKE_MODULE_PATH})
 
 # Required PCRE2 Library for SAT and UNSAT matching
-find_package(PCRE2 REQUIRED)
+find_package(PCRE2)
 
 set(CMAKE_CXX_VISIBILITY_PRESET hidden)
 set(CMAKE_C_VISIBILITY_PRESET hidden)
 set(CMAKE_VISIBILITY_INLINES_HIDDEN 1)
 
 option(DEBUG_ENABLE_ADDRESS_SANITIZER "enable address sanitizer" OFF)
+option(ENABLE_ZEROCOPY "enable \"zerocopy\" using vmsplice, splice, memfd, and mmap for pipe communication" OFF)
 
 set(LIBASAN_PATH "")
 

common/CMakeLists.txt

@@ -1,5 +1,6 @@
 set(COMMON_SRCS
     src/common.c
+    src/zero-copy-pipes-linux.c
     )
 
 add_library(quapi_common ${COMMON_SRCS})
@@ -8,3 +9,7 @@ target_include_directories(quapi_common
     PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}/include)
 
 set_property(TARGET quapi_common PROPERTY POSITION_INDEPENDENT_CODE ON)
+
+if(ENABLE_ZEROCOPY)
+    target_compile_definitions(quapi_common PUBLIC QUAPI_USE_ZEROCOPY_IF_AVAILABLE)
+endif()

common/include/quapi/definitions.h

@@ -30,7 +30,7 @@ extern "C" {
 /// The API version may increase with time and is sent with the header message.
 /// The runtime then may switch to other processing strategies if older API
 /// versions were received.
-#define QUAPI_API_VERSION 1
+#define QUAPI_API_VERSION 2
 
 typedef enum quapi_state {
   QUAPI_INPUT,
@@ -118,12 +118,21 @@ dbg(const char* format, ...);
 void
 err(const char* format, ...);
 
+struct gzFile_s {
+  unsigned have;
+  unsigned char* next;
+  int64_t pos;
+};
+
 typedef ssize_t (*read_t)(int, void*, size_t);
 typedef ssize_t (*fread_t)(void*, size_t, size_t, FILE*);
 typedef int (*getc_t)(FILE*);
 typedef int (*fgetc_t)(FILE*);
 typedef int (*getc_unlocked_t)(FILE*);
 typedef int (*fgetc_unlocked_t)(FILE*);
+typedef struct gzFile_s* (*gzdopen_t)(int fd, const char* mode);
+typedef int (*gzread_t)(struct gzFile_s*, char* buf, unsigned int len);
+typedef int (*gzclose_t)(struct gzFile_s*);
 
 #ifdef __cplusplus
 }

common/include/quapi/message.h

@@ -2,6 +2,7 @@
 #define QUAPI_MESSAGE_H
 
 #include <quapi/definitions.h>
+#include <quapi/zero-copy-pipes-linux.h>
 
 #ifdef __cplusplus
 extern "C" {
@@ -18,13 +19,17 @@ typedef enum quapi_msg_type {
   QUAPI_MSG_LITERAL,
   QUAPI_MSG_FORK,
   QUAPI_MSG_FORK_REPORT,
+  QUAPI_MSG_STARTED,
   QUAPI_MSG_SOLVE,
   QUAPI_MSG_EXIT_CODE,
   QUAPI_MSG_DESTRUCTED,
 } quapi_msg_type;
 
 typedef uint8_t quapi_msg_type_packed;
 
+bool
+quapi_msg_is_known(quapi_msg_type t);
+
 const char*
 quapi_msg_type_str(quapi_msg_type t);
 
@@ -44,6 +49,10 @@ typedef struct quapi_msg_fork {
   int wait_for_exit_code_and_report : 1;
 } quapi_msg_fork;
 
+typedef struct quapi_msg_started {
+  int32_t api_version;
+} quapi_msg_started;
+
 typedef struct quapi_msg_fork_report {
   pid_t solver_child_pid;
 } quapi_msg_fork_report;
@@ -61,11 +70,13 @@ typedef union quapi_msg_data {
   quapi_msg_lit literal;
   quapi_msg_fork fork;
   quapi_msg_fork_report fork_report;
+  quapi_msg_started started;
   quapi_msg_solve solve;
   quapi_msg_exit_code exit_code;
 } quapi_msg_data;
 
-typedef struct quapi_msg_inner {
+// Packed, so that only 5 bytes have to be communicated.
+typedef struct __attribute__((__packed__)) quapi_msg_inner {
   quapi_msg_data data;
   quapi_msg_type_packed type;
 } quapi_msg_inner;
@@ -90,7 +101,9 @@ quapi_write_msg_to_fd(int fd, quapi_msg* msg, quapi_msg_header_data* hdata);
  * when sending a header message.
  */
 quapi_status
-quapi_write_msg_to_file(FILE* f, quapi_msg* msg, quapi_msg_header_data* hdata);
+quapi_write_msg_to_file(ZEROCOPY_PIPE_OR_FILE* f,
+                        quapi_msg* msg,
+                        quapi_msg_header_data* hdata);
 
 /** @brief Read a message from a file descriptor
  */
@@ -102,11 +115,18 @@ quapi_read_msg_from_fd(int fd,
 
 /** @brief Read a message from a file stream
  */
+#ifdef USING_ZEROCOPY
+quapi_msg*
+quapi_read_msg_from_file(ZEROCOPY_PIPE_OR_FILE* f,
+                         quapi_msg_header_data* hdata,
+                         fread_t fread);
+#else
 bool
-quapi_read_msg_from_file(FILE* f,
+quapi_read_msg_from_file(ZEROCOPY_PIPE_OR_FILE* f,
                          quapi_msg* msg,
                          quapi_msg_header_data* hdata,
                          fread_t fread);
+#endif
 
 #ifdef __cplusplus
 }

common/include/quapi/zero-copy-pipes-linux.h

@@ -0,0 +1,66 @@
+#ifndef QUAPI_ZERO_COPY_LINUX_H
+#define QUAPI_ZERO_COPY_LINUX_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/* This optimization is based on this article:
+ * https://mazzo.li/posts/fast-pipes.html
+ *
+ * It replaces FILE and fwrite with a custom implementation based on zero-copy
+ * splicing into and out of buffers.
+ */
+
+#if defined(__linux__) && defined(QUAPI_USE_ZEROCOPY_IF_AVAILABLE)
+#define USING_ZEROCOPY
+
+#include <stddef.h>
+#include <stdint.h>
+#include <sys/types.h>
+
+typedef struct quapi_zerocopy_pipe quapi_zerocopy_pipe;
+
+quapi_zerocopy_pipe*
+quapi_zerocopy_pipe_fdopen(int fd, const char* mode);
+
+void
+quapi_zerocopy_pipe_close(quapi_zerocopy_pipe* pipe);
+
+ssize_t
+quapi_zerocopy_pipe_write(const void* data,
+                          size_t size,
+                          size_t count,
+                          quapi_zerocopy_pipe* pipe);
+
+void*
+quapi_zerocopy_pipe_prepare_write(size_t size,
+                                  size_t count,
+                                  quapi_zerocopy_pipe* pipe);
+
+void
+quapi_zerocopy_pipe_flush(quapi_zerocopy_pipe* pipe);
+
+void*
+quapi_zerocopy_pipe_read(size_t size, quapi_zerocopy_pipe* pipe);
+
+#define QUAPI_GIVE_MSGS(NAME, COUNT, PIPE) \
+  quapi_msg* NAME =                        \
+    quapi_zerocopy_pipe_prepare_write(sizeof(quapi_msg), COUNT, PIPE);
+
+#define ZEROCOPY_PIPE_OR_FILE quapi_zerocopy_pipe
+
+#else
+
+#define QUAPI_GIVE_MSGS(NAME, COUNT, IGNORED) \
+  quapi_msg NAME##_[COUNT];                   \
+  quapi_msg* NAME = &NAME##_[0];
+
+#define ZEROCOPY_PIPE_OR_FILE FILE
+#endif
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif