Klever does not support standard deployment means because it consists of several components that may require complicating setup, e.g. configuring and running a web service with a database access, running system services that perform some preliminary actions with superuser rights, etc. Also, Klever will likely always require several specific addons that can not be deployed in a normal way. Please, be ready to spend quite much time if you follow this instruction first time.
We recommend following hardware to run Klever:
x86-64 CPU with 4 cores
16 GB of memory
100 GB of free disk space
We do not guarantee that Klever will operate well if you will use less powerful machines. Increasing specified hardware characteristics in 2-4 times can reduce total verification time very considerably. To generate Klever Build Bases for large programs, such as the Linux kernel, you need 3-5 times more free disk space.
Klever deployment is designed to work on:
You can try it for other versions of these distributions, as well as for their derivatives on your own risk.
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
Alternatively one can use https://github.com/ldv-klever/klever.git.
Then you need to install all required dependencies.
First of all it is necessary to install packages listed at the following files:
Then you need to install Python 3.7 or higher and a corresponding development package. If your distribution does not have them you can get them from:
To install required Python packages we recommend to create a virtual environment using installed Python. For instance, you can run following commands within $KLEVER_SRC:
$ /usr/local/python3-klever/bin/python3 -m venv venv $ source venv/bin/activate
To avoid some unpleasant issues during installation we recommend to upgrade PIP and associated packages:
$ pip install --upgrade pip wheel setuptools
Later we assume that you are using the Klever Python virtual environment created in the way described above.
Then you need to install Python packages including the Klever one:
For production use it is necessary to run the following command within $KLEVER_SRC:
$ pip install -r requirements.txt .
Later to upgrade the Klever Python package you should run:
$ pip install --upgrade -r requirements.txt .
If one is going to develop Klever one should install Klever Python package in the editable mode (with flag -e). To do it, run the following command within $KLEVER_SRC:
$ pip install -r requirements.txt -e .
In this case the Klever Python package will be updated automatically, but you may still need to upgrade its dependencies by running the following command:
$ pip install --upgrade -r requirements.txt -e .
Removing -r requirements.txt from the command will install latest versions of required packages. However, it is not guaranteed that they will work well with Klever.
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.
If Klever Addons are provided locally the best place for them is directory
$KLEVER_SRC (see Structure of Klever Git Repository).
Git does not track
addons from $KLEVER_SRC.
Klever Addons include the following:
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.
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 from here. In addition, you can clone CPAchecker Git or Subversion repository and build other versions of CPAchecker from source referring corresponding instructions.
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 should provide Klever Build Bases obtained for software to be verified.
Klever Build Bases should be obtained using Clade.
All Klever Build Bases should be provided as directories, archives or links to remote archives.
The best place for Klever Build Bases is the directory
build bases within $KLEVER_SRC (see
Structure of Klever Git Repository).
Git does not track
build bases from $KLEVER_SRC.
Content of Klever Build Bases is not modified during verification.
Deployment Configuration File
After getting Klever Addons and Klever Build Bases one needs to describe them within
Deployment Configuration File.
By default deployment scripts use
klever/deploys/conf/klever.json from $KLEVER_SRC.
We recommend to copy this file somewhere and adjust it appropriately.
There are 2 pairs within Deployment Configuration File with names Klever Addons and Klever Build Bases. The first 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 checkout, so, all uncommitted changes will be ignored. To bypass Git checkout 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
In the latter case deployment scripts will use specified Git repositories for cleaning up and checkout required
versions straightforwardly without cloning them to temporary directories.
Setting allow use local Git repository to True will result in removing all your uncommitted changes!
Besides, ignore rules from, say,
.gitignore will be ignored and corresponding files and directories
will be removed!
Klever Build Bases is a JSON object where each pair represents a name of a particular
Build Base and its description as a JSON object.
Each such JSON object should always have some value for path:
it should be either an absolute path to the directory that directly contains Build Base,
or an absolute path to the archive with a Build Base,
or a link to the remote archive with a Build Base.
Particular structure of directories inside such archive doesn’t matter:
it is only required that there should be a single valid Build Base somewhere inside.
job.json you should specify the name of the Build Base.
You can prepare multiple deployment configuration files, but be careful when using them to avoid unexpected results due to tricky intermixes.
Structure of Klever Git Repository
$KLEVER_SRC ├── addons │ ├── cif-1517e57.tar.xz │ ├── consul │ ├── CPAchecker-1.6.1-svn ea117e2ecf-unix.tar.gz │ ├── CPAchecker-35003.tar.xz │ ├── toplevel.opt.tar.xz │ └── ... ├── build bases │ ├── linux-3.14.79.tar.xz │ └── linux-4.2.6 │ ├── allmodconfig │ └── defconfig └── ...
There are several variants for deploying Klever: