[klee-dev] FilePerm.c test fails

[Cristian Cadar]

Hi Emil, we need to look exactly at the code generated in each case. 
Can you open an issue on GitHub with the text of your original email?

Thanks,
Cristian

On 09/10/14 08:23, Emil Rakadjiev wrote:
> 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
>>
>> .
>>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev