Hello,
[email protected] on 2015-02-13:
I have a question about how Klee goes about creating test cases at the end of
its run. It seems that it goes through the cexPreferences that are associated
with each MemoryObject, adding on as many as it possibly can. (as seen in
lib/Core/Executor.cpp::getSymbolicSolution())
In many cases, however, it seems that not all of these additional constraints
can be added to the state. I assume this because when I just stick on all of
the cexPreferences to the state and call getInitialValues(), I get a lot of
errors in the test suite.
A Klee state can correspond to many different possible test cases. For example,
in this program:
int main(int argc, char **argv) {
return argv[1][0] ? 1 : 0;
}
Klee will have two states, one of which corresponds to the condition
"argv[1][0] != 0". When Klee generates a test case for that state, there are
255 possible values for argv[1][0].
Without cexPreferences, Klee would just tell the solver to solve
"argv[1][0] != 0" and it might return "argv[1][0] = '\x01'". That could be hard
to read, though, especially with a longer string. Klee uses cexPreferences to
prefer "nicer" test cases when possible, so you get "argv[1][0] = 'A'" instead
of "argv[1][0] = '\x01'".
My Questions are:
1) Where do the constraints in cexPrefences come from when Klee simulates
running a command line program? Are there different types of constraints on
command line arguments and input files?
They are added by the klee_prefer_cex intrinsic, which you can call just like
you call klee_make_symbolic. If you use the POSIX runtime, it already calls
klee_prefer_cex in a few places to prefer printable characters in argv and so
on.
2) What does not fully applying all of the constraints in cexPreferences mean
about the testcase that is created? Is it not fully representative of the path
that was actually taken through the program or is their a possibility of two
tests traversing equivalent paths?
Klee should always generate one representative test case per path.
CexPreferences are only used to try to generate "nice" test cases, like an
argument of "AA" instead of "\x01\x01". If they fail, it means only an "ugly"
test case will follow the right path, so that's what Klee will produce.
3) What does it mean about a state when a constraint in cexPreferences can't be
applied? (i.e. solver->mustBeTrue(tmp, Expr::createIsZero(*pi), mustBeTrue ==
false);
As above.
3) Are paths leading to states where all the constraints in cexPreferences
aren't possible traversing impossible paths?
No.
4) Why are the constraints stored in the cexPreferences not simply added in the
beginning of the run so that unused information isn't calculated?
Because that would rule out paths that require "ugly" inputs. For instance, if
your program crashes only when you give it an argument of "\x01", forcing the
cexPreferences to hold would prevent you from ever seeing the crash. That's why
Klee allows the preferences to fail.
Sorry for the multitude of questions and thanks,
Eric Rizzi
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
