[klee-dev] Question about how Klee performs symbolic execution

[Rutledge, Richard L]

Thanks Christian, 

I did search the mail list archive before posting (I promise!). Of course, now I find plenty of references…

Thanks for not offering to google that for me :)

Rick



> On 10 Nov 2016, at 14:05, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> 
> Hi, this question was asked on the mailing list before, but might not be easy to find.  In a nutshell, when KLEE encounters a symbolic memory access, it forks one path for each object which can be referenced there.
> 
> Cristian
> 
> On 10/11/2016 01:10, Rutledge, Richard L wrote:
>> I hope someone can clarify up a little klee-fundlement on my part regarding how Klee performs symbolic execution. Consider the following example program:
>> 
>> --------------------------------------------------------
>> #include <klee/klee.h>
>> 
>> #define MAXSTR 10
>> 
>> int test(char *str, int offset) {
>> 
>>  if (str[offset] == '\n') {
>>    return 1;
>>  }
>>  return 0;
>> }
>> 
>> int main(int argc, char *argv[]) {
>> 
>>  char str[MAXSTR];
>>  int offset;
>> 
>>  klee_make_symbolic(str, MAXSTR, "str");
>>  offset = klee_int("offset");
>>  klee_assume(offset >= 0);
>>  klee_assume(offset < MAXSTR);
>> 
>>  int result = test(str, offset);
>> 
>>  return result;
>> }
>> --------------------------------------------------------
>> 
>> There are two paths through this program. As expected, Klee finds exactly two paths and generates two test cases.
>> 
>> However, if I delete to two klee_assume() statements, then Klee finds 186 paths/test cases.
>> 
>> What leads to the path explosion? Without the assumes, the program admits undefined behavior, but does not introduce any new paths. It still only has two and execution should fork into two states at the test() if statement. What condition forks the other 184 states?
>> 
>> Cheers and Thanks!
>> Rick Rutledge
>> 
>> 
>> 
>> 
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev