-
Notifications
You must be signed in to change notification settings - Fork 43
End to End Testing of Verifiers Based on Silver
There are a series of useful classes in viper.silver.testing that
perform most of the things needed to set up a test suite of end to end
tests in Silver-based tools. See Carbon or Silicon for an example of how
to do that. There are also utility classes and traits for parsing test
annotations (see below) and similar things.
A base test suite for Silver based verifiers (see viper.silver.testing.SilSuite which extends viper.silver.testing.ResourceBasedTestSuite) creates a ScalaTest unit test for each Silver file it finds in registered test directories. Each such unit test is tagged with the path of the file it corresponds to, relative to the test directory it was found in. Additional tags are the file name with and without extension. See the following subsection for examples of how to use such tags.
To execute the whole test suite, including both files (or other
resources) that give rise to test cases, as well as regular ScalaTest
unit tests, simply invoke the sbt command test. At the end of the
output you should see a summary such as
Passed: : Total 135, Failed 0, Errors 0, Passed 127, Skipped 8
stating that all executed tests passed (8 have been skipped, though), or
Failed: : Total 135, Failed 2, Errors 0, Passed 125, Skipped 8
stating that 2 tests failed.
If only a single test should be executed, then the sbt command
testOnly can be used as follows:
testOnly -- -n tag
where tag is a ScalaTest tag identifying none, one or multiple unit
tests.
If, for example, a directory all has been registered as a test
directory, which contains a test file at all/basic/arithmetic.sil,
then the following commands can be used to execute the unit test
corresponding to this file (and potentially others that were tagged with
the same tag):
testOnly -- -n arithmetic
testOnly -- -n arithmetic.sil
testOnly -- -n all/basic/arithmetic.sil
It is even possible to define an sbt alias for this in a build.sbt,
using:
addCommandAlias("tn", "testOnly -- -n ")
Options to the test framework or to the underlying tool, for example,
the verifier that is to be tested, can only be passed when using
testOnly. Options must be prefixed with -D and consist of
key=value pairs, for example,
testOnly -- -n arithmetic -Dfoo=bar
testOnly -- -n arithmetic -Dfoo=bar -Dyou=me
These options are passed to ScalaTest tests in the form of a
configMap <: Map[String, Any]. If you want to forward options to your
tool, it is recommended to require a tool-specific prefix to distinguish
between options for your tool and other options. Silicon, for example,
requires you to execute
testOnly -- -n arithmetic -Dsilicon:logLevel=DEBUG
if you want to increase the verbosity of its output.
Currently, the only option that the Silver test framework defines is
includeFiles=<regex> (used by ResourceBasedTestSuite, defaults to
.*\.sil"), which specifies which files inside registered test
directories are recognised as test cases, that is, give rise to unit
tests.
Technical detail: Currently, all files inside registered test
directories that match includeFiles are turned into unit tests and
parsed for test annotations (see sections further down), even if in the
end only a single test is executed because of testOnly -- -n. This
(currently) doesn't waste much time since the test suite is still fairly
small, but if you nevertheless want to narrow down the number of files
the test framework works on, consider passing
-DincludeFiles=<more-specific-regex> to testOnly.
To test our verifiers and translators, we have some common infrastructure that can be reused. It is based on annotating the input program (either in Silver, or in a source language that is later translated to Silver) with expected verification errors (using their unique IDs).
The annotations (the expression annotation is used in a broad sense
here, and does not refer to Java/Scala annotations) always start with
//:: (which is in many languages a single-line comment starting with
::). The most basic annotation then is
//:: ExpectedOutput(ERROR_ID)
Its semantics are that on the next line that is not simply a comment (i.e. a line which
starts with whitespace followed by //) an error identified by
ERROR_ID is expected. If multiple verification errors
are expected, then an annotation for each of them can appear on a
separate line before the statement or expression.
Furthermore, there are two annotations to express a bug or incompleteness in a toolchain. The annotation
//:: UnexpectedOutput(ERROR_ID, /<project-name>/issue/<n>/)
indicates that currently an error occurs, but should not. Details are
explained in the issue tracker of project <project-name> as issue
number <n>. Specifying "silver" for <project-name> indicates that the described behaviour applied to both (all) verifiers, otherwise a specific back-end (carbon or silicon) can be specified. Similarly,
//:: MissingOutput(ERROR_ID, /<project-name>/issue/<n>/)
indicates that currently no error is issued, but one with identifier
ERROR_ID is expected; again linked to an item in the
issue tracker.
See the end of this document for a summary of the possible values for ERROR_ID
In general, a test can consist of several files. If some directory
contains <testname>_file1<suffix>, <testname>_file2<suffix> etc, one
test called <testname> is created from those files. If this behaviour
is unwanted, it can be turned off by either not using filenames
according to that convention or by mixing the trait SingleFileSuite
into the test suite.
Finally, it is possible to ignore files (and lists of files), using:
//:: IgnoreFile(/<project-name>/issue/<n>/)
//:: IgnoreFileList(/<project-name>/issue/<n>/)
As before, the reason for ignoring the method or file should be given on
the issue tracker. Sometimes, it can happen that a certain line should
cause an error in a test, but it is implementation dependent or not
important for the test, if it causes other problems, as well. In that
case, IgnoreOthers should be added after all the other error
annotations.
//:: ExpectedOutput(verification.error.id)
//:: IgnoreOthers
The next line is expected to cause error <verification.error.id>, but
it is ok for the test if it also causes other errors.
Some nice properties of this system (also compared to previous testing infrastructure) include:
- We can have multiple expected errors on a single line.
- The expected output appear in the same file as the test code.
- The annotations with verification identifiers (as short but descriptive strings) make the annotations easily understandable.
- Changes in the user-friendly error messages do not affect the annotations (for example, fixing a typo does not require a change to the tests).
- Unexpected and missing errors can be annotated as such.
- Furthermore, unexpected and missing errors are clearly linked to a bug report, making it easier to keep track of open issues and search for all affected test-cases for an entry in the bug tracker (without having to list all of the tests in the bug tracker).
- A common implementation can be shared by all front-ends.
- Not every language we might want to verify has annotations (for example, Chalice, …)
- Annotations might require more overhead as we cannot fully choose the
syntax. For example, in Java/Scala we would need to add
""around string identifiers. - It becomes less likely that we can share the test infrastructure among different front-ends with different syntax for annotations.
- Annotations can not be used everywhere in Java or Scala. They can only be used before a declaration, i.e.if a local variable, a field, a method or a class is declared.
For the full (and latest) details, check the file src/main/scala/viper/silver/verifier/VerificationError.scala :in the Silver sources
An error identifier consists of a string representing an error type, followed by the : symbol, followed by a string identifying an error reason. For example: assert.failed:assertion.false
The possibilities are listed below:
###Strings for Error Types (corresponding messages shown in parentheses, for understanding)###
- internal ("An internal error occurred.")
- assignment.failed ("Assignment might fail.")
- call.failed ("Method call might fail.")
- not.wellformed ("Contract might not be well-formed.")
- call.precondition ("The precondition of method ${offendingNode.methodName} might not hold.")
- application.precondition ("Precondition of function ${offendingNode.funcname} might not hold.")
- exhale.failed ("Exhale might fail.")
- inhale.failed ("Inhale might fail.")
- if.failed ("Conditional statement might fail.")
- while.failed ("While statement might fail.")
- assert.failed ("Assert might fail.")
- postcondition.violated ("Postcondition of ${member.name} might not hold.")
- fold.failed ("Folding ${offendingNode.acc.loc} might fail.")
- unfold.failed ("Unfolding ${offendingNode.acc.loc} might fail.")
- package.failed ("Packaging wand might fail.")
- apply.failed ("Applying wand might fail.")
- invariant.not.preserved ("Loop invariant $offendingNode might not be preserved.")
- invariant.not.established ("Loop invariant $offendingNode might not hold on entry.")
- function.not.wellformed ("Function might not be well-formed.")
- predicate.not.wellformed ("Predicate might not be well-formed.")
- wand.not.wellformed ("Magic wand might not be well-formed.")
- letwand.failed ("Referencing a wand might fail.")
- heuristics.failed ("Applying heuristics failed.")
- internal (custom message)
- feature.unsupported ("$offendingNode is not supported. $explanation")
- unexpected.node ("$offendingNode occurred unexpectedly. $explanation")
- assertion.false ("Assertion $offendingNode might not hold.")
- epsilon.as.param ("The parameter $offendingNode might be an epsilon permission, which is not allowed for method parameters.")
- receiver.null ("Receiver of $offendingNode might be null.")
- division.by.zero ("Divisor $offendingNode might be zero.")
- negative.permission ("Fraction $offendingNode might be negative.")
- insufficient.permission ("There might be insufficient permission to access $offendingNode.")
- invalid.perm.multiplication ("Permission multiplication might not be possible, as an operand might contain epsilons.")
- wand.not.found ("Magic wand instance not found.")
- wand.not.found ("Magic wand instance not found.")
- wand.outdated ("Found magic wand instance, but now-expressions might not match.")
- receiver.not.injective ("Receiver of $offendingNode might not be injective.")
- labelled.state.not.reached ("Did not reach labelled state $lbl required to evaluate $offendingNode.")