Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 166 insertions, 0 deletions

diff --git a/examples/regexp/Regexp.c b/examples/regexp/Regexp.c
new file mode 100644
index 00000000..f3e751f9
--- /dev/null
+++ b/examples/regexp/Regexp.c
@@ -0,0 +1,62 @@
+/* 
+ * Simple regular expression matching.
+ *
+ * From:
+ *   The Practice of Programming
+ *   Brian W. Kernighan, Rob Pike
+ *
+ */ 
+
+#include <klee/klee.h>
+
+static int matchhere(char*,char*);
+
+static int matchstar(int c, char *re, char *text) {
+  do {
+    if (matchhere(re, text))
+      return 1;
+  } while (*text != '\0' && (*text++ == c || c== '.'));
+  return 0;
+}
+
+static int matchhere(char *re, char *text) {
+  if (re[0] == '\0')
+     return 0;
+  if (re[1] == '*')
+    return matchstar(re[0], re+2, text);
+  if (re[0] == '$' && re[1]=='\0')
+    return *text == '\0';
+  if (*text!='\0' && (re[0]=='.' || re[0]==*text))
+    return matchhere(re+1, text+1);
+  return 0;
+}
+
+int match(char *re, char *text) {
+  if (re[0] == '^')
+    return matchhere(re+1, text);
+  do {
+    if (matchhere(re, text))
+      return 1;
+  } while (*text++ != '\0');
+  return 0;
+}
+
+/*
+ * Harness for testing with KLEE.
+ */
+
+// The size of the buffer to test with.
+#define SIZE 7
+
+int main() {
+  // The input regular expression.
+  char re[SIZE];
+  
+  // Make the input symbolic. 
+  klee_make_symbolic_name(re, sizeof re, "re");
+
+  // Try to match against a constant string "hello".
+  match(re, "hello");
+
+  return 0;
+}
diff --git a/examples/regexp/notes.txt b/examples/regexp/notes.txt
new file mode 100644
index 00000000..7d25585c
--- /dev/null
+++ b/examples/regexp/notes.txt
@@ -0,0 +1,26 @@
+clang -m32 -I ~/private/klee/include -c -emit-llvm Regexp.c
+
+klee Regexp.o
+klee --only-output-states-covering-new Regexp.o
+ls -l klee-out-0
+ls -l klee-out-1
+ls -l klee-last
+
+cd klee-last
+klee-bout-tool *.bout
+klee-bout-tool --trim-zeros *.bout
+
+Stuff to show:
+Adding klee_prefer_cex
+
+PrintStats.py klee-last
+
+PrintStats.py klee-last
+Why not 100% coverage?
+
+clang -g -m32 -I ~/private/klee/include -c -emit-llvm Regexp.c
+
+KCachegrind?
+
+Disable klee_assume, show coverage again (why is klee-check-div getting pulled
+in?)
diff --git a/examples/sort/sort.c b/examples/sort/sort.c
new file mode 100644
index 00000000..a1629c6b
--- /dev/null
+++ b/examples/sort/sort.c
@@ -0,0 +1,78 @@
+#include <klee/klee.h>
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <assert.h>
+
+static void insert_ordered(int *array, unsigned nelem, int item) {
+  unsigned i = 0;
+
+  for (; i != nelem; ++i) {
+    if (item < array[i]) {
+      memmove(&array[i+1], &array[i], sizeof(*array) * (nelem - i));
+      break;
+    }
+  }
+
+  array[i] = item;
+}
+
+void bubble_sort(int *array, unsigned nelem) {
+  for (;;) {
+    int done = 1;
+
+    for (unsigned i = 0; i + 1 < nelem; ++i) {
+      if (array[i+1] < array[i]) {
+        int t = array[i + 1];
+        array[i + 1] = array[i];
+        array[i] = t;
+        done = 0;
+      }
+    }
+
+    break;
+  }
+}
+
+void insertion_sort(int *array, unsigned nelem) {
+  int *temp = malloc(sizeof(*temp) * nelem);
+
+  for (unsigned i = 0; i != nelem; ++i)
+    insert_ordered(temp, i, array[i]);
+
+  memcpy(array, temp, sizeof(*array) * nelem);
+  free(temp);
+}
+
+void test(int *array, unsigned nelem) {
+  int *temp1 = malloc(sizeof(*array) * nelem);
+  int *temp2 = malloc(sizeof(*array) * nelem);
+
+  printf("input: [%d, %d, %d, %d]\n",
+         array[0], array[1], array[2], array[3]);
+
+  memcpy(temp1, array, sizeof(*array) * 4);
+  memcpy(temp2, array, sizeof(*array) * 4);
+
+  insertion_sort(temp1, 4);
+  bubble_sort(temp2, 4);
+
+  printf("insertion_sort: [%d, %d, %d, %d]\n",
+         temp1[0], temp1[1], temp1[2], temp1[3]);
+
+  printf("bubble_sort   : [%d, %d, %d, %d]\n",
+         temp2[0], temp2[1], temp2[2], temp2[3]);
+
+  for (unsigned i = 0; i != nelem; ++i)
+    assert(temp1[i] == temp2[i]);
+}
+
+int main() {
+  int input[4] = { 4, 3, 2, 1};
+
+  klee_make_symbolic(&input, sizeof(input));
+  test(input, 4);
+
+  return 0;
+}