FilePerm.c test fails

Discussion:

Emil Rakadjiev

2014-08-22 04:19:58 UTC

Hello,

I built KLEE and its dependencies (LLVM 2.9, STP upstream, klee-uclibc klee_0_9_29 branch) and tried running the regression and unit tests. Everything works fine, except the FilePerm.c test.
The problem is that in the FilePerm test definition there are 3 test cases, but KLEE generates only two, and thus "RUN: test -f %T/klee-last/test000003.ktest" fails, because the file does not exist.

The relevant output files are at the end of this mail. I'm using Ubuntu 14.04.

Do you know what is the reason for the test failure? Which should be the 3 test cases (open is successful, open fails, ...)?

I also have another, loosely related question: What is the point of making stdout symbolic?

Thank you very much! Best regards,
Emil

---

FilePerm.c.tmp.log:

KLEE: NOTE: Using klee-uclibc : /home/er/workspace/klee/build/debug/Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/er/workspace/klee/build/debug/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/klee-out-9"
KLEE: WARNING: undefined reference to function: lseek64
KLEE: WARNING: undefined reference to function: stat64
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 61845200)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: stat64(61760464, 62008240)
File 'A' opened successfully
Cannot open file 'A'

KLEE: done: total instructions = 8832
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

---
info:

/home/er/workspace/klee/build/debug/Release+Asserts/bin/klee --libc=uclibc --posix-runtime /home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/FilePerm.c.tmp.bc --sym-files 1 10 --sym-stdout
PID: 15303
Started: 2014-08-22 12:03:08
BEGIN searcher description
<InterleavedSearcher> containing 2 searchers:
RandomPathSearcher
WeightedRandomSearcher::CoveringNew
</InterleavedSearcher>
END searcher description
Finished: 2014-08-22 12:03:08
Elapsed: 00:00:00
KLEE: done: explored paths = 2
KLEE: done: avg. constructs per query = 69
KLEE: done: total queries = 58
KLEE: done: valid queries = 2
KLEE: done: invalid queries = 56
KLEE: done: query cex = 58

KLEE: done: total instructions = 8832
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

---
test000001.ktest:

ktest file : 'test000001.ktest'
args : ['/home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/FilePerm.c.tmp.bc', '--sym-files', '1', '10', '--sym-stdout']
num objects: 7
object 0: name: 'A-data'
object 0: size: 10
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 1: name: 'A-data-stat'
object 1: size: 144
object 1: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\xaf\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 2: name: 'stdin'
object 2: size: 10
object 2: data: '\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 3: name: 'stdin-stat'
object 3: size: 144
object 3: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\xaf\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 4: name: 'stdout'
object 4: size: 1024
object 4: data:
'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0
0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 5: name: 'stdout-stat'
object 5: size: 144
object 5: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\xaf\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 6: name: 'model_version'
object 6: size: 4
object 6: data: '\x01\x00\x00\x00'

---
test000002.ktest:

ktest file : 'test000002.ktest'
args : ['/home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/FilePerm.c.tmp.bc', '--sym-files', '1', '10', '--sym-stdout']
num objects: 7
object 0: name: 'A-data'
object 0: size: 10
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 1: name: 'A-data-stat'
object 1: size: 144
object 1: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x12\x80\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\xaf\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 2: name: 'stdin'
object 2: size: 10
object 2: data: '\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 3: name: 'stdin-stat'
object 3: size: 144
object 3: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\xaf\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 4: name: 'stdout'
object 4: size: 1024
object 4: data:
'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0
0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 5: name: 'stdout-stat'
object 5: size: 144
object 5: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\xaf\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe5\xb2\xf6S\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 6: name: 'model_version'
object 6: size: 4
object 6: data: '\x01\x00\x00\x00'

Emil Rakadjiev

2014-08-22 11:30:17 UTC

Permalink

