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 what we've
historically done was to check it out from Valgrind's SVN repository,
where it was a sub-project. Unfortunately for us the VEX interface
changes incompatibly from time to time. The way we handled this is by
having the configure process generate a preprocessor macro named
VEX_VERSION, which we then use for conditional compilation like
"#if VEX_VERSION >= xxxx" in the interface code under libasmir.

In 2017 the Valgrind developers transitioned from SVN to Git. The good
news is that Git's distributed nature makes it easier for us to keep
track of the changes to VEX that we need. What may be less convenient
is how to keep track of VEX interface changes: as of this writing
there haven't yet been any incompatible changes in the Git version,
but it's probably only a matter of time until there are. We've set up
some configure machinery to create fake VEX_VERSION values of Git
checkouts, by count the number of commits back to the merge point and
adding 3400 (the final SVN revision number). This is a bit of a hack,
but it seems it may work OK because the Valgrind developers are
planning to only do linear (SVN-like, rebase-based) development.

Our fork of Valgrind/VEX is at:

https://github.com/bitblaze-fuzzball/valgrind-vex-for-fuzzball.git

We'll try to always keep it in a state that's compatible with
FuzzBALL. Commands to check out and compile VEX from this repository
look like:

   % git clone https://github.com/bitblaze-fuzzball/valgrind-vex-for-fuzzball.git
   % cd valgrind-vex-for-fuzzball/VEX
   % make -f Makefile-gcc

The most recent SVN version of VEX we've tested with (and probably the
final one) is r3400. As of this writing the repository is still
available read-only. The build process of recent VEX versions
needs some workarounds to compile outside of Valgrind's autoconf
environment, so you'll want to apply one of the patches like
vex-r3400.patch. r3260 is another version we've used
extensively. Before it we recommended r2737, but on recent x86-64
systems you need a version that's at least r2858 to deal with MPX
instructions (even as no-ops).

Thus, some typical commands to check out and compile VEX from SVN look
like:

   % svn co -r3260 svn://svn.valgrind.org/vex/trunk vex-r3260
   % cd vex-r3260
   % patch -p0 <$HERE/vex-r3260.patch
   % 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 may want to compile your
own version of the Binutils. (Debian has a binutils-multiarch, but for
a long time there was no binutils-multiarch-dev, and we haven't done
much testing with it.) You can get the source at:

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

and compile it with, for instance:

../configure --disable-werror --disable-shared --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. In this case where you're using the Binutils
compiled in a non-system location, the choice that will make later
steps easiest is to compile only a static version of the Binutils
libraries, which is what --disable-shared does. Shared libraries save
space, but they make the build process more complicated because they
need to be found both at compile time and at runtime. (FuzzBALL's
build process doesn't currently incorporate libtool, which would be
the most standard way to automate the linking decisions.)

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