Fuse

Our artifact is available on dockerhub platform. Please follow the following steps to install the docker image of Fuse, analyze the motivation program, and reproduce the results in our paper.

Install docker-engine

We suppose that the host OS is Linux or Mac OS X on which docker can be installed. We suppose that you have installed the docker environment; otherwise, please go to this link for help.

Download Fuse's docker image and load it

Download docker image:

$ sudo docker pull fuseengine/fuse-engine:v3

If the image is pulled successfully, you can use the following command to have a check. You should find that an image named fuseengine/fuse-engine exists.

$ sudo docker images
REPOSITORY              TAG       IMAGE ID       CREATED          SIZE
fuseengine/fuse-engine  v3        a0be2fab59d2   2 hours ago      3.08GB

Start to run the container in interactive mode.

$ sudo docker run -it fuseengine/fuse-engine:v3 bash

Some Tips for better use of Docker:

when inside the Fuse container,

(1) to exit the Fuse docker container and terminate all running jobs inside the container, use:

 $ exit

(2) to turn interactive mode into daemon mode (detach from the running Fuse container without stopping it),

press CTRL+P followed by CTRL+Q

(3) when outside the Fuse container and looking to attach to it, use:

$ sudo docker attach <container_id>

Experimental environment

The following items can be found in the directory:

• Z3-4.6.2,llvm-6,zlib-1.2.11,klee-ublibc,json-c,gsl_runtime_lib are the infrastructures of our work

• gsl is GSL-2.7 math library source code for expriments, but we use gsl_bench dictionary as the expriment dictionary.

• coreutils-6.11 is coreUtils library source code for expriments, but we use coreutils-exp dictionary as the expriment dictionary.

• klee-2.3-float is original KLEE with float-point support.

• smse is our tools.

• motiexample is a simple motivation example program.

Run Motivation Example

Navigate to /home/aaa/motiexample and list the contents.

$ cd /home/aaa/motiexample

We have prepared two shell scripts (run_smse.sh, run_klee.sh) to run different configurations. And we can use clean.sh to clean all outputs generated by the tools.

The source code of our example (complex_function.c) is as follows.

#include <klee/klee.h>

int main() {
  double a,b;
  klee_make_symbolic(&a, sizeof(a), "a");
  klee_make_symbolic(&b, sizeof(b), "b");

  double sinx,z;
  sinx = sin(a);
  if(b == 3.0){
    z = 100 * sinx;
    if (z > 99.9)
      printf("This is bug\n");
  }else{
    z = 10 * sinx;
  }
  return 0;
}

Before analyzing, we need to configure the running options:

$ vi run_smse.c

SMSE_PATH="/home/aaa/smse"
SMSE_EXE_PATH=${SMSE_PATH}"/build/bin/klee"
SEARCH="bfs" # ["bfs","dfs"]
SOLVER_TYPE="jfs-smt" #["smt","jfs","jfs-smt","smt-part"]
......

There are two search modes

• bfs: BFS search heuristic.
• dfs: DFS search heuristic.

and four solving modes

• smt: only use SMT solver to solve path condition.
• jfs: only use JFS (fuzzing solver) to solve path condtion.
• jfs-smt: this is the algorithm which we purposed in our paper. Combining SMT and JFS to solve path constraints.
• smt-part: this is the related work for MCS algorithm.

Suppose we run script with the bfs + jfs-smt configuration

$ (exit vim)
$ ./run_smse.sh

Less than a second, we can see the output at the terminal. The bug is reached successfully.

...... # in a second

[dbg] enter CF : sin  stack size : 4
[dbg] ret from CF : sin
KLEE: WARNING ONCE: calling external: printf(94013300729200) at [no debug info]
This is bug

KLEE: done: total instructions = 13534
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3

If you want to analyze this program using KLEE with floating point support, run run_klee.sh (we can also modify the configuration in this shell, but can only change search heuristic). KLEE will soon finish the analysis of the program, because the source code of sin is not avalible. it can not find bug in moti-example:

$ ./run_klee.sh

...... # in a second

KLEE: ERROR: (location information missing) external call with symbolic argument: sin
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 13198
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1

Reproduce the experimental results

We can use docker to repoduce the experimental results presented in the paper. Our experiments were performed on a server with Intel(R) Xeon(R) Platinum 8269CY CPU (2.50GHz) and the operating system is Ubuntu 18.04 LTS. To reproduce the results, a machine with similar CPUs(~2.50GHz) is required. Running the artifact on a different machine could possibly diverge the execution and lead to different results. Moreover, our experiments were run in parallel.

Run a simple benchmark in GSL

Navigate to /home/aaa/gsl_bench and list the contents.

$ cd /home/aaa/gsl_bench

The basic configuration of the current experiment is as follows.

$ cat run_smse.sh

