<div dir="ltr"><div>Dear Ahmet,</div><div><br>As Evgeny Novikov promised (he is giving a talk at a conference), 
below is the short guide for deploying and running the Klever 2.0 
software verification framework.<br></div><div><br></div><div>1. Choose your favorite Ubuntu/Debian image. The instruction below is prepared for Ubuntu 18 but it not strictly required.<br></div><div>2. Download and create a new desktop installation or virtual machine with the system.  Don't forget about our hardware <a href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements" target="_blank">requirements</a>!<br></div><div>3. Download our software verification framework:</div><div>sudo apt-get install git<br></div><div>git clone <a href="https://github.com/ldv-klever/klever.git" target="_blank">https://github.com/ldv-klever/klever.git</a></div><div><br></div><div>4. Then follow <a href="https://klever.readthedocs.io/en/latest/deploy_local.html" target="_blank">deployment steps</a>
 for the local deployment. In particular modify 
klever-minimal.json.sample and save it as klever.json in 
$KLEVER_SRC/deployment/conf/ directory. Also set environment variables 
to specify $KLEVER_SRC directory with Klever source files and target 
installation directory $KLEVER_DEPLOY_DIR. Then install Klever with the 
command:<br>sudo $KLEVER_SRC/deploys/bin/deploy-local --deployment-directory $KLEVER_DEPLOY_DIR install production<br></div><div><br></div><div>5. After Klever installation you can build the kernel and create build base. <br></div><div><br></div><div>Download the kernel: <br></div><div><div>wget <a href="https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz" target="_blank">https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz</a><br>tar -xf linux-3.14.79.tar.gz<br><br></div><div>Install a suitable compiler:<br>sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 10<br>sudo update-alternatives --config gcc</div><div>And choose 4.8 compiler there</div><div><br></div><div>Prepare your PATH environment variable:<br>export PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH</div><div><br></div><div>Then run the following commands. It will take a lot of time<br>make allmodconfig<br>clade-intercept make -j8 modules_prepare</div><div>clade-intercept -a make -j8 all</div><div>clade-all -p linux_kernel ./cmds.txt</div><div>echo "[\"$(readlink -f .)\"]" > ./clade/Storage/working source trees.json<br><br></div><div>6.
 Move this build base to another place. This is an optional step but 
if you are going to build more bases in this directory then it is better
 to do it. Note, then you need a new base for each new configuration or 
kernel version. <br></div><div>mv clade $NEW_PLACE/linux-3.14.79</div><div><br></div><div>7.
 Modify your deployment klever.json file in $KLEVER_DEPLOY_DIR and add 
there a new section at the end of the file in the root JSON object:<br>"Klever Build Bases": ["$NEW_PLACE/linux-3.14.79"]</div><div><br></div><div>Instead of $NEW_PLACE set an absolute path to the directory with your build base.<br><br></div><div>8 Update the Klever installation:<br>sudo $KLEVER_SRC/deploys/bin/deploy-local --deployment-directory $KLEVER_DEPLOY_DIR update production<br><br></div><div>9. Now you can run verification.<br></div><div><div>Open localhost:8998 in the web browser.</div><div>Input username: manager, password: manager.</div><div>Click "Linux 3.14".</div><div>Click Job->Edit or ->Copy and edit job.json and other files depending on your needs.</div><div>In the job.json set "build base": "linux-3.14.79" or an another name if you named your build base differently.<br></div><div>Before running any large target such as all modules first try to verify modules given with the example.<br></div><div>10. Click Decision->Start.</div><div>11. Click "Start" or "Start with default values".</div><div>13. Wait for verification results. It can take very much time especially if your hardware isn't powerful enough. <br></div><div><br>If
 you will meet some issues, please, report them to us. We will try to 
