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

[Cristian Cadar]

Hi,

You should also take a look at --only-output-states-covering-new, which 
only outputs a .ktest file if it increases coverage.

Best,
Cristian

On 08/07/2024 02:30, Yuzhou Fang wrote:
>  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 
> <mailto: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 <mailto:klee-dev at imperial.ac.uk>
>     https://urldefense.com/v3/__https://mailman.ic.ac.uk/mailman/listinfo/klee-dev__;!!LIr3w8kk_Xxm!t8Kx0voiCW0XNJ_FW8UwXh3WmlV3gFRsXixKoptIiIISYyG2ECBI0szqQQY0qZ5uODvbgyKf7GcoL4heD7oyRPw$ <https://urldefense.com/v3/__https://mailman.ic.ac.uk/mailman/listinfo/klee-dev__;!!LIr3w8kk_Xxm!t8Kx0voiCW0XNJ_FW8UwXh3WmlV3gFRsXixKoptIiIISYyG2ECBI0szqQQY0qZ5uODvbgyKf7GcoL4heD7oyRPw$>
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev