Installing SAW

There are three ways to install SAW: you can download the binary distribution of a release, compile it from source yourself, or download either or both of the Docker images.

If you are using the Python scripting interface you will also need to install the Python bindings.

Binary Distributions

SAW releases include binary builds for several platforms. These can be downloaded from the releases page of the GitHub repository.

There are two sets of binary builds: one that includes solver executables (from a what4-solvers build) and one that does not. If you use one of the non-solver builds, you will need to install your own solver executables. SAW requires at least the Z3 solver and many proofs use others. See below.

A SAW binary distribution includes:

  • executables for SAW and Cryptol;

  • as noted, optionally executables for a range of SMT solvers;

  • PDFs for the SAW manual and tutorials;

  • the SAW examples;

  • the Cryptol standard library;

  • a copy of the cryptol-specs library of cryptographic algorithm specifications;

  • top-level README and LICENSE files.

Note that the structure of the release is not suitable for unpacking directly into /usr/local/bin or any other Unix installation prefix. The recommended procedure is to unpack it somewhere in your home directory and include its bin directory in your $PATH.

Building from Source

To build from source you must first get the source. The recommended way to do that is to clone the git repository from GitHub.

If you want to build a release rather than the current development version, check out the tag for the release you want. For example, use git checkout v1.3 to get the 1.3 release.

Then, you will need to also fetch a number of git submodules. This can be done with git submodule update --init. Note that the often-used --recursive flag to git submodule update is not needed, and is not recommended either as it will unnecessarily download substantially more material, including duplicate copies of some repositories. The SAW repository and others related to it are specifically set up to only require one layer of submodules.

Now follow the build instructions in the repository README. (Those instructions are not duplicated here in the interests of having one canonical copy.)

The build process places the SAW and Cryptol executables in a bin subdirectory of the source tree. Typical usage is to add this directory to your $PATH rather than installing them anywhere.

You will need to install Z3 and possibly other solvers, as described below.

Release Sources

In theory you can download the sources from a release; however, the source downloads as generated by GitHub are missing their submodule dependencies as well as the proper versions of those submodules to use. This makes them unbuildable and useless. See issue #2532.

Starting with release 1.6 there is a separate properly-built source distribution in addition to the broken GitHub-generated one. For example, for release 1.6 you want saw-1.6-sources.tar.gz rather than the link that says “Source code” and downloads v1.6.tar.gz.

Installing Solvers

Unless you use one of the binary snapshots that comes with solvers, you will need to install your own. One easy way to do this is to download a what4-solvers binary snapshot. This includes all the external solvers SAW can use, and provides the versions that we are using upstream.

However, you can install your own copies in whatever way is convenient.

Be aware though that using either a newer or older version of any given solver can lead to regressions where given proofs stop working. This unfortunately happens more or less randomly. If you discover regressions with newer versions of solvers than we ship with what4-solvers, it will often make sense to report them to us and/or the upstream for the solver in question.

SAW requires the Z3 solver from Microsoft Research. In addition, it is capable of using the following other external solvers:

Note that the full picture of solver usage in SAW is considerably more complex than this (because among other things, there are also internal solvers); see the Using Solvers section for the full discussion.

Because each solver reacts differently to each problem, there is a strong tendency to eventually end up using all of them.

Installing the Python Bindings

The Python bindings for SAW are published on PyPI as the saw-client package. You can install this, or depend on it in your own project, using your favorite Python package management solution.

You can also install from the source tree using poetry as follows:

cd saw-python
poetry install

Using the Docker Images

The packages page of the GitHub repository contains prebuilt Docker images for SAW. These include both release images and a “nightly” image that is built from the current development version. All of these include solver executables and are ready to run.

These provide a simple way to get the current development version without having to build it, and are convenient if you are already using Docker.

Note that there are separate Docker images for the standalone SAW executable saw (for developments using SAWScript) and the server executable saw-remote-api used with the Python bindings for developments scripted using Python.

(And also note: there is a third image built from the SAW repository that you may see. It is called crux-mir-comp and provides an environment for running that tool, which is a version of Crux that uses some of SAW’s infrastructure on the back end. See the Crux documentation for further information.)

If you are verifying Rust code you will likely also want the Docker image for mir-json.

Building the Docker Images

You can, if desired, build the Docker images yourself. To do this, clone the repository as described above, including the git submodule init step, or download the sources; then run the following shell commands:

./build.sh gitrev
docker build -t saw -f saw/Dockerfile .
docker build -t saw-remote-api -f saw-remote-api/Dockerfile .

You can of course build either or both images as needed.