Skip to content

Home

Jump to bottom
Aurel edited this page Mar 9, 2021 · 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 Bitbucket.

If you want to quickly try Viper without installing it, check out the Viper Online section. For the best interactive experience, try the Viper plugin for Visual Studio Code. If you just need a command line version of the tool, refer to the Binary Packages 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 Online

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

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://bitbucket.org/viperproject/viper-ide/wiki/Home.

Binary Packages

Ubuntu Linux 64bit

For Ubuntu Linux, we have a repository from which you can install Viper tools. The repository is still in beta, please report all problems at the issue tracker.

  1. Add our public key to the known key list:

     wget -c http://pmserver.inf.ethz.ch/viper/debs/xenial/key.asc -O /tmp/key.asc
 sudo apt-key add /tmp/key.asc

  2. Add the repository to the repositories list:

     echo 'deb http://pmserver.inf.ethz.ch/viper/debs/xenial /' | sudo tee /etc/apt/sources.list.d/viper.list

  3. Update the package list and install Viper:

     sudo apt-get update
 sudo apt-get install viper

  4. Test:

     echo 'field a: Int' > /tmp/test.sil
 silicon /tmp/test.sil

If you want to use Carbon, you need to install Mono additionally:

sudo apt-get install mono-complete

Mac OS X

For Mac OS X, we have a Homebrew tap. The tap is still in beta, please report all problems at the issue tracker.

  1. Install Mono.

  2. Enable tap:

     brew tap vakaras/viper

  3. Install Viper:

     brew install viper

  4. Test:

     echo 'field x: Int' >> test.sil
 silicon test.sil

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.

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

It is recommended to install the Viper tools as project-named subfolders under a common Viper directory. For example, a directory for the Viper tools might include subdirectories named silver, silicon, carbon, etc. The instructions below assume that you have chosen such a top-level Viper folder.

Common Dependencies

1. Java JRE (or Java JDK for developers)

The tested and recommended version to use is Java 8.

2. SBT

Windows Linux Mac OS X
Instructions Instructions Instructions

3. Mercurial

Windows Linux Mac OS X
Instructions Instructions Instructions

4. Z3

There are three options:

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

  • Alternatively, obtain a nightly Z3 pre-compiled binary from the Z3 GitHub repository (not recommended).

  • Alternatively, obtain the Z3 source code from the Z3 GitHub repository and build Z3 (not recommended).

Linux

$ mkdir z3 
$ cd z3
$ git clone https://github.com/Z3Prover/z3.git .
$ mkdir build
$ cd build
$ make
$ make install PREFIX=/usr/local

Mac OS X

$ mkdir z3
$ cd z3
$ git clone https://github.com/Z3Prover/z3.git .
$ CXX=clang++ CC=clang python scripts/mk_make.py
$ mkdir build
$ cd build
$ make
$ sudo make install

Warning: do not use Z3 4.1.1 because it contains an unsoundness bug. It is recommended to use the latest version of Z3 (currently 4.8.3).

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).

Dependencies

Compilation

  • Obtain the Silver source code. Checkout the Silver Bitbucket repository. Place the contents in a silver subdirectory of your Viper directory.
$ mkdir silver
$ cd silver
$ hg clone https://bitbucket.org/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 Bitbucket repository. Place the contents in a silicon subdirectory of your Viper directory.
$ mkdir silicon
$ cd silicon
$ hg clone https://bitbucket.org/viperproject/silicon .
  • From the silicon subdirectory, create a symbolic link to the directory where you installed silver. On Linux and Mac OS X, type:
$ ln -s ../silver
  • On Windows, type:
$ mklink /D silver ..\silver
  • 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.
$ 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 regressiont 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/2021 we use the commit: https://github.com/boogie-org/boogie/commit/bae82d3a7b383161f1c42312555cc9548ce23733 (which is built using .NET Core Version 3.1). Boogie can be compiled as follows (on Windows, Mac, and Linux), assuming .NET Core is included in the Path environment variable:

dotnet build -c Release Source/Boogie.sln

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. If .NET Core 3.1 is used, then ${FRAMEWORK} is given by netcoreapp3.1.

If compilation leads to an error due to something related to "GitVersion", then set the environment variable BOOGIE_NO_GITVERSION to 1.

Compilation

  • Obtain the Carbon source code. Checkout the Carbon Bitbucket repository. Place the contents in a carbon subdirectory of your Viper directory.
$ mkdir carbon
$ cd carbon
$ hg clone https://bitbucket.org/viperproject/carbon .
  • Create a symbolic link to the directory where you installed silver. On Linux and Mac OS X, type:
$ ln -s ../silver
  • On Windows, type:
$ mklink /D silver ..\silver
  • 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