saw-script

[![Build Status](https://github.com/GaloisInc/saw-script/workflows/SAWScript/badge.svg)](https://github.com/GaloisInc/saw-script/actions?query=event%3Aschedule)

# SAW

This repository contains the code for SAW, the Software
Analysis Workbench.
SAW provides the ability to reason about
formal models describing the denotation of programs written in
languages such as C, Java, Rust, and Cryptol.

SAWScript is the scripting language that serves as the primary
user interface to SAW.
The repository is named after it for historical reasons.

## Documentation

There are two SAW tutorials that give an introduction to using the
SAWScript interpreter:

* [This tutorial](https://github.com/GaloisInc/saw-script/blob/master/doc/pdfs/llvm-java-verification-with-saw.pdf) gives an
  introduction to verifying C code (using LLVM) and Java code (using JVM).
* [This tutorial](https://github.com/GaloisInc/saw-script/blob/master/doc/pdfs/rust-verification-with-saw.pdf)
  gives an introduction to verifying Rust code (using MIR).

There is also a longer
[manual](https://github.com/GaloisInc/saw-script/blob/master/doc/pdfs/saw-user-manual.pdf)
that describes the breadth of SAW's features.

## Precompiled Binaries

Precompiled SAW binaries for a variety of platforms are available
on the [releases
page](https://github.com/GaloisInc/saw-script/releases).

## Docker Images

Alternatively, there is a Docker image available from the [packages
page](https://github.com/orgs/GaloisInc/packages/container/package/saw).

## Getting Z3

SAW can use many theorem provers, but because of its use of Cryptol it
always needs to have Microsoft Research's [Z3 SMT
solver](https://github.com/Z3Prover/z3) installed.  You can download Z3
binaries for a variety of platforms from their [releases
page](https://github.com/Z3Prover/z3/releases).
You can also download binaries for Z3 and other solvers from our
[what4-solvers](https://github.com/GaloisInc/what4-solvers/releases)
package.

We currently recommend Z3 4.8.10. If you plan to use path satisfiability
checking, you'll also need Yices version 2.6.1 or newer.

After installation, make sure that `z3` (or `z3.exe` on Windows)
is on your PATH.

## Cloning the Repository

After cloning the saw-script repository, you need to also clone
submodules.
Run `git submodule update --init`.
The commonly used `--recursive` option is not required, and also not
recommended as it results in cloning a considerable number of
additional unused subtrees.

## Downloading Release Sources

Starting with SAW 1.4, to download the sources for a release from the
[releases page](https://github.com/GaloisInc/saw-script/releases),
be sure to get the file `saw-<release>-sources.tar.gz` and not the
default GitHub-generated file `v<release>.tar.gz`.
The latter does not include SAW's submodules and is, alas, therefore
unbuildable.
(This is
[a GitHub problem](https://github.com/orgs/community/discussions/6003)
and there's no sign of it being likely to get fixed.)

For releases prior