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@imperial.ac.uk
https://urldefense.com/v3/__https://mailman.ic.ac.uk/mailman/listinfo/klee-dev__;!!IBzWLUs!ULO9Hl20ug8BW2AKvi84--l4PLbb7NQ_3pyq-AkTN0OfwCPsFniuFW3b2jS8lA56Q90H8TjQz3pMjWg5VmPZ$
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
