[klee-dev] KLEE --allow-seed-extension

[HONG Jiaqi]

I was trying to figure out the strength the klee’s -allow-seed-extension. If a symbolic object buf[2] has two bytes, but the .ktest file used only specify the concrete value for the first byte buf[0], would klee treat the second byte buf[1] as a free symbol with the -allow-seed-extension?


I run the following experiment to verify. It seems KLEE set a default value \x00 for buf[1] instead of treat it as a free symbol and explore all the possible paths determined by it.


In the following experiment, the seed file in use specifies buf[0] = 0x80 (represents a negative value), which follows the true branch of line 4.


line 16 only executes once which means only one path execute to the end. (Even though KLEE reports 4 completed paths, but i think three of them are partially explored, only one path executes to the end.) Line 16 dumps a = 0, so, only the branch line 7 & 8 executes to the end. I was expecting KLEE also fully explores the path line 5 & 6 and invoke line 16, but the experiment results violate with my thought.


I want to make clear does klee treat buf[1] as a free symbol or not, if yes, why the branch specified by line 5 & 6 does not execute to the end; if no, does KLEE set a default value \x00 to buf[1]? I check the entire handler of klee_make_symbolic() in klee source code, still do not understand where the magic is. Would be very appreciate if anyone can help :)



*******The test program seed-test-1.c ********

        int main() {



1.            int8_t buf[2];

2.            klee_make_symbolic(buf, 2, “buf”);

3.            int a;

4.            if (buf[0] < 5) {

5.                            if (buf[1] == 5)

6.                                            a = 5;

7.                            else if (buf[1] == 0)

8.                                            a = 0;

9.            }

10.          else

11.                          a = -1;

12.          if (buf[1] == -15)

13.                          a = 22;

14.          else if (buf[1] == -10)

15.                          a = 32;

16.          printf ("a = %d. \n", a);

17.          return 0;

         }



*******The .ktest file used in seed mode ********

ktest file : 'klee-out-70/test000001.ktest'
args       : ['seed-test-1.bc']
num objects: 2
object 0: name: 'model_version'
object 0: size: 4
object 0: data: b'\x01\x00\x00\x00'
object 0: hex : 0x01000000
object 0: int : 1
object 0: uint: 1
object 0: text: ....
object 1: name: 'buf'
object 1: size: 1
object 1: data: b'\x80'
object 1: hex : 0x80
object 1: int : -128
object 1: uint: 128
object 1: text: .

*********The command line in use***********
~/Documents/klee/build/bin/klee --seed-file=klee-out-70/test000001.ktest --only-seed --allow-seed-extension -posix-runtime seed-test-1.bc


***********klee results******************
KLEE: seeding done (3 states remain)
KLEE: halting execution, dumping remaining states

KLEE: done: total instructions = 1315
KLEE: done: completed paths = 4
KLEE: done: generated tests = 4


********** resulted .ktest files**************
ktest file : 'klee-last/test000001.ktest'
args       : ['seed-test-1.bc']
num objects: 2
object 0: name: 'model_version'
object 0: size: 4
object 0: data: b'\x01\x00\x00\x00'
object 0: hex : 0x01000000
object 0: int : 1
object 0: uint: 1
object 0: text: ....
object 1: name: 'buf'
object 1: size: 2
object 1: data: b'\x00\x00'
object 1: hex : 0x0000
object 1: int : 0
object 1: uint: 0
object 1: text: ..

ktest file : 'klee-last/test000002.ktest'
args       : ['seed-test-1.bc']
num objects: 2
object 0: name: 'model_version'
object 0: size: 4
object 0: data: b'\x01\x00\x00\x00'
object 0: hex : 0x01000000
object 0: int : 1
object 0: uint: 1
object 0: text: ....
object 1: name: 'buf'
object 1: size: 2
object 1: data: b'\x00\x06'
object 1: hex : 0x0006
object 1: int : 1536
object 1: uint: 1536
object 1: text: ..

ktest file : 'klee-last/test000003.ktest'
args       : ['seed-test-1.bc']
num objects: 2
object 0: name: 'model_version'
object 0: size: 4
object 0: data: b'\x01\x00\x00\x00'
object 0: hex : 0x01000000
object 0: int : 1
object 0: uint: 1
object 0: text: ....
object 1: name: 'buf'
object 1: size: 2
object 1: data: b'\x05\xff'
object 1: hex : 0x05ff
object 1: int : -251
object 1: uint: 65285
object 1: text: ..

ktest file : 'klee-last/test000004.ktest'
args       : ['seed-test-1.bc']
num objects: 2
object 0: name: 'model_version'
object 0: size: 4
object 0: data: b'\x01\x00\x00\x00'
object 0: hex : 0x01000000
object 0: int : 1
object 0: uint: 1
object 0: text: ....
object 1: name: 'buf'
object 1: size: 2
object 1: data: b'\x00\x01'
object 1: hex : 0x0001
object 1: int : 256
object 1: uint: 256
object 1: text: ..

Thanks and regards,
Jiaqi






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