[klee-dev] .kteest & .kquery files

Thu Jul 1 10:12:05 BST 2021

Hi,

Thank you for your response and it was exactly what I was looking for.
-I was able to follow your leads and able to understand the format of a
.ktest file.
-My next step was to understand different elements in .ktest files. I've
experimented with .ktest files generated with the use of different options
in KLEE symbolic environment etc. Really appreciate it if you could help
clarify the following questions.

a.Below test cases have 3 objects. Can you help clarify the significance &
usage of the 2nd('stat') and 3rd('model_version') objects.
b.What is the logic for the content of the 'stat' object & 'model_version'
objects? Hard coded ?
c.Is the stat object always 144 bytes and 'model version' 4 bytes ?
d.Some of the generated test cases in different experiments did not contain
'stat' object, also some did not contain both 'stat' & 'model_version'
objects.
Are these optional ? Can I omit these objects altogether If I'm generating
custom .ktest files ?

*#Test case 1 ************************************************************
----
ktest file : 'klee-out-0/test000001.ktest'
args       : ['password.bc', 'A', '-sym-files', '1', '10']
num objects: 3
object 0: name: 'A-data'
object 0: size: 10
object 0: data: b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 0: hex : 0x00000000000000000000
object 0: text: ..........
object 1: name: 'A-data-stat'
object 1: size: 144
object 1: data:
b'&\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\xff\xff\xff\xff\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x00\x10\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x00\x7f\xdd`\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x04\x7f\xdd`\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x04\x7f\xdd`\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
object 1: hex :
0x260000000000000001000000ffffffff0100000000000000a4810000e8030000e8030000ffffffff0000000000000000ffffffffffffffff0010000000000000ffffffffffffffff007fdd6000000000ffffffffffffffff047fdd6000000000ffffffffffffffff047fdd6000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
object 1: text:
&..........................................................................`...............`...............`....................................
object 2: name: 'model_version'
object 2: size: 4
object 2: data: b'\x01\x00\x00\x00'
object 2: hex : 0x01000000
object 2: int : 1
object 2: uint: 1
object 2: text: ....

*#Test case 2 ************************************************************
----
ktest file : 'klee-out-0/test000001.ktest'
args       : ['test.bc', '-sym-stdin', '1']
num objects: 3
object 0: name: 'stdin'
object 0: size: 1
object 0: data: b'\x80'
object 0: hex : 0x80
object 0: int : -128
object 0: uint: 128
object 0: text: .
object 1: name: 'stdin-stat'
object 1: size: 144
object 1: data:
b'&\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\xff\xff\xff\xff\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x00\x10\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xdb`\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x12\x00\xdc`\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\x12\x00\xdc`\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
object 1: hex :
0x260000000000000001000000ffffffff0100000000000000a4810000e8030000e8030000ffffffff0000000000000000ffffffffffffffff0010000000000000ffffffffffffffffffffdb6000000000ffffffffffffffff1200dc6000000000ffffffffffffffff1200dc6000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
object 1: text:
&..........................................................................`...............`...............`....................................
object 2: name: 'model_version'
object 2: size: 4
object 2: data: b'\x01\x00\x00\x00'
object 2: hex : 0x01000000
object 2: int : 1
object 2: uint: 1
object 2: text: ....

Thanks & Kind regards !
Pansilu

On Sun, Jun 27, 2021 at 6:48 PM Frank Busse <f.busse at imperial.ac.uk> wrote:

> Hi,
>
>
> On Wed, 23 Jun 2021 23:30:29 +0800
> Pansilu Pitigalaarachchi <pansilu.pitigalaarachchi at gmail.com> wrote:
>
> > *.ktest files*
> > I was able to use KLEE generated .ktest files in seed mode. My current
> > requirement is to dictate a portion of a parth in the form of a seed.
> > Therefore, I would like to craft .ktest files to be used as a seed.
> > Can I please know if there is any documentation or info on the
> > content/format & attributes of a .ktest file that I can follow in my
> > attempt to craft .ktest files of my choice.
>
> The ktest format is quite simple:
>
>
> https://github.com/klee/klee/blob/df04aeadefb4e1c34c7ef8b9123947ff045a34d9/include/klee/ADT/KTest.h#L24
>
>
> https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/lib/Basic/KTest.cpp#L94
>
> Or if you prefer Python:
>
>
> https://github.com/klee/klee/blob/df04aeadefb4e1c34c7ef8b9123947ff045a34d9/tools/ktest-tool/ktest-tool#L30
>
> But maybe https://klee.github.io/docs/tools/#gen-bout (gen-bout) solves
> your problem already.
>
>
> Kind regards,
>
> Frank
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>

-- 

Pansilu Pitigalaarachchi
-------------- next part --------------
HTML attachment scrubbed and removed