Implement basic support for vectorized instructions.

We use LLVM's Scalarizer pass to remove most vectorized code so that the
Executor only needs to support the InsertElement and ExtractElement
instructions.

This pass was not available in LLVM 3.4 so to support that LLVM version
the pass has been back ported.

To check that the Executor is not receiving vector operand types
that it can't handle assertions have been added.

There are a few limitations to this implementation.

* The InsertElement and ExtractElement index cannot be symbolic.
* There is no support for LLVM < 3.4.

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;
+}