I ran the tests on Ubuntu 12.04 (upstream STP doesn't build, so I used r940); the result is the same, FilePerm.c fails.

But while trying to find out the reason for the test failure, I tried analyzing the assembly.ll files and noticed that they are broken. At least one line is truncated, and not just in the FilePerm.c test files. Examples:

FilePerm.c test:
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt -analyze -view-cfg assembly.ll
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt:assembly.ll:76:1: error: expected end of struct constant

The contents of assembly.ll are:
...
74 @.str23 = private constant [18 x i8] c"ignoring (ENOENT)\00", align 1
75 @__exe_env = global %struct.exe_sym_env_t { [32 x %struct.exe_file_t] [%struct.exe_file_t { i32 0, i32 5, i64 0, %struct.exe_disk_file_t* null }, %struct.exe_file_t { i32 1, i32 9, i64 0, %struct.exe_disk_file_t* null }, %struct.exe_file_t { i32 2, i32 9
76 @.str24 = private constant [6 x i8] c"-stat\00", align 1
...
(the end of line 75 is missing)

---

FD_Fail2.c test:
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt -analyze -view-cfg assembly.ll
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt: assembly.ll:69:254: error: expected type

The contents of assembly.ll are:
...
68 @unknown.1225 = internal constant [14 x i8] c"Unknown error "
69 @_stdio_streams = internal global [3 x %struct.FILE] [%struct.FILE { i16 544, [2 x i8] zeroinitializer, i32 0, i8* null, i8* null, i8* null, i8* null, i8* null, i8* null, %struct.FILE* getelementptr inbounds ([3 x %struct.FILE]* @_stdio_streams, i64 0, i
70 @stdin = global %struct.FILE* getelementptr inbounds ([3 x %struct.FILE]* @_stdio_streams, i64 0, i64 0)
...
(the end of line 69 is missing)

----

This is probably unrelated to the FilePerm.c test failure, but it'd still be good to know why the lines are truncated.

Thank you,
Emil

PS: A minor correction to my previous email: I noticed that I posted the contents of FilePerm.c.tmp.log, after I manually added "-libc=uclibc" to the special RUN comment, thus there are less warnings. The log of the original, unmodified version is below. This doesn't make any difference in the test outcome, though.
KLEE: NOTE: Using model: /home/er/workspace/klee/build/debug/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/klee-out-44"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: __fgetc_unlocked
KLEE: WARNING: undefined reference to function: __fputc_unlocked
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to function: stat64
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: stat64(59728192, 59825904)
KLEE: WARNING ONCE: calling external: __errno_location()
KLEE: WARNING ONCE: calling external: fwrite(59701472, 1, 21, 140474038325696)
Cannot open file 'A'
File 'A' opened successfully

KLEE: done: total instructions = 2382
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

Cristian Cadar

2014-08-22 11:43:40 UTC

Permalink

Hi Emil,

Lines are truncated to go over a kcachegrind bug; to avoid this problem,
just pass -no-truncate-source-lines to KLEE.

I'm not sure why FilePerm.c fails on your machine, it might be a fragile
test. But I noticed that you run the test with uclibc enabled, while
the default configuration is to run w/o uclibc. Have you changed some
of the default options?

Cristian

Post by Emil Rakadjiev
I ran the tests on Ubuntu 12.04 (upstream STP doesn't build, so I used
r940); the result is the same, FilePerm.c fails.
But while trying to find out the reason for the test failure, I tried
analyzing the assembly.ll files and noticed that they are broken. At
least one line is truncated, and not just in the FilePerm.c test files.
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt -analyze -view-cfg assembly.ll
error: expected end of struct constant
...
%struct.exe_file_t] [%struct.exe_file_t { i32 0, i32 5, i64 0,
%struct.exe_disk_file_t* null }, %struct.exe_file_t { i32 1, i32 9, i64
0, %struct.exe_disk_file_t* null }, %struct.exe_file_t { i32 2, i32 9
...
(the end of line 75 is missing)
---
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt -analyze -view-cfg assembly.ll
error: expected type
...
i16 544, [2 x i8] zeroinitializer, i32 0, i8* null, i8* null, i8* null,
i8* null, i8* null, i8* null, %struct.FILE* getelementptr inbounds ([3 x
...
(the end of line 69 is missing)
----
This is probably unrelated to the FilePerm.c test failure, but it'd
still be good to know why the lines are truncated.
Thank you,
Emil
PS: A minor correction to my previous email: I noticed that I posted the
contents of FilePerm.c.tmp.log, after I manually added "-libc=uclibc" to
the special RUN comment, thus there are less warnings. The log of the
original, unmodified version is below. This doesn't make any difference
in the test outcome, though.
/home/er/workspace/klee/build/debug/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is
"/home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/klee-out-44"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: __fgetc_unlocked
KLEE: WARNING: undefined reference to function: __fputc_unlocked
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to function: stat64
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: stat64(59728192, 59825904)
KLEE: WARNING ONCE: calling external: __errno_location()
KLEE: WARNING ONCE: calling external: fwrite(59701472, 1, 21,
140474038325696)
Cannot open file 'A'
File 'A' opened successfully
KLEE: done: total instructions = 2382
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Daniel Liew

2014-08-22 13:04:19 UTC

Permalink

Post by Cristian Cadar
Hi Emil,
Lines are truncated to go over a kcachegrind bug; to avoid this problem,
just pass -no-truncate-source-lines to KLEE.

Does KCacheGrind work with .ll files? If not I don't see a reason to
truncate the .ll file. Also is this bug in kcachegrind still relevant
with a modern version (e.g. I have 0.7.4).

I also tried looking FilePerm.c . Whilst the test does pass for me I
tried adding the -write-cov option. The coverage files seem completely
wrong (I'm assuming each .cov file is supposed to show the set of
lines that were visited), lots lines that ought to be there are
missing.

Cristian Cadar

2014-08-22 17:18:51 UTC

Permalink

Unfortunately, we haven't documented that issue very well, but this is
why I remember we had that option. We could consider enabling that
option by default and see if we encounter any problems.

Regarding .cov files, they only record any previously uncovered lines
executed by that path.

Cristian

Post by Daniel Liew

Post by Cristian Cadar
Hi Emil,
Lines are truncated to go over a kcachegrind bug; to avoid this problem,
just pass -no-truncate-source-lines to KLEE.

Does KCacheGrind work with .ll files? If not I don't see a reason to
truncate the .ll file. Also is this bug in kcachegrind still relevant
with a modern version (e.g. I have 0.7.4).
I also tried looking FilePerm.c . Whilst the test does pass for me I
tried adding the -write-cov option. The coverage files seem completely
wrong (I'm assuming each .cov file is supposed to show the set of
lines that were visited), lots lines that ought to be there are
missing.

Emil Rakadjiev

2014-08-25 02:23:43 UTC

Permalink

Hello Cristian and Daniel,

Thank you for the replies!

The -no-truncate-source-lines argument fixes the issue with the assembly files, and opt generates nice CFGs. KCachegrind seems to show the same results with and without that argument (I checked for FilePerm.c and FD_Fail2.c).

What are the 3 FilePerm.c test cases that KLEE generates for you? Should close() on a symbolic file branch? If yes, then this would indeed result in 3 test cases:
1) open() == -1
2) open() != -1 && close() == -1
3) open() != -1 && close() == 0
For me only 1) and 3) are explored.

Also, could you explain please why stdout is declared symbolic? What effect does this have?

But I noticed that you run the test with uclibc enabled, while the default configuration is to run w/o uclibc. Have you changed some of the default options?

Cristian, yes, I was trying various things, and the output I posted in my first message was with uclibc included. I noticed this later and in the PS of my second message I mentioned it, and attached the output with the default parameters (results are the same, though).

Thanks and best regards,
Emil

Emil Rakadjiev

2014-09-25 05:02:01 UTC

Permalink

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

Cristian Cadar

2014-10-08 09:37:48 UTC

Permalink

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

Post by Emil Rakadjiev
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
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
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Emil Rakadjiev

2014-10-09 07:23:03 UTC

Permalink

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

Post by 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

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.

Cristian Cadar

2014-10-09 14:28:08 UTC

Permalink

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

Post by 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

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Emil Rakadjiev

2014-10-10 09:25:23 UTC

Permalink

Hello Cristian,

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

Best regards,
Emil

Post by 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

Post by Emil Rakadjiev
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
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
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.