[klee-dev] FilePerm.c test fails

[Emil Rakadjiev]

Hello Cristian,

Yes, this issue is a corner case; it happens only when LLVM 2.9 is used 
to make a debug build of KLEE (maybe it happens due to a bug in LLVM?). 
Nonetheless, it is strange why only one of the branches in 
has_permissions() is executed, even though the permissions of the file 
are symbolic. And it is also counter-intuitive that a non-optimized run 
fails because it executes less code than an optimized one.
I didn't dive into this deeper to investigate the exact cause.

Best regards,
Emil


On 10/8/2014 6:37 PM, Cristian Cadar wrote:
> Hi Emil,
>
> Thanks for the explanation.  Yes, some of our test cases are fragile, 
> because they can be affected by the exact code generated by the 
> compiler.  I've pushed quite a number of patches to address these 
> issues (e.g., by disabling optimizations), but cases like this still 
> occur. This particular case it's a bit different, because it also 
> depends on the way the POSIX environment is compiled.  The quick 
> partial fix would be to simply check that both branches are hit at 
> least once.
>
> Cristian
>
> On 25/09/14 06:02, Emil Rakadjiev wrote:
>> 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
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> .
>