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