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.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).
• col/print: logic to translate COL into text again for different frontends. Only Java is well-supported, as it's the default diagnostic output.
• col/rewrite: this is where all rewrite passes are defined. They are under-documented, but the Main class offers a brief explanation for each of them.
• col/syntax: abstract representation of the syntax of various frontends.
• demo: unclear why this is in the source tree.
• error: probably an attempt at better abstracting errors from the backend
• learn: experiment that counts the different types of nodes in the AST, to attempt to correlate verification time with the presence of particular nodes.
• logging: barely used; abstracts messages and errors for a particular pass
• main: entry points for VerCors, as well as some poorly-sorted classes.
  • ApiGen: echoes back a java program immediately after parsing something; purpose unclear.
  • BoogieFOL: another prototype to interface with boogie, a deprecated backend (?)
  • Brain, SMTinter, SMTresult, Translator: attempt by student (?) to interface with z3
  • Main: the true entry point of Vercors.
• silver: maps COL to Silver, the language used by the viper project.
• test: the testing framework of Vercors. Collects cases from the examples directory and tests each in an isolated process.
• util/Configuration.java: contains most command-line options, as well as the logic to determine the location of external tools (z3, silicon, etc.)

/viper

More logic to interface with the viper backend(s), unclear where exactly the cut is with regards to /src/main/java/vct/silver.

/viper/hre

The general utilities project ("Hybrid Runtime Environment"), located here so /viper may depend on it. From here under src/main/java:

• hre/ast: definitions for the different types of Origin.
• hre/config: defines different types of command line options (integer, choice, collect...)
• hre/debug/HeapDump: dumps a class and its fields recursively using reflection. Largely replaced by DebugNode
• hre/io: inter-process communication.
• hre/lang/System: defines the logging system. Currently output to stdout and stderr directly is forbidden programatically, so that you're forced to use the logging framework.