Installing Stainless

General Requirement

  • Java 17 JRE It suffices to have headless OpenJDK JRE 17 (e.g. one that one gets with apt install openjdk-17-jre-headless on Debian/Ubuntu). Make sure that java -version reports a version starting with 1.17, such as openjdk version "1.17 or java version "1.17.

Stainless bundles Scala 3 compiler front-end and runs it before it starts compilation.

Running Code with Stainless dependencies

If you are debugging your scala code before running stainless on it (e.g. using a simple editor with scala-cli –watch), you can use this workflow with stainless as well; you just need to make sure that Stainless libraries are visible to the Scala compiler.

The simplest way is to use the release package, which contains stainless-cli script, a simple wrapper around scala-cli that adds the jar dependency on the compiled and source version of stainless library.

Building a jar:

You can package the Stainless library into a jar like this:

$ cd path/to/stainless/
$ sbt stainless-library/packageBin

Add the generated Stainless library jar file when invoking the compiler with scalac and the JVM with scala or java. For instance:

$ mkdir -p ~/.scala_objects
$ scalac -d ~/.scala_objects -cp /path/to/stainless/frontends/library/target/scala-3.3.3/stainless-library_3-X.Y.Z-A-BCDEFGHI.jar MyFile1.scala MyFile2.scala # and so on
$ scala -cp ~/.scala_objects:/path/to/stainless/frontends/library/target/scala-3.3.3/stainless-library_3-X.Y.Z-A-BCDEFGHI.jar MyMainClass

where X.Y.Z is the Stainless version and A-BCDEFGHI is some hash (which can be autocompleted by the terminal).

Using sources:

  1. Clone the sources from https://github.com/epfl-lara/stainless

  2. Create a folder to put compiled Scala objects: mkdir -p ~/.scala_objects

  3. Compile your code (here in MyFile.scala, though you can have more than one file) while referring to the Stainless library sources: scalac -d ~/.scala_objects $(find /path/to/stainless/frontends/library/stainless/ -name "*.scala") MyFile.scala

  4. Run your code (replace MyMainClass with the name of your main object): scala -cp ~/.scala_objects MyMainClass

External Solver Binaries

If no external SMT solvers (such as Z3 or cvc5) are found, Stainless will use the bundled Scala-based Princess solver

To improve performance, we highly recommend that you install the following two additional external SMT solvers as binaries for your platform:

You can enable these solvers using --solvers=smt-z3 and --solvers=smt-cvc5 flags.

Solver binaries that you install should match your operating system and your architecture. We recommend that you install these solvers as a binary and have their binaries available in the $PATH (as z3 or cvc5).

Note that somewhat lower version numbers of solvers should work as well and might even have different sets of soundness-related issues.

You can use multiple solvers in portfolio mode, as with the options --timeout=15 --solvers=smt-z3,smt-cvc5, where verification succeeds if at least one of the solvers proves (within the given number of seconds) each the verification conditions. We suggest to order the solvers starting from the one most likely to succeed quickly.

For final verification runs of highly critical software, we recommend that (instead of the portfolio mode) you obtain several solvers and their versions, then try a single solver at a time and ensure that each verification run succeeds (thus applying N-version programming to SMT solver implementations).

Install Z3 4.12.2

  1. Download Z3 4.12.2 from https://github.com/Z3Prover/z3/releases/tag/z3-4.12.2

  2. Unzip the downloaded archive

  3. Copy the z3 binary found in the bin/ directory of the inflated archive to a directory in your $PATH, eg., /usr/local/bin.

  4. Make sure z3 can be found, by opening a new terminal window and typing:

$ z3 --version

  1. The output should read:

