[klee-dev] STP-Make copy of solver object

[Saksham Jain]

Hi,

This question is not strictly wrt to KLEE. I am trying to make my own
symbolic executioner in python. I am using STP for this. The issue I am
facing is wrt to making an independent copy of STP solver. During symbolic
execution, whenever my program encounter a branch, I try to make a
duplicate copy of the Solver for the current path (To copy all the symbolic
variables and constraints encountered in present path until now for future
multiple paths). But I am not able to make independent copy of the Solver.

Can someone tell me how is this achieved in KLEE? Does klee instead of
copying the constraint solver, makes a new solver for each new path and add
all the constraints witnessed till now into this new solver?


I am hoping that someone could guide me here.( I couldn't find the mailing
list of STP.If someone knows please let me know)
Example:

>>> import stp
>>> import copy
>>>
>>> s=stp.Solver()
>>> a=s.bitvec('a',32)
>>> s.add(a==1)
>>> s.check()
True
>>> s2=copy.deepcopy(s)
>>> s2.check()
True
>>> s.add(a==2)
>>> s.check()
False
>>> s2.check()
False

Though I have made a copy (using deepcopy) of Solver 's', but even after
that when 's' fails (s.check gives False), 's2' also fails.So both 's' and
's2' are not independent.

I suspect this is because of recursive nature of solver object and hence
deepcopy doesn't work properly.

Can someone tell me how to achieve this? What does KLEE do wrt to Symbolic
Executioner whenever it witness a branch instruction?

Thanks in advance.

Regards,
Saksham Jain
-------------- next part --------------
HTML attachment scrubbed and removed