[klee-dev] Modifying the DFS searcher.

[Papapanagiotakis-Bousy, Iason]

Hi everyone and happy new year,

I am working on my a searcher that will "force" KLEE to follow a path defined by a constraint.
So far I've been overwriting the DFS searcher but I am having some issues, here is what I've done:

I am only modifying the update function of the class.
Update()

  1.  Copy-paste the part of the code that loops thought the removed states to delete them from the searcher
  2.  Insert new states (this is where it is different)
     *   Create a copy of the current state
     *   Create the expression of the constraint I want KLEE to follow (i.e. x = 100)
     *   Call executor.solver->mayBeTrue(tempState, constraint, result) to see whether the constraint is satisfiable in the state.
     *   If yes, save that state.

I then run this on a simple main.c
if x == 100 then
print this
else
print that

My problem is that mayBeTrue with the arguments I pass always gives result=1 and so both states are added/explored (while I would like only one of them to be added).

To verify that I have created the correct constraint, I call e.get()->dump() that prints : (Eq 100     (ReadLSB w32 0 x))
While the two .kquery files generated are:

  1.  (Eq false             (Eq 100               (ReadLSB w32 0 x)))
  2.  (Eq 100             (ReadLSB w32 0 x))

So why are both queries resulting in true?
How is the solver determining satisfiability? What "links" my expression with the states I am exploring is only syntax of the constraint as I am using the exact same name for the variable, is sufficient for the solver to "match" x from the expression with x from the state? If not, do you have any ideas on how could I make this work?

I've attached a file containing the code of the update function.

In order to have access to the solver in the Searcher I had to modify some code, these changes might not be within the best practices but I figured it was the fastest way to prototype. I can share the full list of changes if necessary.

Thank you in advance for any hints that might help, I am looking forward to your comments.

Best regards,
Jason

-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: update.cpp
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20170105/7649e24e/attachment.ksh>