Project Structure

Functional Overview

VerCors verifies programs by going through four stages:

• The frontend, or parsing: in this step a collection of files is read and parsed into COL, the common object language. This is the internal intermediate representation of programs in VerCors.
• Resolution: here we figure out what names in the AST mean. Every name must point to (part of) a declaration. Afterwards, we forget about the name and only remember a pointer to the relevant declaration.
• The rewrite stage: The COL AST (usually referred to as just the AST) is transformed into a different AST, or it is checked for some property, together called a "pass". Depending on user-supplied options many passes are applied to the AST. They can be divided in several categories:
  • Reducing a feature: The subset of COL used is reduced, by encoding the proof obligations of a language construct in some other way. An example is that we reduce for loops to while loops, by placing the initialization before a new while loop, retaining the condition, and appending the update to the end of the loop body.
  • Checking for consistency: in some places it is useful that the type structure of the AST is not as strict as the set of ASTs we want to allow. Almost all checks are done in the type check, a single pass executed many times.
  • Standardization: many passes expect certain properties to be true about the AST (e.g. "expresions have no side effects"), but on the other hand it is useful not to constrain passes too much in what they can generate. Therefor we standardize the AST between passes, to reduce simple language features.
  • Importing builtins: some features are supported by importing a header of sorts into the AST.
  • Optimization: optimizing passes transform the AST (in particular expressions) such that they are faster to prove, or rely less on heuristics of the backend.
• The backend, or verification: the very much reduced AST is transformed once more, into the language of the selected backend. The backend makes a judgement on the program. This judgement is translated back into useful information about the program.

There are also a few cross-cutting concerns:

• The origin system tracks how the frontend parse tree is transformed via COL into a backend language. This means that if a message from the backend mentions a part of the AST in the backend language, it can be translated all the way back to its origin in the frontend input.

Technical Setup

The VerCors project sources are managed on GitHub, at https://github.com/utwente-fmt/vercors. The unstable development branch is dev, from where we branch to develop new features and bugfixes. Those with access may push feature branches to the main repository, or create a fork if they prefer. A pull request is then made and reviewed by someone appropriate.

Pushed commits as well as pull requests are checked via continuous integration, currently Github Actions. Github builds Vercors and runs the test suite. Once the checks pas and a code review is completed, the PR is merged in dev. In dev is also where we hope to notice bad interactions between new features.

We aim to make a new VerCors release once per month, which is done via a tagged merge commit to the master branch, followed by a GitHub release.

VerCors is written in java and scala. Code is accepted in either language, but we encourage you to take the time to learn some Scala - it is much better suited to manipulating ASTs. The build structure is defined in the mill build tool.

Project Structure

NB: this information quickly becomes out of date as vercors is refactored.

/

• build.sc is the root build definition. It configures global plugin options, wires sub-project dependencies, configures run-time build information, denotes external dependencies, configures metadata about the project and configures compiler options.
• mill/mill.bat bootstrap and run the build tool Mill.

/.github/workflows

• scalatest.yml configures Github Actions to run the test suite
• build-wiki-pdf.yml assembles the Github wiki into a latex-flavoured pdf

/bin

Convenience run scripts that compile and then run VerCors. They are helpful because they start up slightly quicker than e.g. ./mill vercors.run, and VerCors starts in the foreground so pretty-printing is supported.

• bashComplete generates a bash command completion script

/examples

This directory serves the dual purpose of being an archive of past case studies and competition results, as well as the test suite of VerCors. Files in this directory have a header denoting how they are used in the test suite. Names denoted by "case" or "cases" are collected, where overlapping names are joined together as one test case. Files may occur in more than one "case." "tools" denotes the backend used (silicon by default), "verdict" the expected final result (Pass by default).

• private: this can be created as a subdirectory and is ignored by git. Contributing examples (however small) that reproduce issues are however appreciated.
• archive contains examples that are broken or irrelevant: generally a lower priority.
• concepts contain examples sorted by topic
• demo is a standard set of demo files, suitable of e.g. a ~1 hour presentation.
• publications contains examples that are mentioned or reproduced in publications by us.
• technical has no good reason to exist: they should most likely be inline test fixtures.
• verifythis is a verification competition that takes place every year, this is the archive of our results there.

/lib

.jar files that VerCors depends on, that cannot be specified as e.g. a maven dependency.

/out

Output of the mill build tool.

/res/<project>

Contains the resources root that is related to <project>

/res/universal

Named universal historically after the universal plugin, this directory contains files that must be available on the classpath, but must not be packed into a jar (e.g. executables)

/res/universal/deps/<platform>

Files that are specific to <platform>, not included on build for other platforms.

• boogie: The boogie program verifier
• z3: The Z3 theorem prover

/res/universal/res

Files that are included on all platforms

• adt: definitions for VerCors' datatypes
• c: header files that specify C functions
• include: miscellaneous library files that are loaded into vercors
• jdk: Java files that specify Java methods and classes
• simplify: Term rewriting rules for simplifying expressions
• systemc/config: Configuration files for the SystemC component

