Skip to content

Getting Started

Jump to bottom
Malte Schwerhoff edited this page Jun 27, 2021 · 6 revisions

Changelog:

  • 27.06.2021: Java 11 works, as might newer versions; Z3 4.8.6 is known to work
  • 03.01.2020: Removed outdated "Development" section; Minor updates of remaining text
  • 28.09.2015: The latest Sbt version (0.13.9) seems to work with Java 8
  • Currently (4.3.2015), Sbt still requires Java 7, it is not yet compatible with Java 8.

Downloading and setting up Silicon

General instructions (instructions for Linux can be found here):

  1. Check out the Silver & Silicon projects
  2. Download and install Z3 4.8.6 (https://github.com/Z3Prover/z3).
  3. Per default, Silicon assumes that Z3 (z3 or z3.exe) is in the path. If the environment variable Z3_EXE is set, then Silicon will use the executable that it points to. As a third option, you can also specify the Z3 executable by passing --z3Exe <path/to/z3> as a command line option to Silicon.
  4. Download Sbt (http://www.scala-sbt.org/), the build tool used to build Silicon and Silver. Installing Sbt simply means that there will be a script (sbt.bat on Windows) in your path that starts a JVM with the Sbt launcher (sbt-launch.jar) in its classpath.
  5. Quite a bit of memory in required to run and compile Silver and Silicon. Have a look at the script that launches Sbt (e.g., sbt.bat) and ensure that the Java options are such that the JVM's maximal heap size is at least 2GiB (-Xmx2048m), and that the maximal stack size is at least 16MiB (-Xss16m).
  6. Check if your setup is all right by running the test suite via sbt test. This will compile Silicon, run the test suite and analyse the results. Ideally, all tests succeed (green), modulo some which are (currently) ignored (yellow).

Note: Silicon assumes that default encoding used by JVM is UTF-8. Therefore, if you experience problems like crashing sbt test, try to set environment variable JAVA_TOOL_OPTIONS to -Dfile.encoding=UTF8.

Running Silicon

  • Silicon comes with a batch file that you can use to run it on Windows: silicon.bat [options] <file.sil>
  • OS-independently, you can also run Silicon via sbt, by running sbt "run [options] <file.sil>". Note: The quotation marks around the arguments are necessary on Windows, they also appear to be necessary on Linux (I only tried with a standard Ubuntu 12.04 installation).
  • You can also use sbt test and sbt testOnly to run the whole test suite, respectively, individual tests. Read more in the section on testing

Testing

Tests are run using Sbt's support for testing frameworks (Silicon currently uses ScalaTest). You can run the whole test suite via sbt test, or you can run tests selectively via sbt testOnly -- -n <tag>, where <tag> can be a relative test file path (more about that soon), or a file name with or without file extension. If you want to know more, you should start by looking at the sources of SilSuite.scala.

If you want to pass arguments to Silicon when running tests via sbt, you must use testOnly (test does not support additional arguments). For example, if you want to increase the verbosity of Silicon's output, run testOnly -- -n arithmetic.sil -Dsilicon:logLevel=debug. The -D syntax is defined by ScalaTest, the prefix silicon: marks options that will be forwarded to Silicon, and logLevel=debug is passed to Silicon as --logLevel debug, which is the option format expected by Silicon.

For example, here is how you run Silicon on the default test suite, but with a timeout of 180s:

testOnly viper.silicon.tests.SiliconTests -- -Dsilicon:timeout=180

Since Silicon depends on Silver, its testing scope consists of all Silver files that are in Silver:src/test/resources or in Silicon:src/test/resources. Per default, none of the tests in the scope are used. Only those located in subdirectories that are mentioned in SiliconTests.scala are considered.

Currently, nearly all test files are located in Silver's repository, that is, at Silver:src/test/resources. This is, because they are (or at least, should be) handleable by all Silver verifiers (or in general, all Silver tools). Thus, if you want to add a test case, the Silver repository is usually the right place it. This also holds for tests that illustrate a bug or another issue of Silicon! Ultimately, they should work in other verifiers as well. Silicon issues are currently located at Silver:src/test/resources/all/issues/silicon. Only if your test case is really Silicon-specific, for example, because it uses an extension of Silver that is specific to Silicon, or ... well, actually, there probably isn't a single good reason for adding tests to Silicon's repository.

Run your own tests

Edit Silicon:src/test/scala/SiliconTests.scala and adapt silTestDirectories to include your custom test directory, e.g.,

private val silTestDirectories: Seq[String] = List("all/my")

Sbt test will now look for tests in the folder Silver:/src/test/resources/all/my.

Clone this wiki locally