INSTALL

Prerequisites:

1. Available as Linux distribution packages

Many of FuzzBALL dependencies are commonly found packaged for Linux
distributions, and if that's available it's usually the easiest way to
install them. For instance here's a list of the packages you'd need on
Debian/Ubuntu, last tested on Ubuntu 14.04:

# Git for FuzzBALL, SVN for VEX, one or both for STP
apt-get install git subversion
apt-get install build-essential automake
# Before 14.04, libiberty-dev was included in binutils-dev
apt-get install binutils-dev libiberty-dev zlib1g-dev
apt-get install ocaml ocaml-findlib camlidl libextlib-ocaml-dev

Here's a longer list of packages that includes things useful in
conjunction with FuzzBALL, for other BitBlaze software, for building
prerequisite software, etc:

sudo apt-get install build-essential
sudo apt-get install valgrind
sudo apt-get build-dep valgrind
sudo apt-get install qemu
sudo apt-get build-dep qemu
sudo apt-get install binutils-multiarch
sudo apt-get build-dep binutils-multiarch
sudo apt-get install binutils-dev
sudo apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev camlidl
sudo apt-get build-dep ocaml
# ocaml-native-compilers improves compilation speed
sudo apt-get install libextlib-ocaml-dev ocaml-native-compilers
sudo apt-get install libocamlgraph-ocaml-dev
sudo apt-get install libsqlite3-ocaml-dev
# texlive is big, but used with ocamldoc, etc.
sudo apt-get install texlive texlive-latex-extra transfig hevea
sudo apt-get install subversion
sudo apt-get install libgmp3-dev
sudo apt-get install zsh
sudo apt-get install automake
# STP always needs bison and flex.
# Modern (Git) STP requires cmake and some Boost libraries
sudo apt-get install bison flex cmake
sudo apt-get install libboost-system-dev libboost-program-options-dev

Fedora rough equivalents:

sudo yum install make automake gcc gcc-c++ kernel-devel
sudo yum install glibc-devel glibc-static glibc-utils
sudo yum install bison flex
sudo yum install strace
sudo yum install valgrind
sudo yum-builddep valgrind
sudo yum install qemu
sudo yum-builddep qemu
sudo yum install binutils-arm-linux-gnu binutils-x86_64-linux-gnu
sudo yum install binutils-devel
sudo yum install ocaml
sudo yum install ocaml-findlib ocaml-findlib-devel
sudo yum install ocaml-camlidl ocaml-camlidl-devel
sudo yum-builddep ocaml
sudo yum install ocaml-extlib ocaml-extlib-devel
sudo yum install ocaml-ocamlgraph ocaml-ocamlgraph-devel
sudo yum install ocaml-sqlite ocaml-sqlite-devel
sudo yum install texlive transfig hevea
sudo yum install subversion git
sudo yum install gmp gmp-devel
sudo yum install zsh
sudo debuginfo-install coreutils

2. VEX

We use the VEX library for instruction processing, best known for its
use in Valgrind. It's not distributed separately, so you can just
check it out from Valgrind's SVN repository (and we refer to versions
by their SVN revision number). Unfortunately for us the VEX interface
changes incompatibly from time to time, requiring matching updates in
our interface code (look for "#if VEX_VERSION > xxxx" in
libasmir/src).

The most recent version of VEX we've tested with is r3206. However it
doesn't work out of the box because the Valgrind developers have
broken their Makefile. A patch for this is in vex-r3206.patch. You'll
want to use this version if you're running x86-64 binaries new enough
to contain MPX instructions, since VEX versions before r2858 can't
deal with them. However ARM support hasn't been tested in this version
yet.

The more recent stable version of VEX we recommend is r2737. For x86
and x86-64 it works out of the box. Typical commands to check out and
compile it look like:

   % svn co -r2737 svn://svn.valgrind.org/vex/trunk vex-r2737
   % cd vex-r2737
   % make -f Makefile-gcc

For many uses of FuzzBALL, and especially on x86-32, any version of
VEX will work just fine. If you want to run on ARM code it's more
important to use a more recent version. Some changes to VEX to make it
work better for our purposes are in vex-r????.patch. For x86, these
only affect a few obscure instructions. But for ARM they also disable
a Thumb instruction optimization that tries to peek directly at other
instruction bytes in a way that usually crashes FuzzBALL.

The oldest version we've traditionally used is r1856. Back then the
build steps instead looked like:

   % make version
   % make libvex.a

3. GNU Binutils

