Initial upstream commit
The history contained unlicensed code so everything got squashed, sorry.
Change-Id: Ie1335ecfcee7f740bb6de2e9887606be30a2deff
Signed-off-by: Nico Huber <nico.huber@secunet.com>
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..69f6818
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,5 @@
+/proof-allconfigs/
+/build/
+/dest/
+/*.gpr
+/.config
diff --git a/COPYING b/COPYING
new file mode 100644
index 0000000..d159169
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,339 @@
+ GNU GENERAL PUBLIC LICENSE
+ Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+ Preamble
+
+ The licenses for most software are designed to take away your
+freedom to share and change it. By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users. This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it. (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.) You can apply it to
+your programs, too.
+
+ When we speak of free software, we are referring to freedom, not
+price. Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+ To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+ For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have. You must make sure that they, too, receive or can get the
+source code. And you must show them these terms so they know their
+rights.
+
+ We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+ Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software. If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+ Finally, any free program is threatened constantly by software
+patents. We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary. To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+ The precise terms and conditions for copying, distribution and
+modification follow.
+
+ GNU GENERAL PUBLIC LICENSE
+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+ 0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License. The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language. (Hereinafter, translation is included without limitation in
+the term "modification".) Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope. The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+ 1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+ 2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+ a) You must cause the modified files to carry prominent notices
+ stating that you changed the files and the date of any change.
+
+ b) You must cause any work that you distribute or publish, that in
+ whole or in part contains or is derived from the Program or any
+ part thereof, to be licensed as a whole at no charge to all third
+ parties under the terms of this License.
+
+ c) If the modified program normally reads commands interactively
+ when run, you must cause it, when started running for such
+ interactive use in the most ordinary way, to print or display an
+ announcement including an appropriate copyright notice and a
+ notice that there is no warranty (or else, saying that you provide
+ a warranty) and that users may redistribute the program under
+ these conditions, and telling the user how to view a copy of this
+ License. (Exception: if the Program itself is interactive but
+ does not normally print such an announcement, your work based on
+ the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole. If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works. But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+ 3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+ a) Accompany it with the complete corresponding machine-readable
+ source code, which must be distributed under the terms of Sections
+ 1 and 2 above on a medium customarily used for software interchange; or,
+
+ b) Accompany it with a written offer, valid for at least three
+ years, to give any third party, for a charge no more than your
+ cost of physically performing source distribution, a complete
+ machine-readable copy of the corresponding source code, to be
+ distributed under the terms of Sections 1 and 2 above on a medium
+ customarily used for software interchange; or,
+
+ c) Accompany it with the information you received as to the offer
+ to distribute corresponding source code. (This alternative is
+ allowed only for noncommercial distribution and only if you
+ received the program in object code or executable form with such
+ an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it. For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable. However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+ 4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License. Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+ 5. You are not required to accept this License, since you have not
+signed it. However, nothing else grants you permission to modify or
+distribute the Program or its derivative works. These actions are
+prohibited by law if you do not accept this License. Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+ 6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions. You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+ 7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all. For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices. Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+ 8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded. In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+ 9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time. Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation. If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+ 10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission. For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this. Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+ NO WARRANTY
+
+ 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+ 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+ END OF TERMS AND CONDITIONS
+
+ How to Apply These Terms to Your New Programs
+
+ If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+ To do so, attach the following notices to the program. It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+ <one line to give the program's name and a brief idea of what it does.>
+ Copyright (C) <year> <name of author>
+
+ 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; either version 2 of the License, or
+ (at your option) any later version.
+
+ 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.
+
+ You should have received a copy of the GNU General Public License along
+ with this program; if not, write to the Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+ Gnomovision version 69, Copyright (C) year name of author
+ Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+ This is free software, and you are welcome to redistribute it
+ under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License. Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary. Here is a sample; alter the names:
+
+ Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+ `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+ <signature of Ty Coon>, 1 April 1989
+ Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs. If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library. If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..2509b58
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,268 @@
+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
+
+binary := $(obj)/lib$(name).a
+$(binary):
+
+space :=
+space +=
+comma := ,
+
+$(foreach dep,$($(name)-deplibs), \
+ $(eval -include $($(dep)-dir)/config))
+-include $(cnf)
+
+include $(libhw-dir)/Makefile.proof
+
+CC = $(CROSS_COMPILE)gcc
+GNATBIND = $(CROSS_COMPILE)gnatbind
+
+ADAFLAGS += -gnatA -gnatec=$(libhw-dir)/gnat.adc
+ADAFLAGS += -gnatg -gnatp
+ADAFLAGS += -Wuninitialized -Wall -Werror
+ADAFLAGS += -pipe -g
+ADAFLAGS += -Wstrict-aliasing -Wshadow
+ADAFLAGS += -fno-common -fomit-frame-pointer
+ADAFLAGS += -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 += -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:
+
+$(binary): $$($(name)-objs)
+ @printf " AR $(subst $(obj)/,,$@)\n"
+ ar cr $@ $^
+
+$(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 %.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)-gen-y :=) \
+ $(eval $(name)-proof-y :=) \
+ $(eval subdirs-y :=) \
+ $(eval include $(1)/Makefile.inc) \
+ $(eval $(name)-srcs += \
+ $(subst $(top)/,, \
+ $(abspath $(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)
+
+# 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 a source type
+# $1 source type (ads, adb)
+# $2 source files (including the colon)
+# $3 obj path prefix (including the trailing slash)
+define add_ada_rule
+$(2) $(3)%.o: %.$(1)
+ @printf " COMPILE $$(subst $(obj)/,,$$@)\n"
+ $(CC) \
+ $(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(). Every stage that
+# uses Ada code has to call it!
+$(obj)/b__lib$(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)-extra-objs))) \
+ -a -n -L$(name)_ada -o $(notdir $@) \
+ $(subst $(dir $@),,$^)
+$(eval $(call add_ada_rule,adb,$(obj)/b__lib$(name).o:,))
+$(name)-objs += $(obj)/b__lib$(name).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
diff --git a/Makefile.inc b/Makefile.inc
new file mode 100644
index 0000000..d4fac0b
--- /dev/null
+++ b/Makefile.inc
@@ -0,0 +1,2 @@
+subdirs-y += ada common proof
+subdirs-y += debug
diff --git a/Makefile.proof b/Makefile.proof
new file mode 100644
index 0000000..91b98c9
--- /dev/null
+++ b/Makefile.proof
@@ -0,0 +1,97 @@
+PROOF_MODE ?= all
+
+jobs ?= 4
+
+$(foreach dep,$($(name)-deplibs), \
+ $(eval SPARKFLAGS += -aP=$($(dep)-dir)))
+
+SPARKFLAGS += -j$(jobs)
+SPARKFLAGS += -k
+SPARKFLAGS += -m
+SPARKFLAGS += --mode=$(PROOF_MODE)
+SPARKFLAGS += --report=fail
+SPARKFLAGS += --warnings=error
+SPARKFLAGS += --prover=cvc4,z3 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken
+
+quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))
+
+$(name)-exclude-srcs = \
+ $(filter-out \
+ $(sort $(notdir $($(name)-proof) $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs))), \
+ $(sort $(notdir \
+ $(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs))))))
+
+# Has to reside in the working directory. gnatprove takes paths relative
+# to the directory wher it's placed and reports internal errors if used
+# with absolute paths.
+gpr := $(name).gpr
+gpr-name = $(subst -,_,$(subst .,_,$(basename $(notdir $@))))
+
+# Will be installed for inclusion
+libgpr := $(obj)/lib$(name).gpr
+
+.SECONDEXPANSION:
+
+$(gpr):
+ @printf " GENERATE $(subst $(obj)/,,$@)\n"
+ printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
+ echo 'library project $(gpr-name) is' >>$@
+ echo ' for Library_Name use "$(name)";' >>$@
+ echo ' for Library_Dir use "$(obj)/adalib";' >>$@
+ echo ' for Source_Dirs use' \
+ '($(call quote-list,$($(name)-proof-dirs)));' >>$@
+ echo ' for Object_Dir use "$(obj)";' >>$@
+ echo ' package Builder is' >>$@
+ echo ' for Global_Configuration_Pragmas use' \
+ '"$(abspath $(libhw-dir)/spark.adc)";' >>$@
+ echo ' end Builder;' >>$@
+ echo ' for Excluded_Source_Files use' \
+ '($(call quote-list,$($(name)-exclude-srcs)));' >>$@
+ echo 'end $(gpr-name);' >>$@
+
+.INTERMEDIATE: $(gpr)
+
+$(libgpr): $$(MAKEFILE_LIST)
+ @printf " GENERATE $(subst $(obj)/,,$@)\n"
+ printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
+ echo 'library project lib$(name) is' >>$@
+ echo ' for Library_Name use "$(name)";' >>$@
+ echo ' for Library_Dir use "lib";' >>$@
+ echo ' for Library_ALI_Dir use "lib";' >>$@
+ echo ' for Source_Dirs use ("proof");' >>$@
+ echo ' for Object_Dir use external ("obj", "build");' >>$@
+ echo 'end lib$(name);' >>$@
+
+$(obj)/gnatprove/gnatprove.out: $(gpr) $$($(name)-gens) $(obj)/proofmode
+ gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj))
+
+proof:
+ if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \
+ echo "$(PROOF_MODE)" >$(obj)/proofmode; \
+ fi
+ $(MAKE) $(obj)/gnatprove/gnatprove.out
+
+check: export override PROOF_MODE=check
+check: proof
+
+flow: export override PROOF_MODE=flow
+flow: proof
+
+full: export override PROOF_MODE=all
+full: proof
+
+allconfigs = $(wildcard configs/*)
+allconfigs-targets = $(addprefix allconfigs-,$(notdir $(allconfigs)))
+
+$(allconfigs-targets): allconfigs-%: configs/%
+ rm -rf proof-allconfigs/$* $(name)_$*.gpr
+ mkdir -p proof-allconfigs/$*
+ echo "$(PROOF_MODE)" >proof-allconfigs/$*/proofmode
+ $(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=1 proof-allconfigs/$*/gnatprove/gnatprove.out
+
+proof-allconfigs: $(allconfigs-targets)
+
+clean::
+ rm -rf proof-allconfigs/
+
+.PHONY: proof check flow full $(allconfigs-targets) proof-allconfigs
diff --git a/ada/Makefile.inc b/ada/Makefile.inc
new file mode 100644
index 0000000..e09f1a5
--- /dev/null
+++ b/ada/Makefile.inc
@@ -0,0 +1,3 @@
+hw-$(CONFIG_HWBASE_STATIC_MMIO) += static_mmio/hw-mmio_range.adb
+hw-$(CONFIG_HWBASE_DYNAMIC_MMIO) += dynamic_mmio/hw-mmio_range.adb
+hw-$(CONFIG_HWBASE_TIMER_CLOCK_GETTIME) += clock_gettime/hw-time-timer.adb
diff --git a/ada/clock_gettime/hw-time-timer.adb b/ada/clock_gettime/hw-time-timer.adb
new file mode 100644
index 0000000..914b201
--- /dev/null
+++ b/ada/clock_gettime/hw-time-timer.adb
@@ -0,0 +1,61 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+with Interfaces.C;
+
+use type Interfaces.C.long;
+
+package body HW.Time.Timer
+with
+ Refined_State => (Timer_State => null,
+ Abstract_Time => null)
+is
+ CLOCK_MONOTONIC_RAW : constant := 4;
+
+ subtype Clock_ID_T is Interfaces.C.int;
+ subtype Time_T is Interfaces.C.long;
+
+ type Struct_Timespec is record
+ TV_Sec : aliased Time_T;
+ TV_NSec : aliased Interfaces.C.long;
+ end record;
+ pragma Convention (C_Pass_By_Copy, Struct_Timespec);
+
+ function Clock_Gettime
+ (Clock_ID : Clock_ID_T;
+ Timespec : access Struct_Timespec)
+ return Interfaces.C.int;
+ pragma Import (C, Clock_Gettime, "clock_gettime");
+
+ function Raw_Value_Min return T
+ is
+ Ignored : Interfaces.C.int;
+ Timespec : aliased Struct_Timespec;
+ begin
+ Ignored := Clock_Gettime (CLOCK_MONOTONIC_RAW, Timespec'Access);
+ return T (Timespec.TV_Sec * 1_000_000_000 + Timespec.TV_NSec);
+ end Raw_Value_Min;
+
+ function Raw_Value_Max return T
+ is
+ begin
+ return Raw_Value_Min + 1;
+ end Raw_Value_Max;
+
+ function Hz return T
+ is
+ begin
+ return 1_000_000_000; -- clock_gettime(2) is fixed to nanoseconds
+ end Hz;
+
+end HW.Time.Timer;
diff --git a/ada/dynamic_mmio/hw-mmio_range.adb b/ada/dynamic_mmio/hw-mmio_range.adb
new file mode 100644
index 0000000..78cc048
--- /dev/null
+++ b/ada/dynamic_mmio/hw-mmio_range.adb
@@ -0,0 +1,76 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+with HW.Debug;
+with GNAT.Source_Info;
+with System.Storage_Elements;
+with System.Address_To_Access_Conversions;
+
+package body HW.MMIO_Range
+with
+ Refined_State =>
+ (State => Range_A, -- the contents accessed
+ Base_Address => null) -- the address, so actually Range_A too
+is
+ pragma Warnings (Off, "implicit dereference",
+ Reason => "This is what this package is about.");
+
+ Debug_Reads : constant Boolean := False;
+ Debug_Writes : constant Boolean := False;
+
+ type Range_Access is access all Array_T;
+ package Conv_Range is new System.Address_To_Access_Conversions (Array_T);
+
+ Range_A : Range_Access :=
+ Range_Access (Conv_Range.To_Pointer (System'To_Address (Base_Addr)))
+ with Volatile;
+
+ procedure Read (Value : out Element_T; Index : in Index_T)
+ is
+ use type Word32;
+ begin
+ Value := Range_A (Index);
+ pragma Debug (Debug_Reads, Debug.Put
+ (GNAT.Source_Info.Enclosing_Entity & ": "));
+ pragma Debug (Debug_Reads, Debug.Put_Word32 (Word32 (Value)));
+ pragma Debug (Debug_Reads, Debug.Put (" <- "));
+ pragma Debug (Debug_Reads, Debug.Put_Word32
+ (Word32 (System.Storage_Elements.To_Integer
+ (Conv_Range.To_Address (Conv_Range.Object_Pointer (Range_A)))) +
+ Word32 (Index) * (Element_T'Size / 8)));
+ pragma Debug (Debug_Reads, Debug.New_Line);
+ end Read;
+
+ procedure Write (Index : in Index_T; Value : in Element_T)
+ is
+ use type Word32;
+ begin
+ pragma Debug (Debug_Writes, Debug.Put
+ (GNAT.Source_Info.Enclosing_Entity & ": "));
+ pragma Debug (Debug_Writes, Debug.Put_Word32 (Word32 (Value)));
+ pragma Debug (Debug_Writes, Debug.Put (" -> "));
+ pragma Debug (Debug_Writes, Debug.Put_Word32
+ (Word32 (System.Storage_Elements.To_Integer
+ (Conv_Range.To_Address (Conv_Range.Object_Pointer (Range_A)))) +
+ Word32 (Index) * (Element_T'Size / 8)));
+ pragma Debug (Debug_Writes, Debug.New_Line);
+ Range_A (Index) := Value;
+ end Write;
+
+ procedure Set_Base_Address (Base : Word64) is
+ begin
+ Range_A := Range_Access
+ (Conv_Range.To_Pointer (System'To_Address (Base)));
+ end Set_Base_Address;
+
+end HW.MMIO_Range;
diff --git a/ada/static_mmio/hw-mmio_range.adb b/ada/static_mmio/hw-mmio_range.adb
new file mode 100644
index 0000000..fb72152
--- /dev/null
+++ b/ada/static_mmio/hw-mmio_range.adb
@@ -0,0 +1,35 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+package body HW.MMIO_Range
+with
+ Refined_State =>
+ (State => MMIO,
+ Base_Address => null)
+is
+
+ MMIO : Array_T with Volatile, Address => System'To_Address (Base_Addr);
+
+ procedure Read (Value : out Element_T; Index : in Index_T) is
+ begin
+ Value := MMIO (Index);
+ end Read;
+
+ procedure Write (Index : in Index_T; Value : in Element_T) is
+ begin
+ MMIO (Index) := Value;
+ end Write;
+
+ procedure Set_Base_Address (Base : Word64) is null;
+
+end HW.MMIO_Range;
diff --git a/common/Makefile.inc b/common/Makefile.inc
new file mode 100644
index 0000000..b8e4f35
--- /dev/null
+++ b/common/Makefile.inc
@@ -0,0 +1,10 @@
+hw-y += hw.ads
+hw-y += hw-mmio_range.ads
+hw-y += hw-mmio_regs.adb
+hw-y += hw-mmio_regs.ads
+hw-y += hw-port_io.adb
+hw-y += hw-port_io.ads
+hw-y += hw-sub_regs.ads
+hw-y += hw-time.ads
+hw-y += hw-time.adb
+hw-y += hw-time-timer.ads
diff --git a/common/hw-mmio_range.ads b/common/hw-mmio_range.ads
new file mode 100644
index 0000000..1b33630
--- /dev/null
+++ b/common/hw-mmio_range.ads
@@ -0,0 +1,35 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+with System;
+
+generic
+ Base_Addr : Word64;
+ type Element_T is mod <>;
+ type Index_T is range <>;
+ type Array_T is array (Index_T) of Element_T;
+package HW.MMIO_Range
+with
+ Abstract_State =>
+ ((State with External),
+ Base_Address),
+ Initializes => Base_Address
+is
+
+ procedure Read (Value : out Element_T; Index : in Index_T);
+
+ procedure Write (Index : in Index_T; Value : in Element_T);
+
+ procedure Set_Base_Address (Base : Word64);
+
+end HW.MMIO_Range;
diff --git a/common/hw-mmio_regs.adb b/common/hw-mmio_regs.adb
new file mode 100644
index 0000000..5eea563
--- /dev/null
+++ b/common/hw-mmio_regs.adb
@@ -0,0 +1,92 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+package body HW.MMIO_Regs
+is
+
+ generic
+ type Word_T is mod <>;
+ procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T);
+
+ procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T)
+ is
+ Off : constant Range_P.Index_T := Range_P.Index_T
+ ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+ pragma Warnings
+ (GNAT, Off, """Mask"" is not modified, could be declared constant",
+ Reason => "Ada RM forbids making it constant.");
+ Mask : Word64 := Shift_Left (1, Regs (Idx).MSB + 1 - Regs (Idx).LSB) - 1;
+ pragma Warnings
+ (GNAT, On, """Mask"" is not modified, could be declared constant");
+ Temp : Range_P.Element_T;
+ begin
+ Range_P.Read (Temp, Off);
+ Value := Word_T (Shift_Right (Word64 (Temp), Regs (Idx).LSB) and Mask);
+ end Read_G;
+
+ procedure Read_I is new Read_G (Word8);
+ procedure Read (Value : out Word8; Idx : Subs_P.Index_T) renames Read_I;
+
+ procedure Read_I is new Read_G (Word16);
+ procedure Read (Value : out Word16; Idx : Subs_P.Index_T) renames Read_I;
+
+ procedure Read_I is new Read_G (Word32);
+ procedure Read (Value : out Word32; Idx : Subs_P.Index_T) renames Read_I;
+
+ procedure Read_I is new Read_G (Word64);
+ procedure Read (Value : out Word64; Idx : Subs_P.Index_T) renames Read_I;
+
+ ----------------------------------------------------------------------------
+
+ generic
+ type Word_T is mod <>;
+ procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T);
+
+ procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T)
+ is
+ Off : constant Range_P.Index_T := Range_P.Index_T
+ ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+ pragma Warnings
+ (GNAT, Off, """Mask"" is not modified, could be declared constant",
+ Reason => "Ada RM forbids making it constant.");
+ Mask : Word64 :=
+ Shift_Left (1, Regs (Idx).MSB + 1) - Shift_Left (1, Regs (Idx).LSB);
+ pragma Warnings
+ (GNAT, On, """Mask"" is not modified, could be declared constant");
+ Temp : Range_P.Element_T;
+ begin
+ if Regs (Idx).MSB - Regs (Idx).LSB + 1 = Range_P.Element_T'Size then
+ Range_P.Write (Off, Range_P.Element_T (Value));
+ else
+ -- read/modify/write
+ Range_P.Read (Temp, Off);
+ Temp := Range_P.Element_T
+ ((Word64 (Temp) and not Mask) or
+ (Shift_Left (Word64 (Value), Regs (Idx).LSB)));
+ Range_P.Write (Off, Temp);
+ end if;
+ end Write_G;
+
+ procedure Write_I is new Write_G (Word8);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word8) renames Write_I;
+
+ procedure Write_I is new Write_G (Word16);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word16) renames Write_I;
+
+ procedure Write_I is new Write_G (Word32);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word32) renames Write_I;
+
+ procedure Write_I is new Write_G (Word64);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word64) renames Write_I;
+
+end HW.MMIO_Regs;
diff --git a/common/hw-mmio_regs.ads b/common/hw-mmio_regs.ads
new file mode 100644
index 0000000..9aafed9
--- /dev/null
+++ b/common/hw-mmio_regs.ads
@@ -0,0 +1,127 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+with HW.Sub_Regs;
+with HW.MMIO_Range;
+
+use type HW.Word64;
+
+generic
+ with package Range_P is new MMIO_Range (<>);
+ Byte_Offset_O : Natural := 0;
+
+ with package Subs_P is new Sub_Regs (<>);
+ Regs : Subs_P.Array_T;
+
+package HW.MMIO_Regs
+is
+
+ Byte_Offset : Natural := Byte_Offset_O;
+
+ ----------------------------------------------------------------------------
+
+ procedure Read (Value : out Word8; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word8'Size;
+
+ procedure Read (Value : out Word16; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word16'Size;
+
+ procedure Read (Value : out Word32; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word32'Size;
+
+ procedure Read (Value : out Word64; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word64'Size;
+
+ ----------------------------------------------------------------------------
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word8)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word16)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word32)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word64)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+end HW.MMIO_Regs;
diff --git a/common/hw-port_io.adb b/common/hw-port_io.adb
new file mode 100644
index 0000000..e8adfc2
--- /dev/null
+++ b/common/hw-port_io.adb
@@ -0,0 +1,71 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+with System;
+with System.Machine_Code;
+
+package body HW.Port_IO
+with
+ Refined_State => (State => null),
+ SPARK_Mode => Off
+is
+
+ generic
+ type Word is private;
+ procedure Port_In (Value : out Word; Port : Port_Type);
+
+ procedure Port_In (Value : out Word; Port : Port_Type) is
+ begin
+ System.Machine_Code.Asm
+ ("in %1, %0",
+ Inputs => (Port_Type'Asm_Input ("Nd", Port)),
+ Outputs => (Word'Asm_Output ("=a", Value)),
+ Volatile => True);
+ end Port_In;
+
+ procedure InB_Body is new Port_In (Word => Word8);
+ procedure InB (Value : out Word8; Port : Port_Type) renames InB_Body;
+
+ procedure InW_Body is new Port_In (Word => Word16);
+ procedure InW (Value : out Word16; Port : Port_Type) renames InW_Body;
+
+ procedure InL_Body is new Port_In (Word => Word32);
+ procedure InL (Value : out Word32; Port : Port_Type) renames InL_Body;
+
+ ----------------------------------------------------------------------------
+
+ generic
+ type Word is private;
+ procedure Port_Out (Port : Port_Type; Value : Word);
+
+ procedure Port_Out (Port : Port_Type; Value : Word) is
+ begin
+ System.Machine_Code.Asm
+ ("out %1, %0",
+ Inputs => (Port_Type'Asm_Input ("Nd", Port),
+ Word'Asm_Input ("a", Value)),
+ Volatile => True);
+ end Port_Out;
+
+ procedure OutB_Body is new Port_Out (Word => Word8);
+ procedure OutB (Port : Port_Type; Value : Word8) renames OutB_Body;
+
+ procedure OutW_Body is new Port_Out (Word => Word16);
+ procedure OutW (Port : Port_Type; Value : Word16) renames OutW_Body;
+
+ procedure OutL_Body is new Port_Out (Word => Word32);
+ procedure OutL (Port : Port_Type; Value : Word32) renames OutL_Body;
+
+end HW.Port_IO;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-port_io.ads b/common/hw-port_io.ads
new file mode 100644
index 0000000..a5d0e9e
--- /dev/null
+++ b/common/hw-port_io.ads
@@ -0,0 +1,61 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+package HW.Port_IO
+with
+ Abstract_State => (State with External => (Async_Readers, Async_Writers))
+is
+
+ type Port_Type is mod 2**16;
+
+ procedure InB (Value : out Word8; Port : Port_Type)
+ with
+ Global => (In_Out => State),
+ Depends => ((Value, State) => (Port, State)),
+ Inline_Always;
+
+ procedure InW (Value : out Word16; Port : Port_Type)
+ with
+ Global => (In_Out => State),
+ Depends => ((Value, State) => (Port, State)),
+ Pre => Port mod 2 = 0,
+ Inline_Always;
+
+ procedure InL (Value : out Word32; Port : Port_Type)
+ with
+ Global => (In_Out => State),
+ Depends => ((Value, State) => (Port, State)),
+ Pre => Port mod 4 = 0,
+ Inline_Always;
+
+ procedure OutB (Port : Port_Type; Value : Word8)
+ with
+ Global => (In_Out => State),
+ Depends => (State =>+ (Port, Value)),
+ Inline_Always;
+
+ procedure OutW (Port : Port_Type; Value : Word16)
+ with
+ Global => (In_Out => State),
+ Depends => (State =>+ (Port, Value)),
+ Pre => Port mod 2 = 0,
+ Inline_Always;
+
+ procedure OutL (Port : Port_Type; Value : Word32)
+ with
+ Global => (In_Out => State),
+ Depends => (State =>+ (Port, Value)),
+ Pre => Port mod 4 = 0,
+ Inline_Always;
+
+end HW.Port_IO;
diff --git a/common/hw-sub_regs.ads b/common/hw-sub_regs.ads
new file mode 100644
index 0000000..ca04c1d
--- /dev/null
+++ b/common/hw-sub_regs.ads
@@ -0,0 +1,26 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+generic
+ type Index_T is (<>);
+package HW.Sub_Regs is
+
+ type T is record
+ Byte_Offset : Natural;
+ MSB : Natural;
+ LSB : Natural;
+ end record;
+
+ type Array_T is array (Index_T) of T;
+
+end HW.Sub_Regs;
diff --git a/common/hw-time-timer.ads b/common/hw-time-timer.ads
new file mode 100644
index 0000000..4676815
--- /dev/null
+++ b/common/hw-time-timer.ads
@@ -0,0 +1,41 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+private package HW.Time.Timer
+ with
+ Abstract_State => ((Timer_State with Part_Of => HW.Time.State),
+ (Abstract_Time with
+ Part_Of => HW.Time.State,
+ External => Async_Writers)),
+ Initializes => (Timer_State)
+is
+
+ -- Returns the highest point in time that has definitely passed.
+ function Raw_Value_Min return T
+ with
+ Volatile_Function,
+ Global => (Input => Abstract_Time),
+ Depends => (Raw_Value_Min'Result => Abstract_Time);
+
+ -- Returns the highest point in time that might have been reached yet.
+ function Raw_Value_Max return T
+ with
+ Volatile_Function,
+ Global => (Input => Abstract_Time),
+ Depends => (Raw_Value_Max'Result => Abstract_Time);
+
+ function Hz return T
+ with
+ Global => (Input => Timer_State);
+
+end HW.Time.Timer;
diff --git a/common/hw-time.adb b/common/hw-time.adb
new file mode 100644
index 0000000..3162de1
--- /dev/null
+++ b/common/hw-time.adb
@@ -0,0 +1,105 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+with HW;
+with HW.Time.Timer;
+
+use type HW.Word64;
+
+package body HW.Time
+ with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
+is
+
+ function Now return T
+ with
+ Refined_Global => (Input => Timer.Abstract_Time)
+ is
+ Current : constant T := Timer.Raw_Value_Min;
+ begin
+ return Current;
+ end Now;
+
+ function US_From_Now (US : Natural) return T
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Current : constant T := Timer.Raw_Value_Max;
+ begin
+ return Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
+ end US_From_Now;
+
+ function MS_From_Now (MS : Natural) return T
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Current : constant T := Timer.Raw_Value_Max;
+ begin
+ return Current + (T (MS) * Timer.Hz + 999) / 1_000;
+ end MS_From_Now;
+
+ function Now_US return Int64
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ MHz : constant T := Timer.Hz / 1_000_000;
+ Current : constant T := Timer.Raw_Value_Min;
+ begin
+ return Int64 ((Current and (2 ** 63 - 1)) / (if MHz = 0 then 1 else MHz));
+ end Now_US;
+
+ ----------------------------------------------------------------------------
+
+ procedure Delay_Until (Deadline : T)
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time))
+ is
+ Current: T;
+ begin
+ loop
+ Current := Timer.Raw_Value_Min;
+ exit when Current >= Deadline;
+ end loop;
+ end Delay_Until;
+
+ procedure U_Delay (US : Natural)
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Deadline : constant T := US_From_Now (US);
+ begin
+ Delay_Until (Deadline);
+ end U_Delay;
+
+ procedure M_Delay (MS : Natural)
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Deadline : constant T := MS_From_Now (MS);
+ begin
+ Delay_Until (Deadline);
+ end M_Delay;
+
+ ----------------------------------------------------------------------------
+
+ function Timed_Out (Deadline : T) return Boolean
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time))
+ is
+ Current : constant T := Timer.Raw_Value_Min;
+ begin
+ return Current >= Deadline;
+ end Timed_Out;
+
+end HW.Time;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-time.ads b/common/hw-time.ads
new file mode 100644
index 0000000..743279b
--- /dev/null
+++ b/common/hw-time.ads
@@ -0,0 +1,75 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- 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.
+--
+
+package HW.Time
+ with Abstract_State => (State with External => Async_Writers)
+is
+
+ type T is private;
+
+ function Now return T
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ function US_From_Now (US : Natural) return T
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ function MS_From_Now (MS : Natural) return T
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ function Now_US return Int64
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ ----------------------------------------------------------------------------
+
+ pragma Warnings
+ (GNATprove, Off, "subprogram ""*Delay*"" has no effect",
+ Reason => "No effect on dataflow but time always passes.");
+
+ -- Delay execution until Deadline has been reached.
+ procedure Delay_Until (Deadline : T)
+ with
+ Global => (Input => State);
+
+ procedure U_Delay (US : Natural)
+ with
+ Global => (Input => State);
+
+ procedure M_Delay (MS : Natural)
+ with
+ Global => (Input => State);
+
+ pragma Warnings
+ (GNATprove, On, "subprogram ""*Delay*"" has no effect");
+
+ ----------------------------------------------------------------------------
+
+ function Timed_Out (Deadline : T) return Boolean
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+private
+
+ type T is new Word64;
+
+end HW.Time;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw.ads b/common/hw.ads
new file mode 100644
index 0000000..6bfca91
--- /dev/null
+++ b/common/hw.ads
@@ -0,0 +1,58 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+with Interfaces;
+
+package HW is
+
+ type Bit is mod 2 ** 1;
+
+ subtype Byte is Interfaces.Unsigned_8;
+ subtype Word8 is Byte;
+ function Shift_Left (Value : Word8; Amount : Natural) return Word8
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word8; Amount : Natural) return Word8
+ renames Interfaces.Shift_Right;
+
+ subtype Word16 is Interfaces.Unsigned_16;
+ function Shift_Left (Value : Word16; Amount : Natural) return Word16
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word16; Amount : Natural) return Word16
+ renames Interfaces.Shift_Right;
+
+ subtype Word32 is Interfaces.Unsigned_32;
+ function Shift_Left (Value : Word32; Amount : Natural) return Word32
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word32; Amount : Natural) return Word32
+ renames Interfaces.Shift_Right;
+
+ subtype Word64 is Interfaces.Unsigned_64;
+ function Shift_Left (Value : Word64; Amount : Natural) return Word64
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word64; Amount : Natural) return Word64
+ renames Interfaces.Shift_Right;
+
+ subtype Int8 is Interfaces.Integer_8;
+ subtype Int16 is Interfaces.Integer_16;
+ subtype Int32 is Interfaces.Integer_32;
+ subtype Int64 is Interfaces.Integer_64;
+
+ subtype Pos8 is Interfaces.Integer_8 range 1 .. Interfaces.Integer_8'Last;
+ subtype Pos16 is Interfaces.Integer_16 range 1 .. Interfaces.Integer_16'Last;
+ subtype Pos32 is Interfaces.Integer_32 range 1 .. Interfaces.Integer_32'Last;
+ subtype Pos64 is Interfaces.Integer_64 range 1 .. Interfaces.Integer_64'Last;
+
+ subtype Buffer_Range is Natural range 0 .. Natural'Last - 1;
+ type Buffer is array (Buffer_Range range <>) of Byte;
+
+end HW;
diff --git a/configs/defconfig b/configs/defconfig
new file mode 100644
index 0000000..17bb699
--- /dev/null
+++ b/configs/defconfig
@@ -0,0 +1,5 @@
+CONFIG_HWBASE_DEBUG_NULL = y
+CONFIG_HWBASE_DEBUG_TEXT_IO =
+CONFIG_HWBASE_STATIC_MMIO = y
+CONFIG_HWBASE_DYNAMIC_MMIO =
+CONFIG_HWBASE_TIMER_CLOCK_GETTIME = y
diff --git a/debug/Makefile.inc b/debug/Makefile.inc
new file mode 100644
index 0000000..b636a6f
--- /dev/null
+++ b/debug/Makefile.inc
@@ -0,0 +1,4 @@
+hw-y += hw-debug.ads
+hw-y += hw-debug.adb
+hw-$(CONFIG_HWBASE_DEBUG_NULL) += null/hw-debug_sink.ads
+hw-$(CONFIG_HWBASE_DEBUG_TEXT_IO) += text_io/hw-debug_sink.ads
diff --git a/debug/hw-debug.adb b/debug/hw-debug.adb
new file mode 100644
index 0000000..3ffa9b5
--- /dev/null
+++ b/debug/hw-debug.adb
@@ -0,0 +1,284 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+with HW;
+with HW.Time;
+with HW.Debug_Sink;
+
+use type HW.Word64;
+use type HW.Int64;
+
+package body HW.Debug
+with
+ SPARK_Mode => Off
+is
+
+ Start_Of_Line : Boolean := True;
+ Register_Write_Delay_Nanoseconds : Word64 := 0;
+
+ type Base_Range is new Positive range 2 .. 16;
+ type Width_Range is new Natural range 0 .. 64;
+
+ procedure Put_By_Base
+ (Item : Word64;
+ Min_Width : Width_Range;
+ Base : Base_Range);
+
+ procedure Do_Put_Int64
+ (Item : Int64);
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Time
+ is
+ Now_US : Int64;
+ begin
+ if Start_Of_Line then
+ Start_Of_Line := False;
+ Now_US := Time.Now_US;
+ Debug_Sink.Put_Char ('[');
+ Do_Put_Int64 ((Now_US / 1_000_000) mod 1_000_000);
+ Debug_Sink.Put_Char ('.');
+ Put_By_Base (Word64 (Now_US mod 1_000_000), 6, 10);
+ Debug_Sink.Put ("] ");
+ end if;
+ end Put_Time;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put (Item : String) is
+ begin
+ Put_Time;
+ HW.Debug_Sink.Put (Item);
+ end Put;
+
+ procedure Put_Line (Item : String) is
+ begin
+ Put (Item);
+ New_Line;
+ end Put_Line;
+
+ procedure New_Line is
+ begin
+ HW.Debug_Sink.New_Line;
+ Start_Of_Line := True;
+ end New_Line;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_By_Base
+ (Item : Word64;
+ Min_Width : Width_Range;
+ Base : Base_Range)
+ is
+ Temp : Word64 := Item;
+
+ subtype Chars_Range is Width_Range range 0 .. 63;
+ Index : Width_Range := 0;
+
+ type Chars_Array is array (Chars_Range) of Character;
+ Chars : Chars_Array := (others => '0');
+
+ Digit : Natural;
+ begin
+ while Temp > 0 loop
+ Digit := Natural (Temp rem Word64 (Base));
+ if Digit < 10 then
+ Chars (Index) := Character'Val (Character'Pos ('0') + Digit);
+ else
+ Chars (Index) := Character'Val (Character'Pos ('a') + Digit - 10);
+ end if;
+ Temp := Temp / Word64 (Base);
+ Index := Index + 1;
+ end loop;
+ if Index < Min_Width then
+ Index := Min_Width;
+ end if;
+ for I in reverse Width_Range range 0 .. Index - 1 loop
+ HW.Debug_Sink.Put_Char (Chars (I));
+ end loop;
+ end Put_By_Base;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Word
+ (Item : Word64;
+ Min_Width : Width_Range;
+ Print_Ox : Boolean := True) is
+ begin
+ Put_Time;
+ if Print_Ox then
+ Put ("0x");
+ end if;
+ Put_By_Base (Item, Min_Width, 16);
+ end Put_Word;
+
+ procedure Put_Word8 (Item : Word8) is
+ begin
+ Put_Word (Word64 (Item), 2);
+ end Put_Word8;
+
+ procedure Put_Word16 (Item : Word16) is
+ begin
+ Put_Word (Word64 (Item), 4);
+ end Put_Word16;
+
+ procedure Put_Word32 (Item : Word32) is
+ begin
+ Put_Word (Word64 (Item), 8);
+ end Put_Word32;
+
+ procedure Put_Word64 (Item : Word64) is
+ begin
+ Put_Word (Item, 16);
+ end Put_Word64;
+
+ ----------------------------------------------------------------------------
+
+ procedure Do_Put_Int64 (Item : Int64)
+ is
+ Temp : Word64;
+ begin
+ if Item < 0 then
+ Debug_Sink.Put_Char ('-');
+ Temp := Word64 (-Item);
+ else
+ Temp := Word64 (Item);
+ end if;
+ Put_By_Base (Temp, 1, 10);
+ end Do_Put_Int64;
+
+ procedure Put_Int64 (Item : Int64)
+ is
+ begin
+ Put_Time;
+ Do_Put_Int64 (Item);
+ end Put_Int64;
+
+ procedure Put_Int8 (Item : Int8) is
+ begin
+ Put_Int64 (Int64 (Item));
+ end Put_Int8;
+
+ procedure Put_Int16 (Item : Int16) is
+ begin
+ Put_Int64 (Int64 (Item));
+ end Put_Int16;
+
+ procedure Put_Int32 (Item : Int32) is
+ begin
+ Put_Int64 (Int64 (Item));
+ end Put_Int32;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Reg8 (Name : String; Item : Word8) is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word8 (Item);
+ New_Line;
+ end Put_Reg8;
+
+ procedure Put_Reg16 (Name : String; Item : Word16)
+ is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word16 (Item);
+ New_Line;
+ end Put_Reg16;
+
+ procedure Put_Reg32 (Name : String; Item : Word32)
+ is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word32 (Item);
+ New_Line;
+ end Put_Reg32;
+
+ procedure Put_Reg64 (Name : String; Item : Word64)
+ is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word64 (Item);
+ New_Line;
+ end Put_Reg64;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Buffer
+ (Name : String;
+ Buf : Buffer;
+ Len : Buffer_Range)
+ is
+ Line_Start, Left : Natural;
+ begin
+ if Len = 0 then
+ if Name'Length > 0 then
+ Put (Name);
+ Put_Line ("+0x00:");
+ end if;
+ else
+ Line_Start := 0;
+ Left := Len - 1;
+ for I in Natural range 1 .. ((Len + 15) / 16) loop
+ if Name'Length > 0 then
+ Put (Name);
+ Debug_Sink.Put_Char ('+');
+ Put_Word16 (Word16 (Line_Start));
+ Put (": ");
+ end if;
+ for J in Natural range 0 .. Natural'Min (7, Left)
+ loop
+ Put_Word (Word64 (Buf (Line_Start + J)), 2, False);
+ Debug_Sink.Put_Char (' ');
+ end loop;
+
+ Debug_Sink.Put_Char (' ');
+ for J in Natural range 8 .. Natural'Min (15, Left)
+ loop
+ Put_Word (Word64(Buf (Line_Start + J)), 2, False);
+ Debug_Sink.Put_Char (' ');
+ end loop;
+ New_Line;
+
+ Line_Start := Line_Start + 16;
+ Left := Left - Natural'Min (Left, 16);
+ end loop;
+ end if;
+ end Put_Buffer;
+
+ ----------------------------------------------------------------------------
+
+ procedure Set_Register_Write_Delay (Value : Word64)
+ is
+ begin
+ Register_Write_Delay_Nanoseconds := Value;
+ end Set_Register_Write_Delay;
+
+ ----------------------------------------------------------------------------
+
+ Procedure Register_Write_Wait
+ is
+ begin
+ if Register_Write_Delay_Nanoseconds > 0 then
+ Time.U_Delay (Natural ((Register_Write_Delay_Nanoseconds + 999) / 1000));
+ end if;
+ end Register_Write_Wait;
+
+end HW.Debug;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/debug/hw-debug.ads b/debug/hw-debug.ads
new file mode 100644
index 0000000..fd8ce9c
--- /dev/null
+++ b/debug/hw-debug.ads
@@ -0,0 +1,42 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+
+package HW.Debug is
+
+ procedure Put (Item : String);
+ procedure Put_Line (Item : String);
+ procedure New_Line;
+
+ procedure Put_Word8 (Item : Word8);
+ procedure Put_Word16 (Item : Word16);
+ procedure Put_Word32 (Item : Word32);
+ procedure Put_Word64 (Item : Word64);
+
+ procedure Put_Int8 (Item : Int8);
+ procedure Put_Int16 (Item : Int16);
+ procedure Put_Int32 (Item : Int32);
+ procedure Put_Int64 (Item : Int64);
+
+ procedure Put_Reg8 (Name : String; Item : Word8);
+ procedure Put_Reg16 (Name : String; Item : Word16);
+ procedure Put_Reg32 (Name : String; Item : Word32);
+ procedure Put_Reg64 (Name : String; Item : Word64);
+
+ procedure Put_Buffer (Name : String; Buf : in Buffer; Len : in Buffer_Range);
+
+ procedure Set_Register_Write_Delay (Value : Word64);
+ Procedure Register_Write_Wait;
+end HW.Debug;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/debug/null/hw-debug_sink.ads b/debug/null/hw-debug_sink.ads
new file mode 100644
index 0000000..dcd2dd1
--- /dev/null
+++ b/debug/null/hw-debug_sink.ads
@@ -0,0 +1,22 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+package HW.Debug_Sink is
+
+ procedure Put (Item : String) is null;
+
+ procedure Put_Char (Item : Character) is null;
+
+ procedure New_Line is null;
+
+end HW.Debug_Sink;
diff --git a/debug/text_io/hw-debug_sink.ads b/debug/text_io/hw-debug_sink.ads
new file mode 100644
index 0000000..2f0b2d2
--- /dev/null
+++ b/debug/text_io/hw-debug_sink.ads
@@ -0,0 +1,23 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+with Ada.Text_IO;
+
+package HW.Debug_Sink is
+
+ procedure Put (Item : String) renames Ada.Text_IO.Put;
+ procedure Put_Char (Item : Character) renames Ada.Text_IO.Put;
+ procedure New_Line (Spacing : Ada.Text_IO.Positive_Count := 1)
+ renames Ada.Text_IO.New_Line;
+
+end HW.Debug_Sink;
diff --git a/gnat.adc b/gnat.adc
new file mode 100644
index 0000000..eab8a17
--- /dev/null
+++ b/gnat.adc
@@ -0,0 +1,25 @@
+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_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/proof/Makefile.inc b/proof/Makefile.inc
new file mode 100644
index 0000000..dae0b0d
--- /dev/null
+++ b/proof/Makefile.inc
@@ -0,0 +1 @@
+hw-proof-y += hw-mmio_range.adb
diff --git a/proof/hw-mmio_range.adb b/proof/hw-mmio_range.adb
new file mode 100644
index 0000000..d96fc4b
--- /dev/null
+++ b/proof/hw-mmio_range.adb
@@ -0,0 +1,44 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- 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.
+--
+
+package body HW.MMIO_Range
+with
+ Refined_State =>
+ (State => Range_A,
+ Base_Address => Address)
+is
+
+ Range_A : Array_T
+ with
+ Volatile,
+ Async_Readers, Async_Writers, Effective_Reads, Effective_Writes,
+ Import;
+
+ Address : Word64 := Base_Addr;
+
+ procedure Read (Value : out Element_T; Index : in Index_T) is
+ begin
+ Value := Range_A (Index);
+ end Read;
+
+ procedure Write (Index : in Index_T; Value: in Element_T) is
+ begin
+ Range_A (Index) := Value;
+ end Write;
+
+ procedure Set_Base_Address (Base : Word64) is
+ begin
+ Address := Base;
+ end Set_Base_Address;
+
+end HW.MMIO_Range;
diff --git a/spark.adc b/spark.adc
new file mode 100644
index 0000000..576a120
--- /dev/null
+++ b/spark.adc
@@ -0,0 +1,23 @@
+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_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
+ (Debug => Disable);
+pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
+pragma SPARK_Mode (On);