diff --git a/wiki/docker/viperproject_-_viperserver.md b/wiki/docker/viperproject_-_viperserver.md new file mode 100644 index 0000000..8a83730 --- /dev/null +++ b/wiki/docker/viperproject_-_viperserver.md @@ -0,0 +1,37 @@ +# viperproject - viperserver + +This is a [Docker](/wiki/docker.md) container for a [Viper](/wiki/programming_language/viper.md) +server, which is used for building the Viper verifiers +[Silicon and Carbon](/wiki/programming_language/viper.md#setup). +The official container and documentation was made by +[viperproject](https://hub.docker.com/r/viperproject/viperserver). + +## Set-up + +Create the file `rebuild.sh`. +Change the settings according to your needs and run `./rebuild.sh` afterwards. +Due to this container being used to build the Silicon and Carbon verifiers it is recommended to be +started in interactive mode as demonstrated in the [rebuild section](#rebuildsh). +Make sure to substitute `` and ``. +If only one of them is to be built, omit the other. +Additionally the version of viperproject has to be added for ``. +It also depends on the Z3 version which will be used later. +For example the version `v4_z3_4.8.7` is working for Z3 versions `4.8.7` and later. + +## Volumes + +Set the following volumes with the -v tag. + +| Outside mount/volume name | Container mount | Description | +| ------------------------- | --------------- | ----------------------------------------- | +| `` | `/mnt/silicon` | (optional) mount Silicon for installation | +| `` | `/mnt/carbon` | (optional) mount Carbon for installation | + +## rebuild.sh + +```sh +docker run -it --name viperserver \ + -v :/mnt/silicon \ + -v :/mnt/carbon \ + viperproject/viperserver: +``` diff --git a/wiki/programming_language/viper.md b/wiki/programming_language/viper.md new file mode 100644 index 0000000..68a934f --- /dev/null +++ b/wiki/programming_language/viper.md @@ -0,0 +1,87 @@ +# Viper + +[Viper](https://www.pm.inf.ethz.ch/research/viper.html) is a verification language among other +tools. + +## Setup + +For the Viper language to work a verifier needs to be set up. +The two possibilities are [Carbon](https://github.com/viperproject/carbon) and +[Silicon](https://github.com/viperproject/silicon). + +This section explains the installation for [Linux-based systems](/wiki/linux.md), but they are also +available for [Windows](/wiki/windows.md) systems though the steps to setup differ. +For this navigate download the code from [Silicons Github](https://github.com/viperproject/silicon) +and/or [Carbon Github](https://github.com/viperproject/carbon). + +There are some dependencies. +For both Carbon and Silicon to work correctly Z3 has to be installed. +This can easily be done, for example by installing the `z3` package, which is available from +various [package managers](/wiki/linux/package_manager/pacman_and_aur.md). +For Carbon Boogie has to be installed too. +This is best done by installing a .NET SDK which is often packaged in a package called `dotnet-sdk` +or a similar named one. +Afterwards boogie can be installed using the following command. + +```sh +dotnet tool install -g boogie +``` + +Afterwards the building of Silicon and/or Carbon can follow. + +The easiest way to build one or both verifiers locally is creating a `.jar` file via +[Docker](/wiki/docker.md) using the +[viperproject image](/wiki/docker/viperproject_-_viperserver.md). + +Start the Docker container as explained in the +[corresponding wiki entry](/wiki/docker/viperproject_-_viperserver.md). +Make sure to change the setting as described. +Then in the Docker container build Silicon by running the following commands. + +```sh +cd /mnt/silicon +sbt assembly +``` + +For Carbon similarly run the following commands. + +```sh +cd /mnt/carbon +sbt assembly +``` + +Afterwards leave the Docker container. +It is no longer needed. + +The `.jar` files are now available in `/target/scala-/carbon.jar` or +`/target/scala-2.13/silicon.jar` and are ready to be used outside the docker +container from the host machine. + +Afterwards Carbon and/or Silicon are ready to be [used](#usage). + +## Usage + +This section addresses the usage of Viper. + +### Basic Verifier Usage + +After [Silicon](https://github.com/viperproject/silicon) and/or +[Carbon](https://github.com/viperproject/carbon) have been setup according to the +[setup section](#setup), they can be used. + +For Silicon run the following command. +`` describes the path of the Silicon jar which was set in the [setup](#setup). +`` is the path to the Viper file to verify. + +```sh +java -jar +``` + +For Carbon run the following command. +`` describes the path of the Carbon jar which was set in the [setup](#setup). +`` is the path to the Z3 binary (for example `/bin/z3`) and `` is the +path to the boogie binary (for example `~/.dotnet/tools/boogie` when set up with .NET). + +```sh +java -jar --z3Exe --boogieExe +```