Common Deployment¶
To execute deployment scripts you need to install:
- Python 3.4 or higher (if you build Python from source, you need to install development files for xz in advance).
- tar, gz, bzip2, xz, unzip, git and wget (if you are going to deploy entities from corresponding sources).
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.
- CIL.
- Consul.
- One or more Verification Backends.
- Optional Addons.
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 │ └── ... └── ...