Remove klever dependencies

Makefile

@@ -21,7 +21,7 @@ cpu_cores=$(shell nproc)
 
 
 # Additional tools.
-klever="klever"
+cvv="cvv"
 cil="cil"
 frama_c_cil="frama_c_cil"
 benchexec="benchexec"
@@ -36,8 +36,8 @@ auto_script="auto_check.py"
 # Directories
 root_dir=$(shell pwd)
 install_dir=tools
-klever_dir=${install_dir}/${klever}
-mea_lib=${install_dir}/${klever}/bridge/reports/mea/core.py
+cvv_dir=${install_dir}/${cvv}
+mea_lib=bridge/reports/mea/core.py
 cil_dir=${install_dir}/${cil}
 frama_c_cil_dir=${install_dir}/${frama_c_cil}
 benchexec_dir=${install_dir}/${benchexec}
@@ -50,10 +50,10 @@ cil_arch="cil.xz"
 compiled_cil_arch="frama_c_cil.xz"
 
 # Repositories
-klever_repo="https://github.com/mutilin/klever.git"
+cvv_repo="https://github.com/vmordan/cvv.git"
 benchexec_repo="https://github.com/sosy-lab/benchexec.git"
-cif_repo="https://github.com/ldv-klever/cif.git"
-cif_compiled_link="https://github.com/ldv-klever/cif/releases/download/v1.2/linux-x86_64-cif-1.2.tar.xz"
+cif_repo="https://github.com/ldv-cvv/cif.git"
+cif_compiled_link="https://github.com/ldv-cvv/cif/releases/download/v1.2/linux-x86_64-cif-1.2.tar.xz"
 cil_compiled_link="https://forge.ispras.ru/attachments/download/9905/frama-c-cil-c012809.tar.xz"
 
 # Aux constants.
@@ -64,9 +64,9 @@ cif_revision=master
 tools_config_file=${install_dir}/config.json
 
 
-download-klever:
-	@$(call download_tool,${klever},${klever_dir},${klever_repo})
-	@cd ${klever_dir}; git checkout ${cvwi_branch}; git pull
+download-cvv:
+	@$(call download_tool,${cvv},${cvv_dir},${cvv_repo})
+	@cd ${cvv_dir}; git checkout ${cvwi_branch}; git pull
 
 download-benchexec:
 	@$(call download_tool,${benchexec},${benchexec_dir},${benchexec_repo})
@@ -84,14 +84,13 @@ download-frama-c-cil:
 	@rm -f ${compiled_cil_arch}
 	@cd ${install_dir}; wget ${cil_compiled_link} -O ${compiled_cil_arch}
 
-download: download-klever download-benchexec download-cpa
+download: download-cvv download-benchexec download-cpa
 	@echo "*** Downloading has been completed ***"
 
-build-klever: download-klever
-	@echo "*** Building ${klever} ***"
-	@echo "from bridge.development import *" > ${klever_dir}/bridge/bridge/settings.py
-	@echo "{}" > ${klever_dir}/bridge/bridge/db.json
-	@cp -r ${mea_lib} ${root_dir}/scripts/aux/mea.py
+build-cvv: download-cvv
+	@echo "*** Building ${cvv} ***"
+	@echo "from bridge.development import *" > ${cvv_dir}/bridge/bridge/settings.py
+	@echo "{}" > ${cvv_dir}/bridge/bridge/db.json
 
 build-benchexec: download-benchexec
 	@echo "*** Building ${benchexec} ***"
@@ -117,7 +116,7 @@ build-frama-c-cil: download-frama-c-cil
 	@mkdir -p ${frama_c_cil_dir}
 	@cd ${frama_c_cil_dir}; tar -xf ../${compiled_cil_arch}
 
-build: build-klever build-benchexec build-cil build-cpa
+build: build-cvv build-benchexec build-cil build-cpa
 	@echo "*** Building has been completed ***"
 
 clean-cpa:
@@ -139,20 +138,20 @@ check-deploy-dir:
 	@$(call check_dir,${DEPLOY_DIR},DEPLOY_DIR)
 
 
