diff --git a/Makefile b/Makefile index 54a55b36d7..66dbe32334 100644 --- a/Makefile +++ b/Makefile @@ -183,16 +183,32 @@ add-special-class= \ $(eval special-classes+=$(1)) # Converts one or more source file paths to their corresponding build/ paths. -# Only .c and .S get converted to .o, other files (like .ld) keep their name. +# Only .ads, adb, .c and .S get converted to .o, other files (like .ld) keep +# their name. # $1 stage name # $2 file path (list) src-to-obj=\ $(patsubst $(obj)/%,$(obj)/$(1)/%,\ $(patsubst $(obj)/$(1)/%,$(obj)/%,\ $(patsubst src/%,$(obj)/%,\ + $(patsubst %.ads,%.o,\ + $(patsubst %.adb,%.o,\ $(patsubst %.c,%.o,\ $(patsubst %.S,%.o,\ - $(subst .$(1),,$(2))))))) + $(subst .$(1),,$(2))))))))) + +# Converts one or more source file paths to the corresponding build/ paths +# of their Ada library information (.ali) files. +# $1 stage name +# $2 file path (list) +src-to-ali=\ + $(patsubst $(obj)/%,$(obj)/$(1)/%,\ + $(patsubst $(obj)/$(1)/%,$(obj)/%,\ + $(patsubst src/%,$(obj)/%,\ + $(patsubst %.ads,%.ali,\ + $(patsubst %.adb,%.ali,\ + $(subst .$(1),,\ + $(filter %.ads %.adb,$(2)))))))) # Clean -y variables, include Makefile.inc # Add paths to files in X-y to X-srcs @@ -229,7 +245,22 @@ endif # Eliminate duplicate mentions of source files in a class $(foreach class,$(classes),$(eval $(class)-srcs:=$(sort $($(class)-srcs)))) +# 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). +$(foreach class,$(classes),$(eval $(class)-extra-specs := \ + $(filter \ + $(addprefix %/,$(patsubst %.adb,%.ads,$(notdir $(filter %.adb,$($(class)-srcs))))), \ + $(filter %.ads,$($(class)-srcs))))) +$(foreach class,$(classes),$(eval $(class)-srcs := \ + $(filter-out $($(class)-extra-specs),$($(class)-srcs)))) + $(foreach class,$(classes),$(eval $(class)-objs:=$(call src-to-obj,$(class),$($(class)-srcs)))) +$(foreach class,$(classes),$(eval $(class)-alis:=$(call src-to-ali,$(class),$($(class)-srcs)))) + +# For Ada includes +$(foreach class,$(classes),$(eval $(class)-ada-dirs:=$(sort $(dir $(filter %.ads %.adb,$($(class)-srcs)) $($(class)-extra-specs))))) # Save all objs before processing them (for dependency inclusion) originalobjs:=$(foreach var, $(addsuffix -objs,$(classes)), $($(var))) @@ -242,6 +273,17 @@ allsrcs:=$(foreach var, $(addsuffix -srcs,$(classes)), $($(var))) allobjs:=$(foreach var, $(addsuffix -objs,$(classes)), $($(var))) alldirs:=$(sort $(abspath $(dir $(allobjs)))) +# Reads dependencies from an Ada library information (.ali) file +# Only basenames (with suffix) are preserved so we have to look the +# paths up in $($(stage)-srcs). +# $1 stage name +# $2 ali file +create_ada_deps=$$(if $(2),\ + gnat.adc \ + $$(filter \ + $$(addprefix %/,$$(shell sed -ne's/^D \([^\t]\+\).*$$$$/\1/p' $(2) 2>/dev/null)), \ + $$($(1)-srcs) $$($(1)-extra-specs))) + # macro to define template macros that are used by use_template macro define create_cc_template # $1 obj class @@ -250,9 +292,13 @@ define create_cc_template # $4 additional dependencies ifn$(EMPTY)def $(1)-objs_$(2)_template de$(EMPTY)fine $(1)-objs_$(2)_template -$$(call src-to-obj,$1,$$(1).$2): $$(1).$2 $(KCONFIG_AUTOHEADER) $(4) +$$(call src-to-obj,$1,$$(1).$2): $$(1).$2 $$(call create_ada_deps,$1,$$(call src-to-ali,$1,$$(1).$2)) $(KCONFIG_AUTOHEADER) $(4) @printf " CC $$$$(subst $$$$(obj)/,,$$$$(@))\n" - $(CC_$(1)) -MMD $$$$(CPPFLAGS_$(1)) $$$$(CFLAGS_$(1)) -MT $$$$(@) $(3) -c -o $$$$@ $$$$< + $(CC_$(1)) \ + $$(if $$(filter-out ads adb,$(2)), \ + -MMD $$$$(CPPFLAGS_$(1)) $$$$(CFLAGS_$(1)) -MT $$$$(@), \ + $$$$(ADAFLAGS_$(1)) $$$$(addprefix -I,$$$$($(1)-ada-dirs))) \ + $(3) -c -o $$$$@ $$$$< en$(EMPTY)def end$(EMPTY)if endef @@ -267,6 +313,30 @@ $(foreach class,$(classes), \ foreach-src=$(foreach file,$($(1)-srcs),$(eval $(call $(1)-objs_$(subst .,,$(suffix $(file)))_template,$(basename $(file))))) $(eval $(foreach class,$(classes),$(call foreach-src,$(class)))) +# To supported complex package initializations, we need to call the +# emitted code explicitly. gnatbind gathers all the calls for us +# and exports them as a procedure $(stage)_adainit(). Every stage that +# uses Ada code has to call it! +define gnatbind_template +# $1 class +$$(obj)/$(1)/b__$(1).adb: $$$$(filter-out $$(obj)/$(1)/b__$(1).ali,$$$$($(1)-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_$(1)) -a -n \ + -L$(1)_ada -o $$(notdir $$@) \ + $$(subst $$(dir $$@),,$$^) +$$(obj)/$(1)/b__$(1).o: $$(obj)/$(1)/b__$(1).adb + @printf " CC $$(subst $$(obj)/,,$$@)\n" + $(CC_$(1)) $$(ADAFLAGS_$(1)) -c -o $$@ $$< +$(1)-objs += $$(obj)/$(1)/b__$(1).o +$($(1)-alis): %.ali: %.o +endef + +$(eval $(foreach class,$(classes), \ + $(if $($(class)-alis),$(call gnatbind_template,$(class))))) + DEPENDENCIES += $(addsuffix .d,$(basename $(allobjs))) -include $(DEPENDENCIES) diff --git a/Makefile.inc b/Makefile.inc index 21b07e666c..316cd22921 100644 --- a/Makefile.inc +++ b/Makefile.inc @@ -359,6 +359,50 @@ CFLAGS_common += -Wstrict-aliasing -Wshadow -Wdate-time CFLAGS_common += -fno-common -ffreestanding -fno-builtin -fomit-frame-pointer CFLAGS_common += -ffunction-sections -fdata-sections +ADAFLAGS_common += -gnatg -gnatp +ADAFLAGS_common += -Wuninitialized -Wall -Werror +ADAFLAGS_common += -pipe -g -nostdinc +ADAFLAGS_common += -Wstrict-aliasing -Wshadow +ADAFLAGS_common += -fno-common -fomit-frame-pointer +ADAFLAGS_common += -ffunction-sections -fdata-sections +# 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_common += -gnatwa.eeD.HHTU.U.W.Y +# Disable style checks for now +ADAFLAGS_common += -gnatyN + LDFLAGS_common := --gc-sections -nostdlib -nostartfiles -static --emit-relocs ifeq ($(CONFIG_COMPILER_GCC),y) @@ -371,8 +415,10 @@ CFLAGS_common += -Werror endif ifneq ($(GDB_DEBUG),) CFLAGS_common += -Og +ADAFLAGS_common += -Og else CFLAGS_common += -Os +ADAFLAGS_common += -Os endif additional-dirs := $(objutil)/cbfstool $(objutil)/romcc $(objutil)/ifdtool \ diff --git a/gnat.adc b/gnat.adc new file mode 100644 index 0000000000..3b463dc26a --- /dev/null +++ b/gnat.adc @@ -0,0 +1,40 @@ +-- +-- This file is part of the coreboot project. +-- +-- This program is free software; you can redistribute it and/or modify +-- it under the terms of the GNU General Public License as published by +-- the Free Software Foundation; version 2 of the License. +-- +-- This program is distributed in the hope that it will be useful, +-- but WITHOUT ANY WARRANTY; without even the implied warranty of +-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +-- GNU General Public License for more details. +-- + +pragma Restrictions (No_Access_Subprograms); +pragma Restrictions (No_Allocators); +pragma Restrictions (No_Calendar); +pragma Restrictions (No_Dispatch); +pragma Restrictions (No_Exception_Handlers); +pragma Restrictions (No_Fixed_Point); +pragma Restrictions (No_Floating_Point); +pragma Restrictions (No_Implicit_Dynamic_Code); +pragma Restrictions (No_Implicit_Heap_Allocations); +pragma Restrictions (No_Implicit_Loops); +pragma Restrictions (No_Initialize_Scalars); +pragma Restrictions (No_IO); +pragma Restrictions (No_Local_Allocators); +pragma Restrictions (No_Recursion); +pragma Restrictions (No_Secondary_Stack); +pragma Restrictions (No_Streams); +pragma Restrictions (No_Tasking); +pragma Restrictions (No_Unchecked_Access); +pragma Restrictions (No_Unchecked_Deallocation); +pragma Restrictions (No_Wide_Characters); +pragma Restrictions (Static_Storage_Size); +pragma Assertion_Policy + (Statement_Assertions => Disable, + Pre => Disable, + Post => Disable); +pragma Overflow_Mode (General => Strict, Assertions => Eliminated); +pragma SPARK_Mode (On); diff --git a/toolchain.inc b/toolchain.inc index 21b07b4cba..2876990b02 100644 --- a/toolchain.inc +++ b/toolchain.inc @@ -117,11 +117,13 @@ CC_$(1) := $(CC_$(2)) LD_$(1) := $(LD_$(2)) NM_$(1) := $(NM_$(2)) AR_$(1) := $(AR_$(2)) +GNATBIND_$(1) := $(GNATBIND_$(2)) OBJCOPY_$(1) := $(OBJCOPY_$(2)) OBJDUMP_$(1) := $(OBJDUMP_$(2)) STRIP_$(1) := $(STRIP_$(2)) READELF_$(1) := $(READELF_$(2)) CFLAGS_$(1) = $$(CFLAGS_common) $$(CFLAGS_$(2)) +ADAFLAGS_$(1) = $$(ADAFLAGS_common) $$(ADAFLAGS_$(2)) CPPFLAGS_$(1) = $$(CPPFLAGS_common) $$(CPPFLAGS_$(2)) -D__ARCH_$(2)__ COMPILER_RT_$(1) := $$(COMPILER_RT_$(2)) COMPILER_RT_FLAGS_$(1) := $$(COMPILER_RT_FLAGS_$(2))