tests: add Feature/KleeStatsBranches.c

1 files changed, 84 insertions, 0 deletions

diff --git a/test/Feature/KleeStatsBranches.c b/test/Feature/KleeStatsBranches.c
new file mode 100644
index 00000000..a1bf2721
--- /dev/null
+++ b/test/Feature/KleeStatsBranches.c
@@ -0,0 +1,84 @@
+// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-no-tests --output-dir=%t.klee-out %t.bc 2> %t.log
+// RUN: %klee-stats --print-columns 'BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal' --table-format=csv %t.klee-out > %t.stats
+// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s
+
+#include "klee/klee.h"
+
+#include <stdlib.h>
+
+
+void foo(void) {}
+void bar(void) {}
+
+int memop(void) {
+  int *p;
+  klee_make_symbolic(&p, sizeof(p), "p");
+  return *p;
+}
+
+
+int main(void) {
+  // alloc
+  size_t size0;
+  klee_make_symbolic(&size0, sizeof(size_t), "size0");
+  klee_assume(size0 < 10);
+  void *p;
+
+  // realloc
+  size_t size1;
+  klee_make_symbolic(&size1, sizeof(size_t), "size1");
+  klee_assume(size1 < 20);
+
+  // conditional
+  int cond;
+  klee_make_symbolic(&cond, sizeof(cond), "cond");
+
+  // switch
+  int sw_cond;
+  klee_make_symbolic(&sw_cond, sizeof(sw_cond), "sw_cond");
+
+  // call
+  void (*fptr)(void);
+  klee_make_symbolic(&fptr, sizeof(fptr), "fptr");
+  klee_assume((fptr == &foo) | (fptr == &bar));
+
+  // indirectbr
+  void *lptr;
+  klee_make_symbolic(&lptr, sizeof(lptr), "lptr");
+  klee_assume((lptr == &&one) | (lptr == &&two));
+  goto *lptr;
+
+
+one:
+  p = malloc(size0);
+  if (p) {
+    p = realloc(p, size1);
+    if (p) {
+      // free
+      klee_make_symbolic(&p, sizeof(p), "p");
+      free(p);
+    }
+  }
+
+  return 1;
+
+two:
+  switch (sw_cond) {
+  case 8: memop(); break; // memop
+  case 15: (*fptr)(); break;
+  default: {
+    int c = 42;
+    // conditional
+    if (cond) c++;
+    return c;
+  }
+  }
+
+  return 2;
+}
+
+// Check that we create branches
+// CHECK-STATS: BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal
+// CHECK-STATS: 1,1,2,1,{{[1-9][0-9]*}},{{[1-9][0-9]*}},2,1,1,0