[klee-dev] Test cases generated for symbolic file

[Andrew Santosa]

 Thanks Sang.
I hope to find time to write the tests to make codecov happy.
Andrew

    On Saturday, 23 June 2018, 2:33:20 pm GMT+8, Sang Phan <phanquocsang at gmail.com> wrote:  
 
 Hi Andrew,

I only build the tool for my own task, and I don't intend to submit a
PR, so please go ahead with yours.

Sang

On Fri, Jun 22, 2018 at 9:32 PM, Andrew Santosa <asantosa1999 at gmail.com> wrote:
> Hi Sang,
>
> I urgently need a tool like you mentioned, so I wrote one myself within KLEE
> source tree. You can find the source as tools/gen-bout.cpp in the gen-bout
> branch
> of 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 the
> actual 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 917
> https://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