naegling/icse19-zop2 repository overview

⁠Artifact Description

This artifact contains the tools, benchmark programs, and results supporting the evaluation sections of Zero-Overhead Path Prediction with Progressive Symbolic Execution published at ICSE 2019. Its purpose is to:

• demonstrate tools implementing the techniques discussed in the paper.
• enable reproduction of the experiments used in its evaluation.
• serve as a publicly accessible repository for the software and data developed for the paper.

The artifact is packaged as a self-contained docker image with all tool source codes, benchmarks, and data with the exception of raw wave-form recordings. Since electro-magnetic (EM) recording requires access to specialized hardware (a digital spectrum analyzer), the processed wave-form recording data are provided for each experiment. Although the artifact image does not contain a matlab runtime, the scripts and data can be exported for reproduction. The image is available at "https://hub.docker.com/r/naegling/icse19-zop2⁠". We vetted our artifact on Ubuntu 18.04 and assume that a reviewer evaluating this artifact has:

• CLI docker installation
• ~12 GB available storage
• at least an intermediate familiarity with the bash and docker CLI.
• access to matlab equipped workstation (only required for EM analysis reproduction)

While working on the paper, one of our authors placed an outdated version of the path prediction accuracy results in Table II, and failed to confirm that the values were consistent with the latest experiments. The latest values do not change our results in any qualitative way and do not affect our findings. We have supplied both the original submitted paper (icse2019-zop2.pdf) and a pre-camera ready version with a corrected Table II (icse2019-zop2-updated.pdf). We apologize for any confusion.

⁠Status

We submit this artifact in support of the Available badge.

⁠License

See separate LICENSE.txt

⁠Install

The docker image contains tool source code, pre-built binaries, experiments, and a linux environment to reproduce our experimental results.

⁠Prerequisites

• docker community edition⁠
• about 12GB of available disk space

⁠Obtaining the Artifact

We publish our artifact as a self-contained docker image available at: https://hub.docker.com/r/naegling/icse19-zop2⁠

Run the following commands from a terminal prompt:

docker pull naegling/icse19-zop2:latest

The last command will launch a bash prompt in the container as zopuser with password zopuser.

⁠Quick Start to Reproducing a Complete Input Generation Experiment

We start with a quick walk-through of one component of our experiments as an introduction to the zop-2 artifact. The steps below will replicate the source code preparation, function-sliced symbolic execution, and training replay for the replace benchmark. Subsequent sections of this document provide sufficient detail to reproduce all input generation experiments reported in our paper. Although this walk-through should require less than 5 minutes, most steps require from a few hours to more than a day to complete. See details below for expected step runtimes. To permit selective reproduction, this image is pre-populated with the results of our execution.

After obtaining the artifact, run the following commands from a terminal prompt:

docker run -it --name zop2 naegling/icse19-zop2:latest bash
cd zop-2/experiments/replace
./prep                # prepare and instrument source code
./run-fn              # generate inputs with function-sliced symbolic execution and replay
./show-results        # calculate coverage statistics
exit                  # stop container
docker rm zop2        # restore container state

⁠Exploring the Artifact

Start a bash prompt within the container by executing the following command from a terminal prompt:

docker run -it --name zop2 naegling/icse19-zop2:latest bash

The zopuser home directory contains two sub-directories: src and zop-2. The src subdirectory contains tools for generic progressive symbolic execution. The zop-2 directory contains zop-2 specific tools and experiments.

⁠src/

Each tool in the src directory contains build instructions for Ubuntu 18.04 linux in its own README file. Other distributions may require minor modifications to build steps and/or required packages. The docker image contains pre-built binaries for each tool installed to /usr/local/stow and symlinked into bash environment with stow.

pg-klee: A fork of klee 1.3⁠ implementing progressive symbolic execution as described in our paper. This directory contains the original klee (pg-klee/klee) and its dependencies. Additionally, the pg-klee/pg-klee directory contains our modified klee symbolic execution engine.

cilium: A modified version of CIL⁠. We use CIL as a source-to-source translation of benchmark programs to simplify the automated generation of program fragments. However, off-the-shelf CIL injects integral type-casting into pointer comparison operations, inhibiting later warnings during progressive symbolic execution on unexplored paths. Our modification prevents the undesirable type-casting.

llvm-5.0: Both klee and pg-klee require llvm-3.4. Our zop-2 source analysis tools and replay harnesses are built with version 5.0 of llvm.

⁠zop-2/

This directory contains zop-2 specific tools in its src subdirectory. As above, C programs contain build instructions, are pre-built, and symlinked into the bash environment. Python3 programs are symlinked into the zop-2/bin directory added to the zopuser path by the container. It also contains a collection of zop-1 files for reference. The experiments subdirectory contains the evaluated benchmarks. The following sections describe the tools and scripts provided herein.

⁠Reproducing the Input Generation Experiments

The directory layout for all experiments is identical. Each experiment directory contains a three classes of bash scripts: prep, run-${MODE}, and show-results. Complete reproduction of a training input generation experiment requires running these scripts in sequence. The docker image is pre-populated with our reported experiment output products, so an evaluation need not start with the first step (prep). The targeted ZOP embedded device contains a 32-bit processor without operating system or runtime. Therefore, we compile all benchmarks to 32-bit binaries and include a minimal C runtime (called zopc) to support our benchmarks. Due to differing processor speeds and a random component to symbolic execution state space exploration, reproduction may produce slightly different results.

⁠./prep

