SE-ESOC tool (FSE'18)

The purpose of this demo is to reproduce the find.091557f6 example from Section 5 of the paper using a demo version of SE-ESOC. Note that some of the results may differ from the results in the paper, because behaviour of find depends on the filesystem, and the filesystems in the given Docker container has slightly different file system structure/configuration from our experimental environment.

The demo version of SE-ESOC is distributed in the following docker container: https://hub.docker.com/r/mechtaev/fse18-demo/.

In order to download and install SE-ESOC, you could create a temporary container using the following command (the container will be automatically removed on exit):

sudo docker run --rm -ti mechtaev/fse18­demo /bin/bash

In order to inject a symbolic variables, the buggy statement is replaced with a call of the function klee_apply_symbolic in the file find/ftsfind.c:

 /* Not an error, cope with the usual cases. */ 
  if (klee_apply_symbolic(3, (int[]){ent­>fts_info, ent­>fts_errno, prev_depth})) 
    { 
      assert(!state.have_stat); 
      assert(!state.have_type);

Then, first-order symbolic execution can be executed using the following command:

/tools/run­fo

Which should produce the following output:

...
KLEE: done: total instructions = 26798398 
KLEE: done: completed paths = 642 
KLEE: done: generated tests = 513

Second-order symbolic execution can be executed using the following command:

/tools/run­so

Which should produce the following output:

...
KLEE: done: total instructions = 1716822 
KLEE: done: completed paths = 10 
KLEE: done: generated tests = 9

As can be seen, second-order symbolic execution significantly reduced the number of explored paths. In order to view function interpretations synthesized along explored paths, the following command can be used e.g. for path with the index 6:

/tools/encoder pse 10 3 /tmp/encoding.smt2 findutils/objllvm/find/klee­last/test000006.smt2

Which will produce the following interpretation:

((angelix!arg!1 == angelix!arg!2) || (9 < angelix!arg!0))