genode/tool/cbe_autopilot
Martin Stein 30b8f4efc8 gems: import Genode-specific code of the CBE
The CBE repository contained a lot of Genode-specific code despite the fact
that the CBE core logic is not bound to Genode in any way. Therefore the
Genode-specific CBE code is moved to the 'gems' repository to form part of
Genode mainline. The remaining CBE code becomes a port in Genode instead of
being invoked as sub-repository.

The commit combines the following work steps:

* add all files removed from CBE repository
* add CBE port files
* make all CBE libs and targets build again
* make all CBE run scripts succeed again
* make all CBE recipes build again
* make CBE autopilot succeed again
* let CBE autopilot use 'libsparcrypto' contrib dir and Genode build dir
  instead of '.ci' dir in CBE contrib dir (remove '.ci' dir from CBE repo)
* let CBE autopilot always check for all ports
* make CBE autopilot directly executable
* fix license headers in all Genode CBE files
* remove unused VFS replay component
* remove unused CBE test
* remove unused external crypto
* remove unused files in run dir
* remove unused external trust anchor
* add cbe_tester test to autopilot list
* get rid of directories 'include/cbe_*' and 'include/utils'

Fixes #3937
2020-11-27 09:19:08 +01:00

200 lines
6.5 KiB
Makefile
Executable File

