Developer Documentation

How to Write This Documentation

This documentation is created using Sphinx from reStructuredText source files. To improve existing documentation or to develop the new one you need to read at least the following chapters of the Sphinx documentation:

  1. Defining document structure.
  2. Adding content.
  3. Running the build.
  4. reStructuredText Primer.
  5. Sphinx Markup Constructs.
  6. Sphinx Domains (you can omit language specific domains).

Please, follow these advises:

  1. Do not think that other developers and especially users are so smart as you are.
  2. Clarify ambiguous things and describe all the details without missing anything.
  3. Avoid and fix misprints.
  4. Write each sentence on a separate line.
  5. Do not use blank lines except it is required.
  6. Write a new line at the end of each source file.
  7. Break sentences longer than 120 symbols to several lines if possible.

To develop documentation it is recommended to use some visual editor.

Warning

Please do not reinvent the wheel! If you are a newbie then examine carefully the existing documentation and create the new one on that basis. Just if you are a guru then you can suggest to improve the existing documentation.

Using Git Repository

Klever source code resides in the Git repository. There is plenty of very good documentation about Git usage. This section describes just rules specific for the given project.

Update

  1. Periodically synchronize your local repository with the main development repository (it is available just internally at ISP RAS):

    branch $ git fetch origin
branch $ git remote prune origin

    Note

    This is especially required when you are going to create a new branch or to merge some branch to the master branch.

  2. Pull changes if so:

    branch $ git pull --rebase origin branch

    Warning

    Forget about pulling without rebasing!

  3. Resolve conflicts if so.

Fixing Bugs and Implementing New Features

  1. One must create a new branch to fix each individual bug or implement a new feature:

    master $ git checkout -b fix-conf

    Warning

    Do not intermix fixes and implementation of completely different bugs and features into one branch. Otherwise other developers will need to wait or to make some tricky things like cherry-picking and merging of non-master branches. Eventually this can lead to very unpleasant consequences, e.g. the master branch can be broken because of one will merge there a branch based on another non working branch.

  2. Push all new branches to the main development repository. As well re-push them at least one time a day if you make some commits:

    fix-conf $ git push origin fix-conf

  3. Merge the master branch into your new branches if you need some recent bug fixes or features:

    fix-conf $ git merge master

    Note

    Do not forget to update the master branch from the main development repository.

    Note

    Do not merge remote-tracking branches.

  4. Ask senior developers to review and to merge branches to the master branch when corresponding bugs/features are fixed/implemented.

  5. Delete merged branches:

    master $ git branch -d fix-conf

Releases

Generally we follow the same rules as for development of the Linux kernel.

Each several months a new release will be issued, e.g. 0.1, 0.2, 1.0.

Just after this a merge window of several weeks will be opened. During the merge window features implemented after a previous merge window or during the given one will be merged to master.

After the merge window just bug fixes can be merged to the master branch. During this period we can issue several release candidates, e.g. 1.0-rc1, 1.0-rc2.

In addition, after issuing a new release we can decide to support a stable branch. This branch will start from a commit corresponding to the given release. It can contain just bug fixes relevant to an existing functionality and not to a new one which is supported within a corresponding merge window.

Updating List of Required Python Packages

To update the list of required Python packages first you need to install Klever package from scratch in the newly created virtual environment without using the old requirements.txt file. Run the following commands within $KLEVER_SRC:

$ python3 -m venv venv
$ source venv/bin/activate
$ pip install -e .

This will install latest versions of required packages. After confirming that Klever works as expected, you should run the following command within $KLEVER_SRC:

$ python -m pip freeze > requirements.txt

Updated list of requirements will be saved and should be committed to the repository afterwards.

How to generate build bases for testing Klever

Most likely you can get actual, prepared in advance build bases for testing Klever from ldvuser@ldvdev:/var/lib/klever/workspace/Branches-and-Tags-Processing/build-bases.tar.gz (this works just within the ISP RAS local network).

To generate build bases for testing Klever you need to perform following preliminary steps:

  1. Install Klever locally for development purposes according to the user documentation (see Deployment).

  2. Create a dedicated directory for sources and build bases and move to it. Note that there should be quite much free space. We recommend at least 100 GB. In addition, it would be best of all if you will name this directory “build bases” and create it within the root of the Klever Git repository (this directory is not tracked by the repository).

  3. Clone a Linux kernel stable Git repository to linux-stable (scripts prepare build bases for different versions of the Linux kernel for which the Git repository serves best of all), e.g.:

    $ git clone https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux.git/ linux-stable

    You can use alternative sources of the Git repository, if the above one is not working well and fast enough:

    1. https://kernel.googlesource.com/pub/scm/linux/kernel/git/stable/linux-stable
    2. https://github.com/gregkh/linux

  4. Read notes regarding the compiler after the end of this list.

  5. Run the following command to find out available descriptions of build bases for testing Klever:

    $ klever-build -l

  6. Select appropriate build bases descriptions and run the command like below:

    $ klever-build "linux/testing/requirement specifications" "linux/testing/common models"

  7. Wait for a while. Prepared build bases will be available within directory “build bases”. Note that there will be additional identifiers, e.g. “build bases/linux/testing/6e6e1c”. These identifiers are already specified within corresponding preset verification jobs.

  8. You can install prepared build bases using deployment scripts, but it is boring. If you did not follow an advice regarding the name and the place of the dedicated directory from item 2, you can create a symbolic link with name “build bases” that points to the dedicated directory within the root of the Klever Git repository.

Providing an appropriate compiler

