summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile78
-rw-r--r--Makefile.inc46
-rw-r--r--gnat.adc40
-rw-r--r--toolchain.inc2
4 files changed, 162 insertions, 4 deletions
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))