Home

Awesome

HOMI

<img src= "./img/homi_logo.png" width="200" height="200">

HOMI is a tool that performs symbolic execution while maintaining only a small number of promising states via online learning. This tool is implemented on the top of KLEE, a publicly available symbolic execution tool for testing C programs. For more technical details, please read our paper.

Table of Contents

Installation

We provide a simple way to install HOMI:

Please see INSTALL.md for full installation instructions.

Artifact

We design a shorter experiment that performs Homi and pure KLEE, respectively, on our benchmark trueprint-5.4 for an hour once. This is because all the experiments in our paper take at least hundreds of hours; for instance, to reproduce the experimental result for a benchmark in Figure 1 of our paper with a single core, it takes a total of 150 hours (5 hours * 6 testing techniques * 5 iterations). In this section, we will show the commands to run the short experiment.

Running Homi.

The following command will run our tool, Homi with the given search heuristic, to test one of our benchmarks, trueprint-5.4, for an hour once.

$  cd ~/Homi/script
$  python3.7 Homi.py pgm_config/1trueprint.json 3600 homi nurs:md2u 1

Each argument of the last command means as follows:

If the Homi scipt successfully ends, you can see the following command:

#############################################
################Time Out!!!!!################
#############################################

Running pure KLEE.

if you want to run pure KLEE with the given search heuristic on trueprint-5.4, the command is as:

$  cd ~/Homi/script
$  python3.7 Homi.py pgm_config/1trueprint.json 3600 pureklee nurs:md2u 1

Visualizing the experimental results.

To visualize the experimental results, we first use gcov, one of the most popular tools for measuring code coverage and then generate two graphs in terms of the number of covered branches and candidate states. To do so, the command is as:

$  cd ~/Homi/script
$  python3.7 graph_generate.py pgm_config/1trueprint.json ../experiments/result_All/

Each argument of the last command means as follows:

if the script successfully ends, you can see the following command:

#############################################
trueprint_cov.pdf produced
trueprint_statenum.pdf produced
#############################################

Now, you can find trueprint_cov.pdf and trueprint_statenum.pdf in ~/Homi/script/ folder.

How to run Homi on arbitary C open-source programs.

We also provide the detailed instructions to run our tool, Homi, for arbitary open-source C programs.

1) The first step is to download the program and build it with gcov and LLVM.

# Download an open-source C program you want.
$  cd ~/Homi/benchmarks/
$  wget https://ftp.gnu.org/gnu/enscript/enscript-1.6.6.tar.gz
$  tar -zxvf enscript-1.6.6.tar.gz

# Build the program with gcov
$  cd ~/Homi/benchmarks/enscript-1.6.6
$  mkdir 1obj-gcov
$  cd 1obj-gcov
$  ../configure --disable-nls CFLAGS="-g -fprofile-arcs -ftest-coverage"
$  make

# Build the program with LLVM
$  cd ~/Homi/benchmarks/enscript-1.6.6
$  mkdir obj-llvm
$  cd obj-llvm
$  CC=wllvm ../configure --disable-nls CFLAGS="-g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES  -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__"
$  make
$  cd src
# This command extracts the LLVM bitcode from a build project.
$  find . -executable -type f | xargs -I '{}' extract-bc '{}'

2) The second step is to generate the json file to describe the program as follows:

$  cd ~/Homi/script
$  python3.7 json_generator.py enscript-1.6.6 1
$  # "Successfully generate 1enscript.json in the `pgm_config' directory"

3) Lastly, run Homi with the search heuristic (nurs:cpicnt) on enscript-1.6.6 for 30 minutes as:

$  cd ~/Homi/script
$  python3.7 Homi.py pgm_config/1enscript.json 1800 homi nurs:cpicnt 1

How to extend the standard KLEE.

We extended the standard KLEE in order to prune the states based on the given n features and n-dimensional weight vectors. We mainly implemented it in the files 'Homi/klee/lib/Core/Executor.cpp' and 'Homi/klee/lib/Core/Executor.h'. That is, our pruning technique is not available in the original KLEE.

Our new implementation is able to prune states through three steps; the first step is to transform each state into a n-dimensional boolean vector when given n features. Second, it scores each state with a given weight vector. Third, it prunes the states based on the scores and the pruning ratio.