You need a version of the Binutils library suitable for development;
for instance, the "binutils-dev" package in Debian or Ubuntu.

If you want cross-architecture support, you'll probably need to
compile your own version of the Binutils. (Debian has a
binutils-multiarch, but no binutils-multiarch-dev.) You can get the
source at:

http://www.gnu.org/s/binutils/

and compile it with:

../configure --disable-werror --enable-targets=arm-linux-gnueabi,i486-linux-gnu,x86_64-linux-gnu --prefix=<wherever>/binutils-multiarch

and then pass --with-binutils=<wherever>/binutils-multiarch to
Vine's ./configure.

4. STP

Historically we kept STP binaries in our SVN repository, but for space
and cleanliness they're not included here, so you'll need to compile
STP yourself and put the "stp" binary and "libstp.a" library in the
"stp" directory. FuzzBALL can use STP either as a separate program or
via a library interface, which have various performance/engineering
tradeoffs. For the library interface we patch STP to get
counterexamples in a different format.

The ongoing development of STP is now in a GitHub repository, and has
switched to a CMake-based build process. This newer version is where
all the upstream support has moved. As a convenience to provide a bit
of isolation from possible incompatibilities and to include any
FuzzBALL-specific patches, we now keep a branch of this under the
FuzzBALL GitHub area. That build process looks like:

    % git clone https://github.com/bitblaze-fuzzball/stp
    % cd stp
    % mkdir build
    % cd build
    % cmake -G 'Unix Makefiles' ..
      (or /.../path/to/recent/cmake cmake -G 'Unix Makefiles' .. -DBOOST_ROOT=/.../path/to/recent/boost )
    % make
    % cp stp lib/libstp.a $HERE/stp

Where $HERE is the directory this INSTALL file is in.

Older versions of STP are kept in a SourceForge SVN repository, which
is a good choice if you want stability, and it doesn't have any
show-stopping bugs. The apparently final revision is r1673, which you
can build like:

    % svn co -r1673 https://svn.code.sf.net/p/stp-fast-prover/code/trunk/stp stp-r1673+vine
    % cd stp-r1673+vine
    % patch -p0 <$HERE/stp/stp-r1673-true-ce+bison3.patch
    % ./clean-install.sh --with-prefix=$(pwd)/install
    % cp install/bin/stp install/lib/libstp.a $HERE/stp

The "+bison3" in the latest version of the patch refers to the fact
that includes a backported compatibility fix for use with Bison 3,
which is needed for STP to build on Ubuntu 14.04, for instance. Fixes
like this now appear first in the GIT version, though.

Note that actually only libstp.a is used as part of the build process
right now. FuzzBALL's default mode is to use the external "stp"
binary, but it doesn't automatically look in the "stp" directory; you
need to either put it in a directory that's on your $PATH or pass the
-stp-path option to FuzzBALL.

5. OCaml tools

You need OCaml itself, plus ocamlfind and ocamlidl.

At the moment we're going to try to maintain compatibility back to
OCaml 3.12, which means continuing to use some features that are
deprecated in 4.x. However recent OCaml versions have some advantages
if you can them conveniently, such as including enough debug
information in native binaries to let GDB print backtraces.

6. OCaml libraries

You need ExtLib, http://code.google.com/p/ocaml-extlib/


FuzzBALL build process:

  ./autogen.sh
  ./configure --with-vex=<...> ...
  make

Notes:

 'make' will build native-code binaries with debugging information
        for everything
 'make bytecode' will build bytecode with debugging information for
        everything
 You can also run 'make' or 'make bytecode' in a single directory if
 you've only changed files there, but running make at the top level
 is recommended to handle inter-directory dependencies.

Modern versions of OCaml (3.10 and later) include enough debugging
information in native code compilation in order to make stack
backtraces work, so that's our default behavior. To get stack traces
on fatal errors you just need to set the environment variable
OCAMLRUNPARAM=b.

If you have an old version of OCaml and want backtraces, or you want
to run "ocamldebug", you'll need to compile bytecode versions of the
programs. This is now done with a "make bytecode" target, and will
create executables with the suffix ".dbg".

If you are using the Debian/Ubuntu packaged versions of OCaml 3.12 or
later, there's an additional issue with the way bytecode OCaml code
and native code libraries are combined in "custom" executables that
will interfere with debugging. The easiest workaround for this is make
sure you have package version 3.12.0-6 or later, and set the
environment variable OCAML_COMPAT=c. More details on this are at:

http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=627761