Command Line Reference

This chapter documents the command-line interfaces of the saw and saw-remote-api executables in full detail.

saw Command Line

There are three ways to run the saw executable:

  • saw [options] : runs the interactive REPL.

  • saw [options] filename.saw : loads and runs the SAWScript proof logic in the given filename.

  • saw [options] -B filename.isaw : loads and runs the filename as a series of REPL commands.

The -I option forces REPL mode, even if a filename is given. Any such filename is ignored. There is, for the time being at least, no easy way to first load a file and then enter the REPL. (The best way to do that is to start the REPL and then load the file manually with include. Another way is to add the experimental command subshell to the end of the file.)

The -I and -B options cannot be used together.

Files loaded with the -B option can contain REPL :-commands. However, because the file is fed into the system one line at a time, as if each line were typed separately, each line must be syntactically complete. The adjustments and affordances in the REPL meant for interactive use are also engaged, which can in some cases produce unexpected results. In general the -B option is mostly useful for testing SAW.

The -B option can also be spelled --batch and the -I option can also be spelled --interactive.

A number of the following options take lists of filenames and/or directories. Per convention, on Unix (including MacOS) these lists are delimited by colons; on Windows, use semicolons.

The following additional options are available:

-b list, --java-bin-dirs=list

Specify a list of directories to search for a Java executable. If this option is not given, the PATH environment variable will be used instead.

-c list, --classpath=list

Specify a list of directories to search for Java classes. If multiple -c options are found, the lists given are concatenated in the order seen on the command line. The CLASSPATH environment variable is also used; its contents go on the search path last. (That is, directories given with -c are searched before directories in CLASSPATH.)

--clean-mismatched-versions-solver-cache[=dir]

Run the clean_mismatched_versions_solver_cache command on the solver cache in the given directory. If no directory is given, the SAW_SOLVER_CACHE_PATH environment variable is used to find the solver cache. After cleaning out the cache, exit. See Caching Solver Results for a description of the clean_mismatched_versions_solver_cache command and the solver caching feature in general.

-d num, --sim-verbose=num

Set the verbosity level of the LLVM/Java/MIR symbolic simulator.

--detect-vacuity

Check for contradictory assumptions. This is not the default because it can be expensive and is rarely needed.

-f format, --summary-format=format

Set the output format for the verification summary generated with -s. The recognized formats are json and pretty; the default is json. pretty is intended to be more human-readable.

-h, --help, -?

Print a usage message. This lists all the available options.

-i list, --import-path=list

Specify a list of directories to search for SAWScript includes. If multiple -i options are found, the lists given are concatenated in the order seen on the command line. The SAW_IMPORT_PATH environment variable is also used; its contents go on the search path last. (That is, directories given with -i are searched before directories in SAW_IMPORT_PATH.)

-j list, --jars=list

Specify a list of paths to .jar files to search for Java classes. The search ordering of .jar files given with -j relative to .jar files given with -c or in the CLASSPATH environment variable is not specified.

--no-color

Disable terminal colors and also Unicode character output.

--output-locations

Print the current SAWScript source location with every output message. This feature is eventually intended to be replaced with a more helpful tracing facility.

-s filename, --summary=filename

Write a verification summary to the given file after all proofs are done.

-t, --extra-type-checking

Perform extra type checking of intermediate values. This option no longer does anything and will be removed eventually.

-T, --timestamping

Add a timestamp to messages printed during execution.

-v num, --verbose=num

Set the verbosity level of the SAWScript interpreter. Recognized verbosity levels range from 0 to 5, and the default is 4. This option is eventually intended to be replaced with a more directed scheme for controlling the output of different operations and subsystems.

-V, --version

Show the version of the SAWScript interpreter.

saw Environment Variables

The following environment variables also affect saw.

Some of these hold lists of filenames and/or directories. Per convention, on Unix (including MacOS) these lists are delimited by colons; on Windows, use semicolons.

