Merge pull request #2366 from marek-trtik/full_slicer/adapted_benchmarks_from_security_scanner

SEC-477: Added three regression tests for the full-slicer.

Author: tautschnig

regression/goto-instrument/slice_general007/main.c

@@ -0,0 +1,79 @@
+// This is a benchmark for the full-slicer
+// This is a simplified version of end-to-end regression tests
+// 'general005', 'general006', and 'general007' of the security-scanner.
+
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+struct object
+{
+  bool Tainted_stream;
+};
+
+struct java_array
+{
+  struct object super;
+  char *data;
+  int length;
+};
+
+struct java_array_wrapper
+{
+  struct java_array super;
+  bool Tainted_byte_array;
+};
+
+struct InputStream
+{
+  struct object super;
+  struct java_array_wrapper *s;
+};
+
+struct ServletInputStream
+{
+  struct InputStream super;
+};
+
+struct HttpServletRequest
+{
+  struct ServletInputStream *s;
+};
+
+void getBytes(struct java_array_wrapper *data, struct InputStream *in)
+{
+  // These 2 lines are wrongly sliced away!
+  if(in->super.Tainted_stream)
+    data->Tainted_byte_array = true;
+}
+
+struct InputStream *getInputStream(struct HttpServletRequest *this)
+{
+  return &this->s->super;
+}
+
+struct InputStream *getInStream(struct HttpServletRequest *request)
+{
+  struct InputStream *x = getInputStream(request);
+  x->super.Tainted_stream = true;
+  return x;
+}
+
+extern void *CProver_nondetWithNull();
+
+int main()
+{
+  struct HttpServletRequest *request = CProver_nondetWithNull();
+  struct InputStream *in0 = getInStream(request);
+  struct InputStream *in = in0;
+  struct java_array_wrapper *data,
+    *tmp1 =
+      (struct java_array_wrapper *)malloc(sizeof(struct java_array_wrapper));
+  tmp1->Tainted_byte_array = false;
+  tmp1->super.super.Tainted_stream = false;
+  data = tmp1;
+  getBytes(data, in);
+  if(data->Tainted_byte_array)
+    assert(false);
+  return 0;
+}

regression/goto-instrument/slice_general007/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--full-slice --add-library
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is a simplified version of end-to-end regression tests 'general005', 'general006', and 'general007' of the security-scanner.

regression/goto-instrument/slice_taint_crossing_substr_and_concatenation/main.c

@@ -0,0 +1,62 @@
+// This is a benchmark for the full-slicer
+// It is a simplified version of end-to-end regression test
+// 'taint_crossing_substr_and_concatenation' of the security-scanner.
+
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+extern int CProver_nondetInt();
+
+struct object
+{
+  bool X;
+  bool SBX;
+};
+
+struct String
+{
+  struct object super;
+};
+
+struct StringBuilder
+{
+  struct object super;
+};
+
+struct String *source()
+{
+  return (struct String *)malloc(sizeof(struct String));
+}
+
+struct StringBuilder *append(struct StringBuilder *sb, struct String *s)
+{
+  return sb;
+}
+
+struct String *toString(struct StringBuilder *sb)
+{
+  return (struct String *)malloc(sizeof(struct String));
+}
+
+int main()
+{
+  struct StringBuilder *tmp1, *sb;
+  struct String *tmp2, *tainted;
+
+  sb = (struct StringBuilder *)malloc(sizeof(struct StringBuilder));
+  tainted = source();
+  tainted->super.X = true;
+  tmp1 = append(sb, tainted);
+
+  // Next 2 lines are wrongly sliced away!
+  if(tainted->super.X)
+    sb->super.SBX = true;
+
+  tmp2 = toString(tmp1);
+  if(tmp1->super.SBX)
+    tmp2->super.X = true;
+  if(tmp2->super.X)
+    assert(false);
+  return 0;
+}

regression/goto-instrument/slice_taint_crossing_substr_and_concatenation/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is a simplified version of end-to-end regression test 'taint_crossing_substr_and_concatenation' of the security-scanner.

regression/goto-instrument/slice_taint_over_list/main.c

@@ -0,0 +1,70 @@
+// This is a benchmark for the full-slicer
+// This is a simplified version of end-to-end regression test
+// 'taint_over_list' of the security-scanner.
+
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+extern void *CProver_nondetWithNull();
+
+struct object
+{
+  bool Tainted_data;
+};
+
+struct java_array
+{
+  struct object super;
+  void **data;
+  int length;
+};
+
+struct ArrayList
+{
+  struct java_array *data;
+  int last;
+};
+
+struct A
+{
+  struct object super;
+};
+
+void ArrayList_init(struct ArrayList *this)
+{
+  this->data = CProver_nondetWithNull();
+  this->last = 0;
+}
+
+void ArrayList_add(struct ArrayList *this, struct object *o)
+{
+  // Next 2 lines are wrongly sliced away!
+  this->data->data[this->last] = o;
+  this->last += 1;
+}
+
+struct object *ArrayList_get(struct ArrayList *this, int idx)
+{
+  return this->data->data[idx];
+}
+
+int main()
+{
+  struct ArrayList *L;
+  struct A *tmp1;
+  struct object *tmp2, *tmp3;
+  L = CProver_nondetWithNull();
+  ArrayList_init(L);
+  tmp1 = (struct A *)malloc(sizeof(struct A));
+  ArrayList_add(L, (struct object *)&tmp1->super);
+  tmp2 = ArrayList_get(L, 0);
+
+  // The next line is wrongly sliced away!
+  ((struct A *)tmp2)->super.Tainted_data = true;
+
+  tmp3 = ArrayList_get(L, 0);
+  if(((struct A *)tmp3)->super.Tainted_data)
+    assert(false);
+  return 0;
+}

regression/goto-instrument/slice_taint_over_list/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is a simplified version of end-to-end regression test 'taint_over_list' of the security-scanner.