Support gzip-based compression of raw_outstreams

Provide initial zlib-based compression support for
raw_outstreams. Replacing llvm::raw_fd_outstreams
with compressed_fd_outstreams automatically compresses
data in gzip format before writing to file.

Options added:
* --compress-log to compress all query log files (e.g. *.pc, *.smt2) on
  the fly. Every query log file gets extended with .gz.
* --debug-compress-instructions to compress logfile for instruction
  stream on the fly.

1 files changed, 42 insertions, 0 deletions

diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c
new file mode 100644
index 00000000..a2a07d8b
--- /dev/null
+++ b/test/Feature/CompressedExprLogging.c
@@ -0,0 +1,42 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
+// We disable the cex-cache to eliminate nondeterminism across different
+// solvers, in particular when counting the number of queries in the last two
+// commands
+// RUN: rm -rf %t.klee-out %t.klee-out2
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc %t1.bc
+// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:pc %t1.bc
+// RUN: gunzip -d %t.klee-out2/all-queries.pc.gz
+// RUN: diff %t.klee-out/all-queries.pc %t.klee-out/all-queries.pc
+
+#include <assert.h>
+
+int constantArr[16] = {1 << 0,  1 << 1,  1 << 2,  1 << 3, 1 << 4,  1 << 5,
+                       1 << 6,  1 << 7,  1 << 8,  1 << 9, 1 << 10, 1 << 11,
+                       1 << 12, 1 << 13, 1 << 14, 1 << 15};
+
+int main() {
+  char buf[4];
+  klee_make_symbolic(buf, sizeof buf);
+
+  buf[1] = 'a';
+
+  constantArr[klee_range(0, 16, "idx.0")] = buf[0];
+
+  // Use this to trigger an interior update list usage.
+  int y = constantArr[klee_range(0, 16, "idx.1")];
+
+  constantArr[klee_range(0, 16, "idx.2")] = buf[3];
+
+  buf[klee_range(0, 4, "idx.3")] = 0;
+  klee_assume(buf[0] == 'h');
+
+  int x = *((int *)buf);
+  klee_assume(x > 2);
+  klee_assume(x == constantArr[12]);
+
+  klee_assume(y != (1 << 5));
+
+  assert(0);
+
+  return 0;
+}