Project Structure

Functional Overview

VerCors verifies programs by going through three 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.
• 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.
• Logging: we have a bespoke logging system and outputting via stdout or stderr is forbidden programatically. This makes it possible to set verbosity with the granularity we want (e.g. only verdict, progress information, filter debug information by class)

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 Travis + Sonarcloud. Travis builds Vercors and runs the test suite. The (committed) code is linted by Sonarcloud. 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 all things being equal scala is preferred. The build structure is defined in the scala build tool. We use the sbt-native-packager plugin to package the tool as a .deb and a .tar.gz (compiled). The sbt-buildinfo plugin supplies the tool with run-time access to versioning and build time information.

Project Structure

/

• build.sbt 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.
• .travis.yml sets up caching and parallelizes the build. The actual build steps are in .travis/build.sh.

/.travis

• travis_fold.sh: Wrapper script that causes travis to make a foldable section of text.
• travis_tar.sh: Replacement for the system tar that packs our cache in a format that SBT ends up being happy with. Should be default by now https://travis-ci.community/t/change-tar-format-to-posix/5467

/bin

Convenience run scripts that targets the last-compiled classes in the vercors directory. This is the least stable method of running Vercors. If bleeding edge features are not needed, use the release version. If possible, run Vercors imported in an IDE instead. Failing that, the run scripts can be useful.

• run-class.sh and .classpath: run-class obtains the run-time class path from SBT and caches it in .classpath. A supplied main class + arguments is run from this class path. Other scripts in the directory only select a main class and refer to run-class.

/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.

/parsers

A sub-project of Vercors that implements the parsing infrastructure of Vercors.

• build.sbt: runs ANTLR 4, the parser generator, prior to compilation if necessary. Grammar source sets are encoded explicitly in the build file.
• src/main/antlr/*.g4: root grammars from which parsers are generated. These only glue a language grammar to the specification grammar, though the language grammar itself is also modified somewhat.
• lib/antlr4/*.g4: non-root grammars, defining languages (such as C and Java), embedded languages (such as OpenMP) and specifications.

/project

An artifact of how SBT works. SBT projects are layered, not in the sense that we have sub-project dependencies, but that you can define meta-projects. This directory defines a meta-project, which means it is available in compiled form in the upper build definition. We just use it to add some plugins to the compiler.

/SplitVerify

This tool is not part of VerCors itself, but interacts with VerCors to cache the verification result of parts of a test case. That means that changing part of a test case only requires re-verifying the changed part. Refer to the readme there for further information.

/util

• VercorsPVL.tmbundle: textmate bundle, defining PVL as a grammar, enabling syntax highlighting for PVL in some editors.

/src

The sources associated with the top-level SBT project, i.e. the main part of VerCors.

/src/universal/res

Here live the resources of VerCors. Normally they would be in a directory res or so in the root, but we have a custom solution to ensure that they remain regular files, even when packed into a jar by the build tool. Universal refers to the native-packager also being called the "Universal" plugin. "res" is the name of the directory in which the resources end up in .tar.gz deployment.

• config: Include files ("headers") that are put in the AST at some intermediate stage.
  • config/prelude(_C)?.sil: here the standard axiomatic data types that we need are defined
  • *.jspec: simplification rules that we assume to be true, applied at various stages.
• deps: Software dependencies that we do not refer to in the project structure, but rather by including the binary.
• include: Include files ("headers") that are available to front-end files, though currently only C.
• selftest: Ancient test files that are still accessible via the test suite. Unclear if they still work.

/src/main/scala

Please don't use this directory anymore. Scala sources also compile fine when included in the java directory, so this "mirror" of the package structure only serves to confuse where classes are defined. Only a few rewrite passes are defined here.

/src/main/java

• col/lang: I believe this is an implementation of some verification constructs, to facilitate compiling PVL to Java.
• puptol, rise4fun: external tool support, now obsolete.

/src/main/java/vct

• antlr/parser: Takes ANTLR parse trees and converts them to COL. The classes ending in Parser guide the conversion process. Classes ending in ToCOL do the actual immediate translation. Finally there are a few rewrite passes that solve language-specific problems.
• boogie: Old (?) prototypes for supporting boogie, dafny and chalice.
• col/annotate: A single feature rewrite pass, unclear why it's in a different package.
• col/ast: the AST of COL, divided into expressions (expr), declarations (stmt/decl), statements (stmt/{composite,terminal}) and types (type). Also defines some abstract intermediate node types (generic) and utility classes for traversing the tree in various ways (util).