[klee-dev] Inquiry on path record and reply component of KLEE

[Wei Chen]

Dear developers,

Hi, I found there is a case that KLEE would generate the same .path files
for different paths in programs. Further, when given different path files,
the replay feature of Klee produces the same input for these two paths.
Here are the details:

For the attached file test_1.c, the aforementioned problem can be
reproduced by executing the following commands:

[image: Attachment-1.png]

KLEE would generate 3 paths for this program, then unfortunately
klee-out-0/test000002.path and klee-out-0/test000003.path are exactly the
same as each other. That’s weird because they are regarded as different
paths by klee.

For the replay feature of klee, given klee-out-0/test000001.path and
klee-out-0/test000002.path (two different paths), by executing klee with
—-replay-path option, two paths will be replayed and two test cases will be
generated.

However, the two test cases klee-out-1/test000001.ktest and
klee-out-2/test000001.ktest are exactly the same with each other.

[image: Attachment.png]

The attachment test_2.c also has the same .path problem, but the reply
feature works fine.

In that case, I’m wondering if there are some bugs inside the path-related
component of klee. The version of klee that I used is shown as below:

[image: image.png]

Looking forward to your kind reply.

Best,
Harper
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Attachment-1.png
Type: image/png
Size: 305965 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210710/58d96408/attachment.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Attachment.png
Type: image/png
Size: 147739 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210710/58d96408/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 41883 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210710/58d96408/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_1.c
Type: application/octet-stream
Size: 1063 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210710/58d96408/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_2.c
Type: application/octet-stream
Size: 589 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210710/58d96408/attachment-0001.obj>