......
#### SMSE running config ####
MAX_EXE_TIME=30
MAX_LOOP_TIME=5
SOLVER_TYPE="jfs-smt"
SEARCH="bfs"

########################################################################

# get all dictionary 
#all_dicts=`ls -d */`

# or we can manual define which dictionary to work:
all_dicts="gegenbauer"

# or get dictionaries from cmdline
#all_dicts=$*

Note that you now need to pay attention to several parameters:

• MAX_EXE_TIME: Maximum symbolic execution time
• SOLVER_TYPE: This option is used to specify the solution method, which is supported only in SMSE, but not in KLEE.
• SEARCH: Search heuristic.
• all_dicts: Specify the benchmark directory in which to run. Here we specify the simplest directory gegenbauer for analysis

Now, let's run this script:

$ ./run_smse.sh


==== Enter ==== > /home/aaa/gsl_bench/gegenbauer
     TestCase Num :1
     Running ==== > gsl_sf_gegenpoly_array
KLEE: KLEE: WATCHDOG: watching 58


...... # some info 
gsl: gegenbauer.c:148: ERROR: domain error
Default GSL error handler invoked.
KLEE: ERROR: error.c:47: abort failure
KLEE: NOTE: now ignoring this error at this location
gsl: gegenbauer.c:148: ERROR: domain error
Default GSL error handler invoked.

KLEE: done: total instructions = 15200
KLEE: done: completed paths = 13
KLEE: done: partially completed paths = 2
KLEE: done: generated tests = 5

After running, test cases are generated in the corresponding directory:

$ cd gegenbauer/gsl_sf_gegenpoly_array_output && ls

execute_time.txt  test000001.ktest      test000002.ktest  test000004.ktest  warnings.txt
info              test000001.time       test000002.time   test000004.time
messages.txt      test000002.abort.err  test000003.ktest  test000005.ktest
run.stats         test000002.kquery     test000003.time   test000005.time

We can get the coverage information by running the script. All coverage information can be found in res_all.txt. The four columns are the name of benchmark, the coverage of analyzed function, total covered lines of code, and the execution time, respectively.:

$ cd /home/aaa/gsl_bench
$ ./repaly.sh
$ cat res_all.txt

...... 
gsl_sf_gegenpoly_array ,92.85714285714286 , 15,10
......

After running, you can use clean_all.sh to clear all outputs (remember to save if necessary):

$ ./clean_all.sh

Using KLEE to analyze the program is also similar to the above steps, which is not presented here.

Run all benchmark in GSL

Before running, please check the configuration of run_smse.sh and manually modify it to keep consistent with the configuration below, which is also the configuration in our evaluation. Then, open the first comment of all_dicts=ls -d */:

$ vi run_smse.sh

#### SMSE running config ####
MAX_EXE_TIME=1800
MAX_LOOP_TIME=5
SOLVER_TYPE="jfs-smt"
SEARCH="bfs"

########################################################################

# get all dictionary 
all_dicts=`ls -d */`

# or we can manual define which dictionary to work:
#all_dicts="gegenbauer"

# or get dictionaries from cmdline
#all_dicts=$*

Save the above changes and run run_smse.sh:

$ ./run_smse.sh

==== Enter ==== > /home/aaa/gsl_bench/airy
     TestCase Num :6
     Running ==== > gsl_sf_airy_Ai_deriv_e
KLEE: KLEE: WATCHDOG: watching 500
......

ctrl + c

This configuration will execute all benchmarks in order. It will take a long time to finish.

Run in parallel on the server

Before running the script, you must ensure that the machine used has more than 16 cores and 32GB of memory. Similarly, you should configure your running options.

Suppose we use DFS + SMSE (jfs-smt) configuration for running half an hour. Then, run_smse.sh must be set as:

$ vi run_smse.sh

......
#### SMSE running config ####
MAX_EXE_TIME=1800
MAX_LOOP_TIME=5
SOLVER_TYPE="jfs-smt"
SEARCH="dfs"

########################################################################

# get all dictionary 
#all_dicts=`ls -d */`

# or we can manual define which dictionary to work:
#all_dicts="gegenbauer"

# or get dictionaries from cmdline
all_dicts=$*
......

Note that this variable all_dicts captures parameters from the command line.

Then you can use multi_run.sh with an argument smse to execute all benchmarks in parallel.

$ ./multi_run.sh smse

You can use the command top to trace the execution and find many KLEE processes running in the backend.

$ top

......
 PID USER      PR  NI    VIRT    RES    SHR S  %CPU %MEM     TIME+   COMMAND
 521 root      20   0  730408 690480  34160 R 100.0  8.5     0:47.31 klee
 533 root      20   0  730408 690480  34160 R 100.0  7.2     0:46.21 klee
 540 root      20   0  730408 690480  34160 R 100.0  6.4     0:43.12 klee
......