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
void DFSSearcher::update(ExecutionState *current,
const std::vector ,
const std::vector ) {
// loop through the removed states to delete them from the searcher
for (std::vector::const_iterator it = removedStates.begin(),
ie = removedStates.end(); it != ie; ++it)
{
ExecutionState *es = *it;
if (es == states.back())
{
states.pop_back();
}
else
{
bool ok = false;
for (std::vector::iterator it = states.begin(), ie =
states.end(); it != ie; ++it)
{
if (es==*it)
{
states.erase(it);
ok = true;
break;
}
}
assert(ok && "invalid state removed");
}
}
// insert new states
// this part is different as we want to for each state to query the SAT
solver for satisfiability
// of AND
for(std::vector::const_iterator it = addedStates.begin(),
end = addedStates.end(); it != end; ++it)
{
ExecutionState* currentState = *it;
// currentState is state we will be processing now
ExecutionState temporaryState = ExecutionState(*currentState); // create a
copy
// The above line might not be necessary, it was introduced at first for
safety (to not modify the original data)
// build the extra constraint expression
//
int width = 32;
ArrayCache ac;
const Array* array_X = ac.CreateArray("x", width);
ref tempRead_X = Expr::createTempRead(array_X, width); //symbolic
read from the array
ref e = EqExpr::create(tempRead_X, klee::ConstantExpr::alloc(100,
width));
e.get()->dump();
//
// solver is a TimingSolver object, member of the Executor
// use the mayBeTrue function
bool result = false;
bool success = executor.solver->mayBeTrue(temporaryState, e, result);
// after that, if result == false , it means that
// the constraint we added is not satisfiable in the current state.
// in that case we should delete the state and proceed to the next one.
if(result==true)
{
states.push_back(currentState);
printf("Pushing some state\n");
printf("success = %d\n", success);
printf("result = %d\n", result);
// here we have added a state, we could `break;`
// to avoid adding more than one states
//break;
}
}
///END OF NEW CODE
}___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
