From 00cdc62b7a8df39d13f734ecc77077e427912f64 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Fri, 8 Jul 2016 14:42:34 +0200 Subject: 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. --- test/Feature/CompressedExprLogging.c | 42 ++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 test/Feature/CompressedExprLogging.c (limited to 'test/Feature/CompressedExprLogging.c') 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 + +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; +} -- cgit 1.4.1