[klee-dev] klee - mmap - error

[Sandeep Romana]

Hi list,

While experimenting with the klee we found that klee does not work with mmap.
Can anybody in the list help with this. Used klee version 1.2 1.3, klee-uclibc
klee_0_9_29 and llvm and clang 3.4. Also crosschecked with the docker image.
Compiled our sample program with clang and executed with "klee --emit-all-errors
--posix-runtime -libc=uclibc exp.bc try"

sample test program (taken from stackoverflow):

int main(int argc, char const *argv[])
{
    unsigned char *f;
    int size;
    struct stat s;
    const char * file_name = argv[1];
    int fd = open (argv[1], O_RDONLY);

    /* Get the size of the file. */
    int status = fstat (fd, & s);
    size = s.st_size;
        klee_make_symbolic(&size,sizeof(size),"sym");

    f = (unsigned char *) mmap (0, size, PROT_READ, MAP_PRIVATE, fd, 0);
    for (int i = 0; i < size; i++) {
        char c;

        c = f[i];
        putchar(c);
    }

        if(size==5)
        {
                printf("five\n");
        }
        else if(size<5)
        {
                printf("less\n");
                klee_assert(0);
        }
        else
                printf("else\n");

    return 0;
}

output:

KLEE: NOTE: Using klee-uclibc :
/home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model:
/home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/klee-out-1"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 38712064)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled.
Using alignment of 8.
KLEE: WARNING: mmap: ignoring (EPERM)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: WARNING ONCE: calling external: printf(51025216)
less
KLEE: ERROR: (location information missing) ASSERTION FAIL: 0

KLEE: done: total instructions = 5928
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

Thanks,

Sandeep
-------------------------------------------------------------------------------------------------------------------------------
[ C-DAC is on Social-Media too. Kindly follow us at:
Facebook: https://www.facebook.com/CDACINDIA & Twitter: @cdacindia ]

This e-mail is for the sole use of the intended recipient(s) and may
contain confidential and privileged information. If you are not the
intended recipient, please contact the sender by reply e-mail and destroy
all copies and the original message. Any unauthorized review, use,
disclosure, dissemination, forwarding, printing or copying of this email
is strictly prohibited and appropriate legal action will be taken.
-------------------------------------------------------------------------------------------------------------------------------

-------------- next part --------------
HTML attachment scrubbed and removed