diff --git a/tool/cbe_autopilot b/tool/cbe_autopilot deleted file mode 100755 index 05a6df050c..0000000000 --- a/tool/cbe_autopilot +++ /dev/null @@ -1,199 +0,0 @@ -#!/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)