[klee-dev] How to Reduce the Number of .ktest Files Generated by KLEE

[Yuzhou Fang]

>From my understanding, Klee has no idea about how long the current
execution path will be, only when the current ExecutionState is terminated.
Thus, I don't think it would be a good idea to prioritize ExecutionStates
by path length. The most intuitive approach to limit the test case number
is to add a threshold to invoke the `KleeHandler::processTestCase` method.
Every time the function is called, increase the counter and stop generating
test cases when reaching the limit. Other heuristics can also be built atop
this idea. Correct me if I am wrong.

Yuzhou


On Sun, Jul 7, 2024 at 4:25 PM Sun <shutong255 at gmail.com> wrote:

> Dear KLEE Community,
> I am currently working on a project using KLEE, and I have encountered an
> issue with the number of .ktest files generated during the execution.
> Specifically, my project generates a large number of .ktest files, which
> is not efficient for my needs. I am looking for a way to limit the number
> of .ktest files generated to only the top 10 longest paths based on the
> number of instructions executed.
> Here is what I have attempted so far:
>
>    1. I modified the Executor.cpp file to track the number of
>    instructions executed for each path.
>    2. I attempted to implement a priority queue to keep track of the top
>    10 longest paths.
>    3. I tried to modify the shouldWriteTest function to only write .ktest files
>    for the longest paths.
>
> However, my current implementation results in a segmentation fault, and I
> am not sure if my approach is correct.
> Could you please provide guidance on the following:
>
>    1. Is there an existing way to limit the number of .ktest files
>    generated by KLEE?
>    2. If not, what would be the best approach to modify the KLEE source
>    code to achieve this?
>    3. Any specific functions or parts of the codebase that I should focus
>    on to implement this feature?
>
> Thank you for your time, best regards,
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
>
> https://urldefense.com/v3/__https://mailman.ic.ac.uk/mailman/listinfo/klee-dev__;!!LIr3w8kk_Xxm!t8Kx0voiCW0XNJ_FW8UwXh3WmlV3gFRsXixKoptIiIISYyG2ECBI0szqQQY0qZ5uODvbgyKf7GcoL4heD7oyRPw$
>
-------------- next part --------------
HTML attachment scrubbed and removed