This repository supports my paper submission to VMCAI 2017.
If you think that something is missing, please open an issue.
See EBAinfer.pdf.
I have run on a machine running Ubuntu 14.04.5 LTS (GNU/Linux 3.19.0-25-generic x86_64). Some fine installation details given here may be different if you are using a different operating system.
Install some basic packages:
sudo apt-get install build-essential autoconf pkg-config
Get Linux 4.7-rc1 and gunzip it:
wget https://github.com/torvalds/linux/archive/v4.7-rc1.tar.gz
You may need to install a few packages ...
sudo apt-get install libelf-dev libssl-dev
... before configuring the kernel with allyesconfig:
make allyesconfig
Get EBA and follow follow the installation instructions (see README.md):
git clone https://github.com/models-team/eba.git
When EBA is invoked by Kbuild, we need a wrapper that "simulates" GCC, this is bin/eba-gcc.hs. Install the Haskell Platform and compile the script:
sudo apt-get install haskell-platform
ghc -O2 eba-gcc.hs
If you want to run EBA over already preprocessed files, in paralell, you should use the bin/eba-linux.sh script. You must install parallel:
sudo apt-get install parallel
Get Smatch and follow the installation instructions, essentially:
git clone git://repo.or.cz/smatch.git
cd smatch
git checkout 78b2ea64f3dc
I had to install a few extra packages to compile Smatch:
sudo apt-get install sqlite3 libsqlite3-dev python-pysqlite2 libdbd-sqlite3-perl
Get Coccinelle and follow the installation instructions (see install.txt):
git clone https://github.com/coccinelle/coccinelle.git
cd coccinelle
git checkout 99f1de0f8cad
I had to install a few extra packages to compile Coccinelle:
sudo apt-get install python-dev libpcre3-dev
Coccinelle also depends on some OCaml packages that you can easily install through OPAM:
opam install --deps-only coccinelle
The preprocessed files for running EBA and Smatch are located in 5.1/cpped, the raw unpreprocessed files for running Coccinelle are located in 5.1/raw.
Running EBA:
eba -L --all-locks --externs-do-nothing path/to/cpped/file.c 2>/dev/null
Running Smatch:
smatch -p=kernel path/to/cpped/file.c |& grep -i " lock"
Running Coccinelle:
spatch --very-quiet --sp-file path/to/linux/scripts/coccinelle/locks/double_lock.cocci -D report path/to/raw/file.c
You can find my scripts in 5.2/, just put all of them in your $PATH. Some of the scripts have recognize --help.
To run EBA:
eba-linux-make-drivers 16 # to run 16 jobs in parallel
All the bug warnings are placed in eba.warns.
To run Smatch:
smatch-test-kernel-drivers
All the bug warnings are placed in smatch_warns.txt.
To run Coccinelle:
make coccicheck COCCI=scripts/coccinelle/locks/double_lock.cocci MODE=report M=drivers/