diff --git a/.gitattributes b/.gitattributes
index 8914d1ecbc2c12f32a711ee3626905ce321dc3c8..6b6e7dbd13fecd449f71079dc2169f2caacd15f4 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -18,10 +18,35 @@ demos/demo.jan_21_2011/gdb.demo.script -text
demos/demo.jan_21_2011/ps_demo.sh -text
demos/demo.jan_21_2011/run_gdb.sh -text
demos/demo.jan_21_2011/test_infinite.sh -text
+dyna_examples/Makefile -text
+dyna_examples/block_copy.c -text
+dyna_examples/cmd_args_005.c -text
+dyna_examples/concolic_test_handshake.c -text
+dyna_examples/data.txt -text
+dyna_examples/dumbledore_cmd.c -text
+dyna_examples/dumbledore_file.c -text
+dyna_examples/dumbledore_file_with_fopen_check.c -text
+dyna_examples/dumbledore_stdin.c -text
+dyna_examples/fptest.c -text
+dyna_examples/globalfield.c -text
+dyna_examples/hanoi.c -text
+dyna_examples/hanoi_heap_overrun.c -text
+dyna_examples/hanoi_nostrata.c -text
+dyna_examples/hanoi_overrun.c -text
+dyna_examples/hanoi_overrun_tainted.c -text
+dyna_examples/hanoi_overrun_taintedenv.c -text
+dyna_examples/hanoi_stack_overrun.c -text
+dyna_examples/hello.c -text
+dyna_examples/malloc.c -text
+dyna_examples/memcpy.c -text
+dyna_examples/myhanoi.c -text
+dyna_examples/print_ptr.c -text
+dyna_examples/recover_example.c -text
examples/Makefile -text
examples/block_copy.c -text
examples/cmd_args_005.c -text
examples/concolic_test_handshake.c -text
+examples/data.txt -text
examples/dumbledore_cmd.c -text
examples/dumbledore_file.c -text
examples/dumbledore_file_with_fopen_check.c -text
diff --git a/dyna_examples/Makefile b/dyna_examples/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..7b44cf83918ef2202c14fafcad631c859ac80205
--- /dev/null
+++ b/dyna_examples/Makefile
@@ -0,0 +1,69 @@
+
+
+
+
+CC=gcc
+CXX=g++
+CFLAGS=-O2
+
+.SUFFIXES: .o .c .cpp .exe
+
+exes=hanoi.exe hanoi_overrun.exe hanoi_heap_overrun.exe hanoi_stack_overrun.exe print_ptr.exe malloc.exe block_copy.exe hello.exe hanoi_overrun_tainted.exe hanoi_overrun_taintedenv.exe memcpy.exe cmd_args_005.exe dumbledore_stdin.exe dumbledore_cmd.exe dumbledore_file.exe
+
+
+all: env_check ${exes}
+
+
+
+.PHONY: env_check
+
+
+.o.exe:
+ $(CC) $< -o $@
+ ${PEASOUP_HOME}/tools/ps_analyze.sh $@ $@
+
+.c.o:
+ ${CC} $< -c
+
+.cpp.o:
+ ${CXX} $<
+
+chopzero:
+ @ if [ ! -f chopzero ]; then gcc chopzero.c -o chopzero -O3 ; fi
+
+$(exes): ${STRATA}/lib/x86_linux/libstrata.a
+
+
+
+env_check:
+ @echo checking env vars; \
+ if [ "X${TOOLCHAIN}" = "X" ]; then \
+ echo TOOLCHAIN environment variable should be set.; \
+ exit -1;\
+ elif [ "X${STRATA}" = "X" ]; then \
+ echo STRATA environment variable should be set. ;\
+ exit -1;\
+ elif [ "X${SMPSA_HOME}" = "X" ]; then \
+ echo SMPSA_HOME environment variable should be set.; \
+ exit -1;\
+ elif [ "X${PEASOUP_HOME}" = "X" ]; then \
+ echo PEASOUP_HOME environment variable should be set.; \
+ exit -1;\
+ elif [ "X${STRATA_HOME}" = "X" ]; then \
+ echo STRATA_HOME environment variable should be set.; \
+ exit -1;\
+ fi ;
+
+
+clean:
+ rm -f *.o *.syms *.map chopzero hanoi hanoi_overrun hanoi_heap_overrun malloc block_copy print_ptr hanoi_stack_overrun dumbledore a.out memcpy hanoi_overrun_taintedenv dumbledore_cmd hanoi_overrun_tainted hello cmd_args_005
+ rm -f *.exe *.dis *.data *.idb *.log *.ncexe *.annot *.readelf temp.* *.temp *.stratafied *.asm *.SMPobjdump *.id0 *.id1 *.til *.nam
+ rm -Rf concolic.files_*
+ rm -Rf peasoup_executable_directory.*
+ rm -f strata.log.*
+ rm -f *.sym
+ if [ ! "X" = "X"${PGUSER} ]; then sh ../tools/db/drop_my_tables.sh; sh ../tools/db/pdb_setup.sh; fi
+
+concclean:
+ rm -Rf concolic.files_*
+ rm strata.log.*
diff --git a/dyna_examples/block_copy.c b/dyna_examples/block_copy.c
new file mode 100644
index 0000000000000000000000000000000000000000..5bd8c97bed4e460e36b94f8036a6b92ed25230bf
--- /dev/null
+++ b/dyna_examples/block_copy.c
@@ -0,0 +1,46 @@
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+
+int block_copy(char* dst, char* src, int len)
+{
+
+ while(len-- > 0)
+ {
+ *dst++=*src++;
+ }
+
+}
+
+int k=0;
+int main (int argc, char **argv)
+{
+
+ int **i, **j;
+
+
+ i=malloc(4);
+ j=malloc(4);
+
+ *i=&k;
+
+ block_copy((char*)j,(char*)i,4);
+
+
+ **j=1;
+
+ printf("k=%d\n", k);
+
+
+
+
+ exit(0);
+}
+
diff --git a/dyna_examples/cmd_args_005.c b/dyna_examples/cmd_args_005.c
new file mode 100755
index 0000000000000000000000000000000000000000..934fd9979033eadc263eb22d8c770dbc03e179e4
--- /dev/null
+++ b/dyna_examples/cmd_args_005.c
@@ -0,0 +1,170 @@
+#ifdef _MSC_VER
+ #include "gtr/src/lang/gtr_config.h"
+#endif
+#include <stdio.h>
+
+
+#pragma runtime_checks("s", off)
+
+
+int my_ischar(char c)
+{
+ if (c < '0') return 0;
+ if (c > '9') return 0;
+ return 1;
+}
+
+int my_atoi(char * str)
+{
+ int result = 0;
+
+ int i = 0;
+ while (str[i] != 0) {
+
+ if (!my_ischar(str[i])) break;
+
+ int digit = (int) (str[i] - '0');
+
+ result = result * 10 + digit;
+
+ i++;
+ }
+
+ return result;
+}
+
+int my_str_cmp(char * s1, char * s2)
+{
+ int i;
+ for (i = 0; (s1[i] != 0) && (s2[i] != 0); i++) {
+ if (s1[i] != s2[i]) {
+ return 0;
+ }
+ }
+
+ if ((s1[i] != 0) || (s2[i] != 0))
+ return 0;
+
+ return 1;
+}
+
+
+// date January 10, 1973
+
+
+struct Date {
+ int day;
+ int month;
+ int year;
+};
+
+
+int lookup_month(char * month)
+{
+ if (my_str_cmp(month, "January")) return 1;
+ if (my_str_cmp(month, "February")) return 2;
+ if (my_str_cmp(month, "March")) return 3;
+ if (my_str_cmp(month, "April")) return 4;
+ if (my_str_cmp(month, "May")) return 5;
+ if (my_str_cmp(month, "June")) return 6;
+ if (my_str_cmp(month, "July")) return 7;
+ if (my_str_cmp(month, "August")) return 8;
+ if (my_str_cmp(month, "September")) return 9;
+ if (my_str_cmp(month, "October")) return 10;
+ if (my_str_cmp(month, "November")) return 11;
+ if (my_str_cmp(month, "December")) return 12;
+ return 0;
+}
+
+
+int parse_date(char * str, struct Date * d)
+{
+ int curr_index = 0;
+
+ // extract month
+ int i = 0;
+ char month[11];
+ for(i = 0; (str[curr_index] != ' '); i++, curr_index++) {
+ if (str[curr_index] == '\0')
+ return 0;
+ if (i >= 10)
+ return 0;
+ month[i] = str[curr_index];
+ }
+
+ // terminate month
+ month[i] = '\0';
+
+ // lookup month
+ int m = lookup_month(month);
+ if (m == 0) return 0;
+ d->month = m;
+
+ // skip ' '
+ curr_index++;
+
+ char date[3];
+ int j = 0;
+ while (str[curr_index] != ',') {
+ if (!my_ischar(str[curr_index])) return 0;
+ if(j >= 2) return 0;
+ date[j] = str[curr_index];
+ curr_index++;
+ j++;
+ }
+
+ // terminate date
+ date[j] = '\0';
+
+ // get date [check?]
+ int day = my_atoi(date);
+ d->day = day;
+
+ // skip ',' and ' '
+ curr_index++;
+ if (str[curr_index++] != ' ') return 0;
+
+ // get year
+ char year[5];
+ int k = 0;
+ while (str[curr_index] != '\0') {
+ if (!my_ischar(str[curr_index])) return 0;
+ if(k >= 4) return 0;
+ year[k] = str[curr_index];
+ curr_index++;
+ k++;
+ }
+
+ // terminate date
+ year[k] = '\0';
+
+ // get year
+ int y = my_atoi(year);
+ d->year = y;
+
+ return 1;
+}
+
+int main(int argc, char * argv[])
+{
+ if (argc != 2) return 0;
+
+ struct Date d;
+ int r;
+ if (parse_date(argv[1], &d)) {
+
+ // if date is February 13, 2009 do something
+ if ((d.day == 13) && (d.month == 2) && (d.year == 2009)) {
+// printf ("Opa");
+ r = 2;
+ }
+ else {
+ r = 1;
+ }
+ }
+ else {
+ r = 0;
+ }
+
+ return r;
+}
diff --git a/dyna_examples/concolic_test_handshake.c b/dyna_examples/concolic_test_handshake.c
new file mode 100644
index 0000000000000000000000000000000000000000..c8d76478b1db2230ca237cb7af161c9c9878ce37
--- /dev/null
+++ b/dyna_examples/concolic_test_handshake.c
@@ -0,0 +1,59 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <sys/types.h>
+#include <sys/ipc.h>
+#include <sys/msg.h>
+
+
+
+main(int argc, char* argv[])
+{
+ printf("Testing started\n");
+ if(!fork())
+ {
+ printf("fork started\n");
+ system(argv[1]);
+ printf("system finished\n");
+ sleep(2);
+ return 0;
+ }
+ else
+ {
+
+ printf("fork started in controller\n");
+ int msgflg = IPC_CREAT | 0666;
+ key_t key;
+ size_t buflen;
+ int msqid;
+ int len;
+
+ struct msgbuf
+ {
+ long mtype;
+ int args[3];
+ } sbuf;
+
+
+
+ key = 1234;
+
+ printf("setting up msgq\n");
+ if ((msqid = msgget(key, msgflg )) < 0) /* Get the message queue ID for the given key */
+ perror("msgget");
+
+
+ printf("getting from msgq\n");
+ len=sizeof(sbuf)-sizeof(int);
+ if (msgrcv(msqid, &sbuf, len, 0, 0) < 0)
+ {
+ perror("msgrcv:");
+ }
+
+ printf("Got message from Strata: type=%d, arg1=%x, arg2=%x, arg3=%x\n", (int)sbuf.mtype, sbuf.args[0], sbuf.args[1], sbuf.args[2]);
+
+ sleep(2);
+ return 0;
+
+ }
+}
+
diff --git a/dyna_examples/data.txt b/dyna_examples/data.txt
new file mode 100644
index 0000000000000000000000000000000000000000..d00bf42f05b7188e65ea616e5e994e3f7977215c
--- /dev/null
+++ b/dyna_examples/data.txt
@@ -0,0 +1 @@
+Jason
diff --git a/dyna_examples/dumbledore_cmd.c b/dyna_examples/dumbledore_cmd.c
new file mode 100644
index 0000000000000000000000000000000000000000..7aff3c7e9b440b4a18f43699b5f5fc713d24c4a1
--- /dev/null
+++ b/dyna_examples/dumbledore_cmd.c
@@ -0,0 +1,44 @@
+#include <stdio.h>
+#include <sys/mman.h>
+#include <string.h>
+#include <stdlib.h>
+
+enum {BUFSIZE = 24};
+
+char grade = 'D';
+char Name[BUFSIZE];
+
+void readString(char *in, char *s) {
+ char buf[BUFSIZE];
+ int i = 0;
+ int c;
+
+ for (;;)
+ {
+ c = in[i];
+ if ((c == '\0') || (c == '\n'))
+ break;
+
+ buf[i] = c;
+ i++;
+ }
+ buf[i] = '\0';
+
+ for (i = 0; i < BUFSIZE; i++)
+ s[i] = buf[i];
+}
+
+
+int main(int argc, char * argv[])
+{
+ if (argc == 2)
+ readString(argv[1], Name);
+
+ if (strcmp(Name, "Wizard in Training") == 0)
+ grade = 'B';
+
+ printf("Thank you, %s.\n", Name);
+ printf("I recommend that you get a grade of %c on this assignment.\n", grade);
+
+ return 0;
+}
diff --git a/dyna_examples/dumbledore_file.c b/dyna_examples/dumbledore_file.c
new file mode 100644
index 0000000000000000000000000000000000000000..f7c5e203b6e1139822e01be0697c4612fa08da48
--- /dev/null
+++ b/dyna_examples/dumbledore_file.c
@@ -0,0 +1,46 @@
+#include <stdio.h>
+#include <sys/mman.h>
+#include <string.h>
+#include <stdlib.h>
+
+enum {BUFSIZE = 98};
+
+char grade = 'D';
+char Name[BUFSIZE];
+FILE *f;
+
+void readString(char *s) {
+ char buf[BUFSIZE];
+ int i = 0;
+ int c;
+
+ for (;;)
+ {
+ c = fgetc(f);
+ if ((c == EOF) || (c == '\n'))
+ break;
+ buf[i] = c;
+ i++;
+ }
+ buf[i] = '\0';
+
+ for (i = 0; i < BUFSIZE; i++)
+ s[i] = buf[i];
+}
+
+
+int main(void)
+{
+ f = fopen("data.txt", "r");
+
+ readString(Name);
+
+ if (strcmp(Name, "Wizard in Training") == 0)
+ grade = 'B';
+
+ printf("Thank you, %s.\n", Name);
+ printf("I recommend that you get a grade of %c on this assignment.\n", grade);
+
+ exit(0);
+}
+
diff --git a/dyna_examples/dumbledore_file_with_fopen_check.c b/dyna_examples/dumbledore_file_with_fopen_check.c
new file mode 100644
index 0000000000000000000000000000000000000000..06d056a7459c0bdf3ec4ff2286d3683da70cd372
--- /dev/null
+++ b/dyna_examples/dumbledore_file_with_fopen_check.c
@@ -0,0 +1,46 @@
+#include <stdio.h>
+#include <sys/mman.h>
+#include <string.h>
+#include <stdlib.h>
+
+enum {BUFSIZE = 98};
+
+char grade = 'D';
+char Name[BUFSIZE];
+FILE *f;
+
+void readString(char *s) {
+ char buf[BUFSIZE];
+ int i = 0;
+ int c;
+
+ for (;;)
+ {
+ c = fgetc(f);
+ if ((c == EOF) || (c == '\n'))
+ break;
+ buf[i] = c;
+ i++;
+ }
+ buf[i] = '\0';
+
+ for (i = 0; i < BUFSIZE; i++)
+ s[i] = buf[i];
+}
+
+
+int main(void)
+{
+ f = fopen("data.txt", "r");
+
+ readString(Name);
+
+ if (strcmp(Name, "Wizard in Training") == 0)
+ grade = 'B';
+
+ printf("Thank you, %s.\n", Name);
+ printf("I recommend that you get a grade of %c on this assignment.\n", grade);
+
+// exit(0);
+}
+
diff --git a/dyna_examples/dumbledore_stdin.c b/dyna_examples/dumbledore_stdin.c
new file mode 100644
index 0000000000000000000000000000000000000000..44c93c0b31f99c4784e1cfbb7260122463b04088
--- /dev/null
+++ b/dyna_examples/dumbledore_stdin.c
@@ -0,0 +1,50 @@
+
+#include <stdio.h>
+#include <sys/mman.h>
+#include <string.h>
+#include <stdlib.h>
+
+enum {BUFSIZE = 98};
+
+char grade = 'D';
+char Name[BUFSIZE];
+FILE *f;
+
+void readString(char *s) {
+ char buf[BUFSIZE];
+ int i = 0;
+ int c;
+
+ for (;;)
+ {
+ c = getchar();
+ if ((c == EOF) || (c == '\n'))
+ break;
+ buf[i] = c;
+ i++;
+ }
+ buf[i] = '\0';
+
+ for (i = 0; i < BUFSIZE; i++)
+ s[i] = buf[i];
+}
+
+
+int main(void)
+{
+#if 0
+/* needed for some exploit, but not really part of the program! */
+ mprotect((void*)((unsigned int)Name & 0xfffff000), 1,
+ PROT_READ | PROT_WRITE | PROT_EXEC);
+#endif
+ readString(Name);
+
+ if (strcmp(Name, "Wizard in Training") == 0)
+ grade = 'B';
+
+ printf("Thank you, %s.\n", Name);
+ printf("I recommend that you get a grade of %c on this assignment.\n", grade);
+
+ exit(0);
+}
+
diff --git a/dyna_examples/fptest.c b/dyna_examples/fptest.c
new file mode 100644
index 0000000000000000000000000000000000000000..6f9df4854172a89abc112faf2c36753f15ee200d
--- /dev/null
+++ b/dyna_examples/fptest.c
@@ -0,0 +1,15 @@
+#ident "$Id: fptest.c,v 1.1 2008-01-11 17:05:47 jdh8d Exp $"
+
+#include <stdio.h>
+
+int main (int argc, char *argv[]) {
+ int i, *p;
+ double d=3.1415;
+
+
+ fprintf(stdout, "When Strata controls me I say: %g\n",d);
+
+
+ fflush(stdout);
+ fprintf(stdout, "When I control me I still say: %g\n",d);
+}
diff --git a/dyna_examples/globalfield.c b/dyna_examples/globalfield.c
new file mode 100644
index 0000000000000000000000000000000000000000..e02376e384915d77970fe16074582c2d299eb391
--- /dev/null
+++ b/dyna_examples/globalfield.c
@@ -0,0 +1,54 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+#define TRUE 1
+#define FALSE 0
+
+
+struct ASI {
+ int valid;
+ float (*pt2func)(float, float);
+ int buf[128];
+ int *uid_ptr;
+};
+
+float FloatingAdd(float a, float b) {
+ return (a + b);
+}
+
+float FloatingSub(float a, float b) {
+ return (a - b);
+}
+
+struct ASI GlobalStruct1;
+
+int main() {
+ int x, index;
+ float y, z, result;
+
+ GlobalStruct1.valid = FALSE;
+ GlobalStruct1.uid_ptr = 0;
+ y = 2.0;
+ z = 13.0;
+
+ printf("Enter a positive integer. Greater than 128 overflows.\n");
+ scanf("%d", &x);
+
+ GlobalStruct1.uid_ptr = &x;
+ if (x < 0) {
+ GlobalStruct1.pt2func = &FloatingAdd;
+ }
+ else {
+ GlobalStruct1.pt2func = &FloatingSub;
+ }
+
+ result = GlobalStruct1.pt2func(y, z);
+
+ for (index = 0; index < x; ++index) {
+ GlobalStruct1.buf[index] = index; // buffer overflow vulnerability
+ }
+
+ GlobalStruct1.valid = TRUE;
+ printf("x = %d y = %f z = %f result = %f uid_ptr=%xl\n", x, y, z, result, GlobalStruct1.uid_ptr);
+ return 0;
+}
diff --git a/dyna_examples/hanoi.c b/dyna_examples/hanoi.c
new file mode 100644
index 0000000000000000000000000000000000000000..380fc838b29363b081996c9757fc6f21e3fa960b
--- /dev/null
+++ b/dyna_examples/hanoi.c
@@ -0,0 +1,67 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+#include <assert.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+void dohanoi(int N, int from, int to, int using)
+{
+ static int count=0;
+
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(N, FROM, TO, USING);
+
+ printf("Hanoi %d\n", i);
+ fflush(stdout);
+ }
+
+ exit(0);
+}
+
diff --git a/dyna_examples/hanoi_heap_overrun.c b/dyna_examples/hanoi_heap_overrun.c
new file mode 100644
index 0000000000000000000000000000000000000000..90d8bbe227790956cbd2b0d59471ba8939bd18a2
--- /dev/null
+++ b/dyna_examples/hanoi_heap_overrun.c
@@ -0,0 +1,76 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+int *arr=NULL;
+
+void dohanoi(int N, int from, int to, int using, int arr_count)
+{
+ static int count=0;
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+
+ arr[arr_count]++;
+
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to, arr_count);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from, arr_count);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ arr=malloc(15*4);
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(i, FROM, TO, USING, i);
+
+ printf("Hanoi %d, arr[i]=%d\n", i, arr[i]);
+ fflush(stdout);
+ }
+
+ free(arr); arr=0;
+
+
+ exit(0);
+}
+
diff --git a/dyna_examples/hanoi_nostrata.c b/dyna_examples/hanoi_nostrata.c
new file mode 100644
index 0000000000000000000000000000000000000000..380fc838b29363b081996c9757fc6f21e3fa960b
--- /dev/null
+++ b/dyna_examples/hanoi_nostrata.c
@@ -0,0 +1,67 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+#include <assert.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+void dohanoi(int N, int from, int to, int using)
+{
+ static int count=0;
+
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(N, FROM, TO, USING);
+
+ printf("Hanoi %d\n", i);
+ fflush(stdout);
+ }
+
+ exit(0);
+}
+
diff --git a/dyna_examples/hanoi_overrun.c b/dyna_examples/hanoi_overrun.c
new file mode 100644
index 0000000000000000000000000000000000000000..c9e347c04866dc1c3120e50205b3d0cef5cfd095
--- /dev/null
+++ b/dyna_examples/hanoi_overrun.c
@@ -0,0 +1,75 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+int arr[15]={0,0,0,0,0,0,0,0,0,0,0,0,0,0,0};
+int user_group_id_number=0;
+
+void dohanoi(int N, int from, int to, int using, int arr_count)
+{
+ static int count=0;
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+
+ arr[arr_count]++;
+
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to, arr_count);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from, arr_count);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(i, FROM, TO, USING, i);
+
+ printf("Hanoi %d, arr[i]=%d\n", i, arr[i]);
+ fflush(stdout);
+ }
+
+ printf("The users' group id is %d, should be 0\n", user_group_id_number);
+
+
+ return 0;
+}
+
diff --git a/dyna_examples/hanoi_overrun_tainted.c b/dyna_examples/hanoi_overrun_tainted.c
new file mode 100644
index 0000000000000000000000000000000000000000..a34f6926573442893310d5a0d55fbb08d897fcb6
--- /dev/null
+++ b/dyna_examples/hanoi_overrun_tainted.c
@@ -0,0 +1,80 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+int arr[15]={0,0,0,0,0,0,0,0,0,0,0,0,0,0,0};
+int user_group_id_number=0;
+
+void dohanoi(int N, int from, int to, int using, int arr_count)
+{
+ static int count=0;
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+
+ arr[arr_count]++;
+
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to, arr_count);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from, arr_count);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+ int arr_count; /* tainted */
+
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+ printf("Enter offset to array: ");
+ scanf("%d", &arr_count);
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(i, FROM, TO, USING, arr_count);
+
+ printf("Hanoi %d, arr[i]=%d\n", i, arr[i]);
+ fflush(stdout);
+ }
+
+ printf("The users' group id is %d, should be 0\n", user_group_id_number);
+
+
+
+ exit(0);
+}
+
diff --git a/dyna_examples/hanoi_overrun_taintedenv.c b/dyna_examples/hanoi_overrun_taintedenv.c
new file mode 100644
index 0000000000000000000000000000000000000000..1297464ec2c7f480ebbef8fe1d80023567e7ffce
--- /dev/null
+++ b/dyna_examples/hanoi_overrun_taintedenv.c
@@ -0,0 +1,79 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+int arr[15]={0,0,0,0,0,0,0,0,0,0,0,0,0,0,0};
+int user_group_id_number=0;
+
+void dohanoi(int N, int from, int to, int using, int arr_count)
+{
+ static int count=0;
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+
+ arr[arr_count]++;
+
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to, arr_count);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from, arr_count);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+ int arr_count; /* tainted */
+
+
+ if (argc != 3)
+ {
+ fprintf(stderr, "usage: %s N M\n", argv[0]); exit(1);
+ }
+
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+ arr_count = strtol(argv[2], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(i, FROM, TO, USING, arr_count);
+
+ printf("Hanoi %d, arr[i]=%d\n", i, arr[i]);
+ fflush(stdout);
+ }
+
+ printf("The users' group id is %d, should be 0\n", user_group_id_number);
+
+
+
+ exit(0);
+}
+
diff --git a/dyna_examples/hanoi_stack_overrun.c b/dyna_examples/hanoi_stack_overrun.c
new file mode 100644
index 0000000000000000000000000000000000000000..90d8bbe227790956cbd2b0d59471ba8939bd18a2
--- /dev/null
+++ b/dyna_examples/hanoi_stack_overrun.c
@@ -0,0 +1,76 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+int *arr=NULL;
+
+void dohanoi(int N, int from, int to, int using, int arr_count)
+{
+ static int count=0;
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+
+ arr[arr_count]++;
+
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to, arr_count);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from, arr_count);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ arr=malloc(15*4);
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(i, FROM, TO, USING, i);
+
+ printf("Hanoi %d, arr[i]=%d\n", i, arr[i]);
+ fflush(stdout);
+ }
+
+ free(arr); arr=0;
+
+
+ exit(0);
+}
+
diff --git a/dyna_examples/hello.c b/dyna_examples/hello.c
new file mode 100644
index 0000000000000000000000000000000000000000..3780ac55a9bb1270deaeb1f178915d0fade721ba
--- /dev/null
+++ b/dyna_examples/hello.c
@@ -0,0 +1,6 @@
+#include <stdio.h>
+
+main()
+{
+ fprintf(stderr, "Hello %d\n", 2);
+}
diff --git a/dyna_examples/malloc.c b/dyna_examples/malloc.c
new file mode 100644
index 0000000000000000000000000000000000000000..6652a56dedaf1f72104cafa0a490fcb09bbab477
--- /dev/null
+++ b/dyna_examples/malloc.c
@@ -0,0 +1,78 @@
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+#include <assert.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+void dohanoi(int N, int from, int to, int using)
+{
+ static int count=0;
+ static int *malloc_ptr=NULL;
+
+
+ if(malloc_ptr)
+ {
+ free(malloc_ptr);
+ malloc_ptr=0;
+ }
+ else
+ {
+ malloc_ptr=malloc(((1+N)*(from+1)*(1+to)*(1+using)) << 4);
+ }
+
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(N, FROM, TO, USING);
+
+ printf("Hanoi %d\n", i);
+ fflush(stdout);
+ }
+
+ exit(0);
+}
+
diff --git a/dyna_examples/memcpy.c b/dyna_examples/memcpy.c
new file mode 100644
index 0000000000000000000000000000000000000000..8558716e86d892ab5a773a6ad94cbf1234bd804d
--- /dev/null
+++ b/dyna_examples/memcpy.c
@@ -0,0 +1,28 @@
+
+char b[100];
+
+
+extern void memcpy(int,int,int);
+
+main()
+{
+ char a[100];
+
+ foo(a,b);
+ printf("", a);
+}
+
+foo(char *c, char* d)
+{
+
+ int i;
+ int offset=c-d;
+ for(i=0;i<100;i++)
+ {
+ *(d+offset)=*(d);
+ d++;
+ }
+
+
+}
+
diff --git a/dyna_examples/myhanoi.c b/dyna_examples/myhanoi.c
new file mode 100644
index 0000000000000000000000000000000000000000..d55fc4af89ef41220057d03bc9e0bb8bebc3957c
--- /dev/null
+++ b/dyna_examples/myhanoi.c
@@ -0,0 +1,69 @@
+#include <assert.h>
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+#include <assert.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+void dohanoi(int N, int from, int to, int using)
+{
+ static int count=0;
+
+ assert(N<100); /* 100 would take a long time, and recurse really deeply, chnage this const if you want, but this'll avoid unintential segfaults */
+ if (N > 0)
+ {
+ dohanoi(N-1, from, using, to);
+
+/* this edit by JDH - I removed this print statement to make this program more compute bound
+ * also, this comment was added as a test of the branching mechanism we're proposing to use from now on
+ */
+// printf ("move %d --> %d, count=%d\n", from, to, count++);
+ dohanoi(N-1, using, to, from);
+ }
+ else
+ {
+ int j;
+ }
+}
+
+
+int main (int argc, char **argv)
+{
+ long int N;
+ long int i;
+ int j;
+
+ strtok(0);
+
+ if (argc != 2)
+ {
+ fprintf(stderr, "usage: %s N\n", argv[0]); exit(1);
+ }
+ N = strtol(argv[1], (char **)NULL, 10); /* a bit of error checking, LONG_XXX should be there in limits.h */
+
+ if (N == LONG_MIN || N == LONG_MAX || N <= 0)
+ {
+ fprintf(stderr, "illegal value for number of disks\n");
+ exit(2);
+ }
+
+ for(i=0;i<N;i++)
+ {
+
+
+ printf("Hanoi %d ... \n", i);
+ fflush(stdout);
+ dohanoi(N, FROM, TO, USING);
+
+ printf("Hanoi %d\n", i);
+ fflush(stdout);
+ }
+
+ exit(0);
+}
+
diff --git a/dyna_examples/print_ptr.c b/dyna_examples/print_ptr.c
new file mode 100644
index 0000000000000000000000000000000000000000..447b8c65f5a20ba5990fc2eb0b52f7df7f4b947d
--- /dev/null
+++ b/dyna_examples/print_ptr.c
@@ -0,0 +1,30 @@
+/* * The Towers Of Hanoi * C * Copyright (C) 1998 Amit Singh. All Rights Reserved. * * Tested with, ah well ... :) */
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+
+
+#define FROM 1
+#define TO 3
+#define USING 2
+
+
+int main (int argc, char **argv)
+{
+ int *p;
+ char * _itoa_word (unsigned long *value, char *buflim, unsigned int base, int upper_case);
+ char buf[100];
+
+
+
+
+ p=malloc(800);
+
+ printf("Hanoi %d, arr[i]=%d\n", p, p);
+
+
+ free(p);
+
+ exit(0);
+}
+
diff --git a/dyna_examples/recover_example.c b/dyna_examples/recover_example.c
new file mode 100644
index 0000000000000000000000000000000000000000..f2f24a957a13d09eb15e92f25edf49539ed628fc
--- /dev/null
+++ b/dyna_examples/recover_example.c
@@ -0,0 +1,29 @@
+#include <stdio.h>
+
+void fred(char* ptr)
+{
+ scanf("%s", ptr);
+}
+
+void bar(char* ptr)
+{
+ int i;
+ for(i=0;i<10;i++)
+ fred(ptr);
+}
+
+int foo()
+{
+ char ptr[10];
+ bar(ptr);
+ return 1;
+
+}
+
+int main()
+{
+ if(foo())
+ printf("Success");
+
+ return 0;
+}
diff --git a/examples/data.txt b/examples/data.txt
new file mode 100644
index 0000000000000000000000000000000000000000..d00bf42f05b7188e65ea616e5e994e3f7977215c
--- /dev/null
+++ b/examples/data.txt
@@ -0,0 +1 @@
+Jason
diff --git a/tools/do_concolic.sh b/tools/do_concolic.sh
index d0880e6626827be5b337afb474c8f16bb1d0118c..093db5ab8eaddd2531199d73b39292ca3df0d423 100755
--- a/tools/do_concolic.sh
+++ b/tools/do_concolic.sh
@@ -7,6 +7,9 @@ strata_exe=$exe.stratafied
annot=$exe.ncexe.annot
sym=$exe.sym
+
+
+
whoami=`whoami`
#
@@ -39,7 +42,12 @@ for i in `ipcs -q|grep $whoami |cut -d" " -f 2`;
do
ipcrm -q $i
done
+
+
+oldulimit=`ulimit -S -t`
+ulimit -S -t 61
STRATA_GRACE=1 controller $extra_args --start $start_ea --stop $stop_ea --symbols $sym --outputs replay,coverage,instruction_addresses $strata_exe
+ulimit -S -t $oldulimit
echo cleaning up
killall -q controller
diff --git a/tools/ps_analyze.sh b/tools/ps_analyze.sh
index 9f7d084a846b29d7658e47cb4df0ad3684dd5a09..470395418d979618f1ca81522be4c82cee15814c 100755
--- a/tools/ps_analyze.sh
+++ b/tools/ps_analyze.sh
@@ -90,7 +90,7 @@ echo Done.
#
echo Running concolic testing to generate inputs ...
#$PEASOUP_HOME/tools/do_concolic.sh a --iterations 25 --logging tracer,instance_times,trace
-$PEASOUP_HOME/tools/do_concolic.sh a --iterations 25 --logging tracer,trace,inputs > do_concolic.out 2>&1
+$PEASOUP_HOME/tools/do_concolic.sh a --timeout 60 --iteration-timeout 30 --iterations 25 --logging tracer,trace,inputs > do_concolic.out 2>&1
log do_concolic.out
echo Done.
diff --git a/tools/ps_run.sh b/tools/ps_run.sh
index 0ce55fa89ebef06ef3f62de8a7f40e86bc3e8ced..0bcc1d360c3d71a50e8b3586190456a24a75dbff 100755
--- a/tools/ps_run.sh
+++ b/tools/ps_run.sh
@@ -23,6 +23,11 @@ fi
# Run the program with the proper env. vars set., and the arguments to the program specified
#
+if [ ! -z $VERBOSE ]; then
+ echo STRATA_SPRI_FILE=$STRATA_SPRI_FILE STRATA_DOUBLE_FREE=1 STRATA_HEAPRAND=1 STRATA_PC_CONFINE=1 STRATA_PC_CONFINE_XOR=1 STRATA_PC_CONFINE_XOR_KEY_LENGTH=1024 STRATA_ANNOT_FILE=$datapath/a.ncexe.annot $datapath/a.stratafied "$@"
+fi
+
+
STRATA_DOUBLE_FREE=1 \
STRATA_HEAPRAND=1 \
STRATA_PC_CONFINE=1 \
@@ -32,3 +37,5 @@ STRATA_DOUBLE_FREE=1 \
$datapath/a.stratafied "$@"
+
+