#!/usr/bin/make -sf
#
# \brief Tool to GNAT-prove and test the Consistent Block Encrypter (CBE)
# \author Martin Stein
# \date 2020-11-10
#
######################
# User configuration #
######################
DEFAULT_GENODE_DIR := $(realpath $(dir $(MAKEFILE_LIST))/..)
DEFAULT_BUILD_DIR := $(DEFAULT_GENODE_DIR)/.build.cbe_autopilot
DEFAULT_DEPOT_USER := cbe_autopilot
DEFAULT_DEPOT_DIR := $(DEFAULT_GENODE_DIR)/.depot.cbe_autopilot
DEFAULT_JOBS := $(shell nproc)
DEFAULT_CROSS_DEV_PREFIX := genode-x86-
GENODE_DIR ?= $(DEFAULT_GENODE_DIR)
BUILD_DIR ?= $(DEFAULT_BUILD_DIR)
DEPOT_USER ?= $(DEFAULT_DEPOT_USER)
DEPOT_DIR ?= $(DEFAULT_DEPOT_DIR)
JOBS ?= $(DEFAULT_JOBS)
CROSS_DEV_PREFIX ?= $(DEFAULT_CROSS_DEV_PREFIX)
VERBOSE ?= @
##########################
# Internal configuration #
##########################
ARCH := x86_64
CONTRIB_DIR := $(GENODE_DIR)/contrib
BUILD_CONF := $(BUILD_DIR)/etc/build.conf
TOOLS_CONF := $(BUILD_DIR)/etc/tools.conf
CBE_PROJECT_FILE := $(BUILD_DIR)/cbe.gpr
LSC_INSTALL_DIR := $(BUILD_DIR)/libsparkcrypto_install
####################
# Port directories #
####################
REPOSITORIES += $(GENODE_DIR)/repos/base
REPOSITORIES += $(GENODE_DIR)/repos/base-nova
REPOSITORIES += $(GENODE_DIR)/repos/base-linux
REPOSITORIES += $(GENODE_DIR)/repos/os
REPOSITORIES += $(GENODE_DIR)/repos/libports
REPOSITORIES += $(GENODE_DIR)/repos/ports
REPOSITORIES += $(GENODE_DIR)/repos/dde_linux
REPOSITORIES += $(GENODE_DIR)/repos/gems
include $(GENODE_DIR)/repos/base/mk/util.inc
PORTS := \
ada-runtime bash coreutils curl dde_linux libc libiconv libsparkcrypto \
libssh ncurses nova openssl qemu-usb stdcxx virtualbox5 zlib stb \
ttf-bitstream-vera cbe
MISSING_PORTS := \
$(strip $(foreach PORT,$(PORTS),$(if $(call select_from_ports,$(PORT)),,$(PORT))))
CBE_DIR := $(call select_from_ports,cbe)/cbe
LSC_DIR := $(call select_from_ports,libsparkcrypto)/libsparkcrypto
############
# Commands #
############
BUILD_DIR_MAKE := \
CROSS_DEV_PREFIX=$(CROSS_DEV_PREFIX) \
CONTRIB_DIR=$(CONTRIB_DIR) \
DEPOT_DIR=$(DEPOT_DIR) \
KERNEL=linux \
BOARD=linux \
$(MAKE) -sC $(BUILD_DIR)
DEPOT_CREATE := \
CROSS_DEV_PREFIX=$(CROSS_DEV_PREFIX) \
CONTRIB_DIR=$(CONTRIB_DIR) \
DEPOT_DIR=$(DEPOT_DIR) \
UPDATE_VERSIONS=1 \
FORCE=1 \
REBUILD= \
$(GENODE_DIR)/tool/depot/create -j$(JOBS)
CREATE_BUILD_DIR := \
BUILD_DIR=$(BUILD_DIR) \
$(GENODE_DIR)/tool/create_builddir
GNAT_PROVE_FLAGS := \
--mode=flow \
-j0 \
--prover=z3,cvc4 \
--steps=1000 \
--memlimit=1000 \
--checks-as-errors \
--warnings=error \
-U \
-P
GNAT_PROVE := gnatprove $(GNAT_PROVE_FLAGS)
###########
# Targets #
###########
usage:
@echo
@echo "Tool to GNAT-prove and test the Consistent Block Encrypter (CBE)"
@echo
@echo "Usage:"
@echo
@echo " $(firstword $(notdir $(MAKEFILE_LIST))) [clean|prove|basics]"
@echo
@echo "Considered environment variables:"
@echo ""
@echo " VERBOSE= Show individual operations."
@echo ""
@echo " JOBS=4 Number of jobs to execute in parallel."
@echo " Defaults to '$(DEFAULT_JOBS)'."
@echo ""
@echo " GENODE_DIR=~/genode Base directory of Genode repository."
@echo " Defaults to '$(DEFAULT_GENODE_DIR)'."
@echo ""
@echo " DEPOT_USER=shrimp Genode depot user-name."
@echo " Defaults to '$(DEFAULT_DEPOT_USER)'."
@echo ""
@echo " DEPOT_DIR=~/depot Base directory of Genode depot."
@echo " Defaults to '$(DEFAULT_DEPOT_DIR)'."
@echo ""
@echo " BUILD_DIR=~/build Genode build directory."
@echo " Defaults to '$(DEFAULT_BUILD_DIR)'."
@echo ""
@echo " CROSS_DEV_PREFIX=~/bin/genode-x86- GCC command prefix."
@echo " Defaults to '$(DEFAULT_CROSS_DEV_PREFIX)'."
ifneq ($(MISSING_PORTS),)
checked_ports_exist:
@echo ""
@echo "Error: Ports not prepared or outdated:"
@echo " $(MISSING_PORTS)"
@echo ""
@echo "You can prepare respectively update them as follows:"
@echo " $(GENODE_DIR)/tool/ports/prepare_port $(MISSING_PORTS) -j$(JOBS)"
@echo ""
@false
else
checked_ports_exist:
endif
RUN_OPT_DAU := RUN_OPT += --depot-auto-update
$(BUILD_DIR):
$(VERBOSE)$(CREATE_BUILD_DIR) $(ARCH)
$(VERBOSE)sed -i 's/^#REPOSITORIES +=/REPOSITORIES +=/g' $(BUILD_CONF)
$(VERBOSE)sed -i 's/^CONTRIB_DIR :=.*$$//g' $(BUILD_CONF)
$(VERBOSE)sed -i 's/^#MAKE += -j4$$/MAKE += -j$(JOBS)/g' $(BUILD_CONF)
$(VERBOSE)sed -i 's/^#$(RUN_OPT_DAU)$$/$(RUN_OPT_DAU)/g' $(BUILD_CONF)
$(VERBOSE)echo 'REPOSITORIES += $$(GENODE_DIR)/repos/cbe' >> $(BUILD_CONF)
$(VERBOSE)echo 'RUN_OPT += --autopilot' >> $(BUILD_CONF)
$(VERBOSE)echo 'RUN_OPT += --depot-user $(DEPOT_USER)' >> $(BUILD_CONF)
$(VERBOSE)echo 'CROSS_DEV_PREFIX=$(CROSS_DEV_PREFIX)' > $(TOOLS_CONF)
$(CBE_PROJECT_FILE): $(BUILD_DIR) checked_ports_exist
$(VERBOSE)echo 'with "$(LSC_INSTALL_DIR)/libsparkcrypto";' > $(CBE_PROJECT_FILE)
$(VERBOSE)echo 'project CBE is' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' for Create_Missing_Dirs use "True";' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' for Object_Dir use "$(BUILD_DIR)/cbe_gpr_object_dir";' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' for Source_Dirs use ("$(CBE_DIR)/src/lib/sha256_4k", "$(CBE_DIR)/src/lib/cbe", "$(CBE_DIR)/src/lib/cbe_common");' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' for Library_Kind use "static";' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' for Library_Name use "cbe";' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' -- show full paths' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' package Compiler is' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' for Switches ("Ada") use ("-gnatef");' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo ' end Compiler;' >> $(CBE_PROJECT_FILE)
$(VERBOSE)echo 'end CBE;' >> $(CBE_PROJECT_FILE)
$(LSC_INSTALL_DIR): $(BUILD_DIR) checked_ports_exist
$(VERBOSE)$(MAKE) -sC $(LSC_DIR) NO_SPARK=1 DESTDIR=$(LSC_INSTALL_DIR) install
.PHONY: prove
prove: $(LSC_INSTALL_DIR) $(CBE_PROJECT_FILE) checked_ports_exist
$(VERBOSE)$(GNAT_PROVE) $(CBE_PROJECT_FILE)
.PHONY: basics
basics: $(BUILD_DIR) prove checked_ports_exist
$(VERBOSE)$(DEPOT_CREATE) $(DEPOT_USER)/pkg/x86_64/cbe_demo
$(VERBOSE)$(BUILD_DIR_MAKE) run/cbe_tester
$(VERBOSE)$(BUILD_DIR_MAKE) run/vfs_cbe_init
$(VERBOSE)$(BUILD_DIR_MAKE) run/vfs_cbe
.PHONY: clean
clean:
$(VERBOSE)rm -rf $(BUILD_DIR) $(DEPOT_DIR)