-install-klever: build-klever check-deploy-dir
-	@echo "*** Installing ${klever} ***"
+install-cvv: build-cvv check-deploy-dir
+	@echo "*** Installing ${cvv} ***"
 	@mkdir -p ${DEPLOY_DIR}/${install_dir}
-	@rm -rf ${DEPLOY_DIR}/${klever_dir}
-	@cp -r ${klever_dir} ${DEPLOY_DIR}/${klever_dir}
+	@rm -rf ${DEPLOY_DIR}/${cvv_dir}
+	@cp -r ${cvv_dir} ${DEPLOY_DIR}/${cvv_dir}
 	@mkdir -p ${DEPLOY_DIR}/scripts/aux
-	@cp -r ${mea_lib} ${DEPLOY_DIR}/scripts/aux/mea.py
-	@$(call shrink_installation,${DEPLOY_DIR}/${klever_dir})
+	@$(call shrink_installation,${DEPLOY_DIR}/${cvv_dir})
 
-deploy-klever-cv: build-klever check-deploy-dir
-	@echo "*** Deploying ${klever}-CV web-interface ***"
+deploy-cvv: build-cvv check-deploy-dir
+	@echo "*** Deploying ${cvv}-CV web-interface ***"
 	@mkdir -p ${DEPLOY_DIR}
 	@rm -rf ${DEPLOY_DIR}
-	@cp -r ${klever_dir} ${DEPLOY_DIR}
+	@cp -r ${cvv_dir} ${DEPLOY_DIR}
+	@cp -r scripts/aux/mea.py ${DEPLOY_DIR}/${mea_lib}
 	@$(call shrink_installation,${DEPLOY_DIR})
 
 install-benchexec: build-benchexec check-deploy-dir
@@ -200,53 +199,49 @@ install-scripts: check-deploy-dir
 	cp -r ${root_dir}/${plugin_dir} . ; \
 	mkdir -p buildbot
 
-install-witness-visualizer: check-deploy-dir build-klever
+install-witness-visualizer: check-deploy-dir build-cvv
 	@mkdir -p ${DEPLOY_DIR}/${install_dir}
 	@cp ${tools_config_file} ${DEPLOY_DIR}/${install_dir}
