Makefile

libhw-dir := $(dir $(lastword $(MAKEFILE_LIST)))

DESTDIR ?= dest

name ?= hw
hw-install = Makefile Makefile.proof gnat.adc spark.adc

top := $(CURDIR)
cnf := .config
obj := build

link-type ?= archive

ifeq ($(link-type),archive)
prefixed-name ?= lib$(name)
binary-suffix ?= .a
else ifeq ($(link-type),program)
prefixed-name ?= $(name)
binary-suffix ?=
endif
binary := $(obj)/$(prefixed-name)$(binary-suffix)
$(binary):

space :=
space +=
comma := ,

strip_quotes = $(strip $(subst ",,$(1)))
# fix syntax highlighting with an odd emoticon "))

$(foreach dep,$($(name)-deplibs), \
	$(eval -include $($(dep)-dir)/config))
-include $(cnf)

include $(libhw-dir)/Makefile.proof

CC       = $(CROSS_COMPILE)gcc
GNATBIND = $(CROSS_COMPILE)gnatbind

CFLAGS += -Wuninitialized -Wall -Werror
CFLAGS += -pipe -g
CFLAGS += -Wstrict-aliasing -Wshadow
CFLAGS += -fno-common -fomit-frame-pointer
CFLAGS += -ffunction-sections -fdata-sections

ADAFLAGS += $(CFLAGS) -gnatA -gnatec=$(libhw-dir)/gnat.adc -gnatp
# Ada warning options:
#
#  a   Activate most optional warnings.
# .e   Activate every optional warnings.
#  e   Treat warnings and style checks as errors.
#
#  D   Suppress warnings on implicit dereferences:
#      As SPARK does not accept access types we have to map the
#      dynamically chosen register locations to a static SPARK
#      variable.
#
# .H   Suppress warnings on holes/gaps in records:
#      We are modelling hardware here!
#
#  H   Suppress warnings on hiding:
#      It's too annoying, you run out of ideas for identifiers fast.
#
#  T   Suppress warnings for tracking of deleted conditional code:
#      We use static options to select code paths at compile time.
#
#  U   Suppress warnings on unused entities:
#      Would have lots of warnings for unused register definitions,
#      `withs` for debugging etc.
#
# .U   Deactivate warnings on unordered enumeration types:
#      As SPARK doesn't support `pragma Ordered` by now, we don't
#      use that, yet.
#
# .W   Suppress warnings on unnecessary Warnings Off pragmas:
#      Things get really messy when you use different compiler
#      versions, otherwise.
# .Y   Disable information messages for why package spec needs body:
#      Those messages are annoying. But don't forget to enable those,
#      if you need the information.
ADAFLAGS += -gnatwa.eeD.HHTU.U.W.Y
# Disable style checks for now
ADAFLAGS += -gnatyN

MAKEFLAGS += -rR

# Make is silent per default, but 'make V=1' will show all compiler calls.
ifneq ($(V),1)
.SILENT:
endif

# must come rather early
.SECONDEXPANSION:

ifeq ($(link-type),archive)
$(binary): $$($(name)-objs)
	@printf "    AR         $(subst $(obj)/,,$@)\n"
	ar cr $@ $^
else ifeq ($(link-type),program)
$(binary): $$($(name)-objs)
	@printf "    LINK       $(subst $(obj)/,,$@)\n"
	$(CC) -o $@ $^ \
		$(addprefix -L,$(abspath $($(name)-extra-objs))) \
		$(addprefix -l,$(patsubst lib%,%,$($(name)-deplibs))) \
		-lgnat
endif

$(foreach dep,$($(name)-deplibs), \
	$(eval $(name)-extra-objs += $($(dep)-dir)/lib) \
	$(eval $(name)-extra-incs += $($(dep)-dir)/include))

# Converts one or more source file paths to their corresponding build/ paths.
# Only .ads and .adb get converted to .o, other files keep their names.
# $1 file path (list)
src-to-obj = \
	$(addprefix $(obj)/,\
	$(patsubst $(obj)/%,%, \
	$(patsubst %.c,%.o,\
	$(patsubst %.ads,%.o,\
	$(patsubst %.adb,%.o,\
	$(2))))))

# Converts one or more source file paths to the corresponding build/ paths
# of their Ada library information (.ali) files.
# $1 file path (list)
src-to-ali = \
	$(addprefix $(obj)/,\
	$(patsubst $(obj)/%,%, \
	$(patsubst %.ads,%.ali,\
	$(patsubst %.adb,%.ali,\
	$(filter %.ads %.adb,$(2))))))

# Clean -y variables, include Makefile.inc
# Add paths to files in $(name)-y to $(name)-srcs
# Add subdirs-y to subdirs
# $1 dir to read Makefile.inc from
includemakefile = \
	$(eval $(name)-y :=) \
	$(eval $(name)-main-y :=) \
	$(eval $(name)-gen-y :=) \
	$(eval $(name)-proof-y :=) \
	$(eval subdirs-y :=) \
	$(eval include $(1)/Makefile.inc) \
	$(eval $(name)-main-src += \
		$(subst $(top)/,, \
		$(abspath $(patsubst $(1)//%,/%,$(addprefix $(1)/,$($(name)-main-y)))))) \
	$(eval $(name)-srcs += \
		$(subst $(top)/,, \
		$(abspath $(patsubst $(1)//%,/%,$(addprefix $(1)/,$($(name)-y)))))) \
	$(eval $(name)-gens += \
		$(subst $(top)/,, \
		$(abspath $($(name)-gen-y)))) \
	$(eval $(name)-proof += \
		$(subst $(top)/,, \
		$(abspath $(addprefix $(1)/,$($(name)-proof-y))))) \
	$(eval subdirs += \
		$(subst $(top)/,, \
		$(abspath $(addprefix $(1)/,$(subdirs-y))))) \

# For each path in $(subdirs) call includemakefiles
# Repeat until subdirs is empty
evaluate_subdirs = \
	$(eval cursubdirs := $(subdirs)) \
	$(eval subdirs :=) \
	$(foreach dir,$(cursubdirs), \
		$(call includemakefile,$(dir))) \
	$(if $(subdirs), \
		$(call evaluate_subdirs))

# collect all object files eligible for building
subdirs := .
$(call evaluate_subdirs)

$(name)-srcs += $($(name)-main-src)

# Eliminate duplicate mentions of source files
$(name)-srcs := $(sort $($(name)-srcs))
$(name)-gens := $(sort $($(name)-gens))

# For Ada includes
$(name)-ada-dirs := $(sort $(dir $(filter %.ads %.adb,$($(name)-srcs) $($(name)-gens))))

# To track dependencies, we need all Ada specification (.ads) files in
# *-srcs. Extract / filter all specification files that have a matching
# body (.adb) file here (specifications without a body are valid sources
# in Ada).
$(name)-extra-specs := \
	$(filter \
		$(addprefix %/,$(patsubst %.adb,%.ads,$(notdir $(filter %.adb,$($(name)-srcs))))), \
		$(filter %.ads,$($(name)-srcs) $($(name)-gens)))
$(name)-srcs := $(filter-out $($(name)-extra-specs),$($(name)-srcs))
$(name)-gens := $(filter-out $($(name)-extra-specs),$($(name)-gens))

$(name)-objs := $(call src-to-obj,,$($(name)-srcs) $($(name)-gens))
$(name)-alis := $(call src-to-ali,,$($(name)-srcs) $($(name)-gens))

# For gnatprove
$(name)-proof-dirs := \
	$(sort	$(dir $($(name)-proof)) \
		$(filter-out ada/% %/ada/%,$($(name)-ada-dirs)))

# For mkdir
alldirs := $(abspath $(dir $(sort $($(name)-objs))))

# Reads dependencies from an Ada library information (.ali) file
# Only basenames (with suffix) are preserved so we have to look the
# paths up in $($(name)-srcs) $($(name)-gens).
# $1 ali file
create_ada_deps = \
	$(if $(wildcard $(1)),\
		$(filter \
			$(addprefix %/,$(shell sed -ne's/^D \([^\t]\+\).*$$/\1/p' $(1) 2>/dev/null)), \
			$($(name)-srcs) $($(name)-gens) $($(name)-extra-specs)), \
		$($(name)-gens))

# Adds dependency rules
# $1 source file
add_ada_deps = \
	$(call src-to-obj,,$(1)): $(1) \
		$(call create_ada_deps,$(call src-to-ali,,$(1)))

# Writes a compilation rule for Ada sources
# $1 source type (ads, adb)
# $2 source files (including the colon)
# $3 obj path prefix (including the trailing slash)
# $4 compiler flags (if empty, $(ADAFLAGS) apply)
define add_ada_rule
$(2) $(3)%.o: %.$(1)
	@printf "    COMPILE    $$(subst $(obj)/,,$$@)\n"
	$(CC) \
		$(if $(4),$(4),$(ADAFLAGS)) \
		$(addprefix -I,$($(name)-ada-dirs) $($(name)-extra-incs)) \
		-c -o $$@ $$<
endef

# For sources
$(foreach type,ads adb, \
	$(eval $(call add_ada_rule,$(type),$(call src-to-obj,,$(filter %.$(type),$($(name)-srcs))):,$(obj)/)))
$(foreach file,$($(name)-srcs) $($(name)-gens), \
	$(eval $(call add_ada_deps,$(file))))

# For generated sources already in $(obj)/
$(foreach type,ads adb, \
	$(eval $(call add_ada_rule,$(type),$(call src-to-obj,,$(filter %.$(type),$($(name)-gens))):,)))

# Ali files are generated along with the object file. They need an empty
# recipe for correct updating.
$($(name)-alis): %.ali: %.o ;

# To support complex package initializations, we need to call the
# emitted code explicitly. gnatbind gathers all the calls for us
# and exports them as a procedure $(name)_adainit().
ifeq ($(link-type),archive)
$(name)-bind-dirs  := $($(name)-extra-objs)
$(name)-bind-flags := -a -n -L$(name)_ada
$(name)-bind-alis   = $(patsubst /%,%,$(subst $(dir $@),,$^))
else ifeq ($(link-type),program)
$(name)-bind-dirs  := $(sort $(dir $($(name)-objs))) $($(name)-extra-objs)
$(name)-bind-flags :=
$(name)-bind-alis   = $(subst $(dir $@),,$(call src-to-ali,,$($(name)-main-src)))
endif
$(obj)/b__$(prefixed-name).adb: $($(name)-alis)
	@printf "    BIND       $(subst $(obj)/,,$@)\n"
	# We have to give gnatbind a simple filename (without leading
	# path components) so just cd there.
	cd $(dir $@) && \
		$(GNATBIND) $(addprefix -aO,$(abspath $($(name)-bind-dirs))) \
			$($(name)-bind-flags) -o $(notdir $@) $($(name)-bind-alis)
$(eval $(call add_ada_rule,adb,$(obj)/b__$(prefixed-name).o:,,$(filter-out -gnatec=%,$(ADAFLAGS))))
$(name)-objs += $(obj)/b__$(prefixed-name).o

# Compilation rule for C sources
$(call src-to-obj,,$(filter %.c,$($(name)-srcs))): $(obj)/%.o: %.c
	@printf "    COMPILE    $(subst $(obj)/,,$@)\n"
	$(CC) $(CFLAGS) -c -o $@ $<

$(shell mkdir -p $(alldirs))

$(name)-install-srcs = $(sort \
	$($(name)-extra-specs) $(filter %.ads,$($(name)-srcs)) \
	$(foreach adb,$(filter %.adb,$($(name)-srcs)), \
		$(shell grep -q '^U .*\<BN\>' $(call src-to-ali,,$(adb)) 2>/dev/null && echo $(adb))))

$(name)-install-proof = \
	$(filter $(addprefix %/,$(notdir $($(name)-install-srcs))),$($(name)-proof)) \
	$(filter-out $(addprefix %/,$(notdir $($(name)-proof))),$($(name)-install-srcs))

install: $(binary) $($(name)-alis) $(libgpr)
	install -d $(DESTDIR)/lib $(DESTDIR)/include $(DESTDIR)/proof
	printf "    INSTALL    $(subst $(obj)/,,$(binary))\n"
	install $(binary) $(DESTDIR)/lib/
	$(foreach file,$($(name)-install) $(libgpr), \
		printf "    INSTALL    $(subst $(obj)/,,$(file))\n"; \
		install $(file) $(DESTDIR);)
	printf "    INSTALL    $(cnf)\n"
	install $(cnf) $(DESTDIR)/config
	printf "    INSTALL    %s\n" $(subst $(obj)/,,$($(name)-alis))
	install $($(name)-alis) $(DESTDIR)/lib/
	printf "    INSTALL    %s\n" $(subst $(obj)/,,$($(name)-install-srcs))
	install $($(name)-install-srcs) $(DESTDIR)/include/
	printf "    INSTALL    %s\n" $(subst $(obj)/,,$($(name)-install-proof))
	install $($(name)-install-proof) $(DESTDIR)/proof/

clean::
	rm -rf $(obj) $(name).gpr

distclean: clean
	rm -rf dest

.PHONY: install clean distclean