From eba0093c4887473be2562a7ab4e16b3d09793f4e Mon Sep 17 00:00:00 2001 From: Andrea Mattavelli Date: Thu, 12 May 2016 11:17:48 +0100 Subject: Modified -debug-print-instructions to allow to write directly on log file. The option now contains 4 different options: 1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst]; 2) src:stderr, which logs all instructions to file in format [src, inst_id]; 3) compact:stderr, which logs all instructions to file in format [inst_id]; 4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst]; 5) src:file, which logs all instructions to file in format [src, inst_id]; 6) compact:file, which logs all instructions to file in format [inst_id]; Writing to file gives a speedup of ~50x. --- test/Feature/LoggingInstructions.c | 47 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 test/Feature/LoggingInstructions.c (limited to 'test') diff --git a/test/Feature/LoggingInstructions.c b/test/Feature/LoggingInstructions.c new file mode 100644 index 00000000..049aa9da --- /dev/null +++ b/test/Feature/LoggingInstructions.c @@ -0,0 +1,47 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=all:stderr %t2.bc 2>%t3.txt +// RUN: FileCheck -input-file=%t3.txt -check-prefix=CHECK-FILE-SRC %s +// RUN: FileCheck -input-file=%t3.txt -check-prefix=CHECK-FILE-DBG %s +// RUN: not test -f %t.klee-out/instructions.txt +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=all:file %t2.bc +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-DBG %s +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-SRC %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=src:file %t2.bc +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-SRC %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=compact:file %t2.bc +// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-COMPACT %s +// +#include "klee/klee.h" +#include +#include + +char array[5] = { 1, 2, 3, -4, 5 }; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + if (array[k] == -4) + printf("Yes\n"); + + // CHECK-FILE-SRC: LoggingInstructions.c:27 + // CHECK-FILE-SRC: LoggingInstructions.c:28 + // CHECK-FILE-SRC: LoggingInstructions.c:30 + // CHECK-FILE-SRC: LoggingInstructions.c:31 + + // CHECK-FILE-DBG: call void @klee_make_symbolic + // CHECK-FILE-DBG: load + + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:21 + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:22 + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:24 + // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:25 + + return 0; +} -- cgit 1.4.1