Added Files

tutorial-1/get_sign.c

+/*
+ * First KLEE tutorial: testing a small function
+ */
+
+#include <klee/klee.h>
+
+int get_sign(int x) {
+  if (x == 0)
+     return 0;
+  
+  if (x < 0)
+     return -1;
+  else 
+     return 1;
+} 
+
+int main() {
+  int a;
+  klee_make_symbolic(&a, sizeof(a), "a");
+  return get_sign(a);
+} 
\ No newline at end of file

tutorial-2/Regexp.c

+/* 
+ * 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(re, sizeof re, "re");
+
+  // Try to match against a constant string "hello".
+  match(re, "hello");
+
+  return 0;
+}
\ No newline at end of file

tutorial-2/Regexp1.c

+/* 
+ * 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(re, sizeof re, "re");
+  re[SIZE - 1] = '\0';
+
+  // Try to match against a constant string "hello".
+  match(re, "hello");
+
+  return 0;
+}
\ No newline at end of file

tutorial-2/Regexp2.c

+/* 
+ * 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(re, sizeof re, "re");
+  klee_assume(re[SIZE - 1] == '\0');
+
+  // Try to match against a constant string "hello".
+  match(re, "hello");
+
+  return 0;
+}
\ No newline at end of file

tutorial-3/password.c

+#include <stdio.h>
+
+int check_password(char *buf) {
+  if (buf[0] == 'h' && buf[1] == 'e' &&
+      buf[2] == 'l' && buf[3] == 'l' &&
+      buf[4] == 'o')
+    return 1;
+  return 0;
+}
+
+int main(int argc, char **argv) {
+  if (argc < 2)
+     return 1;
+  
+  if (check_password(argv[1])) {
+    printf("Password found!\n");
+    return 0;
+  }
+
+  return 1;
+}
\ No newline at end of file

tutorial-3/password1.c

+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
+#include <stdio.h>
+#include <unistd.h>
+
+int check_password(int fd) {
+  char buf[5];
+  if (read(fd, buf, 5) != -1) {
+    if (buf[0] == 'h' && buf[1] == 'e' &&
+	buf[2] == 'l' && buf[3] == 'l' &&
+	buf[4] == 'o')
+      return 1;
+  }
+  return 0;
+}
+
+int main(int argc, char **argv) {
+  int fd;
+
+  if (argc >= 2) {
+    if ((fd = open(argv[1], O_RDONLY)) != -1) {
+      if (check_password(fd)) {
+        printf("Password found in %s\n", argv[1]);
+        close(fd);
+        return 0;
+      }
+      close(fd);
+      return 1;
+    }
+  }
+
+  if (check_password(0)) {
+    printf("Password found in standard input\n");
+    return 0;
+  }
+
+  return 1;
+}
\ No newline at end of file