CLASSPATH

Specify a list of directories to search for Java classes. Note that paths can also be specified using the -c (aka --classpath) command-line option. Paths given with -c take priority.

CRYPTOLPATH

Specify a list of directories to search for Cryptol imports (including the Cryptol prelude).

PATH

If the --java-bin-dirs option is not given, then the PATH will be searched to find a Java executable.

SAW_IMPORT_PATH

Specify a list of directory paths to search for imports. Note that paths can also be specified using the -i (aka --import-path) command-line option. Paths given with -i take priority.

SAW_JDK_JAR

Specify the path of the .jar file containing the core Java libraries. This is only necessary if a Java executable is not found on the PATH or via the --java-bin-dirs option.

SAW_SOLVER_CACHE_PATH

Specify a path at which to keep a cache of solver results obtained during calls to certain tactics. A cache is not created at this path until it is needed. See Caching Solver Results for further information.

saw-remote-api Command Line

The general form of the saw-remote-api command line is one of:

  • saw-remote-api -h : Print the command-line usage text and exit. -h can also be spelled --help and -? is also accepted.

  • saw-remote-api -v : Print the SAW version and exit. -v can also be spelled --version.

saw-remote-api doc

Dump out the API documentation text.

saw-remote-api mode -h

Print the usage text for the given mode. -h can also be spelled --help.

saw-remote-api [overall-options] mode [mode-options] [mode-args]

Run the remote API server in the given mode.

The available modes are stdio, socket, and http.

Overall Options

The following options are accepted in any mode:

--log destination

Enables fairly verbose connection logs. The destination should be either a filename or the magic string stderr to print to saw-remote-api’s standard error.

--read-only

Avoids generating any output files. Useful if running on a read-only file system. By default saw-remote-api saves state to disk so server crashes don’t lose client context.

--max-occupancy num

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

--no-evict

Don’t evict old sessions if someone connects when the server is full.

stdio mode

saw-remote-api stdio communicates over stdin and stdout.

The only mode-option for stdio mode is -h. There are no mode-args.

socket mode

In socket mode saw-remote-api communicates over a socket using a simple “netstrings” protocol wrapping the basic JSON packets.

The Python bindings will run saw-remote-api in socket mode by default if not pointed to another location.

The mode-options for socket mode (besides -h) are:

--session session-name

Serve as the named session session-name. Fails if there’s already a server for that session.

--host hostname

Set the listen hostname or interface address. On multihomed machines, listening on specific addresses allows accepting connections from some networks and not others. To listen for connections from anywhere, use 0.0.0.0 or ::. To restrict connections to the same machine, use 127.0.0.1 or ::1. The default is ::1.

--port port

Set the listen port number. If no explicit port is selected saw-remote-api lets the OS pick one. In any case the port number is printed to standard output during startup.

Socket mode uses no mode-args.

http mode

In HTTP mode saw-remote-api communicates over a socket using both HTTP and “netstrings” to wrap the basic JSON packets.

The mode-options for HTTP mode (besides -h) are:

--tls

Enable TLS (transport layer security, aka more-modern SSL) and run over HTTPS. Setting the environment variable TLS_ENABLE has the same effect.

--session session-name

This option is recognized but not supported for HTTP.

--host hostname

Set the listen hostname or interface address. On multihomed machines, listening on specific addresses allows accepting connections from some networks and not others. To listen for connections from anywhere, use 0.0.0.0 or ::. To restrict connections to the same machine, use 127.0.0.1 or ::1. The default is 0.0.0.0. Note that this is different from socket mode.

--port port

Set the listen port number. If no explicit port is selected the default is 8080.

In HTTP mode one mode-arg must be provided: the name of the HTTP endpoint to serve the protocol on. For example, saw-remote-api http --host 127.0.0.1 /foo will respond to requests made to http://127.0.0.1:8080/foo.

saw-remote-api Environment Variables

Warning

This section is under construction!