[klee-dev] KLEE with Gzip
Urmas Repinski
urrimus at hotmail.com
Sat Oct 12 06:02:15 BST 2013
Hello,
It is still ok,
the sym-files klee option has following description -
-sym-files - Make stdin and up to NUM symbolic files, each with maximum size N.http://klee.llvm.org/TestingCoreutils.html
The thing is that the stdin then is used by the ./gzip.bc program, but other input A-data is not then, that's why strdin were generated, A-data not.
If stdin will be not used by the code, then it will be avoided, like A-data in this case.
Possibly stdin is that you need actually?
Urmas Repinski
From: ddun.user at gmail.com
Date: Sat, 12 Oct 2013 00:50:27 -0400
Subject: Re: [klee-dev] KLEE with Gzip
To: urrimus at hotmail.com
CC: klee-dev at imperial.ac.uk
Yes, but the object 2 is listed as 'stdin' while the only variable is considered is the symbolic file A. which is still all zeros. Therefore I am confused, which one to refer to as we are not giving input through 'stdin'.
On Sat, Oct 12, 2013 at 12:40 AM, Urmas Repinski <urrimus at hotmail.com> wrote:
Hello,
The thing is that those two test cases are not all zeros and not the same -
They are different at object2 variable's values, and x08 corresponds to the character with ASCII code '8', those are strings 100 character long as it were necessary to generate:
--sym-files 1 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'
and
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'
I see no error,
and if inputs are in the wrong format, then probably you should modify parameters.
Urmas Repinski.
From: ddun.user at gmail.com
Date: Fri, 11 Oct 2013 20:14:04 -0400
To: klee-dev at imperial.ac.uk
Subject: [klee-dev] KLEE with Gzip
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.ktestktest file : 'klee-last/test000031.ktest'
args : ['./gzip.bc', '-d', '--sym-files', '1', '100']num objects: 5object 0: name: 'A-data'object 0: size: 100object 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: 96object 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: 100object 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: 96object 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: 4object 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: 5object 0: name: 'A-data'
object 0: size: 100object 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: 96object 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: 100object 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: 96object 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: 4object 4: data: '\x01\x00\x00\x00'
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list