diff options
Diffstat (limited to 'test/VectorInstructions/integer_ops_signed_symbolic.c')
| -rw-r--r-- | test/VectorInstructions/integer_ops_signed_symbolic.c | 130 |
1 files changed, 130 insertions, 0 deletions
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; +} |