-
Notifications
You must be signed in to change notification settings - Fork 0
/
silhouette.cpp
129 lines (116 loc) · 3.2 KB
/
silhouette.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
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
#include <klee-opencv.h>
#include "cv.h"
#ifndef __CONCRETE
#include <klee.h>
#endif
#include <assert.h>
#include <unistd.h>
#include <stdio.h>
#include <stdlib.h>
double sym_atof(const char *s, const char *name) {
#ifndef __CONCRETE
if (*s == 's') {
double sd;
klee_make_symbolic(&sd, sizeof(sd), name);
return sd;
}
#endif
return atof(s);
}
int main(int argc, char **argv) {
#ifndef __CONCRETE
unsigned sse_count_v, sse_count_s;
#endif
void *mat1data, *mat2data;
size_t mat1size, mat2size;
CvMat mat1, mat2v, mat2s;
int matwidth = 4;
int matheight = 4;
int do_random = 0;
int diffs = 0;
double timestamp = 2.0, duration = 2.0;
int ch;
while ((ch = getopt(argc, argv, "w:h:t:d:r:")) != -1) {
switch (ch) {
case 'w': matwidth = atoi(optarg); break;
case 'h': matheight = atoi(optarg); break;
case 't': timestamp = sym_atof(optarg, "timestamp"); break;
case 'd': duration = sym_atof(optarg, "duration"); break;
#ifdef __CONCRETE
case 'r': do_random = 1; srandom(atoi(optarg)); srand48(atoi(optarg)); break;
#endif
}
}
mat1size = matwidth * matheight;
mat1data = malloc(mat1size);
mat2size = matwidth * matheight * sizeof(float);
mat2data = malloc(mat2size);
#ifdef __CONCRETE
if (do_random) {
char *mat1cdata = (char *) mat1data;
float *mat2fdata = (float *) mat2data;
int left = mat1size;
while (left--) {
*(mat1cdata++) = random();
*(mat2fdata++) = drand48();
}
} else {
memcpy(mat1data, "\x7f\x7f\xba\x00\xb8\x9b/\x00\xde\xa4\x11\x00UH\xfe\x00", mat1size); /* TODO: real data */
}
#else
klee_make_symbolic(mat1data, mat1size, "mat1data");
klee_make_symbolic(mat2data, mat2size, "mat2data");
#endif
mat1 = cvMat(matheight, matwidth, CV_8UC1, mat1data);
mat2v = cvMat(matheight, matwidth, CV_32FC1, mat2data);
mat2s = cvMat(matheight, matwidth, CV_32FC1, mat2data);
cvUseOptimized(true);
#ifndef __CONCRETE
klee_sse_count = 0;
#endif
cvUpdateMotionHistory(&mat1, &mat2v, timestamp, duration);
#ifndef __CONCRETE
sse_count_v = klee_sse_count;
#endif
cvUseOptimized(false);
printf("====================\n");
#ifndef __CONCRETE
klee_sse_count = 0;
#endif
cvUpdateMotionHistory(&mat1, &mat2s, timestamp, duration);
#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
#ifdef __CONCRETE
#define PRINT_AND_CHECK(FLD, S) \
diffs = 0; \
for (int i = 0; i < matwidth*matheight; i++) { \
printf(#FLD "[%d]: " S " vs." S, i, mat2s.data.FLD[i], mat2v.data.FLD[i]); \
if (mat2s.data.FLD[i] != mat2v.data.FLD[i]) { \
printf(" ...NO\n"); \
diffs++; \
} \
else printf("\n"); \
} \
printf("--\n"); \
if (diffs) \
printf("%d mismatches FOUND!\n", diffs); \
else printf("No mismatches found.\n");
#else
bool same = true;
#define PRINT_AND_CHECK(FLD, S) \
for (int i = 0; i < matwidth*matheight; i++) { \
char buf[256]; \
sprintf(buf, "mat2s.data." #FLD "[%d] == mat2v.data." #FLD "[%d]", i, i); \
klee_print_expr(buf, mat2s.data.FLD[i] == mat2v.data.FLD[i]); \
same &= bitwise_eq(mat2s.data.FLD[i], mat2v.data.FLD[i]); \
}
#endif
PRINT_AND_CHECK(fl, "%f")
#ifndef __CONCRETE
klee_print_expr("same", same);
assert(same);
#endif
}