Merge pull request #1574 from diffblue/taint-memcpy-develop

transfer taint with memcpy

Author: Daniel Kroening

regression/goto-analyzer-taint-ansi-c/Makefile

@@ -0,0 +1,19 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c

@@ -0,0 +1,15 @@
+#include <string.h>
+
+void my_f(void *) { }
+void my_h(void *) { }
+
+void my_function()
+{
+  void *o1;
+  my_f(o1); // T1 source
+
+  void *o2;
+  memcpy(o2, o1, 100);
+
+  my_h(o2); // T1 sink
+}

regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o

@@ -0,0 +1,4 @@
+[
+{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "my_f" },
+{ "id": "my_h", "kind": "sink",   "where": "parameter1", "taint": "T1", "function": "my_h", "message": "There is a T1 flow" }
+]

regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json

@@ -0,0 +1,7 @@
+CORE
+main.o
+--taint taint.json
+^EXIT=0$
+^SIGNAL=0$
+^file main.c line 12( function .*)?: There is a T1 flow \(taint rule my_h\)$
+--

regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc

@@ -380,6 +380,19 @@ void custom_bitvector_domaint::transform(
             }
           }
         }
+        else if(identifier=="memcpy" ||
+                identifier=="memmove")
+        {
+          if(code_function_call.arguments().size()==3)
+          {
+            // we copy all tracked bits from op1 to op0
+            // we do not consider any bits attached to the size op2
+            dereference_exprt lhs_deref(code_function_call.arguments()[0]);
+            dereference_exprt rhs_deref(code_function_call.arguments()[1]);
+
+            assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns);
+          }
+        }
         else
         {
           goto_programt::const_targett next=from;