Recommend using the same OS in dynamic validation.

—————–IMPLEMENTATION————–

The static analysis component was implemented using the Clang Tool 3.4. The corresponding directory Static-Analysis.

Our guided symbolic execution was implemented based on KLEE 1.2. The directory is Guided-Symbolic-Execution/klee and Guided-Symbolic-Execution/klee-uclibc, compile it using the instruction at http://klee.github.io/build-llvm34/.

We used Simics virtual platforms 4.6 to implement the dynamic validation phase. The directory is Dynamic-Validation.

——————Static Detection————–

klee-gcc is a tool compiling device driver to clang AST, this tool is in directory Static-Analysis/scripts/klee-gcc.

$ cd Experiment-and-Subjects/moti-example

$ make CC=/path/to/klee-gcc

then compile SRacer

$ cd Static-Analysis/SRacer

$ mkdir build; cd build; cmake ..

$ make

After finishing compiling SRacer and device drivers.

$findfind$(pwd) -name “*.ast” > astList.txt

Note that ast files are generated by klee-gcc.

run the command:

$ SRacer /path/to/astList.txt /path/to/config.txt /output/path

i.e., SRacer astList.txt config.txt ./

config.txt can be found in Experiment-and-Subjects and Static-Analysis/SRacer

A simple warning manager tool provided in directory Experiment-and-Subjects/static-result/ is warningManager.py.

——————Symbolic Execution————–

Use klee-gcc-bc to compile kernel module to llvm IR. The LLVM verison is 3.4.

Note: instrumentations are required to make KLEE able to execute drivers.

First, Experiment-and-Subjects/static-result/autoIns.py is proivided to instrument interupt calls.

Second, determine variables as symbolic by using klee_make_symbolic.

Third, provided guided files named as GuideSrc.txt, so that the modified KLEE could regonize which path sould cover and which not. The file format is as follows:

Info:

filename1 linenumber1

filename2 linenumber2

filename3 linenumber3

Very similar with the output file of SRacer (name of static analysis phase).

$ cd Experiment-and-Subjects/moti-example

$ make CC=/path/to/klee-gcc-bc

$ klee -entry-point=dataRace_init -guidedExe -libc=uclibc exampleSym.bc

——————Dynamic Validation————–

Use Simics4.6 to dynamic validate each potentional data race.

Test case configureation:

Open checkpoint “ubuntu-gcc” (we install ubuntu on Simics)

“simics>” means in command line window (Simics GUI -> “tools”->”command line window”)

“$” means in simulated system.

simics> enable-real-time-mode

The following instructions are used to transform subjects:

$ ftp 10.10.0.1

Press enter

$ bin

$ get example.tar.gz

$ quit

The following instructions are used to compile drivers:

$ tar xf example.tar.gz

$ cd general

$ make

$ sudo insmod example.ko

The following instructions are used to save the status so that we can use it again without redo previous steps:

simics> stop

simics> write-configuration ckp-example

simics> c

The following instructions are used to store symbol file to host:

$ cat /proc/kallsyms > exampleSymbol

$ ftp 10.10.0.1

Press enter

$ put exampleSymbol

$ quit

When performing automatic validation (Scripts are in directory Dynamic-Validation/scripts/analysePDR.py):

If Simics is running and you want to test the next case, open “command line window” and input “quit”.

When performing validation one by one:

Scripts are provided in directory Dynamic-Validation/conf.py. It read Dynamic-Validation/Info.py as information file.

The conf.py can be run by entering run-python-scripts in command line window or selecting python file in Simics menu.