Most of build bases for testing Klever could be built using GCC 4.8 on Debian or Ubuntu. Otherwise there is an explicit division of build bases descriptions, e.g.:

  • linux/testing/environment model specifications/gcc48
  • linux/testing/environment model specifications/gcc63

(the former requires GCC 4.8 while the latter needs GCC 6.3 at least).

That’s why you may need to get GCC 4.8 and make it available through PATH. Users of some other Linux distributions, e.g. openSUSE 15.1, can leverage the default compiler for building all build bases for testing Klever.

The simplest way to get GCC 4.8 on Ubuntu is to execute the following commands:

$ sudo apt update
$ sudo apt install gcc-4.8
$ sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 70
$ sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 48
$ sudo update-alternatives --config gcc

(after executing the last command you need to select GCC 4.8; do not forget to make v.v. after preparing build bases!)

Generating Bare CPAchecker Benchmarks

Development of Klever and development of CPAchecker are not strongly coupled. Thus, verification tasks that are used for testing/validation of Klever including different versions and configurations of CPAchecker as back-ends may be useful to track regressions of new versions of CPAchecker. This should considerably simplify updating CPAchecker within Klever (this process usually involves a lot of various activities both in Klever and in CPAchecker; these activities can take enormous time to be completed that complicates and postpones updates considerably). In addition, this is yet another test suite for CPAchecker. In contrast to other test suites this one likely corresponds to the most industry close use cases.

One can (re-)generate bare CPAchecker benchmarks almost automatically. To do this it is recommended to follow next steps:

  1. Clone https://gitlab.com/sosy-lab/software/ldv-klever-benchmarks.git or git@gitlab.com:sosy-lab/software/ldv-klever-benchmarks.git once.
  2. After some changes within Klever specifications, configurations and test cases you need to solve appropriate verification jobs. To avoid some non-determinism it is better to use the same machine, e.g. LDV Dev, to do this. Though particular verification jobs to be solved depend on changes made, in ideal, it is much easier to consider all verification jobs at once to avoid any tricky interdependencies (even slight improvements or fixes of some specifications may result in dramatic and unexpected changes in some verification results).
  3. Download archives with verifier input files for each solved verification jobs to the root directory of the cloned repository.
  4. Run “python3 make-benchs.py” there.
  5. Estimate changes in benchmarks and verification tasks (there is not any formal guidance). If you agree with these changes, then you need to commit them and to push to the remote. After that one may expect that new commits to trunk of the CPAchecker repository will be checked for regressions against an updated test suite.

Using PyCharm IDE

To use PyCharm IDE for developing Klever follow the following steps.

Installation

  1. Download PyCharm Community from https://www.jetbrains.com/pycharm/download/ (below all settings are given for version 2018.8.8, you have to adapt them for your version by yourself).
  2. Follow installation instructions provided at that site.

Setting Project

At the “Welcome to PyCharm” window:

  1. Specify your preferences.
  2. Open.
  3. Specify the absolute path to directory $KLEVER_SRC.
  4. OK.

Configuring the Python Interpreter

  1. File ‣ Settings ‣ Project: Klever ‣ Project Interpreter ‣ Settings ‣ Show all….
  2. Select the Python interpreter from the Klever Python virtual environment.
  3. OK.
  4. Select the added Python interpreter from the list and press Enter.
  5. Input Python 3.7 (klever) in field name.
  6. OK.
  7. For the rest projects select Python 3.7 (klever) in field Project Interpreter.

Setting Run/Debug Configuration

Common run/debug configurations are included into the Klever project. Common configurations with names starting with $ should be copied to configurations with names without $ and adjusted in accordance with instructions below. If you want to adjust configurations with names that not starting with $ you also have to copy them before.

  1. Run ‣ Edit Configurations….

Klever Bridge Run/Debug Configuration

Note

This is available just for PyCharm Professional.

  • Specify 0.0.0.0 in field Host if you want to share your Klever Bridge to the local network.
  • Specify your preferred port in field Port.

Note

To make your Klever Bridge accessible from the local network you might need to set up your firewall accordingly.

Klever Core Run/Debug Configuration

This run/debug configuration is only useful if you are going to debug Klever Core.

  • Extend existing value of environment variable PATH so that CIF (cif or compiler), Aspectator (aspectator) and CIL (toplever.opt) binaries could be found (edit value of field Environment variables).

  • Specify the absolute path to the working directory in field Working directory.

    Note

    Place Klever Core working directory somewhere outside the main development repository.

    Note

    Klever Core will search for its configuration file core.json in the specified working directory. Thus, the best workflow to debug Klever Core is to set its working directory to the one created previously when it was run without debugging. Besides, you can provide this file by passing its name as a first parameter to the script.

Documentation Run/Debug Configuration

Specify another representation of documenation in field Command if you need it.

Testing

Klever Bridge Testing

Note

This is available just for PyCharm Professional.

  1. Tools ‣ Run manage.py Task…:

    manage.py@bridge > test

Note

To start tests from console:

$ cd bridge
$ python3 manage.py test

Note

Another way to start tests from console:

$ python3 path/to/klever/bridge/manage.py test bridge users jobs reports marks service

Note

The test database is created and deleted automatically. If the user will interrupt tests the test database will preserved and the user will be asked for its deletion for following testing. The user should be allowed to create databases (using command-line option –keedb does not help).

Note

PyCharm has reach abilities to analyse tests and their results.

Additional documentation

A lot of usefull documentation for developing Django projects as well as for general using of the PyCharm IDE is available at the official site.

Extended Violation Witness Format

TODO: Translate from Russian.

Error Trace Format

TODO: Translate from Russian.

Code Coverage Format

TODO: Translate from Russian.