[klee-dev] Test cases generated for symbolic file

[Andrew Santosa]

 Hi Sang,

I urgently need a tool like you mentioned, so I wrote one myself within KLEEsource tree. You can find the source as tools/gen-bout.cpp in the gen-bout branchof my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout
I don't exactly know the answer to your question. For normal files, I get the stat from theactual files whose contents are loaded into the symbolic files. For stdin and stdout,I get the stats using fstat64 of file descriptors 0 and 1, respectively.
I think model_version is mandatory if one wants to use the produced file as a seed.

I had submitted PR 917https://github.com/klee/klee/pull/917
But probably this PR will not pass the CI tests since I had not added the tests.I will also close it now since you publicly announced your tool first.

Best,Andrew

    On Saturday, 23 June 2018, 1:13:31 am GMT+8, Sang Phan <phanquocsang at gmail.com> wrote:  
 
 Thanks Cristian.

I want to feed KLEE with my customized seeds, instead of random ones.
So I need a tool similar to gen-random-bout to generate .ktest file.
To write such a tool, I would like to know how to generate the stat
and model-version

Here is my quick implementation:
https://github.com/qsphan/klee-utils/blob/master/src/gen-ktest.cpp
+ stat is generated randomly, copied from to gen-random-bout
+ model version is always set to 1

It seems to work just fine right now. But as both stat and
model-version appear in the path condition, is there any possible
problem with this settings?

Best,
Sang


On Fri, Jun 22, 2018 at 9:47 AM, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> Hi, you can ignore the model_version, it just keeps track of the version for
> the POSIX model.  The stat buffer keeps the stat info associated with the
> file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html).  If you
> have time, it would be useful to document this on the website (e.g., at
> http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at
> https://github.com/klee/klee.github.io
>
> Best,
> Cristian
>
>
> On 21/06/18 21:55, Sang Phan wrote:
>>
>> Hello,
>>
>> I'm trying to understand the test cases generated when the input is
>> symbolic file.
>> For the password example under this link:
>> https://klee.github.io/tutorials/using-symbolic/, a test case viewed
>> by ktest-tool is the following:
>>
>> https://klee.github.io/tutorials/using-symbolic/
>>
>>
>> ktest file : 'test000004.ktest'
>> args      : ['password.bc', 'A', '-sym-files', '1', '10']
>> num objects: 3
>> object    0: name: b'A-data'
>> object    0: size: 10
>> object    0: data: b'hel\x00\x00\x00\x00\x00\x00\x00'
>> object    1: name: b'A-data-stat'
>> object    1: size: 144
>> object    1: data:
>>
>> b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\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\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\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: b'model_version'
>> object    2: size: 4
>> object    2: data: b'\x01\x00\x00\x00'
>>
>> + I understand A-data is the content of the file, but what is
>> A-data-stat and model-version?
>> + From the gen-random-bout, it seems data-stat can be generated
>> randomly, but how about model-version?
>>
>> Thanks,
>> Sang
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
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