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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
