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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
