[klee-dev] Reducing the Number of .ktest Files Generated for Longest Execution Paths

[Frank Busse]

Hi,


On Tue, 11 Jun 2024 11:41:34 +0000
Sun <shutong255 at gmail.com> wrote:

> When running Klee on various programs, I notice that it generates a
> `.ktest` file for each explored execution path. For my current
> project's scope, this behavior results in excessive data, most of
> which is not relevant to my needs. Specifically, I am interested in
> only retaining the `.ktest` files for the ten longest execution
> paths, which are most relevant to my analysis.

typically one would use, e.g.:

--only-output-states-covering-new

to reduce the number of generated ktest files.

> Could you please advise:
> 1. Is there an existing command-line option or configuration setting
> in Klee that allows for limiting the generation of `.ktest` files to
> only the longest paths?
> 2. If no such setting exists, could you point
> me towards the parts of Klee's source code where modifications might
> be implemented to achieve this functionality?

How would you now the lengths of the longest paths in advance?

You could modify shouldWriteTest in the Executor:
https://github.com/klee/klee/blob/ad557cb0f8e20a0e4a86ea5fcd11ed95f5c3b637/lib/Core/Executor.cpp#L3788

The depth is in the ExecutionState:
https://github.com/klee/klee/blob/ad557cb0f8e20a0e4a86ea5fcd11ed95f5c3b637/lib/Core/ExecutionState.h#L180


Kind regards,

Frank