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

[Rutledge, Richard L]

Thanks for following up!

I did look at the generated test data. Only two distinct values were generated for str, one all zeros and one containing a newline. This was as expected. The unexpected part was in generation of values for offset. There were 185 distinct offset values.

I did not use ‘-only-output-states-covering-new’ since the help describes as ‘Only output test cases covering new code’. That leads me to believe that the option targets statement coverage, which is insufficient in my use case.

I realize that the additional test cases are redundant. The question is: why is Klee forking new states? In my limited understanding, I thought that symbolic execution only forked new states at branches. If so, then Klee would only fork once and produce two test cases as it does with the assume statements. Hence some other condition other than a branch is causing Klee to fork state. I would like to know what that condition is.

Even with the ‘-only-output-states-covering-new’ option, I still get 5 test cases. So, the question still holds.

Thanks!
Rick


On 10 Nov 2016, at 08:11, Shehbaz Jaffer <shehbaz.jaffer at mail.utoronto.ca<mailto:shehbaz.jaffer at mail.utoronto.ca>> wrote:

Hi Rick,

Although I am new to Klee and as such dont know the internals of Klee, I'd like to answer the questions to the best of my ability.
186 cases being generated in case 2 is because there are a lot of redundant testcases.

If you inspect each of your testcases using ktest-tool as below:


ktest-tool klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args       : ['sample_str.o']
num objects: 2
object    0: name: b'str'
object    0: size: 10
object    0: data: b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object    1: name: b'offset'
object    1: size: 4
object    1: data: b'\n\x00\x00\x00'


you will find the values given to "str" and "offset" values for each testcase. To remove redundancy, please try the following command:

klee --only-output-states-covering-new program_name.bc

this will create 4 testcases, for different values of output, even when you dont put klee_assume() intrinsic function.
Again, you can check the four testcase values by using ktest-tool as shown above.

Hope this helps.

Shehbaz

________________________________
From: klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk> <klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk>> on behalf of Rutledge, Richard L <rrutledge at gatech.edu<mailto:rrutledge at gatech.edu>>
Sent: Wednesday, November 9, 2016 8:10:04 PM
To: klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
Subject: [klee-dev] Question about how Klee performs symbolic execution

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<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed