Makefile

# Continuous Verification Launcher prepares and solves verification tasks for
# a given software system. Repository: https://github.com/ispras/cv-launcher
#
# Copyright © 2025 Vitalii Mordan, ISP RAS
#
# SPDX-License-Identifier: Apache-2.0

cpu_cores=$(shell nproc)


# Additional tools.
cvv="cvv"
cil="cil"
frama_c_cil="frama_c_cil"
benchexec="benchexec"
cif="cif"

# Directories
root_dir=$(shell pwd)
install_dir=tools
cvv_dir=${install_dir}/${cvv}
cil_dir=${install_dir}/${cil}
frama_c_cil_dir=${install_dir}/${frama_c_cil}
benchexec_dir=${install_dir}/${benchexec}
cif_dir=${install_dir}/${cif}
plugin_dir="plugin"
deployment_dir="deployment"

compiled_cif_arch="cif.xz"
cil_arch="cil.xz"
compiled_cil_arch="frama_c_cil.xz"

# Repositories
cvv_repo="https://github.com/ispras/cv-visualizer.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"
cil_compiled_link="https://forge.ispras.ru/attachments/download/9905/frama-c-cil-c012809.tar.xz"

# Aux constants.
cvv_branch=master
benchexec_branch=3.16
cif_revision=master

tools_config_file=${install_dir}/config.json


download-cvv:
	@$(call download_tool,${cvv},${cvv_dir},${cvv_repo})
	@cd ${cvv_dir}; git checkout ${cvv_branch}; git pull

download-benchexec:
	@$(call download_tool,${benchexec},${benchexec_dir},${benchexec_repo})
	@cd ${benchexec_dir}; git checkout ${benchexec_branch}

download-cif:
	@$(call download_tool,${cif},${cif_dir},${cif_repo})
	@cd ${cif_dir}; git checkout ${cif_revision}; git submodule update

download-cif-compiled:
	@rm -f ${compiled_cif_arch}
	@cd ${install_dir}; wget ${cif_compiled_link} -O ${compiled_cif_arch}

download-frama-c-cil:
	@rm -f ${compiled_cil_arch}
	@cd ${install_dir}; wget ${cil_compiled_link} -O ${compiled_cil_arch}

download: download-cvv download-benchexec download-cpa
	@echo "*** Downloading has been completed ***"

build-cvv: download-cvv
	@echo "*** Building ${cvv} ***"
	@echo "from web.development import *" > ${cvv_dir}/web/web/settings.py
	@echo "{}" > ${cvv_dir}/web/web/db.json

build-benchexec: download-benchexec
	@echo "*** Building ${benchexec} ***"
	@cd ${benchexec_dir}; ./setup.py build

build-cif: download-cif
	@echo "*** Building ${cif} ***"
	@cd ${cif_dir}; make -j ${cpu_cores}

build-cif-compiled: download-cif-compiled
	@echo "*** Building compiled ${cif} ***"
	@rm -rf ${cif_dir}
	@cd ${install_dir}; tar -xf ${compiled_cif_arch}

build-cil:
	@echo "*** Building ${cil} ***"
	@rm -rf ${cil_dir}
	@cd ${install_dir}; tar -xf ${cil_arch}

build-frama-c-cil: download-frama-c-cil
	@echo "*** Building ${frama_c_cil} ***"
	@rm -rf ${frama_c_cil_dir}
	@mkdir -p ${frama_c_cil_dir}
	@cd ${frama_c_cil_dir}; tar -xf ../${compiled_cil_arch}

build: build-cvv build-benchexec build-cil build-cpa
	@echo "*** Building has been completed ***"

clean-cpa:
	@./build_cpa.py -m clean

custom-build-cpa:
	@./build_cpa.py -m custom

build-cpa:
	@./build_cpa.py -m build

download-cpa:
	@./build_cpa.py -m download

install-cpa:
	@./build_cpa.py -m install -i ${DEPLOY_DIR}

check-deploy-dir:
	@$(call check_dir,${DEPLOY_DIR},DEPLOY_DIR)


install-cvv: build-cvv check-deploy-dir
	@echo "*** Installing ${cvv} ***"
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@rm -rf ${DEPLOY_DIR}/${cvv_dir}
	@cp -r ${cvv_dir} ${DEPLOY_DIR}/${cvv_dir}
	@$(call shrink_installation,${DEPLOY_DIR}/${cvv_dir})


install-benchexec: build-benchexec check-deploy-dir
	@echo "*** Installing ${benchexec} ***"
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@rm -rf ${DEPLOY_DIR}/${benchexec_dir}
	@cp -r ${benchexec_dir} ${DEPLOY_DIR}/${benchexec_dir}

install-cil: build-cil check-deploy-dir
	@echo "*** Installing ${cil} ***"
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@rm -rf ${DEPLOY_DIR}/${cil_dir}
	@cp -r ${cil_dir} ${DEPLOY_DIR}/${cil_dir}

install-frama-c-cil: build-frama-c-cil check-deploy-dir
	@echo "*** Installing ${frama_c_cil} ***"
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@rm -rf ${DEPLOY_DIR}/${frama_c_cil_dir}
	@cp -r ${frama_c_cil_dir} ${DEPLOY_DIR}/${frama_c_cil_dir}