solve or workaround them together. Note also, that we renamed some 
files, so there are some differences from the Klever-1.1 version in job 
files.<br><br></div><div>Best,<br></div><div>Ilia Zakharov</div></div></div><br><br><div class="gmail_quote"><div dir="ltr">ср, 17 окт. 2018 г. в 10:40, Evgeny Novikov <<a href="mailto:novikov@ispras.ru">novikov@ispras.ru</a>>:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>Dear Ahmet,</div><div> </div><div>Your primary question will not be resolved in Klever 2.0. So, I will answer it.</div><div> </div><div>In the deployment documentation you can find <a href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements" target="_blank">hardware requirements</a>. I suggest that your VM does not meet them, so, you either should empower it (I recommend this to get better verification results faster) or use more advanced settings. At page <a href="http://localhost:8998/service/schedulers/" target="_blank">http://localhost:8998/service/schedulers/</a> you can find the maximum amount of computer resources that Klever can spend for solving verification jobs and verification tasks. In the file you attached there are restrictions on computer resources just for verification jobs. But verification tasks are solved during solving verification jobs, so you should also take into account maximum computer resources that are allowed for verification tasks. Usually they are much more than ones for verification jobs! These resources are specified within file "tasks.json" at the job page, say, <a href="http://ldvdev:8998/jobs/5/" target="_blank">http://ldvdev:8998/jobs/5/</a>. I hope that this is enough for you to proceed.  </div><div> </div><div>For answering your second question it is definitely necessary to wait for Klever 2.0 as it will be intended for verification of C software rather than Klever 1.x that can verify just Linux device drivers. But, please, do not expect that Klever 2.0 will be able to verify some C program without additional efforts. Our rich experience and preliminary experiments show that one will need to develop a suitable configuration and specifications for each type of programs while verification tools like CPAchecker do not handle unfamiliar code well sometimes. If you are ready to invest much time, you are welcome! We will be glad to hear some notes and remarks from you.</div><div> </div><div>-- </div><div href="http://mailto:novikov@ispras.ru">Evgeny Novikov<br>Linux Verification Center, ISP RAS<br><a href="http://linuxtesting.org" target="_blank">http://linuxtesting.org</a></div><div> </div><div> </div><div> </div><div>17.10.2018, 09:12, "A. Celenk" <<a href="mailto:ahmet.celenk@procenne.com" target="_blank">ahmet.celenk@procenne.com</a>>:</div><blockquote type="cite"><div bgcolor="#FFFFFF"><p>Hello Evgeny,</p><p>Thank you very much for Klever, and for your help. I will be eagerly waiting for 2.0 release. Till then, I may try to use the current version to learn some basics. Here is what I have done:</p><p>I could reach the web interface and managed to login as manager, and played around a little bit. Considered the warning on the deployment tutorial about messing up the computer, I have installed Klever on a Ubuntu 18.04 VM. Being a VM, it has low resources. I have started the preset Linux 3.14 job with default configurations and got "Given resource limits for job and tasks in sum are too high, we do not have such amount of resources" error. Then I have checked out manual configuration and used "paranoid development" preset configuration, and lowered the resources as much as I can (see my attached configuration). Nevertheless I am still getting the same error and it fails.</p><p>Here are my questions for the current release; if answers would greatly change for v2.0, just ignore these and I will be waiting for the new one:</p><p>    - Is it fine to use Klever in such a low-resourced VM? If so, what my configurations should be? If not, what are the minimum system requirements for Klever?<br>    - How do I upload a new job (e.g. just a single C file, or a project with makefile)?</p><p>Thank you again,</p><p>Regards,</p><p>Ahmet</p> <div>On <span>16-10-2018 18</span>:00, Evgeny Novikov wrote:</div><blockquote type="cite">Also, I would like to inform you that in a couple of weeks we will release Klever 2.0 that will change very many things related with core functionalities. If you have time, then I recommend to wait for this release and try it rather than a version that will be deprecated soon.<br><br>16:08, 16 октября 2018 г., Evgeny Novikov <a href="mailto:novikov@ispras.ru" target="_blank"><novikov@ispras.ru></a>:<blockquote><div> <div>16.10.2018, 13:55, "Evgeny Novikov" <<a href="mailto:novikov@ispras.ru" target="_blank">novikov@ispras.ru</a>>:</div><blockquote type="cite"><div>Hello Ahmed,</div><div> </div><div>Your question is absolutely right. Klever lacks user documentation and I think that it will not have it in a near future. So, if you would like to proceed, most likely you will have many questions.</div><div> </div><div>You shouldn't run any script to start Klever if deployment was successful. You just need to open localhost:8998 in your web browser.</div></blockquote><div><br>I forgot to mention that there are 3 users created in advance:</div><ul><li>The first one is Administrator (login: admin, password: admin) that can change user privileges. Most likely you will not need it unlike you are going to create a multiuser setup.</li><li>The second one is Manager (login: manager, password: manager). This user can almost everything and you should start with it!</li><li>The third one is Service user that serves for internal purposes.</li></ul><div> </div><blockquote type="cite"><div> </div><div>If you will have any other questions, please, ask us. We will be glad to get some feedback from you.</div><div> </div><div>-- </div><div href="http://mailto:novikov@ispras.ru">Evgeny Novikov<br>Linux Verification Center, ISP RAS<br><a href="http://linuxtesting.org/" target="_blank">http://linuxtesting.org</a></div><div> </div><div> </div><div> </div><div>16.10.2018, 11:14, "A. Celenk" <<a href="mailto:ahmet.celenk@procenne.com" target="_blank">ahmet.celenk@procenne.com</a>>:</div><blockquote type="cite"><p>Hello,<br><br>I will ask a dumb question: How do we run Klever? I've completed the<br>deployment; but couldn't figure out which python script (or some other<br>thing) should I run to start testing.<br><br>P.S: I've used example klever-minimal.json.sample as configuration file.<br><br>Thanks a lot,<br><br>Ahmet Celenk<br><br><br>_______________________________________________<br>ldv-project mailing list<br><a href="mailto:ldv-project@linuxtesting.org" target="_blank">ldv-project@linuxtesting.org</a><br><a href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project" target="_blank">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a></p></blockquote></blockquote></div></blockquote></blockquote></div></blockquote>_______________________________________________<br>
ldv-project mailing list<br>
<a href="mailto:ldv-project@linuxtesting.org" target="_blank">ldv-project@linuxtesting.org</a><br>
<a href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project" rel="noreferrer" target="_blank">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a><br>
</blockquote></div></div>