[klee-dev] [Question] What is the correct/efficient way to implement a separate execution without affecting the normal execution in KLEE?

[TU Haoxin]

Dear KLEE developers,

May I ask a question about implementing a separate execution in KLEE? My initial idea is to separate ("simulate") running a state and evaluate whether this state is worthy of exploring in the future further.

I will use the attached figure to explain what I want to do (please take a quick look before you read the following).  Assuming normal KLEE execution forked once, there will be two states "B" and "C" which can be selected using different search strategies to explore. In the first normal execution, I don't know which state is good to explore so I randomly select one (say "C" is selected). Then, I want to use a "simulation" run (a separate execution from a normal execution ) to evaluate the "value/reward" of this state based on the results of the simulation run. After the simulation execution terminates, KLEE will switch to normal execution. The simulation run should not affect the normal run, meaning the switching between normal and simulation runs should have no side effects on each other. Note the simulation run can be just a single path running for the performance consideration.

Currently, I have two alternatives to implement this feature, but I am not sure whether it can work or not


  1.
Deep copy of Executor object, so that the normal/simulation runs will be using different executors for their own. The only thing that needs to be considered is to switch different Executors. However, based on my understanding, the deep copy of an Executor is not supported in the current versions of KLEE so far. Am I correct? I doubt that adding such a deep-copy implementation can be difficult.

  2.
Run under the same Executor but need to restore the required data/objects to switch the runs. I tried this option, but it seems that there are a lot of objects in Executor/ExecutionState that need to be carefully handled. I'd like to know whether I used the correct way to implement this feature.

In summary, do you think the above two solutions make sense or do you have any other alternative suggestions to do this?  Are there any KLEE variants already supporting such a feature? Please kindly advise and I appreciate it very much for your helpful comments and suggestions!


Best regards,
Haoxin
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: runs.png
Type: image/png
Size: 60512 bytes
Desc: runs.png
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20240326/ad5919e0/attachment.png>