Skip to content

Commit

Permalink
firmware/coreboot: Subtree merged libhwbase
Browse files Browse the repository at this point in the history
Signed-off-by: David Hendricks <dhendricks@fb.com>
  • Loading branch information
dhendrix committed Jun 14, 2018
2 parents d4467c3 + 637f2a4 commit 6f4bd2f
Show file tree
Hide file tree
Showing 47 changed files with 3,122 additions and 1 deletion.
1 change: 0 additions & 1 deletion firmware/coreboot/3rdparty/libhwbase
Submodule libhwbase deleted from 637f2a
5 changes: 5 additions & 0 deletions firmware/coreboot/3rdparty/libhwbase/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
/proof-allconfigs/
/build/
/dest/
/*.gpr
/.config
339 changes: 339 additions & 0 deletions firmware/coreboot/3rdparty/libhwbase/COPYING

Large diffs are not rendered by default.

316 changes: 316 additions & 0 deletions firmware/coreboot/3rdparty/libhwbase/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,316 @@
libhw-dir := $(dir $(lastword $(MAKEFILE_LIST)))

DESTDIR ?= dest

name ?= hw
hw-install = Makefile Makefile.proof debug.adc 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

ifeq ($(DEBUG),1)
gnat-adc = $(libhw-dir)/debug.adc
else
gnat-adc = $(libhw-dir)/gnat.adc
endif

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=$(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) $($(name)-gens)) \
$(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) $($(name)-gens) $(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
2 changes: 2 additions & 0 deletions firmware/coreboot/3rdparty/libhwbase/Makefile.inc
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
subdirs-y += ada common proof c
subdirs-y += debug
Loading

0 comments on commit 6f4bd2f

Please sign in to comment.