The prep script prepares a source program for progressive symbolic execution and replay scaffolding generation. It invokes CIL to remove syntactic sugar from the original program source code and produce an equivalent program in a simplified C subset. The script then uses our clang based muilt-purpose tool, zopper, in a series of passes to refactor return statements, insert marker instrumentation, insert call site tags, collect source analysis information, and emit networkx compatible control flow graphs for each contained function. The final step of the script is to compile and link the final transformed source code into an llvm bytecode module.

Principle products of this script:

• instrumented benchmark source code (*_tagged.c)
• source analysis information (${BENCHMARK}.json)
• bytecode module (${BENCHMARK}-main.bc)

Expected Runtime: < 1 minute

⁠./run-${MODE}

The run scripts perform symbolic execution in one of three modes: classical (cs), progressive (pg), and functional (fn).

cs: Tweaks zopc to use native stdin and malloc and runs off-the-shelf klee for one hour. It then filters out non-completing test cases and replays the remaining ktest files to collect the program traces. These ktest files are further filtered to keep only files whose program trace covers at least one new marker-to-marker path. The final list of selected program inputs with their associated program trace is bundled into a single json formated input file for replay on the targeted embedded device.

pg: Runs pg-klee to progressively unconstrain program state to reach the required marker-to-marker path coverage. The script takes the selected test cases and source analysis info and generates a replay scaffold in C source code to be compiled and ran on the targeted embedded device to record fragment traces containing the desired marker-to-marker paths. For validation, the script completes by building the scaffolds on the host and checking for symbolic execution divergence.

fn: Runs pg-klee with limited progression, reaching the same marker-to-marker coverage as pg mode but with greatly reduced analysis execution time. In this mode, all call sites skip native callees and immediately substitute an unconstraining stub. Although this mode achieves equivalent coverage, the loss of execution context around the recorded marker-to-marker paths can negatively effect subsequent signal matching performance.

Principle products of this script:

• (cs) top-level program inputs
• (pg/fn) replay scaffold source for additional marker-to-marker paths.

Expected Runtime:

• (cs) ~ 75 minutes
• (pg) mDNS: ~ 3000 minutes, other benchmarks: < 60 minutes
• (fn) mDNS: ~ 75 minutes, other benchmarks: < 1 minute

⁠./show-results

The show-results bash script produces the raw experimental results tabulated in our paper. For each Table in our work, the reported values may be replicated as follows:

Table I: combines results from two sources:

cloc ${BENCHMARK}.c zopc.c OR (mdns only) cloc src 
./show-results (for each benchmark)

Table II:

The show-pred-accuracy bash script loops through each experiment and calculates the path prediction accuracy.

cd ~/zop-2/experiments
./show-pred-accuracy

Table III, Table IV, and Table V:

./show-results (for each benchmark)

Expected Runtime: < 1 minute

⁠Reproducing the EM Analysis

Each experiment directory contains a zop2-prediction directory containing the EM waveform analysis data and scripts. Each directory contains pre-computed results for the benchmark as well as saved data that can be processed to reproduce the results.

⁠Pre-computed Marker Sequences

The following files contain marker sequences, both the pre-processed ground truth sequence and the predicted sequence by each configuration, in Matlab format.

⁠Pre-computed Results

The followig files store the pre-computed results, also in Matlab format.

⁠High-level Matlab Scripts

To display path prediction accuracy, run the following script:

calc_path_prediction_accuracy.m

To display the prediction accuracy histogram, run the following script:

Script_show_plot.m

To process all the data and generate the results run the following script:
(expected runtime: several hours for Replace, Schedule, and Print Tokens, several days for mDNS)

script_process_all.m

⁠Matlab subroutines

In addition to these top-level Matlab scripts, the folder also contains various Matlab subroutine scripts:

• bl_accuracy.m (compute block-level accuracy)
• calc_cs.m (compute cs path prediction accuracy)
• calc_fn.m (compute fn path prediction accuracy)
• calc_pg.m (compute pg path prediction accuracy)
• get_words.m (learn/create dictionary of words (or windows) from traces)
• get_traces.m (re-sample signal traces)
• match_words.m (match words from the testing traces against the learned dictionary)
• convert2cell (convert marker positions and distances to Matlab cell type)
• reconstruct_marker_seq.m (Reconstruct marker sequence)
• EditDistance (compute the Levenstein edit distance)

⁠Incorporating New Benchmarks

Incorporation of a new benchmark program entails adapting the existing three classes of bash scripts for the new benchmark. The source code transformations in prep are sufficient for progressive symbolic execution as supported by backend solver theories. The most common limitation imposed by pg-klee's solver is to prohibit floating point expressions in a branch condition.

Futher, manual, source transformations may be required to construct the replay scaffolding:

• function pointers should be either eliminated or factored out.
• calls to external, undefined functions should be either eliminated or replaced with simplified stand-ins.
• local variable names that shadow global function names should be refactored with unique identifiers.

Our C source multi-purpose tool, zopper, can aide in identifying these required manual transformations.

zopper -zop-lint src-1.c src-2.c ... src-n.c

⁠Toubleshooting

⁠Docker on OSX

Use homebrew cask to install docker:

brew cask install docker

If docker fails with error message:

docker: Cannot connect to the Docker daemon at unix:///var/run/docker.sock.

see: https://stackoverflow.com/a/44719239⁠

⁠Docker on Linux

In some distributions, the package does not add the current user to docker group. In this case, either add yourself to docker group or run all docker commands with sudo.