-	@rm -rf ${DEPLOY_DIR}/${klever_dir}
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}/core/core/vrp/et/
-	@cp ${klever_dir}/core/core/vrp/et/*.py ${DEPLOY_DIR}/${klever_dir}/core/core/vrp/et/
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}/bridge/
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}/bridge/templates/reports/
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}/bridge/reports/
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}/bridge/bridge/
-	@mkdir -p ${DEPLOY_DIR}/${klever_dir}/bridge/media/
-	@cp -r ${klever_dir}/bridge/static ${DEPLOY_DIR}/${klever_dir}/bridge/
-	@cp ${klever_dir}/bridge/templates/base.html ${DEPLOY_DIR}/${klever_dir}/bridge/templates/
-	@cp ${klever_dir}/bridge/reports/templates/reports/*.html ${DEPLOY_DIR}/${klever_dir}/bridge/templates/reports/
-	@cp -r ${klever_dir}/bridge/reports/mea ${DEPLOY_DIR}/${klever_dir}/bridge/reports/
-	@cp -r ${klever_dir}/bridge/reports/static ${DEPLOY_DIR}/${klever_dir}/bridge/reports/
-	@cp ${klever_dir}/bridge/reports/etv.py ${DEPLOY_DIR}/${klever_dir}/bridge/reports/
-	@cp ${klever_dir}/bridge/bridge/* ${DEPLOY_DIR}/${klever_dir}/bridge/bridge/
-	@rm -rf ${DEPLOY_DIR}/${klever_dir}/bridge/static/codemirror
-	@rm -rf ${DEPLOY_DIR}/${klever_dir}/bridge/static/calendar
-	@rm -rf ${DEPLOY_DIR}/${klever_dir}/bridge/static/jstree
-	@rm -rf ${DEPLOY_DIR}/${klever_dir}/bridge/static/js/population.js
+	@rm -rf ${DEPLOY_DIR}/${cvv_dir}
+	@mkdir -p ${DEPLOY_DIR}/${cvv_dir}
+	@mkdir -p ${DEPLOY_DIR}/${cvv_dir}/bridge/
+	@mkdir -p ${DEPLOY_DIR}/${cvv_dir}/bridge/templates/reports/
+	@mkdir -p ${DEPLOY_DIR}/${cvv_dir}/bridge/reports/
+	@mkdir -p ${DEPLOY_DIR}/${cvv_dir}/bridge/bridge/
+	@mkdir -p ${DEPLOY_DIR}/${cvv_dir}/bridge/media/
+	@cp -r ${cvv_dir}/bridge/static ${DEPLOY_DIR}/${cvv_dir}/bridge/
+	@cp ${cvv_dir}/bridge/templates/base.html ${DEPLOY_DIR}/${cvv_dir}/bridge/templates/
+	@cp ${cvv_dir}/bridge/reports/templates/reports/*.html ${DEPLOY_DIR}/${cvv_dir}/bridge/templates/reports/
+	@cp -r ${cvv_dir}/bridge/reports/mea ${DEPLOY_DIR}/${cvv_dir}/bridge/reports/
+	@cp -r ${cvv_dir}/bridge/reports/static ${DEPLOY_DIR}/${cvv_dir}/bridge/reports/
+	@cp ${cvv_dir}/bridge/reports/etv.py ${DEPLOY_DIR}/${cvv_dir}/bridge/reports/
+	@cp ${cvv_dir}/bridge/bridge/* ${DEPLOY_DIR}/${cvv_dir}/bridge/bridge/
+	@rm -rf ${DEPLOY_DIR}/${cvv_dir}/bridge/static/codemirror
+	@rm -rf ${DEPLOY_DIR}/${cvv_dir}/bridge/static/calendar
+	@rm -rf ${DEPLOY_DIR}/${cvv_dir}/bridge/static/jstree
+	@rm -rf ${DEPLOY_DIR}/${cvv_dir}/bridge/static/js/population.js
 	@cd ${DEPLOY_DIR} ; \
 	cp -r ${root_dir}/scripts/ . ; \
 	rm -f scripts/${launch_script} ; \
 	rm -f scripts/${auto_script} ; \
 	rm -f scripts/${bv_script} ; \
-	cp ${klever_dir}/bridge/reports/mea/core.py scripts/aux/mea.py
 	@echo "*** Witness Visualizer has been successfully installed into the directory ${DEPLOY_DIR} ***"
 
 install-mea: install-witness-visualizer
 	@cd ${DEPLOY_DIR} ; \
 	rm -f scripts/${wv_script} ; \
-	rm -rf ${klever_dir}/bridge/
+	rm -rf ${cvv_dir}/bridge/
 	@echo "*** MEA has been successfully installed into the directory ${DEPLOY_DIR} ***"
 
 install-benchmark-visualizer: install-witness-visualizer
-	@cp -r ${klever_dir}/utils/ ${DEPLOY_DIR}/${klever_dir}/
+	@cp -r ${cvv_dir}/utils/ ${DEPLOY_DIR}/${cvv_dir}/
 	@cp -f ${root_dir}/scripts/${bv_script} ${DEPLOY_DIR}/scripts/
-	@cp ${klever_dir}/core/core/*.py ${DEPLOY_DIR}/${klever_dir}/core/core/
 
-install: check-deploy-dir install-klever install-benchexec install-cil install-cpa install-scripts install-cpa
+install: check-deploy-dir install-cvv install-benchexec install-cil install-cpa install-scripts install-cpa
 	@$(call verify_installation,${DEPLOY_DIR})
 	@echo "*** Successfully installed into the directory ${DEPLOY_DIR}' ***"
 
-install-with-cloud: check-deploy-dir install-klever install-benchexec install-cil install-cpa-with-cloud-links install-scripts
+install-with-cloud: check-deploy-dir install-cvv install-benchexec install-cil install-cpa-with-cloud-links install-scripts
 	@$(call verify_installation,${DEPLOY_DIR})
 	@echo "*** Successfully installed into the directory ${DEPLOY_DIR}' with access to verification cloud ***"
 
@@ -324,7 +319,7 @@ endef
 # $1 - deploy directory
 define verify_installation
 	echo "Verifying installation in directory '$1'"
-	for tool in ${benchexec} ${klever}; do \
+	for tool in ${benchexec} ${cvv}; do \
 		if [ -d "${1}/${install_dir}/$${tool}" ]; then \
 			echo "Tool '$${tool}' is installed" ; \
 		else \
@@ -337,5 +332,5 @@ endef
 # $1 - deploy directory
 define shrink_installation
 	echo "Removing aux files in directory '$1'"
-	@cd ${1} && rm -rf presets/ .git bridge/reports/test_files/
+	@cd ${1} && rm -rf .git .idea
 endef

README.md

@@ -14,7 +14,7 @@ Witness Visualizer converts generic witnesses from [SV-COMP](https://sv-comp.sos
 
 Python (version>=3.4), python modules:
 ```shell
-sudo pip3 install requests ujson graphviz ply pytest atomicwrites more-itertools pluggy py attrs setuptools six django==2.1 psycopg2 pycparser sympy
+sudo pip3 install requests ujson graphviz ply pytest atomicwrites more-itertools pluggy py attrs setuptools six django psycopg2 pycparser sympy
 ```
 
 #### Deployment

configs/example.json

@@ -5,7 +5,7 @@
   },
   "tools": {
     "cil": "abs path to cilly.asm.exe",
-    "klever": "abs path to Klever core",
+    "cvv": "abs path to CVV",
     "benchexec": "abs path to benchexec",
     "cpachecker": {
       "unreachability": "abs path to CPAchecker branch ldv-bam",
@@ -105,10 +105,10 @@
     "master": "host, on which cloud master is running"
   },
   "uploader": {
-    "upload results": "if true, then results will be automatically uploaded into the server (Klever web-interface)",
+    "upload results": "if true, then results will be automatically uploaded into the server (CVV web-interface)",
     "identifier": "job identifier on the server",
     "parent id": "if true, then the given identifier will be treated as parent job identifier",
-    "server": "<host>:<port> of Klever web-interface",
+    "server": "<host>:<port> of CVV web-interface",
     "user": "valid user name on the server (this user should have access for this job identifier)",
     "password": "password for the user",
     "name": "name of the report to be uploaded"

docs/tools_ru.md

@@ -14,8 +14,8 @@ sudo apt install git openjdk-11-jdk python3 python3-dev ant lcov cmake libmpc-de
 sudo pip3 install requests ujson graphviz ply pytest atomicwrites pathlib2 more-itertools pluggy py attrs setuptools six django==2.1 clade psycopg2 pyyaml pycparser sympy
 ```
 
-1. Инструмент klever — web-интерфейс, отвечающий за визуализацию результатов.
-Репозиторий: https://github.com/mutilin/klever.git
+1. Инструмент CVV — web-интерфейс, отвечающий за визуализацию результатов.
+Репозиторий: https://github.com/vmordan/cvv
 Развёртывание web-интерфейса описано в инструкции docs/web_interface.txt.
 
 2. Инструмент CIL отвечает за объединение исходных файлов и их упрощение.

docs/web_interface.txt

@@ -1,9 +1,9 @@
 Deployment of the Continuous Verification web-interface for results visualization
 =================================================================================
 
-1. Deploy Klever-CV web-interface with command:
+1. Deploy CVV web-interface with command:
 
-make deploy-klever-cv DEPLOY_DIR=<deploy path>
+make deploy-cvv DEPLOY_DIR=<deploy path>
 
 WARNING: everything in the <deploy path> will be removed. This path will be used for keeping database files,
 therefore it should not be modified for correct visualization of results.

scripts/components/__init__.py

@@ -23,12 +23,10 @@
 
 # Default location of additional tools.
 CIL = "cil"
-ET_LIB = "klever"
 ET_HTML_LIB = "et html"
 BENCHEXEC = "benchexec"
 CPACHECKER = "cpachecker"
 CIF = "cif"
-CLADE = "clade"
 UPLOADER = "uploader"
 DEFAULT_CPACHECKER_SCRIPTS_PATH = "scripts"
 

scripts/components/coverage_processor.py

@@ -27,11 +27,11 @@
 import os
 import re
 import subprocess
-import sys
 import zipfile
 
 from components import *
 from components.component import Component
+from coverage.lcov import LCOV
 
 TAG_COVERAGE_MODE = "mode"
 TAG_COVERAGE_PERCENT_MODE = "percent mode"
@@ -271,13 +271,6 @@ def __full_coverage(self, source_dirs: set, coverage_file: str):
                 dummy_dir = os.path.join(src_dir, CLADE_WORK_DIR)
                 break
 
-        # Export libs.
-        et_parser_lib = self.get_tool_path(self._get_tool_default_path(ET_LIB),
-                                           self.config.get(TAG_TOOLS, {}).get(ET_LIB))
-        sys.path.append(et_parser_lib)
-        # noinspection PyUnresolvedReferences
-        from core.coverage import LCOV
-
         lcov = LCOV(self.internal_logger, coverage_file, dummy_dir, source_dirs, [],
                     self.launcher_dir, self.full_mode,
                     ignore_files={os.path.join(DIRECTORY_WITH_GENERATED_FILES,

scripts/components/mea.py

@@ -26,22 +26,15 @@
 import json
 import logging
 import multiprocessing
-import operator
-import re
 import resource
 import time
 import zipfile
 
-# noinspection PyUnresolvedReferences
-from aux.mea import DEFAULT_CONVERSION_FUNCTION, CONVERSION_FUNCTION_MODEL_FUNCTIONS, \
-    CONVERSION_FUNCTION_CALL_TREE, CONVERSION_FUNCTION_NOTES, convert_error_trace, \
-    compare_error_traces, is_equivalent, DEFAULT_COMPARISON_FUNCTION, \
-    DEFAULT_SIMILARITY_THRESHOLD, TAG_COMPARISON_FUNCTION, TAG_CONVERSION_FUNCTION, \
-    TAG_ADDITIONAL_MODEL_FUNCTIONS, CONVERSION_FUNCTION_FULL
-
 from aux.common import *
 from components import *
 from components.component import Component
+from mea.core import *
+from mea.et import import_error_trace
 
 ERROR_TRACE_FILE = "error trace.json"
 CONVERTED_ERROR_TRACES = "converted error traces.json"
@@ -86,7 +79,6 @@ def __init__(self, general_config: dict, error_traces: list, install_dir: str, r
                 os.makedirs(self.result_dir, exist_ok=True)
         else:
             self.result_dir = None
-        self.__export_et_parser_lib()
         self.rule = rule
 
         # List of files with error traces.
@@ -323,6 +315,7 @@ def __print_trace_archive(self, error_trace_file_name: str, witness_type=WITNESS
                 'reports',
             )
             django.setup()
+            self.__export_et_parser_lib()
             # noinspection PyUnresolvedReferences
             from reports.etv import convert_json_trace_to_html
             with open(json_trace_name, encoding="utf8") as trace_file:
@@ -348,11 +341,8 @@ def __process_parsed_trace(parsed_error_trace: dict):
         parsed_error_trace['files'] = src_files
 
     def __parse_trace(self, error_trace_file: str, supported_types: set) -> dict:
-        # noinspection PyUnresolvedReferences
-        from core.vrp.et import import_error_trace
-
         # Those messages are waste of space.
-        logger = self._create_logger(
+        logger = Component._create_logger(
             "Witness processor", logging.WARNING if self.debug else logging.ERROR
         )
         try:
@@ -429,9 +419,6 @@ def __get_option_for_rule(self, tag: str, default_value):
         return self.component_config.get(self.rule, {}).get(tag, default)
 
     def __export_et_parser_lib(self):
-        et_parser_lib = self.get_tool_path(self._get_tool_default_path(ET_LIB),
-                                           self.config.get(TAG_TOOLS, {}).get(ET_LIB))
-        sys.path.append(et_parser_lib)
         et_html_lib = self.get_tool_path(self._get_tool_default_path(ET_HTML_LIB),
                                          self.config.get(TAG_TOOLS, {}).get(ET_HTML_LIB))
         sys.path.append(et_html_lib)

scripts/coverage/__init__.py

@@ -0,0 +1,18 @@
+#
+# CV is a framework for continuous verification.
+#
+# Copyright (c) 2018-2023 ISP RAS (http://www.ispras.ru)
+# Ivannikov Institute for System Programming of the Russian Academy of Sciences
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#