[klee-dev] Applying CexPreferences during Dump States

[Sean Bartell]

Hello,

eric.rizzi at huskers.unl.edu 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
>klee-dev at imperial.ac.uk
>https://mailman.ic.ac.uk/mailman/listinfo/klee-dev