Move all overflows from the vector instructions tests into a new file, as the overflow behaviour is different in LLVM 11.

5 files changed, 45 insertions, 45 deletions

diff --git a/test/VectorInstructions/extract_element.c b/test/VectorInstructions/extract_element.c
index e4e73915..6ef1bf18 100644
--- a/test/VectorInstructions/extract_element.c
+++ b/test/VectorInstructions/extract_element.c
@@ -29,7 +29,5 @@ int main() {
   assert(f[2] == 2);
   // CHECK-STDERR-NOT: extract_element.c:[[@LINE+1]]: ASSERTION FAIL
   assert(f[3] == 3);
-  // CHECK-STDERR: extract_element.c:[[@LINE+1]]: Out of bounds read when extracting element
-  printf("f[4]=%u\n", f[4]); // Out of bounds
   return 0;
 }
diff --git a/test/VectorInstructions/extract_element_symbolic.c b/test/VectorInstructions/extract_element_symbolic.c
deleted file mode 100644
index ff9a7164..00000000
--- a/test/VectorInstructions/extract_element_symbolic.c
+++ /dev/null
@@ -1,20 +0,0 @@
-// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: not %klee --output-dir=%t.klee-out --exit-on-error %t1.bc > %t.log 2>&1
-// RUN: FileCheck -input-file=%t.log %s
-#include "klee/klee.h"
-#include <assert.h>
-#include <stdio.h>
-#include <stdint.h>
-
-typedef uint32_t v4ui __attribute__ ((vector_size (16)));
-int main() {
-  v4ui f = { 0, 1, 2, 3 };
-  unsigned index = 0;
-  klee_make_symbolic(&index, sizeof(unsigned), "index");
-  // Performing read should be ExtractElement instruction.
-  // For now this is an expected limitation.
-  // CHECK: extract_element_symbolic.c:[[@LINE+1]]: ExtractElement, support for symbolic index not implemented
-  uint32_t readValue = f[index];
-  return readValue % 255;
-}
diff --git a/test/VectorInstructions/insert_element.c b/test/VectorInstructions/insert_element.c
index edfc9cb4..df09819d 100644
--- a/test/VectorInstructions/insert_element.c
+++ b/test/VectorInstructions/insert_element.c
@@ -22,6 +22,7 @@ int main() {
   klee_print_expr("f after write to [2]", f);
   f[3] = 19;
   klee_print_expr("f after write to [3]", f);
+
   // CHECK-STDOUT: f[0]=255
   printf("f[0]=%u\n", f[0]);
   // CHECK-STDOUT: f[1]=128
@@ -39,7 +40,5 @@ int main() {
   // CHECK-STDERR-NOT: insert_element.c:[[@LINE+1]]: ASSERTION FAIL
   assert(f[3] == 19);
 
-  // CHECK-STDERR: insert_element.c:[[@LINE+1]]: Out of bounds write when inserting element
-  f[4] = 255; // Out of bounds write
   return 0;
 }
diff --git a/test/VectorInstructions/insert_element_symbolic.c b/test/VectorInstructions/insert_element_symbolic.c
deleted file mode 100644
index 6a0fbe03..00000000
--- a/test/VectorInstructions/insert_element_symbolic.c
+++ /dev/null
@@ -1,21 +0,0 @@
-// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: not %klee --output-dir=%t.klee-out --exit-on-error %t1.bc > %t.log 2>&1
-// RUN: FileCheck -input-file=%t.log %s
-#include "klee/klee.h"
-#include <assert.h>
-#include <stdio.h>
-#include <stdint.h>
-
-typedef uint32_t v4ui __attribute__ ((vector_size (16)));
-int main() {
-  v4ui f = { 0, 1, 2, 3 };
-  unsigned index = 0;
-  klee_make_symbolic(&index, sizeof(unsigned), "index");
-  // Performing write should be InsertElement instructions.
-  // For now this is an expected limitation.
-  // CHECK: insert_element_symbolic.c:[[@LINE+1]]: InsertElement, support for symbolic index not implemented
-  f[index] = 255;
-  klee_print_expr("f after write to [0]", f);
-  return 0;
-}
diff --git a/test/VectorInstructions/oob-llvm-lt11.c b/test/VectorInstructions/oob-llvm-lt11.c
new file mode 100644
index 00000000..9d80ef7d
--- /dev/null
+++ b/test/VectorInstructions/oob-llvm-lt11.c
@@ -0,0 +1,44 @@
+// REQUIRES: lt-llvm-11.0
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// NOTE: Have to pass `--optimize=false` to avoid vector operations being
+// constant folded away.
+// RUN: %klee --output-dir=%t.klee-out --optimize=false  %t1.bc > %t.stdout.log 2> %t.stderr.log
+// RUN: FileCheck -input-file=%t.stderr.log %s
+
+#include "klee/klee.h"
+
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+typedef uint32_t v4ui __attribute__((vector_size(16)));
+int main() {
+  v4ui f = {1, 2, 3, 4};
+  int k = klee_range(0, 10, "k");
+
+  if (k == 0) {
+    // CHECK-DAG: [[@LINE+1]]: Out of bounds write when inserting element
+    f[4] = 255; // Out of bounds write
+  }
+
+  if (k == 1) {
+    // CHECK-DAG: [[@LINE+1]]: Out of bounds read when extracting element
+    printf("f[4] = %u\n", f[5]); // Out of bounds
+  }
+
+  if (k > 6) {
+    // Performing read should be ExtractElement instruction.
+    // For now this is an expected limitation.
+    // CHECK-DAG: [[@LINE+1]]: ExtractElement, support for symbolic index not implemented
+    uint32_t readValue = f[k];
+  }
+  else {
+    // Performing write should be InsertElement instructions.
+    // For now this is an expected limitation.
+    // CHECK-DAG: [[@LINE+1]]: InsertElement, support for symbolic index not implemented
+    f[k] = 255;
+  }
+
+  return 0;
+}