Running SAW

There are two almost completely different top-level ways to run SAW, and as hinted at in the previous sections they are even separate executables.

The default way to use SAW is with its native setup and tactic scripting metalanguage called SAWScript. For this approach you use the saw executable.

The other way is to use Python as the scripting language. This involves more moving parts; the Python bindings connect over a JSON-based RPC protocol to a server process. This requires first starting the saw-remote-api executable. Then your (separate) Python script talks to the running saw-remote-api process. SAW can then be used from your choice of Python environments, allowing for example the use of notebooks and other similar interfaces.

Invoking saw

The most common way to run saw is by running it on a file of SAWScript code:

saw myproofs.saw

If you leave the file name off, or give the -I option, SAW will instead start an interactive read-eval-print loop (“REPL”) that you can use for experimentation.

Like many such interfaces, the SAW REPL contains, in addition to the ordinary SAWScript operations, REPL-specific commands that are written beginning with a colon (:). If you have a file of REPL commands that you want to run, you can do that with the -B (“batch”) option.

The most common colon-commands are :help (or :h or :?) which you can use to retrieve the type and help text for a SAWScript command, and :search, which lets you look for SAWScript commands by their SAWScript types.

Invoking saw with Docker

The Docker container for saw is a wrapper around the saw executable, so saw is the default entry point.

The simplest way to run the docker container (on a file called myproofs.saw) is like this:

docker run --rm -v .:/work -w /work \
   ghcr.io/galoisinc/saw:nightly myproofs.saw

This fetches the container image from GitHub, and runs it transiently (with the --rm argument). The -v and -w arguments bind your current working directory to the directory /work within the container, and makes that the current working directory inside. This allows SAW to find your file myproofs.saw.

If you built the container locally and called it saw, you can run that instead like this:

docker run --rm -v .:/work -w /work saw myproofs.saw

You can pass options to the saw executable by including them before the filename, and you can pass environment variables by using the -e option of docker run.

Like with the standalone saw executable, if you don’t pass a filename it will start the REPL. If you want to do that, you’ll also want the -i and -t flags to docker run so you can type into it and so the line editing works. Thus:

docker run -i -t --rm -v .:/work -w /work ghcr.io/galoisinc/saw:nightly

or

docker run -i -t --rm -v .:/work -w /work saw

If you want to start a shell inside the container to look around, instead of running the SAW executable, you can use --entrypoint /bin/sh.

You can also create and start a non-transient container image with docker run and then run SAW from it using docker exec. For more information about using Docker, consult its documentation or one of the many tutorials available on the internet.

saw Options

Common options include:

-h or --help

Show the command-line options summary.

-V or --version

Print the SAW version and exit.

-s file or --summary=file

Write a verification summary to the given file.

-f pretty or --summary-format=pretty

Generate a human-readable verification summary. (The default is JSON.)

--detect-vacuity

Check for specifications whose precondition is unsatisfiable. This defaults to off because it can be expensive and is rarely needed, but can be very helpful if one becomes suspicious that some of one’s specifications are wrong.

--no-color

Disable terminal colors, non-ASCII output, and other terminal control codes.

-i dirs

Add dirs to the search path for SAWScript includes. dirs may be multiple directory names.

Commonly used environment variables include:

CRYPTOLPATH=dirs

Specify the search path used for Cryptol imports, as with Cryptol.

SAW_IMPORT_PATH=dirs

Specify the search path used for SAWScript includes.

SAW_SOLVER_CACHE_PATH=dir

Tells SAW to keep a cache of solver results in the specified directory.

Multiple directory names should be separated by colons on Unix and semicolons on Windows, per standard usage on those platforms.

These options are used with Java verification:

-b dirs or --java-bin-dirs=dirs

Add dirs to the search path used to find a Java executable. dirs may be multiple directory names.

-c dirs or --classpath=dirs

Add dirs to the Java class path. dirs may be multiple directory names.

-j dirs or --jars=dirs

Add dirs to the Java JAR list. dirs may be multiple directory names.

These environment variables are used with Java verification:

SAW_JDK_JAR

Specify the path of the .jar file containing the core Java libraries. Only needed if SAW cannot discover the location by finding a Java executable.

CLASSPATH

Specify the search path for Java class files. Can include .jar files as well as directories.

See the REPL reference for the complete list of supported options and environment variable settings.

Invoking saw-remote-api

There are several ways to run the remote API server.

The simplest way is to just make sure saw-remote-api is on your $PATH and run your Python scripts. The Python bindings code will find and run it as a subprocess in each script. You can also set the environment variable $SAW_SERVER to point to the executable.

You can, however, also run it as a standalone server. Run the following:

saw-remote-api http --host 127.0.0.1 --port 8080 saw

then before running your Python run the following:

export SAW_SERVER_URL=http://localhost:8080/saw/

where you can set the port number (here 8080) and the endpoint name (here saw) on both ends to anything you like within reason.

If you are using Docker, you might do this:

docker run --name=saw-remote-api -v somedir/myfiles:/home/saw/myfiles -p 8080:8080 galoisinc/saw-remote-api:nightly

and

export SAW_SERVER_URL=http://localhost:8080/

This runs the server in its Docker container, exports its socket to the host machine, and shares the myfiles directory.

Note: the Docker container’s port is wired to 8080, and the endpoint is /.

While in principle you can run either or both of these in the background (with & in the shell, or the -d detach option in Docker), currently there is a strong tendency for SAW errors and messages to accidentally print to the saw-remote-api terminal instead of being sent across the RPC connection. (Such cases are bugs; feel free to report any you encounter.)

Also, occasionally it has been known to abort on error, in which case being able to restart it easily is helpful. (Such cases are serious bugs; please report any you encounter.)

Common saw-remote-api Options

-h or --help

Show the command-line options summary.

-v or --version

Print the SAW version and exit.

--max-occupancy num

Set the maximum number of sessions allowed at once. The default is 1.

--no-evict

Don’t evict sessions if the server is full.

The following option can be given after the http verb on the command line when running in HTTP mode.

--tls

Enable HTTPS mode, that is, encrypt the network connection.