[klee-dev] How to solve path explosion caused by loop?

[Oleg Sokolsky]

The number of paths explored by KLEE is exponential in the number of 
iterations: a path discovered in the first iteration is extended by 
every path discovered in the second iteration, and so on.

It seems that you introduce the loop only to explore all possible values 
of event.  If so, just make it symbolic and add constraint using 
klee_assume that event is between 0 and 42.  KLEE will explore it all in 
one run.

Oleg

On 4/2/24 01:33, Wang, Weixuan wrote:
>
> Hi all
>
> I met a problem which loop cause path explosion.
>
> For example, there are 3 variables, control_block, p_data and event. 
> Control_block and p_data are structures and have some fields as 
> symbolic. Event is an integer between 0 to 42.
>
> Now I want to run smp_sm_event(control_block, p_data, event) for each 
> event. When manually set event from 0 to 42 (which means, runs klee 
> for 42 times), klee can get result quickly with each case finishing in 
> controllable instruction number.
>
> However, when I try to run the following:
>
>        for (int event=0; event<=42; event++) {
>
> smp_sm_event(control_block, p_data, event)
>
>        }
>
> Then klee’s running seems never ends. When manually halt klee, it 
> finishes with more than 10 million instructions.
>
> May I get some advice on why this happen, and is there way to solve 
> this problem so that I don’t need to manually run klee for many times? 
> Thank you!
>
> --------------------
>
> Best regards,
>
> Weixuan
>
> Master student in Computer Science, Penn State University
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://urldefense.com/v3/__https://mailman.ic.ac.uk/mailman/listinfo/klee-dev__;!!IBzWLUs!ULO9Hl20ug8BW2AKvi84--l4PLbb7NQ_3pyq-AkTN0OfwCPsFniuFW3b2jS8lA56Q90H8TjQz3pMjWg5VmPZ$  
-------------- next part --------------
HTML attachment scrubbed and removed