8 files changed, 166 insertions, 0 deletions
diff --git a/test/DeterministicAllocation/OneOutOfBounds.c b/test/DeterministicAllocation/OneOutOfBounds.c
new file mode 100644
index 00000000..499ff06b
--- /dev/null
+++ b/test/DeterministicAllocation/OneOutOfBounds.c
@@ -0,0 +1,12 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --kdalloc %t.bc 2>&1 | FileCheck %s
+// RUN: test -f %t.klee-out/test000001.ptr.err
+
+int main() {
+  int *x = malloc(sizeof(int));
+  // CHECK: OneOutOfBounds.c:[[@LINE+1]]: memory error: out of bound pointer
+  x[1] = 1;
+  free(x);
+  return 0;
+}
diff --git a/test/DeterministicAllocation/double-free-loh.c b/test/DeterministicAllocation/double-free-loh.c
new file mode 100644
index 00000000..f37b4777
--- /dev/null
+++ b/test/DeterministicAllocation/double-free-loh.c
@@ -0,0 +1,16 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+
+int main() {
+  void *ptr = malloc(4096);
+  free(ptr);
+
+  // CHECK: double free
+  free(ptr);
+
+  return 0;
+}
diff --git a/test/DeterministicAllocation/double-free.c b/test/DeterministicAllocation/double-free.c
new file mode 100644
index 00000000..141427fa
--- /dev/null
+++ b/test/DeterministicAllocation/double-free.c
@@ -0,0 +1,16 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+
+int main() {
+  void *ptr = malloc(8);
+  free(ptr);
+
+  // CHECK: double free
+  free(ptr);
+
+  return 0;
+}
diff --git a/test/DeterministicAllocation/madvise.c b/test/DeterministicAllocation/madvise.c
new file mode 100644
index 00000000..bbaff5e8
--- /dev/null
+++ b/test/DeterministicAllocation/madvise.c
@@ -0,0 +1,49 @@
+// REQUIRES: not-msan && not-asan
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out %t.log
+// RUN: %klee -kdalloc -kdalloc-quarantine=-1 -output-dir=%t.klee-out %t.bc -exit-on-error 2>&1 | tee %t.log
+// RUN: FileCheck %s -input-file=%t.log
+
+// This test is disabled for asan and msan because they create additional page faults
+
+#include <assert.h>
+#include <stddef.h>
+#include <stdlib.h>
+#include <sys/resource.h>
+
+#include "klee/klee.h"
+
+size_t maxrss() {
+  struct rusage usage;
+  int res = getrusage(RUSAGE_SELF, &usage);
+  assert(!res && "getrusage succeeded");
+  return usage.ru_maxrss;
+}
+
+int main(void) {
+  size_t baseline = maxrss();
+#if defined(__APPLE__)
+  size_t limit = baseline + 100 * 1024 * 1024; // limit is 100 MiB above baseline
+#else
+  size_t limit = baseline + 100 * 1024; // limit is 100 MiB above baseline
+#endif
+
+  // CHECK: Deterministic allocator: Using unlimited quarantine
+
+  size_t bins[] = {1, 4, 8, 16, 32, 64, 256, 2048};
+  for (int i = 0; i < 1000; ++i) {
+    for (size_t j = 0; j < sizeof(bins) / sizeof(*bins); ++j) {
+      void *volatile p = malloc(bins[j]);
+      void *volatile p2 = malloc(4096); // for faster growth
+
+      // CHECK: calling external: getrusage
+      // CHECK-NOT: ASSERTION FAIL
+      assert(maxrss() < limit && "MaxRSS is below limit");
+
+      free(p);
+      free(p2);
+    }
+  }
+
+  return 0;
+}
\ No newline at end of file
diff --git a/test/DeterministicAllocation/nullpage-read.c b/test/DeterministicAllocation/nullpage-read.c
new file mode 100644
index 00000000..15bdfd7d
--- /dev/null
+++ b/test/DeterministicAllocation/nullpage-read.c
@@ -0,0 +1,20 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+#include <string.h>
+
+int main() {
+  struct {
+    int x;
+    int y;
+  } *ptr = NULL;
+
+  // CHECK: null page access
+  int y;
+  memcpy(&y, &ptr->y, sizeof(ptr->y));
+
+  return 0;
+}
diff --git a/test/DeterministicAllocation/nullpage-write.c b/test/DeterministicAllocation/nullpage-write.c
new file mode 100644
index 00000000..950e2e17
--- /dev/null
+++ b/test/DeterministicAllocation/nullpage-write.c
@@ -0,0 +1,19 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+#include <string.h>
+
+int main() {
+  struct {
+    int x;
+    int y;
+  } *ptr = NULL;
+
+  // CHECK: null page access
+  memset(&ptr->y, 0, sizeof(ptr->y));
+
+  return 0;
+}
diff --git a/test/DeterministicAllocation/use-after-free-loh.c b/test/DeterministicAllocation/use-after-free-loh.c
new file mode 100644
index 00000000..5a576b42
--- /dev/null
+++ b/test/DeterministicAllocation/use-after-free-loh.c
@@ -0,0 +1,17 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+#include <string.h>
+
+int main() {
+  void *ptr = malloc(4096);
+  free(ptr);
+
+  // CHECK: use after free
+  memset(ptr, 0, 4096);
+
+  return 0;
+}
diff --git a/test/DeterministicAllocation/use-after-free.c b/test/DeterministicAllocation/use-after-free.c
new file mode 100644
index 00000000..c4a14435
--- /dev/null
+++ b/test/DeterministicAllocation/use-after-free.c
@@ -0,0 +1,17 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+#include <string.h>
+
+int main() {
+  void *ptr = malloc(8);
+  free(ptr);
+
+  // CHECK: use after free
+  memset(ptr, 0, 8);
+
+  return 0;
+}