FilePerm.c test fails with debug build of KLEE (LLVM 2.9)

[erakadjiev]

Hello,

I'm opening this issue as a follow-up to a thread in the mailing list.

Summary:

If LLVM 2.9 is used and a debug build of KLEE is made, the FilePerm.c test fails, because one of the branches in the has_permission() method in runtime/POSIX/fd.c is not explored, and thus only two test cases are generated instead of the expected 3. With LLVM 3.4, or with a regular build this doesn't happen.

Environments where error occured:

Ubuntu 12.04 and 14.04, LLVM 2.9 (LLVM-GCC 4.2), STP r940 and upstream, klee-uclibc 0_9_29, and recent KLEE versions (incl. current newest 10b800d)

Details:

The part of the code that is relevant for this test case is in the has_permission() method in runtime/POSIX/fd.c (this method is called by __fd_open()). At the end of has_permission() there are the following two checks:

if (read_access && ((mode & S_IRUSR) | (mode & S_IRGRP) | (mode & S_IROTH)))
    return 0;
if (write_access && !((mode & S_IWUSR) | (mode & S_IWGRP) | (mode & S_IWOTH)))
    return 0;

Since the method is called with a symbolic file's symbolic stat (and thus the mode in stat, i.e. the permissions are symbolic too), and the file is opened with O_RDWR (so both read_access and write_access are true), the following 3 paths are explored:

1. open() succeeds: first if's condition is false, second if's condition is false -> has_permission() returns 1 -> __fd_open()/open() returns non-negative fd
2. open() fails: first if's condition is true -> has_permission() returns 0 -> __fd_open()/open() returns -1
3. open() fails: first if's condition is false, second if's condition is true -> has_permission() returns 0 -> __fd_open()/open() returns -1

But if a debug build of KLEE is built according to the instructions in the developer's guide, namely using CXXFLAGS="-g -O0" CFLAGS="-g -O0", then path 3 is not explored, thus only 2 test cases are generated and FilePerm.c fails.

Best regards,
Emil

[andreamattavelli]

@ccadar since we deprecated 2.9, I would close this issue.

[ccadar]

OK, let's close it.