Skip to content

Home

Jump to bottom
Marco Eilers edited this page Apr 17, 2023 · 9 revisions

Getting Started with Viper

This wiki introduces the Viper toolset, and in particular gives instructions on how to set up and experiment with the various tools. For a general overview of Viper, please see our home page, and our list of repositories on GitHub.

For the best interactive experience, try the Viper plugin for Visual Studio Code. If you want to quickly try Viper without installing it, check out the Viper Online section. If you need to develop Viper, or if you want to be sure to use the latest version, refer to the Source Compilation section.

Viper Plugin for Visual Studio Code

To install the Viper plugin for Visual Studio Code follow the instructions at http://www.pm.inf.ethz.ch/research/viper/downloads.html.

Alternativelly, refer to the plugin's repository or to the plugin's page on Visual Studio's Marketplace.

For step-by-step instructions regarding how to install or use the plugin, refer to https://github.com/viperproject/viper-ide/wiki.

Viper Online

You can see examples and experiment immediately with the Viper tools at Viper Examples Online.

Source Compilation

For general use we recommend compiling the tools from source. The Viper tools are written in Scala, and are compiled using SBT. Compilation should work on all major platforms (Windows/Mac/Linux). In all cases, you will need a version of SBT on your machine, as well as a recent version of Java (Version 11 or newer).

You will need to set up one (or both) of our two backend verifiers, Silicon and Carbon, along with its dependencies. The instructions for setting up the individual projects are described below.

Installation Requirements

Common Dependencies

1. Java JRE (or Java JDK for developers)

The tested and recommended version to use is Java 11.

2. SBT

Windows Linux Mac OS X
Instructions Instructions Instructions

3. Z3

Viper is tested with Z3 version 4.8.7. Other versions may also work, but could exhibit worse performace. There are two options to install Z3:

  • Obtain a stable Z3 pre-compiled binary from the Z3 GitHub repository (recommended).

  • Alternatively, obtain the Z3 source code from the Z3 GitHub repository and build Z3.

The Viper intermediate language

For historical reasons, the component that defines the Viper intermediate language -- including its parser, typechecker, AST -- is called "Silver". It is used as a library by the Viper backends (Silicon and Carbon). Usually, it is not useful to clone or compile Silver independently (i.e., without one of the backend verifiers); thus, for most purposes, we recommend skipping this section and directly installing a backend (which will install Silver as a dependency).

Dependencies

Compilation

  • Obtain the Silver source code. Checkout the Silver GitHub repository. Place the contents in a silver subdirectory of your Viper directory.
$ mkdir silver
$ cd silver
$ git clone https://github.com/viperproject/silver/ .
  • From a command-prompt, run sbt compile in your silver subdirectory. You may need an internet connection, to allow SBT to download any dependencies. This should result in a successful compilation.
$ cd silver
$ sbt compile
  • You can run some basic regressiont tests with sbt test in the same silver subdirectory. There should be no test failure. However, most tests are run via one of the two backend verifiers, Silicon and Carbon 
$ cd silver
$ sbt test

Usage

Silver is typically used in conjunction with one of the backend verifiers, Silicon and Carbon.

The Silicon Backend

Silicon is a verifier based on symbolic execution.

Dependencies

Compilation

  • Obtain the Silicon source code. Checkout the Silicon GitHub repository along with its submodule Silver. Place the contents in a silicon subdirectory of your Viper directory.
$ mkdir silicon
$ cd silicon
$ git clone --recursive https://github.com/viperproject/silicon .
  • From a command-prompt, run sbt compile in your silicon subdirectory. You may need an internet connection, to allow SBT to download any dependencies. This should result in a successful compilation of both Silver and Silicon.
$ sbt compile

  • In order to run Silicon, you need to specify the location of an appropriate Z3 executable. You can do this via setting an environment variable Z3_EXE, or by passing --z3Exe <path to z3> as a command line option (which overrides any environment variable) to Silicon. In order to run the test suite via SBT, we recommend the environment variables approach.

  • You can run the Silicon regression tests with sbt test in the same silicon subdirectory. This will compile Silicon, run the test suite and analyse the results. There should be no test failure. The test suite can be found in ../silver/src/test/resources/.

$ sbt test
  • You can build a .jar file, containing all necessary dependencies, by running sbt assembly in the same silicon subdirectory (this is only necessary if you want to use Silicon as a plugin for other tools).
$ sbt assembly

Usage

  • You can run Silicon via SBT by running sbt "run [options] <path to Viper file>".

  • Alternatively, you can run individual tests by running sbt test-only -- -n <path to Viper file>.

  • Silicon also comes with a batch file that you can use to run Silicon on Windows by running silicon.bat [options] <path to Viper file>.

  • Finally, you can also run Silicon from Visual Studio Code.

The Carbon Backend

Carbon is a verifier based verification condition generation (via an encoding into Boogie).

Dependencies

Boogie is an intermediate language implemented in C# by Microsoft Research. Compiling it requires the .NET Core SDK. For the Viper release 01/2023 we recommend Boogie version 2.15.9: https://github.com/boogie-org/boogie/releases/tag/v2.15.9 .

However, Carbon may also work with older or newer versions of Boogie.

The compiled Boogie binary on Mac and Linux is given by Source/BoogieDriver/bin/Release/${FRAMEWORK}/BoogieDriver and on Windows it is given by Source/BoogieDriver/bin/Release/${FRAMEWORK}/BoogieDriver.exe. ${FRAMEWORK} indicates which version of .NET Core is used.

Compilation

  • Obtain the Carbon source code. Checkout the Carbon GitHub repository along with its submodule Silver. Place the contents in a carbon subdirectory of your Viper directory.
$ mkdir carbon
$ cd carbon
$ git clone --recursive https://github.com/viperproject/carbon .
  • From a command-prompt, run sbt compile in your carbon subdirectory. You may need an internet connection, to allow SBT to download any dependencies. This should result in a successful compilation.
$ sbt compile

  • In order to run Carbon, you need to specify the location of appropriate Z3 and Boogie executables. You can do this via setting the environment variable Z3_EXE and BOOGIE_EXE, or by passing --z3Exe <path to z3> and --boogieExe <path to boogie> as a command line options (which override any environment variable) to Carbon. In order to run the test suite via SBT, we recommend the environment variables approach.

  • You can run the Carbon regressiont tests with sbt test in the same carbon subdirectory. This will compile Carbon, run the test suite and analyse the results. There should be no test failure. The test suite can be found in ../silver/src/test/resources/.

$ sbt test
  • You can build a .jar file, containing all necessary dependencies, by running sbt assembly in the same carbon subdirectory (this is only necessary if you want to use Carbon as a plugin for other tools).
$ sbt assembly

Usage

  • You can run Carbon via SBT by running sbt "run [options] <path to Viper file>".

  • Alternatively, you can run individual tests by running sbt test-only -- -n <path to Viper file>.

  • Carbon also comes with a batch file that you can use to run Carbon on Windows by running carbon.bat [options] <path to Viper file>.

  • Finally, you can also run Carbon from Visual Studio Code.

Clone this wiki locally