diff options
Diffstat (limited to 'test/VectorInstructions')
| -rw-r--r-- | test/VectorInstructions/extract_element.c | 36 | ||||
| -rw-r--r-- | test/VectorInstructions/extract_element_symbolic.c | 21 | ||||
| -rw-r--r-- | test/VectorInstructions/floating_point_ops_constant.c | 152 | ||||
| -rw-r--r-- | test/VectorInstructions/insert_element.c | 46 | ||||
| -rw-r--r-- | test/VectorInstructions/insert_element_symbolic.c | 22 | ||||
| -rw-r--r-- | test/VectorInstructions/integer_ops_constant.c | 201 | ||||
| -rw-r--r-- | test/VectorInstructions/integer_ops_signed_symbolic.c | 130 | ||||
| -rw-r--r-- | test/VectorInstructions/integer_ops_unsigned_symbolic.c | 129 | ||||
| -rw-r--r-- | test/VectorInstructions/shuffle_element.c | 83 |
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; +} |