Symex taint analysis

regression/symex-taint-analysis/Makefile

@@ -0,0 +1,14 @@
+default: tests.log
+
+test:
+	@../test.pl -c ../../../src/symex/symex
+
+tests.log: ../test.pl
+	@../test.pl -c ../../../src/symex/symex
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/symex-taint-analysis/array-all-taint-inline/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[0];
+
+	int c = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/array-all-taint-inline/taint.json

@@ -0,0 +1,6 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted"
+}
+]

regression/symex-taint-analysis/array-all-taint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/array-all-taint-json/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[0];
+
+	int c = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/array-all-taint-json/taint.json

@@ -0,0 +1,6 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted"
+}
+]

regression/symex-taint-analysis/array-all-taint-json/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/array-taint-inline/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	__CPROVER_set_taint("main::1::x[3]", "tainted");
+
+	int y = x[3];
+
+	x[0] = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/array-taint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/array-taint-json/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[3];
+
+	x[0] = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/array-taint-json/taint.json

@@ -0,0 +1,7 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted",
+	"symbol": "main::1::x[3]"
+}
+]

regression/symex-taint-analysis/array-taint-json/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/array-untaint-inline/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	__CPROVER_set_taint("main::1::x[3]", "tainted");
+
+	int y = x[3];
+
+	x[1] = ++y;
+
+	// assert c is tainted.
+	assert(!__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/array-untaint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/func-taint-inline/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(){
+
+	int *x = malloc(sizeof(int));
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	*x = 9;
+
+	int *y = x;
+
+	assert(__CPROVER_is_taint("main::1::y", "tainted"));
+	free(y);
+
+    return 0;
+}

regression/symex-taint-analysis/func-taint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/loop-taint-inline/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+
+int main() {
+
+	int j;
+
+	__CPROVER_set_taint("main::1::j", "tainted");
+
+	int x[4];
+
+	int i = 0;
+
+	for (i = 0; i < 4; i++) {
+
+		if (i == 3)
+			x[i] = j;
+		else
+			x[i] = 0;
+	}
+
+	assert(__CPROVER_is_taint("main::1::x[0]", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x[1]", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x[2]", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x[3]", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/loop-taint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/loop-untaint-inline/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int main(){
+
+	int j;
+
+	__CPROVER_set_taint("main::1::j", "tainted");
+
+
+	int x[4];
+
+	int i = 0;
+
+	for (i = 0; i < 4; i++){
+
+		 x[i] = (i == 8) ? j : 0;
+	}
+
+
+	assert(__CPROVER_is_taint("main::1::x[3]", "tainted"));
+
+
+	return 0;
+}

regression/symex-taint-analysis/loop-untaint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/pointer-taint-inline/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int main(){
+
+	int y;
+
+	__CPROVER_set_taint("main::1::y", "tainted");
+
+	int *x = &y;
+
+	int *c = x;
+
+	int z = *x;
+
+	assert(__CPROVER_is_taint("main::1::y", "tainted"));
+	assert(__CPROVER_is_taint("main::1::z", "tainted"));
+	assert(__CPROVER_is_taint("main::1::x", "untainted"));
+	assert(__CPROVER_is_taint("main::1::c", "untainted"));
+
+
+	return 0;
+}

regression/symex-taint-analysis/pointer-taint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/pointer-untaint-inline/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int main(){
+
+	int y;
+
+	__CPROVER_set_taint("main::1::y", "tainted");
+
+	int *x = &y;
+
+	int *c = x;
+
+	*c = 0;
+	int z = *x;
+
+
+	assert(__CPROVER_is_taint("main::1::y", "untainted"));
+	assert(__CPROVER_is_taint("main::1::z", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x", "untainted"));
+	assert(__CPROVER_is_taint("main::1::c", "untainted"));
+
+
+	return 0;
+}

regression/symex-taint-analysis/pointer-untaint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/recursive-taint-inline/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int factorial(unsigned int i) {
+
+	if (i <= 1) {
+		return 1;
+	}
+	return i * factorial(i - 1);
+}
+
+int main() {
+
+	unsigned int x = 80;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	unsigned int y = factorial(x);
+
+	assert(__CPROVER_is_taint("main::1::y", "tainted"));
+
+	return 0;
+}

regression/symex-taint-analysis/recursive-taint-inline/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-taint-analysis/recursive-untaint-inline/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+int factorial(unsigned int i) {
+
+	if (i <= 1) {
+		return 1;
+	}
+	return i * factorial(i - 1);
+}
+
+int main() {
+
+	unsigned int y;
+
+	unsigned int x = 80;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	y = factorial(x);
+
+	y = 0;
+
+	assert(!__CPROVER_is_taint("main::1::y", "tainted"));
+
+	return 0;
+}