From 8e8732d482e42e363f0f4c51794ed966701371e7 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 24 May 2017 16:32:47 +0100
Subject: 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.
---
 test/VectorInstructions/shuffle_element.c | 83 +++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)
 create mode 100644 test/VectorInstructions/shuffle_element.c

(limited to 'test/VectorInstructions/shuffle_element.c')

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