/src/<project>

Source files for the <project> project. These may be in any language, such as scala, Java, antlr g4, etc. See also ⌄Project Structure by Package

/test/<project>

Source files for testing the <project> project.

/tmp

Contains debug output from VerCors, Viper, Boogie, and Z3 when configured to output it.

/util

• editors: various grammar definitions for text editors (i.e. text highlighting), in various states of disrepair (but still useful)
• inheritance: A plan to implement better inheritance support
• oldRewriteRules: The old definitions in the term rewriter, to be scoured for good definitions
• processalgebra: A plan to implement process algebra support again
• release: Utility script to draft a VerCors release
• SplitVerify: Tool that can focus on a single method in a verification input, for more rapid prototyping of specifications.
• stubimpl: Helper script to generate NodeImpl traits, useful when adding lots of Nodes.
• stupidUnsatCore: Removes line from an smt2 script until the result is no longer unsat.
• wiki: Utility script that parses the wiki into pdf, html, the website navigation menu for html, a test suite of the examples.

Project Structure by Package

• .: in colhelper: Utilities to generate helper classes for the Node definitions, such as rewriters, comparators, subnode recursors, etc.
• antlr4: Grammar definitions.
• hre: General utilities not necessarily specific to VerCors
• hre/cache: Generates a cache directory in an appropriate place keyed on customizable values (such as application version)
• vct/cache: Uses the cache directory to store verification results, keyed on the vercors and viper versions.
• hre/debug: Debugging utilities,
• hre/io: I/O utilities. Readable and Writeable are the canonical way to describe a resource that can be opened for reading/writing in VerCors, with the default implementation for files RWFile
• hre/perf: Platform-independent profiling utilities, measuring time usages and resource usage
• hre/platform: Detects the current platform (Windows/Unix/Mac), mostly used to determine executable format (PE/ELF/Mach-O)
• hre/progress: Utilities to maintain a tree of tasks currently executing across threads, for accounting profiling information and display.
• hre/resource: Utility to locate platform-approriate resources.
• hre/stages: Named functions, with an input and output type that can be chained, and catch VerificationErrors by default.
• hre/unix: Unix-specific utilities, currently only getrusage (where MacOS here does count as unix)
• hre/util: misc
• viper: The Viper backend
• viper.api: Utilities to interface between VerCors and the Viper backend
• viper.api.transform: Translate between the Viper language (historically referred to as "Silver") and the VerCors intermediate language "COL"
• viper.api.backend: Implements the interface for Carbon and Silicon, the two Viper implementations.
• vct/result: VerificationError may be thrown, which is either a SystemError (always a bug, need not be informational) or a UserError (sometimes a bug, but must describe the situation well)
• vct/importer: Load library files from resources and other paths.
• vct/main: Wires up command line options into executable vercors runs, assembled of Stages.
• vct/modes: A VerCors run is determined by exactly one mode, the default being verification.
• vct/stages: The pieces of VerCors that can be chained together. Might as well be plain functions, the primary difference being these use the progress framework.
• vct/stages/Stages.scala::ofOptions: the meat and potatoes: defines the actual components of VerCors from the command line options. Each stage is _.run(_) in turn.
• vct/main/Main.scala: defines public static void main(String[] args) - the actual entry point.
• vct/options: The command line options.
• vct/resources: Defines the default location for various resources.
• vct/parsers: Uses ANTLR to transform various input sources to a COL tree.
• vct/parsers/transform: Defines how to transform an ANTLR tree to a COL tree.
• vct/rewrite: Transformations on COL ASTs - the most important part of VerCors.
• vct/col: All things related to the internal COL language
• vct/col/ast: Definitions of all nodes in COL. All definitions live in Node.scala, but all implementations are moved into separate subpackages and files.
• vct/col/check: Check errors and utilities to check them, for any kind of error that is not a type error.
• vct/col/debug: Debug utility for checking the lifecycle of declarations.
• vct/col/err: Verification errors related to col
• vct/col/feature: Segments nodes into features, where there is approximately one rewriter per feature. Currently not used for anything useful. (PB: I would prefer to move this out of the col module)
• vct/col/origin: Contains Origin, which explains how a node came to be (e.g. from the user input), and Blame, which explains how to translate errors from the backend to more pointed errors on the input.
• vct/col/print: An implementation of "A prettier printer" that works well with COL. (PB: I would prefer to move this out of the col module)
• vct/col/ref: Implements cross-references in the AST. Rewriters by default make LazyRef such that declarations can be made later than that they are referenced.
• vct/col/resolve: Resolves names and types in the AST according to the semantics of Java, C, PVL and the specification language. (PB: I would prefer to move this out of the col module)
• vct/col/rewrite: Utilities that build on the generated AbstractRewriter.
• vct/col/typerules: Defines the typing rules for the COL language. Transformations can be applied along applications of type rules using CoercingRewriter.
• vct/col/util: General AST utilities, such as a comparator, factory helpers, a subtitutor for expressions and types, and more.