1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
// RUN: %clang %s -emit-llvm %O0opt -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;
}
|