install-cif: build-cif check-deploy-dir
	@echo "*** Installing ${cif} ***"
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@rm -rf ${DEPLOY_DIR}/${cif_dir}
	@cd ${cif_dir}; DESTDIR=$(realpath ${DEPLOY_DIR})/${cif_dir} make install

install-cif-compiled: build-cif-compiled check-deploy-dir
	@echo "*** Installing compiled ${cif} ***"
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@rm -rf ${DEPLOY_DIR}/${cif_dir}
	@cp -r ${cif_dir} ${DEPLOY_DIR}/${cif_dir}

install-scripts: check-deploy-dir
	@mkdir -p ${DEPLOY_DIR}/${install_dir}
	@mkdir -p ${root_dir}/${plugin_dir}
	@cp ${tools_config_file} ${DEPLOY_DIR}/${install_dir}
	@cp ${tools_config_file} cvf/${install_dir}
	@cp -r cvf launcher entrypoints patches properties ${plugin_dir} configs ${DEPLOY_DIR}
	@mkdir -p ${DEPLOY_DIR}/buildbot

install: check-deploy-dir install-cvv install-benchexec install-cil install-cpa install-scripts install-cpa install-cif-compiled
	@$(call verify_installation,${DEPLOY_DIR})
	@echo "*** Successfully installed into the directory ${DEPLOY_DIR}' ***"

install-with-cloud: check-deploy-dir install-cvv install-benchexec install-cil install-cpa-with-cloud-links install-scripts install-cif-compiled
	@$(call verify_installation,${DEPLOY_DIR})
	@echo "*** Successfully installed into the directory ${DEPLOY_DIR}' with access to verification cloud ***"

install-cpa-with-cloud-links: | check-deploy-dir install-cpa
	@$(call check_dir,${VCLOUD_DIR},"VCLOUD_DIR","is_exist")
#	@for cpa in ${cpa_modes}; do \
#		cd "${DEPLOY_DIR}/${install_dir}/$${cpa}" ; \
#		mkdir -p lib/java-benchmark/ ; \
#		cp ${VCLOUD_DIR}/vcloud.jar lib/java-benchmark/ ; \
#	done
	@echo "*** Successfully created links for verification cloud in CPAchecker installation directories ***"

install-plugin:
	@$(call check_dir,${PLUGIN_DIR},"PLUGIN_DIR","is_exist")
	@$(call check_dir,${PLUGIN_ID},"PLUGIN_ID")
	@echo "*** Installing plugin '${PLUGIN_ID}' into directory '${plugin_dir}/${PLUGIN_ID}' ***"
	@if [ -d "${plugin_dir}/${PLUGIN_ID}" ]; then \
		echo "*** Removing old plugin installation '${plugin_dir}/${PLUGIN_ID}' ***" ; \
	fi
	@mkdir -p ${plugin_dir}
	@ln -s ${PLUGIN_DIR} ${plugin_dir}/${PLUGIN_ID}

install-control-groups-daemon:
	@sudo cp ${deployment_dir}/cgroups-boot /etc/init.d/
	@sudo chown root:root /etc/init.d/cgroups-boot
	@sudo update-rc.d cgroups-boot defaults

delete-plugins:
	@echo "*** Removing all installed plugins ***"
	@rm -rf plugin/*

clean:
	@echo "*** Removing old installation ***"
	@find ${install_dir} -mindepth 1 -maxdepth 1 -type d -exec rm -rf {} +
	@rm -f ${install_dir}/cif.xz
	@cd cvf; git reset --hard;


verify-installation: check-deploy-dir
	@$(call verify_installation,${DEPLOY_DIR})

# download_tool(name, path, repository)
define download_tool
	if [ -d "$2" ]; then \
		echo "*** Tool $1 is already downloaded in directory $2 ***" ; \
	else \
		echo "*** Downloading tool $1 into directory $2 ***" ; \
		git clone --recursive $3 $2 ; \
	fi
	cd $2; git fetch
endef

# $1 - absolute directory path, $2 - env variable name, $3 - aux options
define check_dir
	if [ -n "$1" ]; then \
		if [ "$1" -ef "${root_dir}" ]; then \
			echo "Specified directory path '$1' is the same as current directory"; \
			false ; \
		else \
			if [ "$3" = "is_exist" ] ; then \
				if [ -d "$1" ] ; then \
					true ; \
				else \
					echo "Specified directory path '$1' does not exist. Add correct path to the '$2' environment variable"; \
					false; \
				fi ; \
			else \
				true ; \
			fi \
		fi ; \
	else \
		echo "Required variable '$2' was not specified"; \
		false; \
	fi
endef

# $1 - deploy directory
define verify_installation
	echo "Verifying installation in directory '$1'"
	for tool in ${benchexec} ${cvv}; do \
		if [ -d "${1}/${install_dir}/$${tool}" ]; then \
			echo "Tool '$${tool}' is installed" ; \
		else \
			echo "Something went wrong during installation: tool '$${tool}' is not found in directory '${1}/${install_dir}."; \
			exit 1; \
		fi ; \
	done
endef

# $1 - deploy directory
define shrink_installation
	echo "Removing aux files in directory '$1'"
	@cd ${1} && rm -rf .git .idea
endef