about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2016-07-08 14:42:34 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2016-07-08 14:48:28 +0200
commit00cdc62b7a8df39d13f734ecc77077e427912f64 (patch)
tree46ab249dc52b28fdb2cc760a31534ae1333e5cb3 /include
parent0d199e6174fa03893a64e3781368410368a1235c (diff)
downloadklee-00cdc62b7a8df39d13f734ecc77077e427912f64.tar.gz
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.
Diffstat (limited to 'include')
-rw-r--r--include/klee/Config/config.h.in3
-rw-r--r--include/klee/Internal/Support/CompressionStream.h46
2 files changed, 49 insertions, 0 deletions
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 008b2f90..87d6ee75 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -69,6 +69,9 @@
 /* Z3 needs a Z3_context passed to Z3_get_error_msg() */
 #undef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT
 
+/* Define to 1 if you have the <zlib.h> header file. */
+#undef HAVE_ZLIB_H
+
 /* Define to empty or 'const' depending on how SELinux qualifies its security
    context parameters. */
 #undef KLEE_SELINUX_CTX_CONST
diff --git a/include/klee/Internal/Support/CompressionStream.h b/include/klee/Internal/Support/CompressionStream.h
new file mode 100644
index 00000000..fda68d89
--- /dev/null
+++ b/include/klee/Internal/Support/CompressionStream.h
@@ -0,0 +1,46 @@
+//===-- CompressionStream.h --------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_
+#define INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_
+
+#include "llvm/Support/raw_ostream.h"
+#include "zlib.h"
+
+namespace klee {
+const size_t BUFSIZE = 128 * 1024;
+
+class compressed_fd_ostream : public llvm::raw_ostream {
+  int FD;
+  uint8_t buffer[BUFSIZE];
+  z_stream strm;
+  uint64_t pos;
+
+  /// write_impl - See raw_ostream::write_impl.
+  virtual void write_impl(const char *Ptr, size_t Size);
+  void write_file(const char *Ptr, size_t Size);
+
+  virtual uint64_t current_pos() const { return pos; }
+
+  void flush_compressed_data();
+  void writeFullCompressedData();
+
+public:
+  /// compressed_fd_ostream - Open the specified file for writing. If an error
+  /// occurs, information about the error is put into ErrorInfo, and the stream
+  /// should be immediately destroyed; the string will be empty if no error
+  /// occurred. This allows optional flags to control how the file will be
+  /// opened.
+  compressed_fd_ostream(const char *Filename, std::string &ErrorInfo);
+
+  ~compressed_fd_ostream();
+};
+}
+
+#endif /* INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_ */