#!/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)