about summary refs log tree commit diff homepage
path: root/test/Feature/logical-right-overshift-sym-conc.c
blob: 00281ec4787c5cb6c8ce31fde59a32d5401c90b4 (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
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc
// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt
// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info
#include <stdio.h>
#include <assert.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;
}