[klee-dev] KLEE with Gzip

[ddun]

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.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'
>
>
> _______________________________________________ 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