Common Deployment

To execute deployment scripts you need to install:

To deploy Klever one has to clone its Git repository (a path to a directory where it is cloned is referred to as $KLEVER_SRC):

git clone --recursive https://forge.ispras.ru/git/klever.git

Note

Alternatively one can use https://github.com/ldv-klever/klever.git.

Then one has to get Klever Addons and perhaps Klever Build Bases. Both of them should be described appropriately within Deployment Configuration File.

Note

You can omit getting Klever Addons if you will use deploys/conf/klever-minimal.json.sample from $KLEVER_SRC as Deployment Configuration File since it contains URLs for all required Klever Addons.

Klever Addons

You can provide Klever Addons in various forms:

  • Local files, directories, archives or Git repositories.
  • Remote files, archives or Git repositories.

Deployment scripts will take care of their appropriate extracting. The best place for Klever Addons is directory addons within $KLEVER_SRC (see Structure of Klever Git Repository).

Note

Git does not track addons from $KLEVER_SRC.

Klever Addons include the following:

CIF

One can download CIF binaries from here. These binaries are compatible with various Linux distributions since CIF is based on GCC that has few dependencies. Besides, one can clone CIF Git repository and build CIF from source using corresponding instructions.

CIL

CIL is a very legacy Klever addon. You can get its binaries from here. As well, you can build it from this source which has several specific patches relatively to the mainline.

Consul

One can download appropriate Consul binaries from here. We are successfully using version 0.9.2 but newer versions can be fine as well. It is possible to build Consul from source.

Verification Backends

You need at least one tool that will perform actual verification of your software. These tools are referred to as Verification Backends. As verification backends Klever supports CPAchecker well. Some other verification backends are supported experimentally and currently we do not recommend to use them. You can download binaries of CPAchecker suitable for checking most of requirements from here. For finding data races additionally download binaries of another custom version of CPAchecker from here. In addition, you can clone CPAchecker Git or Subversion repository and build other versions of CPAchecker from source referring corresponding instructions.

Optional Addons

If you are going to solve verification tasks using VerifierCloud, you should get an appropriate client. Most likely one can use the client from the CPAchecker verification backend.

Note

For using VerifierCloud you need appropriate credentials. But anyway it is an optional addon, one is able to use Klever without it.

Klever Build Bases

In addition to Klever Addons one can provide Klever Build Bases obtained for software to be verified. Klever Build Bases should be obtained using Clade. All Klever Build Bases should be presented as directories. The best place for Klever Build Bases is directory build bases within $KLEVER_SRC (see Structure of Klever Git Repository).

Note

Git does not track build bases from $KLEVER_SRC.

Deployment Configuration File

After getting Klever Addons and Klever Build Bases one needs to describe them within Deployment Configuration File. First we recommend to copy deploys/conf/klever-minimal.json.sample from $KLEVER_SRC to some JSON file within deploys/conf/ from $KLEVER_SRC (see Structure of Klever Git Repository). Since deployment scripts use deploys/conf/klever.json from $KLEVER_SRC by default this is the best place for that file.

Note

Git does not track deploys/conf/*.json from $KLEVER_SRC.

Note

deploys/conf/klever-minimal.json.sample from $KLEVER_SRC is so consize as possible. One can find much more examples for describing Klever Addons and Klever Build Bases in deploys/conf/klever-deploy-means.json.sample from $KLEVER_SRC.

Then you need to fix the sample to describe Klever and all required Klever Addons and Klever Build Bases. Generally there are 3 pairs within Deployment Configuration File with names Klever, Klever Addons and Klever Build Bases correspondingly. The first one directly represents a JSON object describing Klever. The second one is a JSON object where each pair represents a name of a particular Klever addon and its description as a JSON object. There is the only exception. Within Klever Addons there is Verification Backends that serves for describing Verification Backends.

Each JSON object that describes a Klever addon should always have values for version and path:

  • Version gives a very important knowledge for deployment scripts. Depending on values of this pair they behave appropriately. When entities are represented as files, directories or archives deployment scripts remember versions of installed/updated entities. So, later they update these entities just when their versions change. For Git repositories versions can be anything suitable for a Git checkout, e.g. appropriate Git branches, tags or commits. In this case deployment scripts checkout specified versions first. Also, they clone or clean up Git repositories before checkouting, so, all uncommited changes will be ignored. To bypass Git checkouting and clean up you can specify version CURRENT. In this case Git repositories are treated like directories.
  • Path sets either a path relative to $KLEVER_SRC or an absolute path to entity (binaries, source files, configurations, etc.) or an entity URL.

For some Klever Addons it could be necessary to additionally specify executable path or/and python path within path if binaries or Python packages are not available directly from path. For Verification Backends there is also name with value CPAchecker. Keep this pair for all specified Verification Backends.

Besides, you can set copy .git directory and allow use local Git repository to True. In the former case deployment scripts will copy directory .git if one provides Klever Addons as Git repositories. In the latter case deployment scripts will use specified Git repositories for cleaning up and checkouting required versions straightforwardly without cloning them to temporary directories.

Warning

Setting allow use local Git repository to True will result in removing all your uncommited changes! Besides, ignore rules from, say, .gitignore will be ignored and corresponding files and directories will be removed!

Note

You can prepare multiple deployment configuration files, but be careful when using them to avoid unexpected results due to tricky intermixes.

Note

Actually there may be more Klever Addons or Klever Build Bases within corresponding locations. Deployment scripts will consider just described ones.

Structure of Klever Git Repository

After Common Deployment the Klever Git repository can look as follows:

$KLEVER_SRC
├── addons
│   ├── cif-d95cdf0.tar.gz
│   ├── cil-1.5.1.tar.gz
│   ├── consul
│   ├── CPAchecker-1.6.1-svn ea117e2ecf-unix.tar.gz
│   ├── CPAchecker-1.7-svn 27946-unix.tar.gz
│   └── ...
├── deploys
│   ├── bin
│   │   ├── deploy-local
│   │   └── deploy-openstack
│   ├── conf
│   │   ├── klever.json
│   │   ├── klever-deploy-means.json.sample
│   │   └── klever-minimal.json.sample
│   └── ...
├── build bases
│   ├── linux-3.14
│   └── ...
└── ...