Z3 version 4.12.2 - 64 bit`

Install cvc5 1.0.8

  1. Download cvc5 1.0.8 from https://github.com/cvc5/cvc5/releases/tag/cvc5-1.0.8 for your platform.

  2. Copy or link the downloaded binary under name cvc5 to a directory in your $PATH, eg., /usr/local/bin.

  1. Make sure cvc5 can be found, by opening a new terminal window and typing:

$ cvc5 --version | head

  1. The output should begin with:

This is cvc5 version 1.0.8

Build from Source on Linux & macOS

To build Stainless, we use sbt. In a typical configuration, sbt universal:stage in the root of the source tree should work, yet, in an attempt to be more reproducible and independent from SBT cache and path, the instructions below assume that the directory called stainless does not exist, they instruct sbt to use a relative path for its bootstrap, and do not require adding sbt to your path.

Install SBT

Follow the instructions at http://www.scala-sbt.org/ to install sbt 1.7.3 (or somewhat later version).

Check out sources

Get the sources of Stainless by cloning the official Stainless repository:

$ git clone --recursive https://github.com/epfl-lara/stainless.git
Cloning into 'stainless'...
$ cd stainless
$ git submodule update --init --recursive

Run SBT

The following instructions will invoke SBT while using a stainless sub-directory to download files.

$ sbt universal:stage

Where to find generated files

The compilation will automatically generate the bash script stainless-dotty.

You may want to introduce a soft-link from to a file called stainless:

$ ln -s frontends/dotty/target/universal/stage/bin/stainless-dotty stainless

Analogous scripts work for various platforms and allow additional control over the execution, such as passing JVM arguments or system properties:

$ stainless -Dscalaz3.debug.load=true -J-Xmx6G --help

Note that Stainless is organized as a structure of several projects. The main project lives in core while the Scala 3 frontend can be found in frontends/dotty. From a user point of view, this should most of the time be transparent and the build command should take care of everything.

Build from Source on Windows 10

Before following the infrequently updated instructions in this section, considering running Ubuntu on Windows 10 (through e.g. WSL2) and following the instructions for Linux.

Get the sources of Stainless by cloning the official Stainless repository. You will need a Git shell for windows, e.g. Git for Windows. On Windows, please do not use sbt universal:stage as this generates a Windows batch file which is unusable, because it contains commands that are too long for Windows. Instead, please use sbt stainless-dotty-standalone/assembly as follows:

$ git clone --recursive https://github.com/epfl-lara/stainless.git
Cloning into 'stainless'...
// ...
$ cd stainless
$ git submodule update --init --recursive
$ sbt stainless-dotty-standalone/assembly
// takes about 1 minutes

Running Stainless can then be done with the command: java -jar frontends\stainless-dotty-standalone\target\scala-3.3.3\stainless-dotty-standalone-{VERSION}.jar, where VERSION denotes Stainless version.

Running Tests

Stainless comes with a test suite. Use the following commands to invoke different test suites:

$ sbt test
$ sbt it:test

It’s also possible to run tests in isolation, for example, the following command runs Extraction tests on all files in termination/looping:

$ sbt 'it:testOnly *ExtractionSuite* -- -z "in termination/looping"'

Building Stainless Documentation

Stainless documentation is available at https://epfl-lara.github.io/stainless/ . To build the documentation locally, you will need Sphinx ( http://sphinx-doc.org/ ), a restructured text toolkit that was originally developed to support Python documentation.

  • On Ubuntu 18, you can use sudo apt install sphinx-common

The documentation resides in the core/src/sphinx/ directory and can be built using the provided Makefile. To do this, in a Linux shell, type make html, and open in your web browser the generated top-level local HTML file, by default stored in core/src/sphinx/_build/html/index.html. Also, you can open the *.rst documentation files in a text editor, as they are human-readable in their source form as well.

Note for project maintainers: to build documentation on GitHub Pages, use make gh-pages in the same Makefile, or adapt it to you needs.

Using IDEs with –no-colors option. Emacs illustration

Using command line option --no-colors asks stainless to produce clear 7-bit ASCII output with error messages in a standardized format:

FileName.scala:LineNo:ColNo: text of the error message

This helps IDEs to pick up line numbers and show error location in the source file.

In emacs editor, you can invoke ansi-term and compilation-shell-minor-mode. Then, run

stainless --no-colors <InputFilesAndOptions>

You may also consider using the --watch option.

You should now be able to click on a message for verification condition to jump to the appropriate position in the appropriate file, as well as to use emacs commands previous-error and next-error to navigate through errors and other verification-condition outcomes.

Here is a very simple illustration that introduces an interactive comp-ansi-term command that creates new window with ansi-term and minor compilation mode:

(setq comp-terminal-current-number 1)
(defun create-numbered-comp-terminal ()
  (ansi-term "/bin/bash")
  (rename-buffer (concat "q" (number-to-string comp-terminal-current-number)) 1)
  (setq comp-terminal-current-number (+ comp-terminal-current-number 1))
  (compilation-shell-minor-mode)
)
(defun comp-ansi-term (arg)
  "Run ansi-term with bash and compilation-shell-minor-mode in buffer named q_N for increasing N" (interactive "P")
  (create-numbered-comp-terminal)
  (split-window-vertically)
  (previous-buffer)
  (other-window 1)
)

The following globally binds the above command to the F3 key and binds F7 and F8 to commands for navigating reports:

(global-set-key [f3] 'comp-ansi-term)
(global-set-key [f7] 'previous-error)
(global-set-key [f8] 'next-error)

For more information, please consult the documentation for emacs.