Merge pull request #657 from delcypher/vectorized_instructions

Implement basic support for vectorized instructions.

9 files changed, 820 insertions, 0 deletions

diff --git a/test/VectorInstructions/extract_element.c b/test/VectorInstructions/extract_element.c
new file mode 100644
index 00000000..008691e3
--- /dev/null
+++ b/test/VectorInstructions/extract_element.c
@@ -0,0 +1,36 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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 -check-prefix=CHECK-STDOUT -input-file=%t.stdout.log %s
+// RUN: FileCheck -check-prefix=CHECK-STDERR -input-file=%t.stderr.log %s
+#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 };
+  // Performing these reads should be ExtractElement instructions
+  // CHECK-STDOUT: f[0]=0
+  printf("f[0]=%u\n", f[0]);
+  // CHECK-STDOUT-NEXT: f[1]=1
+  printf("f[1]=%u\n", f[1]);
+  // CHECK-STDOUT-NEXT: f[2]=2
+  printf("f[2]=%u\n", f[2]);
+  // CHECK-STDOUT-NEXT: f[3]=3
+  printf("f[3]=%u\n", f[3]);
+  // CHECK-STDERR-NOT: extract_element.c:[[@LINE+1]]: ASSERTION FAIL
+  assert(f[0] == 0);
+  // CHECK-STDERR-NOT: extract_element.c:[[@LINE+1]]: ASSERTION FAIL
+  assert(f[1] == 1);
+  // CHECK-STDERR-NOT: extract_element.c:[[@LINE+1]]: ASSERTION FAIL
+  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
new file mode 100644
index 00000000..f75bad62
--- /dev/null
+++ b/test/VectorInstructions/extract_element_symbolic.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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/floating_point_ops_constant.c b/test/VectorInstructions/floating_point_ops_constant.c
new file mode 100644
index 00000000..4e567a30
--- /dev/null
+++ b/test/VectorInstructions/floating_point_ops_constant.c
@@ -0,0 +1,152 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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 --exit-on-error %t1.bc
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+typedef float v4float __attribute__((vector_size(16)));
+typedef double v4double __attribute__((vector_size(32)));
+
+#define ASSERT_EL(C, OP, A, B, INDEX) assert(C[INDEX] == (A[INDEX] OP B[INDEX]))
+#define ASSERT_ELV4(C, OP, A, B)                                               \
+  do {                                                                         \
+    ASSERT_EL(C, OP, A, B, 0);                                                 \
+    ASSERT_EL(C, OP, A, B, 1);                                                 \
+    ASSERT_EL(C, OP, A, B, 2);                                                 \
+    ASSERT_EL(C, OP, A, B, 3);                                                 \
+  } while (0);
+
+#define ASSERT_EL_TRUTH(C, OP, A, B, INDEX)                                    \
+  assert(C[INDEX] ? (A[INDEX] OP B[INDEX]) : (!(A[INDEX] OP B[INDEX])))
+#define ASSERT_EL_TRUTH_V4(C, OP, A, B)                                        \
+  do {                                                                         \
+    ASSERT_EL_TRUTH(C, OP, A, B, 0);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 1);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 2);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 3);                                           \
+  } while (0);
+
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, INDEX)          \
+  assert(C[INDEX] == (CONDITION ? A[INDEX] : B[INDEX]))
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(C, CONDITION, A, B)              \
+  do {                                                                         \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 0);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 1);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 2);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 3);                 \
+  } while (0);
+
+int main() {
+  // Float tests
+  {
+    v4float a = {1.0f, 2.5f, -3.5f, 4.0f};
+    v4float b = {-10.0f, 20.2f, -30.5f, 40.1f};
+
+    // Test addition
+    v4float c = a + b;
+    ASSERT_ELV4(c, +, a, b);
+
+    // Test subtraction
+    c = b - a;
+    ASSERT_ELV4(c, -, b, a);
+
+    // Test multiplication
+    c = a * b;
+    ASSERT_ELV4(c, *, a, b);
+
+    // Test division
+    c = a / b;
+    ASSERT_ELV4(c, /, a, b);
+
+    // NOTE: Can't use `ASSERT_ELV4` due to semantics
+    // of GCC vector extensions. See
+    // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
+
+    // Test ==
+    c = a == b;
+    ASSERT_EL_TRUTH_V4(c, ==, a, b);
+
+    // Test <
+    c = a < b;
+    ASSERT_EL_TRUTH_V4(c, <, a, b);
+
+    // Test <=
+    c = a <= b;
+    ASSERT_EL_TRUTH_V4(c, <=, a, b);
+
+    // Test >
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test >=
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test !=
+    c = a != b;
+    ASSERT_EL_TRUTH_V4(c, !=, a, b);
+
+    // Test ternary operator
+    c = 0 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 0, a, b);
+    c = 1 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 1, a, b);
+  }
+
+  // double tests
+  {
+    v4double a = {1.0, 2.5, -3.5, 4.0};
+    v4double b = {-10.0, 20.2, -30.5, 40.1};
+
+    // Test addition
+    v4double c = a + b;
+    ASSERT_ELV4(c, +, a, b);
+
+    // Test subtraction
+    c = b - a;
+    ASSERT_ELV4(c, -, b, a);
+
+    // Test multiplication
+    c = a * b;
+    ASSERT_ELV4(c, *, a, b);
+
+    // Test division
+    c = a / b;
+    ASSERT_ELV4(c, /, a, b);
+
+    // Test ==
+    c = a == b;
+    ASSERT_EL_TRUTH_V4(c, ==, a, b);
+
+    // Test <
+    c = a < b;
+    ASSERT_EL_TRUTH_V4(c, <, a, b);
+
+    // Test <=
+    c = a <= b;
+    ASSERT_EL_TRUTH_V4(c, <=, a, b);
+
+    // Test >
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test >=
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test !=
+    c = a != b;
+    ASSERT_EL_TRUTH_V4(c, !=, a, b);
+
+    // Test ternary operator
+    c = 0 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 0, a, b);
+    c = 1 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 1, a, b);
+  }
+  return 0;
+}
diff --git a/test/VectorInstructions/insert_element.c b/test/VectorInstructions/insert_element.c
new file mode 100644
index 00000000..8397dceb
--- /dev/null
+++ b/test/VectorInstructions/insert_element.c
@@ -0,0 +1,46 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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 -check-prefix=CHECK-STDOUT -input-file=%t.stdout.log %s
+// RUN: FileCheck -check-prefix=CHECK-STDERR -input-file=%t.stderr.log %s
+#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 };
+  klee_print_expr("f:=", f);
+  // Performing these writes should be InsertElement instructions
+  f[0] = 255;
+  klee_print_expr("f after write to [0]", f);
+  f[1] = 128;
+  klee_print_expr("f after write to [1]", f);
+  f[2] = 1;
+  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
+  printf("f[1]=%u\n", f[1]);
+  // CHECK-STDOUT: f[2]=1
+  printf("f[2]=%u\n", f[2]);
+  // CHECK-STDOUT: f[3]=19
+  printf("f[3]=%u\n", f[3]);
+  // CHECK-STDERR-NOT: insert_element.c:[[@LINE+1]]: ASSERTION FAIL
+  assert(f[0] == 255);
+  // CHECK-STDERR-NOT: insert_element.c:[[@LINE+1]]: ASSERTION FAIL
+  assert(f[1] == 128);
+  // CHECK-STDERR-NOT: insert_element.c:[[@LINE+1]]: ASSERTION FAIL
+  assert(f[2] == 1);
+  // 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
new file mode 100644
index 00000000..76df899c
--- /dev/null
+++ b/test/VectorInstructions/insert_element_symbolic.c
@@ -0,0 +1,22 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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/integer_ops_constant.c b/test/VectorInstructions/integer_ops_constant.c
new file mode 100644
index 00000000..189ad4ee
--- /dev/null
+++ b/test/VectorInstructions/integer_ops_constant.c
@@ -0,0 +1,201 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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 --exit-on-error %t1.bc
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+typedef uint32_t v4ui __attribute__((vector_size(16)));
+typedef int32_t v4si __attribute__((vector_size(16)));
+
+#define ASSERT_EL(C, OP, A, B, INDEX) assert(C[INDEX] == (A[INDEX] OP B[INDEX]))
+#define ASSERT_ELV4(C, OP, A, B)                                               \
+  do {                                                                         \
+    ASSERT_EL(C, OP, A, B, 0);                                                 \
+    ASSERT_EL(C, OP, A, B, 1);                                                 \
+    ASSERT_EL(C, OP, A, B, 2);                                                 \
+    ASSERT_EL(C, OP, A, B, 3);                                                 \
+  } while (0);
+
+#define ASSERT_EL_TRUTH(C, OP, A, B, INDEX)                                    \
+  assert(C[INDEX] ? (A[INDEX] OP B[INDEX]) : (!(A[INDEX] OP B[INDEX])))
+#define ASSERT_EL_TRUTH_V4(C, OP, A, B)                                        \
+  do {                                                                         \
+    ASSERT_EL_TRUTH(C, OP, A, B, 0);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 1);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 2);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 3);                                           \
+  } while (0);
+
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, INDEX)          \
+  assert(C[INDEX] == (CONDITION ? A[INDEX] : B[INDEX]))
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(C, CONDITION, A, B)              \
+  do {                                                                         \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 0);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 1);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 2);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 3);                 \
+  } while (0);
+
+int main() {
+  // Unsigned tests
+  {
+    v4ui a = {0, 1, 2, 3};
+    v4ui b = {10, 20, 30, 3};
+
+    // Test addition
+    v4ui c = a + b;
+    ASSERT_ELV4(c, +, a, b);
+
+    // Test subtraction
+    c = b - a;
+    ASSERT_ELV4(c, -, b, a);
+
+    // Test multiplication
+    c = a * b;
+    ASSERT_ELV4(c, *, a, b);
+
+    // Test division
+    c = a / b;
+    ASSERT_ELV4(c, /, a, b);
+
+    // Test mod
+    c = a % b;
+    ASSERT_ELV4(c, %, a, b);
+
+    // Test bitwise and
+    c = a & b;
+    ASSERT_ELV4(c, &, a, b);
+
+    // Test bitwise or
+    c = a | b;
+    ASSERT_ELV4(c, |, a, b);
+
+    // Test bitwise xor
+    c = a ^ b;
+    ASSERT_ELV4(c, ^, a, b);
+
+    // Test left shift
+    c = b << a;
+    ASSERT_ELV4(c, <<, b, a);
+
+    // Test logic right shift
+    c = b >> a;
+    ASSERT_ELV4(c, >>, b, a);
+
+    // NOTE: Can't use `ASSERT_ELV4` due to semantics
+    // of GCC vector extensions. See
+    // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
+
+    // Test ==
+    c = a == b;
+    ASSERT_EL_TRUTH_V4(c, ==, a, b);
+
+    // Test <
+    c = a < b;
+    ASSERT_EL_TRUTH_V4(c, <, a, b);
+
+    // Test <=
+    c = a <= b;
+    ASSERT_EL_TRUTH_V4(c, <=, a, b);
+
+    // Test >
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test >=
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test !=
+    c = a != b;
+    ASSERT_EL_TRUTH_V4(c, !=, a, b);
+
+    // Test ternary operator
+    c = 0 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 0, a, b);
+    c = 1 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 1, a, b);
+  }
+
+  // Signed tests
+  {
+    v4si a = {-1, 2, -3, 4};
+    v4si b = {-10, 20, -30, 40};
+
+    // Test addition
+    v4si c = a + b;
+    ASSERT_ELV4(c, +, a, b);
+
+    // Test subtraction
+    c = b - a;
+    ASSERT_ELV4(c, -, b, a);
+
+    // Test multiplication
+    c = a * b;
+    ASSERT_ELV4(c, *, a, b);
+
+    // Test division
+    c = a / b;
+    ASSERT_ELV4(c, /, a, b);
+
+    // Test mod
+    c = a % b;
+    ASSERT_ELV4(c, %, a, b);
+
+    // Test bitwise and
+    c = a & b;
+    ASSERT_ELV4(c, &, a, b);
+
+    // Test bitwise or
+    c = a | b;
+    ASSERT_ELV4(c, |, a, b);
+
+    // Test bitwise xor
+    c = a ^ b;
+    ASSERT_ELV4(c, ^, a, b);
+
+    // Test left shift
+    v4si shifts = {1, 2, 3, 4};
+    c = b << shifts;
+    ASSERT_ELV4(c, <<, b, shifts);
+
+    // Test arithmetic right shift
+    c = b >> shifts;
+    ASSERT_ELV4(c, >>, b, shifts);
+
+    // Test ==
+    c = a == b;
+    ASSERT_EL_TRUTH_V4(c, ==, a, b);
+
+    // Test <
+    c = a < b;
+    ASSERT_EL_TRUTH_V4(c, <, a, b);
+
+    // Test <=
+    c = a <= b;
+    ASSERT_EL_TRUTH_V4(c, <=, a, b);
+
+    // Test >
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test >=
+    c = a > b;
+    ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+    // Test !=
+    c = a != b;
+    ASSERT_EL_TRUTH_V4(c, !=, a, b);
+
+    // Test ternary operator
+    c = 0 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 0, a, b);
+    c = 1 ? a : b;
+    ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, 1, a, b);
+  }
+  return 0;
+}
diff --git a/test/VectorInstructions/integer_ops_signed_symbolic.c b/test/VectorInstructions/integer_ops_signed_symbolic.c
new file mode 100644
index 00000000..80f4e420
--- /dev/null
+++ b/test/VectorInstructions/integer_ops_signed_symbolic.c
@@ -0,0 +1,130 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// NOTE: Have to pass `--optimize=false` to avoid vector operations being
+// optimized away.
+// RUN: %klee --output-dir=%t.klee-out --optimize=false --exit-on-error %t1.bc
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+typedef int32_t v4si __attribute__((vector_size(16)));
+
+#define ASSERT_EL(C, OP, A, B, INDEX) assert(C[INDEX] == (A[INDEX] OP B[INDEX]))
+#define ASSERT_ELV4(C, OP, A, B)                                               \
+  do {                                                                         \
+    ASSERT_EL(C, OP, A, B, 0);                                                 \
+    ASSERT_EL(C, OP, A, B, 1);                                                 \
+    ASSERT_EL(C, OP, A, B, 2);                                                 \
+    ASSERT_EL(C, OP, A, B, 3);                                                 \
+  } while (0);
+
+#define ASSERT_EL_TRUTH(C, OP, A, B, INDEX)                                    \
+  assert(C[INDEX] ? (A[INDEX] OP B[INDEX]) : (!(A[INDEX] OP B[INDEX])))
+#define ASSERT_EL_TRUTH_V4(C, OP, A, B)                                        \
+  do {                                                                         \
+    ASSERT_EL_TRUTH(C, OP, A, B, 0);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 1);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 2);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 3);                                           \
+  } while (0);
+
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, INDEX)          \
+  assert(C[INDEX] == (CONDITION ? A[INDEX] : B[INDEX]))
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(C, CONDITION, A, B)              \
+  do {                                                                         \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 0);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 1);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 2);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 3);                 \
+  } while (0);
+
+int main() {
+  int32_t data[8];
+  klee_make_symbolic(&data, sizeof(data), "unsigned_data");
+  v4si a = {data[0], data[1], data[2], data[3]};
+  v4si b = {data[4], data[5], data[6], data[7]};
+
+  // Test addition
+  v4si c = a + b;
+  ASSERT_ELV4(c, +, a, b);
+
+  // Test subtraction
+  c = b - a;
+  ASSERT_ELV4(c, -, b, a);
+
+  // Test multiplication
+  c = a * b;
+  ASSERT_ELV4(c, *, a, b);
+
+  // Test division
+  if ((data[4] != 0) & (data[5] != 0) & (data[6] != 0) & (data[7] != 0)) {
+    c = a / b;
+    ASSERT_ELV4(c, /, a, b);
+
+    // Test mod
+    c = a % b;
+    ASSERT_ELV4(c, %, a, b);
+    return 0;
+  }
+
+  // Test bitwise and
+  c = a & b;
+  ASSERT_ELV4(c, &, a, b);
+
+  // Test bitwise or
+  c = a | b;
+  ASSERT_ELV4(c, |, a, b);
+
+  // Test bitwise xor
+  c = a ^ b;
+  ASSERT_ELV4(c, ^, a, b);
+
+  // Test left shift
+  if ((data[0] < 32) & (data[1] < 32) & (data[2] < 32) & (data[3] < 32) &
+      (data[0] >= 0) & (data[1] >= 0) & (data[2] >= 0) & (data[3] >= 0)) {
+    c = b << a;
+    ASSERT_ELV4(c, <<, b, a);
+
+    // Test logic right shift
+    c = b >> a;
+    ASSERT_ELV4(c, >>, b, a);
+    return 0;
+  }
+
+  // NOTE: Can't use `ASSERT_ELV4` due to semantics
+  // of GCC vector extensions. See
+  // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
+
+  // Test ==
+  c = a == b;
+  ASSERT_EL_TRUTH_V4(c, ==, a, b);
+
+  // Test <
+  c = a < b;
+  ASSERT_EL_TRUTH_V4(c, <, a, b);
+
+  // Test <=
+  c = a <= b;
+  ASSERT_EL_TRUTH_V4(c, <=, a, b);
+
+  // Test >
+  c = a > b;
+  ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+  // Test >=
+  c = a > b;
+  ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+  // Test !=
+  c = a != b;
+  ASSERT_EL_TRUTH_V4(c, !=, a, b);
+
+  // Test ternary operator
+  int condition = 0;
+  klee_make_symbolic(&condition, sizeof(condition), "unsigned_condition");
+  c = condition ? a : b;
+  ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, condition, a, b);
+  return 0;
+}
diff --git a/test/VectorInstructions/integer_ops_unsigned_symbolic.c b/test/VectorInstructions/integer_ops_unsigned_symbolic.c
new file mode 100644
index 00000000..21ac90ce
--- /dev/null
+++ b/test/VectorInstructions/integer_ops_unsigned_symbolic.c
@@ -0,0 +1,129 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// NOTE: Have to pass `--optimize=false` to avoid vector operations being
+// optimized away.
+// RUN: %klee --output-dir=%t.klee-out --optimize=false --exit-on-error %t1.bc
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+typedef uint32_t v4ui __attribute__((vector_size(16)));
+
+#define ASSERT_EL(C, OP, A, B, INDEX) assert(C[INDEX] == (A[INDEX] OP B[INDEX]))
+#define ASSERT_ELV4(C, OP, A, B)                                               \
+  do {                                                                         \
+    ASSERT_EL(C, OP, A, B, 0);                                                 \
+    ASSERT_EL(C, OP, A, B, 1);                                                 \
+    ASSERT_EL(C, OP, A, B, 2);                                                 \
+    ASSERT_EL(C, OP, A, B, 3);                                                 \
+  } while (0);
+
+#define ASSERT_EL_TRUTH(C, OP, A, B, INDEX)                                    \
+  assert(C[INDEX] ? (A[INDEX] OP B[INDEX]) : (!(A[INDEX] OP B[INDEX])))
+#define ASSERT_EL_TRUTH_V4(C, OP, A, B)                                        \
+  do {                                                                         \
+    ASSERT_EL_TRUTH(C, OP, A, B, 0);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 1);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 2);                                           \
+    ASSERT_EL_TRUTH(C, OP, A, B, 3);                                           \
+  } while (0);
+
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, INDEX)          \
+  assert(C[INDEX] == (CONDITION ? A[INDEX] : B[INDEX]))
+#define ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(C, CONDITION, A, B)              \
+  do {                                                                         \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 0);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 1);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 2);                 \
+    ASSERT_EL_TERNARY_SCALAR_CONDITION(C, CONDITION, A, B, 3);                 \
+  } while (0);
+
+int main() {
+  uint32_t data[8];
+  klee_make_symbolic(&data, sizeof(data), "unsigned_data");
+  v4ui a = {data[0], data[1], data[2], data[3]};
+  v4ui b = {data[4], data[5], data[6], data[7]};
+
+  // Test addition
+  v4ui c = a + b;
+  ASSERT_ELV4(c, +, a, b);
+
+  // Test subtraction
+  c = b - a;
+  ASSERT_ELV4(c, -, b, a);
+
+  // Test multiplication
+  c = a * b;
+  ASSERT_ELV4(c, *, a, b);
+
+  // Test division
+  if ((data[4] != 0) & (data[5] != 0) & (data[6] != 0) & (data[7] != 0)) {
+    c = a / b;
+    ASSERT_ELV4(c, /, a, b);
+
+    // Test mod
+    c = a % b;
+    ASSERT_ELV4(c, %, a, b);
+    return 0;
+  }
+
+  // Test bitwise and
+  c = a & b;
+  ASSERT_ELV4(c, &, a, b);
+
+  // Test bitwise or
+  c = a | b;
+  ASSERT_ELV4(c, |, a, b);
+
+  // Test bitwise xor
+  c = a ^ b;
+  ASSERT_ELV4(c, ^, a, b);
+
+  // Test left shift
+  if ((data[0]) < 32 & (data[1] < 32) & (data[2] < 32) & (data[3] < 32)) {
+    c = b << a;
+    ASSERT_ELV4(c, <<, b, a);
+
+    // Test logic right shift
+    c = b >> a;
+    ASSERT_ELV4(c, >>, b, a);
+    return 0;
+  }
+
+  // NOTE: Can't use `ASSERT_ELV4` due to semantics
+  // of GCC vector extensions. See
+  // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
+
+  // Test ==
+  c = a == b;
+  ASSERT_EL_TRUTH_V4(c, ==, a, b);
+
+  // Test <
+  c = a < b;
+  ASSERT_EL_TRUTH_V4(c, <, a, b);
+
+  // Test <=
+  c = a <= b;
+  ASSERT_EL_TRUTH_V4(c, <=, a, b);
+
+  // Test >
+  c = a > b;
+  ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+  // Test >=
+  c = a > b;
+  ASSERT_EL_TRUTH_V4(c, >, a, b);
+
+  // Test !=
+  c = a != b;
+  ASSERT_EL_TRUTH_V4(c, !=, a, b);
+
+  // Test ternary operator
+  int condition = 0;
+  klee_make_symbolic(&condition, sizeof(condition), "unsigned_condition");
+  c = condition ? a : b;
+  ASSERT_EL_TERNARY_SCALAR_CONDITION_V4(c, condition, a, b);
+  return 0;
+}
diff --git a/test/VectorInstructions/shuffle_element.c b/test/VectorInstructions/shuffle_element.c
new file mode 100644
index 00000000..cf991b03
--- /dev/null
+++ b/test/VectorInstructions/shuffle_element.c
@@ -0,0 +1,83 @@
+// REQUIRES: geq-llvm-3.4
+// RUN: %llvmgcc %s -emit-llvm -O0 -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 --exit-on-error %t1.bc
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+#define ASSERT_EQ_V4(X, Y) \
+  assert(X[0] == Y[0]); \
+  assert(X[1] == Y[1]); \
+  assert(X[2] == Y[2]); \
+  assert(X[3] == Y[3]);
+
+#define ASSERT_EQ_V8(X, Y) \
+  assert(X[0] == Y[0]); \
+  assert(X[1] == Y[1]); \
+  assert(X[2] == Y[2]); \
+  assert(X[3] == Y[3]); \
+  assert(X[4] == Y[4]); \
+  assert(X[5] == Y[5]); \
+  assert(X[6] == Y[6]); \
+  assert(X[7] == Y[7]); \
+
+typedef uint32_t v4ui __attribute__ ((vector_size (16)));
+typedef uint32_t v8ui __attribute__ ((vector_size (32)));
+int main() {
+  v4ui f = { 0, 19, 129, 255 };
+  klee_make_symbolic(&f, sizeof(v4ui), "f");
+  klee_print_expr("f:=", f);
+
+  // Test Single vector shuffle.
+
+  // Extract same element uniformly
+  for (int index=0; index < 4; ++index) {
+    v4ui mask = { index, index, index, index };
+    v4ui result = __builtin_shufflevector(f, mask);
+    v4ui expectedResult = { f[index], f[index], f[index], f[index]};
+    ASSERT_EQ_V4(result, expectedResult);
+  }
+
+  // Reverse vector
+  v4ui mask = { 3, 2, 1, 0 };
+  v4ui result = __builtin_shufflevector(f, mask);
+  v4ui expectedResult = {f[3], f[2], f[1], f[0]};
+  ASSERT_EQ_V4(result, expectedResult);
+
+  // Extract a single element (Clang requires the mask to be constants so we can't use a for a loop).
+#define TEST_SINGLE_EXTRACT(I)\
+  do \
+  { \
+    uint32_t v __attribute__((vector_size(sizeof(uint32_t)))) = __builtin_shufflevector(f, f, I); \
+    uint32_t expected = f[ I % 4 ]; \
+    assert(v[0] == expected); \
+  } while(0);
+  TEST_SINGLE_EXTRACT(0);
+  TEST_SINGLE_EXTRACT(1);
+  TEST_SINGLE_EXTRACT(2);
+  TEST_SINGLE_EXTRACT(3);
+  TEST_SINGLE_EXTRACT(4);
+  TEST_SINGLE_EXTRACT(5);
+  TEST_SINGLE_EXTRACT(6);
+  TEST_SINGLE_EXTRACT(7);
+
+  // Test two vector shuffle
+  v4ui a = { 0, 1, 2, 3 };
+  v4ui b = { 4, 5, 6, 7 };
+
+  {
+    // [a] + [b]
+    v8ui result = __builtin_shufflevector(a, b, 0, 1, 2, 3, 4, 5, 6, 7);
+    v8ui expected = { a[0], a[1], a[2], a[3], b[0], b[1], b[2], b[3] };
+    ASSERT_EQ_V8(result, expected);
+  }
+
+
+
+  return 0;
+}