[klee-dev] FilePerm.c test fails

[Emil Rakadjiev]

Hello,

In the meantime, I found out under what circumstances the FilePerm.c 
test fails. The problem is compiler-dependent and occurs with LLVM 2.9, 
but not with LLVM 3.4.

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 is 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.

I've tested this on Ubuntu 14.04 with LLVM 2.9 (LLVM-GCC 4.2), STP r-940 
and upstream, klee-uclibc klee_0_9_29, and KLEE revisions e87af57 and 
547dd6f (the current newest one).
As mentioned above, with LLVM 3.4 (Clang 3.4) the error does not occur.

Best regards,
Emil