Skip to content

Home

Jump to bottom
Fábio Pakk Selmi-Dei edited this page Mar 25, 2020 · 6 revisions

Welcome to the Viper-IDE User Documentation

Viper-IDE is a visual environment for developing and verifying programs in the Viper language. It is built as an extension of Microsoft's Visual Studio Code, on top of the Viper command line tools.

Table of Contents

[TOC]

Installation

Further we assume that Java Runtime Environment is installed and the java command is accessible in the default environment. Make sure to have Java 8 (preferably with the JavaServer component installed). Both Oracle JDK and OpenJDK are supported.

Installing Viper-IDE with binary packages

This step requires administrative access to your system.

  1. Unzip the binary packages archive into a folder named Viper in the local programs directory on your system:

    • On Windows, the files should be unzipped into %programfiles%/Viper, where the prefix is the same as for the VS Code installation. Usually it is set to C:\Program Files (x86) on a recent Windows distribution.

      For example, if you have an English installation of 64-bit Windows 10, the location will be C:\Program Files\Viper.

    • On Linux and Mac OS X, the location is /usr/local/Viper.

  2. Install the latest version of Visual Studio Code: https://code.visualstudio.com/Download

  3. Run VS Code, open the extensions interface (View→Extensions), and search for an extension called Viper. After the Viper extension is installed, click Enable and agree to restart the VS Code application.

  4. Viper-IDE will be activated once a .vpr file is opened.

    If something went wrong, continue reading.

Depending on the OS, we assume that the prefix for binary dependencies (%ViperTools%) is:

  1. On Windows, whatever the value of the %programfiles%\Viper variable is.
  2. On the Mac, /usr/local/Viper.
  3. On Linux, /usr/local/Viper.

The proposed file structure in this location includes the following files:

  • %ViperTools%/z3/bin/z3 (used on Linux and Mac)
  • %ViperTools%/z3/bin/z3.exe (used on Windows)
  • %ViperTools%/boogie/Binaries/Boogie.exe (used on Windows and Linux)
  • %ViperTools%/boogie/Binaries/Boogie (used on the Mac)
  • %ViperTools%/nailgun/nailgun.jar (Nailgun Server)
  • %ViperTools%/nailgun/ng (Nailgun Client for Linux and Mac)
  • %ViperTools%/nailgun/ng.exe (Nailgun Client for Windows)
  • %ViperTools%/graphviz/bin/dot (used on Linux and Mac)
  • %ViperTools%/graphviz/bin/dot.exe (used on Windows)
  • %ViperTools%/backends/silicon.jar
  • %ViperTools%/backends/carbon.jar
  • %ViperTools%/backends/infer.jar

These paths will be automatically configured when the extension is installed through the VS Code Marketplace. If necessary, you may customize them in the User Settings.

Installing Viper-IDE with package managers

TODO: document the steps for installing Viper-IDE via package management systems.

Working with Viper-IDE

  1. After the first launch on Windows, you will be asked for restarting the IDE. Press Restart Now.

    Restart Now button

  2. After restarting, Viper-IDE shows an empty file. You can either type your new Viper program in it, or open an existing one (as a separate .vpr file, or as a project folder containing any number of .vpr files).

    2.png

  3. In this demo, we open the main.vpr file from the viper-example-project folder, which is located in the same archive as the portable distribution. Verification starts automatically, and we get the verification failure as a result.

    Note: due to a known bug (issue #16) in the extension, the current MacOS X app requires manually starting verification after opening a new file and after selecting a verification back end.

    3.png

  4. In order to get the message from the verifier, one could hover the cursor over the erroneous part of the source code (underlined with the red squiggly line), as shown on the picture below.

    4.png

  5. The list of all verification results could be accessed through the 52.png button. The list will appear at the top of the window. Clicking on a verification result will shift the focus towards the corresponding error in the sources.

    5.png

  6. One could get the complete list of supported commands by typing viper in the command palette (View→Command Palette...). Currently we support 3 commands:

    1. select verification back end — two back ends are supported: Silicon (default, based on symbolic execution) and Carbon (based on Microsoft Boogie).
    2. stop the running verification — especially useful for long-running examples or non-terminating verification, e.g., caused by matching loops.
    3. verify the opened document — manual verification.

    6.png

  7. Selecting a back end automatically invokes a new verification of the current file.

    7.png

  8. Sometimes, the verification back end generates an unparsable output which might cause the extension to detect an Internal error or even crash. In order to get the full information from the system, one should set the maximum logging depth in the user settings. This could be done with the following steps:

    1. Open the command palette (View→Command Palette...).
    2. Start typing Settings.
    3. Select the following command: Preferences: Open User Settings.
    4. This will open two editor panels side-by-side. The left one contains default settings and is non-modifiable, whereas the right one in for user-specific settings.
    5. Find the following setting: viperSettings.logLevel and change its value from 1 to 5. The new settings are active immediately after they are saved.
    6. Close the settings and return to the problematic example.
    7. Open the extension's output panel (View→Toggle Output).
    8. Select the output Viper from the list on the right of the panel, as shown on the picture below.

    9.png

Clone this wiki locally