State Merging with Quantifiers

This is an extension of KLEE which enables to perform state mering using quantified constraints. It is based on the paper: State Merging with Quantifiers in Symbolic Execution, which is available here.

Usage

Manual State Merging

Consider the following example:

#include <stdlib.h>
#include <string.h>
#include <klee/klee.h>

int main(int argc, char *argv[]) {
  size_t length;
  klee_make_symbolic(&length, sizeof(length), "length");
  klee_assume(length >= 1);
  klee_assume(length <= 4);

  char *str = malloc(length);
  klee_make_symbolic(str, length, "str");
  str[length - 1] = 0;

  klee_open_qmerge();
  char *p = strchr(str, 'a');
  klee_close_qmerge();
  if (p) {
    klee_print_expr("p", p);
  }

  return 0;
}

To compile it, run the following command:

clang -g -c -emit-llvm -I <klee_src>/include <source_file> -o <bitcode_file>

Then, run the following command:

klee \
    -libc=uclibc \
    -solver-backend=z3 \
    -search=dfs \
    -allocate-sym-size=1 \
    -capacity=10 \
    -split-by-pattern=1 \
    -use-quantifiers=1 \
    -optimize-using-exec-tree=1 \
    -use-small-model-solver=1 \
    -write-kqueries \
    <bitcode_file>

This will result in two merged symbolic states. The corresponding quantified path constraints are located in the output directory generated by KLEE:

<klee_out>/test000006.kquery
<klee_out>/test000007.kquery

Automatic State Merging

In the previous example, state merging is applied manually. Our implementation supports automatic application of state merging in size-dependent loops. Consider the following example:

#include <stdlib.h>
#include <string.h>
#include <klee/klee.h>

int main(int argc, char *argv[]) {
  size_t length;
  klee_make_symbolic(&length, sizeof(length), "length");
  klee_assume(length >= 1);
  klee_assume(length <= 4);

  char *str = malloc(length);
  klee_make_symbolic(str, length, "str");
  str[length - 1] = 0;

  char *p = strchr(str, 'a');
  if (p) {
    klee_print_expr("p", p);
  }

  return 0;
}

To compile it, run the following command:

clang -g -c -emit-llvm -I <klee_src>/include <source_file> -o <bitcode_file>

Then, run the following command:

klee \
    -libc=uclibc \
    -solver-backend=z3 \
    -search=dfs \
    -allocate-sym-size=1 \
    -capacity=10 \
    -use-loop-merge=1 \
    -split-by-pattern=1 \
    -use-quantifiers=1 \
    -optimize-using-exec-tree=1 \
    -use-small-model-solver=1 \
    -write-kqueries \
    <bitcode_file>

Here, state merging will be applied in the strchr loop. As in the previous example, this will result in two merged symbolic states.

Incremental State Merging

Consider the following example:

#include <stdlib.h>
#include <string.h>
#include <klee/klee.h>

int main(int argc, char *argv[]) {
  size_t length;
  klee_make_symbolic(&length, sizeof(length), "length");
  klee_assume(length >= 1);
  klee_assume(length <= 4);

  char *str = malloc(length);
  klee_make_symbolic(str, length, "str");
  str[length - 1] = 0;

  size_t k = strspn(str, "ab");
  klee_print_expr("k", k);

  return 0;
}

When we analyze this program with the previous command, state merging is applied in the strspn loop. In this case, we merge 15 symbolic states, since in every iteration we can choose between the characters 'a' and 'b'. To reduce the number of symbolic states resulting from that loop, you can use incremental state merging as follows:

klee \
    -libc=uclibc \
    -solver-backend=z3 \
    -search=dfs \
    -allocate-sym-size=1 \
    -capacity=10 \
    -use-loop-merge=1 \
    -split-by-pattern=1 \
    -use-quantifiers=1 \
    -optimize-using-exec-tree=1 \
    -use-incremental-merging-search=1 \
    -use-small-model-solver=1 \
    -write-kqueries \
    <bitcode_file>

This way, we merge only 4 symbolic states.