[klee-dev] FilePerm.c test fails

[Emil Rakadjiev]

Hello Cristian,

I've opened an issue on GitHub: https://github.com/klee/klee/issues/169

Best regards,
Emil



On 10/9/2014 11:28 PM, Cristian Cadar wrote:
> 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
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> .
>