blob: 4c4b6f98997fc5b6b35a23658b19f314102e51f4 (
plain) (
blame)
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
|
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc
// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt
// RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info
#include "klee/klee.h"
#include <assert.h>
#include <stdio.h>
typedef enum
{
TO_ZERO,
MASKED,
UNKNOWN
} overshift_t;
// We're using unsigned ints so should be doing
// logical right shift.
int overshift(volatile unsigned int y, const char * type)
{
overshift_t ret;
volatile unsigned int x=15;
unsigned int limit = sizeof(x)*8;
volatile unsigned int result;
result = x >> y; // Potential overshift
if (result ==0)
{
printf("%s : Overshift to zero\n", type);
ret = TO_ZERO;
}
else if (result == ( x >> (y % limit)) )
{
printf("%s : Bitmasked overshift\n", type);
ret = MASKED;
}
else
{
printf("%s : Unrecognised behaviour.\n", type);
ret = UNKNOWN;
}
return ret;
}
int main(int argc, char** argv)
{
// Concrete overshift
volatile unsigned int y = sizeof(unsigned int)*8;
overshift_t conc = overshift(y, "Concrete");
assert( conc == TO_ZERO);
// Symbolic overshift
volatile unsigned int y2;
klee_make_symbolic(&y2,sizeof(y),"y2");
// Add constraints so only one value possible
klee_assume(y2 > (y-1));
klee_assume(y2 < (y+1));
overshift_t sym = overshift(y2, "Symbolic");
assert( sym == TO_ZERO);
// Concrete and symbolic behaviour should be the same
assert( conc == sym);
return 0;
}
|
