[klee-dev] KLEE with Gzip

[ddun]

Hi All,

I am trying to run KLEE on gzip to generate input test cases for the
decompression. The problem i am facing is that all the test cases KLEE is
generating are same and they all are all zeros. Can someone point out what
i maybe doing wrong?

This is the command I am using :

klee  --only-output-states-covering-new \
--simplify-sym-indices \
--max-memory=1000 \
--disable-inlining \
--use-forked-stp
-allow-external-sym-calls \
--max-instruction-time=30. \
--use-batching-search \
--batch-instructions=10000 \
 --max-static-solve-pct=1 \
--max-static-cpfork-pct=1 \
--switch-type=internal \
--max-memory-inhibit=false \
--max-static-fork-pct=1  \
--max-sym-array-size=256 \
--libc=uclibc --posix-runtime ./gzip.bc -d --sym-files 1 100



and this is the output test cases i am getting (i am pasting just 2) :

 ktest-tool klee-last/test000031.ktest
ktest file : 'klee-last/test000031.ktest'
args       : ['./gzip.bc', '-d', '--sym-files', '1', '100']
num objects: 5
object    0: name: 'A-data'
object    0: size: 100
object    0: 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'
object    1: name: 'A-data-stat'
object    1: size: 96
object    1: data:
'\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff'
object    2: name: 'stdin'
object    2: size: 100
object    2: data:
'PK\x03\x04\x00\x00\x00\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00=\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\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    3: name: 'stdin-stat'
object    3: size: 96
object    3: data:
'\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff'
object    4: name: 'model_version'
object    4: size: 4
object    4: data: '\x01\x00\x00\x00'





 ktest-tool klee-last/test000013.ktest
ktest file : 'klee-last/test000013.ktest'
args       : ['./gzip.bc', '-d', '--sym-files', '1', '100']
num objects: 5
object    0: name: 'A-data'
object    0: size: 100
object    0: 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'
object    1: name: 'A-data-stat'
object    1: size: 96
object    1: data:
'\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff'
object    2: name: 'stdin'
object    2: size: 100
object    2: data:
'PK\x03\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x80\x03\x00\x16\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\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    3: name: 'stdin-stat'
object    3: size: 96
object    3: data:
'\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff'
object    4: name: 'model_version'
object    4: size: 4
object    4: data: '\x01\x00\x00\x00'
-------------- next part --------------
HTML attachment scrubbed and removed