[coreboot-gerrit] Patch set updated for coreboot: Make Ada a first class citizen
Nico Huber (nico.h@gmx.de)
gerrit at coreboot.org
Tue Jul 19 19:52:49 CEST 2016
Nico Huber (nico.h at gmx.de) just uploaded a new patch set to gerrit, which you can find at https://review.coreboot.org/13044
-gerrit
commit 59e3df7813b1dfc2d8cf146332495e307c47f203
Author: Nico Huber <nico.h at gmx.de>
Date: Thu Jan 14 01:13:33 2016 +0100
Make Ada a first class citizen
Some remarks on the make process:
o We usually leave Ada specs (.ads files which are like c headers)
together with the bodies (implementations in .adb files) in one
directory. So we have to know, where they live.
o If there is no matching .adb an .ads is a valid source file and
we'll generate an object file from it.
o Object files need to have the same basename as their source files :-/
That's why we put them in build/<class>/ dirs now.
o We track dependencies by looking at the compiler output (.ali files
which accompany every .o). This way we don't need any gnatmake
magic, or even more complex, less portable tools.
For ADAFLAGS_common, I simply copied the CFLAGS_common whilst dropping
everything unsupported and adding sane warning options.
The set of language features is highly restricted (see gnat.adc). This
is a requirement to prove absence of runtime errors with SPARK.
Change-Id: I70df9adbd467ecd2dc7c5c1cf418b7765aca4e93
Signed-off-by: Nico Huber <nico.h at gmx.de>
---
Makefile | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
Makefile.inc | 46 +++++++++++++++++++++++++++++++++++
gnat.adc | 40 ++++++++++++++++++++++++++++++
toolchain.inc | 2 ++
4 files changed, 162 insertions(+), 4 deletions(-)
diff --git a/Makefile b/Makefile
index 1c86bf6..e052e0f 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,16 @@ 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),\
+ $$(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 +291,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 +312,31 @@ $(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
+endef
+
+$(eval $(foreach class,$(classes), \
+ $(if $($(class)-alis),$(call gnatbind_template,$(class)))))
+
+%.ali: %.o
+
DEPENDENCIES += $(addsuffix .d,$(basename $(allobjs)))
-include $(DEPENDENCIES)
diff --git a/Makefile.inc b/Makefile.inc
index 69c8843..7ccab60 100644
--- a/Makefile.inc
+++ b/Makefile.inc
@@ -350,6 +350,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)
@@ -362,8 +406,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 0000000..3b463dc
--- /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 c891193..06b87d3 100644
--- a/toolchain.inc
+++ b/toolchain.inc
@@ -116,11 +116,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))
More information about the coreboot-gerrit
mailing list