[klee-dev] FilePerm.c test fails

[Cristian Cadar]

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