-
Notifications
You must be signed in to change notification settings - Fork 0
/
transff.cpp
59 lines (51 loc) · 1.47 KB
/
transff.cpp
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
#include <klee-opencv.h>
#include "cv.h"
#include <klee.h>
#include <assert.h>
#ifndef TRANS_N
#define TRANS_N 4
#endif
#ifndef TRANS_NC
#define TRANS_NC 3
#endif
int main(int argc, char** argv) {
#ifndef __CONCRETE
unsigned sse_count_v, sse_count_s;
#endif
float mat1data[TRANS_N*TRANS_N*TRANS_NC], mat2data[TRANS_NC*TRANS_N];
CvMat mat1, mat2;
CvMat *mat3v = cvCreateMat(TRANS_N, TRANS_N, CV_32FC(TRANS_NC));
CvMat *mat3s = cvCreateMat(TRANS_N, TRANS_N, CV_32FC(TRANS_NC));
klee_make_symbolic(mat1data, sizeof(mat1data), "mat1data");
klee_make_symbolic(mat2data, sizeof(mat2data), "mat2data");
mat1 = cvMat(TRANS_N, TRANS_N, CV_32FC(TRANS_NC), mat1data);
mat2 = cvMat(TRANS_NC, TRANS_N, CV_32FC1, mat2data);
cvUseOptimized(true);
#ifndef __CONCRETE
klee_sse_count = 0;
#endif
cvTransform(&mat1, mat3v, &mat2, NULL);
#ifndef __CONCRETE
sse_count_v = klee_sse_count;
#endif
cvUseOptimized(false);
#ifndef __CONCRETE
klee_sse_count = 0;
#endif
cvTransform(&mat1, mat3s, &mat2, NULL);
#ifndef __CONCRETE
sse_count_s = klee_sse_count;
printf("SSE COUNT: V=%d S=%d\n", sse_count_v, sse_count_s);
assert(sse_count_v > sse_count_s);
#endif
bool same = true;
for (int i = 0; i < TRANS_N*TRANS_N*TRANS_NC; i++) {
char buf[256];
sprintf(buf, "mat3s->data.fl[%d]", i);
klee_print_expr(buf, mat3s->data.fl[i]);
sprintf(buf, "mat3v->data.fl[%d]", i);
klee_print_expr(buf, mat3v->data.fl[i]);
same &= bitwise_eq(mat3s->data.fl[i], mat3v->data.fl[i]);
}
assert(same);
}