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

[Frank Busse]

Hi,


I haven't looked much at the seeding code so take my answer with a
grain of salt.


On Mon, 5 Jul 2021 03:40:52 +0000
HONG Jiaqi <jqhong at smu.edu.sg> wrote:

> 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.

No, it seems KLEE divides seeds among branches:
https://github.com/klee/klee/blob/df04aeadefb4e1c34c7ef8b9123947ff045a34d9/lib/Core/Executor.cpp#L1168

However, which one it picks seems a little fragile: when you disable the
CEX cache (--use-cex-cache=false) for instance, it takes a different
one.

> but i think three of them are partially explored

It stops because of --only-seed - the seeMap is empty when that single
path finishes and it starts dumping (terminating) the remaining states:

https://github.com/klee/klee/blob/df04aeadefb4e1c34c7ef8b9123947ff045a34d9/lib/Core/Executor.cpp#L3520


Kind regards,

Frank