componolit / ada-runtime Goto Github PK

Add support for the STM32F0 Discovery board since this doesn't seem to be available in the Ada Drivers Library.

We currently have 3 log procedures for debug, warning and error. Although we only really use this on Genode (which is also the reason why we initially decided this). I think we should reduce that to a single one (or maybe two for info/error). The rationale is that the runtime log is only used for debugging purposes and other mechanisms should be used in the normal application operation. Also error markers and colours could be added by the runtime itself. This would simplify the platform interface.

Create a specification (.ads file) what needs to be implemented to adapt the generic runtime to a particular system.

Currently the embedded drivers are unproven, we should change that.

Future versions of SPARK will retire Overflow_Mode / -gnato?? in favor of Ada.Numerics.Big_Numbers.Big_Integers whjich is more flexible.

Unless we plan to execute contracts in the runtime, adding the specification should suffice to use big numbers in contracts.

Currently, we are using source code of the original Ada runtime from GCC 6.3. This code is quite old (copyright notice from 2013) and at some points very different from the code of the current GNAT Pro 18.1. For example the implementation of the secondary stack differs. The current GNAT binder generates the symbols __gnat_binder_ss_count, __gnat_default_ss_pool, __gnat_default_ss_size, which are unknown in older implementations.

To solve this issue we could use a more recent version of GCC to be compatible. The Ada-related source code in GCC 7.3 (copyright notice from 2016) still does not contain the changes mentioned above. Any objections against using GCC 8.1? @senier @jklmnn

Create a Genode port that uses a Genode-specific branch of this runtime. Remove duplicate files from Genode. For now, we use the GCC 6.3 runtime source from this repository.

While working on issue #47 I noticed that some properties are harder to prove than expected and are not feasible to prove in the time given. The missing parts are:

• The associativity lemmas for integer conversions between signed and unsigned. Since addition and subtraction are sign-independent the following lemmas are valid but cannot be proven yet (for all ranges):
  • X + Y = To_Int (To_Uns (X) + To_Uns (Y))
  • X - Y = To_Int (To_Uns (X) - To_Uns (Y))
• Multiplication with overflow check is a little more complex than addition and subtraction but it should be provable with moderate effort.
• The division functions are not yet analyzed but after a short overview they're the most complex part of the package and will likely require high effort to prove.

Improve the implementation of string_utils by the following points:

• Proof of termination via pragma Annotate (GNATprove, Terminating, Length);
• Eliminate null pointers via predicate on the Pointer type.

Adaptions to get this version of the runtime into the next Genode release.

The current secondary stack size is hard coded in the runtime with 768kB which works fine for Genode but might be too large for other platforms. The idea is to make this at least compile time configurable. This could be done through gnatbind which provides an option to set the secondary stack size:

-Dnn[k|m] Default secondary stack size = nn [kilo|mega] bytes

Cf. platform/genode.cc

The GNAT personality on ARM is different to that on X86. This leads to undefined behavior on Genode ARM platforms. genodelabs/genode#3395 has a more thorough discussion of this issue.

Update README and platform specification to reflect current state of the runtime (interface, version, ...)

When initializing or copying larger objects (255 byte seems to be large enough) the device crashes. I assume the reason could be the memcpy implementation. I'm not exactly sure how and which implementation is used.

We should add more thorough tests to ensure the correct functioning of the runtime. We should find out if we can reuse tests of the original Ada runtime.

Add support for Ada.Real_Time to the minimal runtime. Whether we need to support the delay statement for Ada.Real_Time.Time needs to be decided (depending on how complicated it is).

Tasks:

• Write test program for Ada.Real_Time.Clock
• Implement (or reuse) POSIX backend
• Test with minimal POSIX runtime
• Implement Genode backend
• Test on Genode

Constructs like

package X is

   type R is private;
   type A is access all R;

private

   generic
      type T is private;
      type T_A is access all T;
   package G
   end G;

   package I is new G (R, A);

   type R is null record;

end X;

This construct causes

ada-runtime/contrib/gcc-6.3.0/s-finmas.ads:32:06: run-time library configuration error
ada-runtime/contrib/gcc-6.3.0/s-finmas.ads:32:06: file s-finmas.ads had semantic errors
ada-runtime/contrib/gcc-6.3.0/s-finmas.ads:32:06: entity "System.Finalization_Masters.Finalization_Master" not available
ada-runtime/contrib/gcc-6.3.0/s-finroo.ads:40:09: run-time configuration error
ada-runtime/contrib/gcc-6.3.0/s-finroo.ads:40:09: entity "System.Soft_Links.Abort_Undefer" not defined

on GCC 6.3 and

ada-runtime/contrib/gcc-6.3.0/a-stream.ads:70:09: expected type "Standard.Boolean"
ada-runtime/contrib/gcc-6.3.0/a-stream.ads:70:09: found type "Ada.Tags.Size_Ptr"
ada-runtime/contrib/gcc-6.3.0/a-stream.ads:70:09: expected type "Ada.Tags.Select_Specific_Data_Ptr"
ada-runtime/contrib/gcc-6.3.0/a-stream.ads:70:09: found a composite type
ada-runtime/contrib/gcc-6.3.0/a-stream.ads:70:09: no value supplied for component "Tags_Table"

with GCC 7.3.

As this yields different results with different GCC versions it will be approached after #26 is done.

A test case is available in https://github.com/m-stein/genode/tree/spunky_generic_queue_runtime_error and can be triggered by running make core KERNEL=hw.

Cloning the repo fails when checking out gcc. I suspect this is related to the shallow checkout of gcc - when removing shallow = true from .gitmodules and updating submodules manually, the checkout succeeds.

$ git clone --recursive [email protected]:jklmnn/ada-runtime.git
Cloning into 'ada-runtime'...                                                                                                                                                                  
remote: Counting objects: 337, done.                             
remote: Compressing objects: 100% (71/71), done.    
remote: Total 337 (delta 53), reused 77 (delta 33), pack-reused 232       
Receiving objects: 100% (337/337), 77.38 KiB | 0 bytes/s, done.                                                                                
Resolving deltas: 100% (167/167), done.                                                 
Submodule 'contrib/gcc' (https://github.com/gcc-mirror/gcc.git) registered for path 'contrib/gcc'
Cloning into '/home/alex/Documents/Componolit_GmbH/Devel/src/ada-runtime/contrib/gcc'...                                           
remote: Counting objects: 84771, done.                                         
remote: Compressing objects: 100% (68216/68216), done.
remote: Total 84771 (delta 18843), reused 50304 (delta 14979), pack-reused 0                                                                   Receiving objects: 100% (84771/84771), 103.91 MiB | 2.10 MiB/s, done.                                                                          
Resolving deltas: 100% (18843/18843), done.               
error: no such remote ref 4b5e15daff8b54440e3fda451c318ad31e532fab                                       
Fetched in submodule path 'contrib/gcc', but it did not contain 4b5e15daff8b54440e3fda451c318ad31e532fab. Direct fetching of that commit failed
.

The builds on Genode and Muen are not adapted and tagged types are not yet tested on these platforms. We should at least compile the tagged type support on Muen and add a smoke test on Genode.

• Muen
• Genode

Compiling the runtime leads to the following error:

gprbuild --RTS=./obj  -Prts
Compile
   [Ada]          ss_utils.adb
ss_utils.ads:2:06: "Ada.Unchecked_Conversion" is not a predefined library unit
ss_utils.ads:2:06: "Ss_Utils (body)" depends on "System.Storage_Elements (body)"
ss_utils.ads:2:06: "System.Storage_Elements (body)" depends on "Ada.Unchecked_Conversion (spec)"
s-stoele.adb:46:10: "Ada" is undefined (more references follow)
s-stoele.adb:46:10: missing "with Ada.Unchecked_Conversion;"
s-stoele.adb:82:54: expected type "System.Storage_Elements.Integer_Address"
s-stoele.adb:82:54: found type "System.Storage_Elements.Storage_Offset"
s-stoele.adb:88:34: expected type "System.Storage_Elements.Integer_Address"
s-stoele.adb:88:34: found type "System.Storage_Elements.Storage_Offset"
s-stoele.adb:98:54: expected type "System.Storage_Elements.Integer_Address"
s-stoele.adb:98:54: found type "System.Storage_Elements.Storage_Offset"
s-stoele.adb:103:14: "To_Offset" is undefined
gprbuild: *** compilation phase failed
make: *** [Makefile:10: obj/adalib/libgnat.a] Error 4

@jklmnn do you have an idea how this issue could be solved? I have added my modifications on the sgx-ada branch.

__gnat_timeval_to_duration is required in GNAT.Calendar used by AUnit.

Implement allocator to enable use of new. On Linux, __gnat_malloc is implemented using malloc(). On Genode, env is passed to the runtime using a platform-specific interface (called by Genode-specific C++ platform code). On SPARK platforms the existing range allocator from secondary stack could be used.

Files that reside in the contrib directory should be identical to their upstream versions. There are currently various files that have small changes and therefor differ from their upstream version. This is especially important as the upstream version is incompatible.

On Muen we need to implement our own function to print integers by moving our Image function to the runtime library. Once we have that, we can remove the external dependency to put_int and put_int_stderr in all runtime variants using our Image function and putc.

All sources that implement some kind of logic should be proven for the absence of runtime errors.

If exception support stays, we need to make sure to handle exceptions correctly. I found a good explanation on how exceptions, the personality function and the .gcc_except_table ELF section work together.

Execute the SPARK/Ada tests in Genode that are realized as depots using the depot autopilot in our CI.

Create a release from PR #53 and then close this project.

Test and adapt the runtime to GNAT Community 2020

According to the GNAT documentation GNAT might insert calls to memcpy, bcopy, memmove, memcmp, malloc and free when required. We should implement especially memcpy and memcmp as this seems to happen quite often when assigning or comparing bigger types. They should only be provided as a weak symbol to avoid collisions with other libraries.

The platform support code is currently done via CFFI linker symbols. On native Ada platforms this breaks the dependency detection (which then leads to non-executed elaboration code). To solve this issue the platform interface will be transformed into an Ada spec that needs to be implemented by the platform. To keep the convenience for CFFI platforms a stub body will be provided that transforms the spec into linker symbols.

Potentially relevant: Support for Ada.Numerics.Big_Numbers.Big_Integers (#68) for overflow elimination in contracts (cf. [T416-051])

Currently we use a 'magic' symbol for passing Genode's env pointer to the runtime. A better - and type-safe - way of doing that is though an initialization function called by startup code.

Using tagged types in Genode causes the following linker errors:

vga.o: In function `vga___assign':
vga.adb:(.text.vga___assign+0x55): undefined reference to `system__soft_links__abort_undefer'
vga.adb:(.text.vga___assign+0x8b): undefined reference to `__gnat_raise_from_controlled_operation'
vga.adb:(.text.vga___assign+0x9d): undefined reference to `__gnat_raise_nodefer_with_msg'
vga.adb:(.text.vga___assign+0xc7): undefined reference to `system__soft_links__abort_undefer'
vga.adb:(.text.vga___assign+0x10c): undefined reference to `__gnat_raise_from_controlled_operation'
vga.adb:(.text.vga___assign+0x125): undefined reference to `__gnat_raise_nodefer_with_msg'
vga.adb:(.text.vga___assign+0x1c5): undefined reference to `system__soft_links__abort_undefer'
vga.adb:(.text.vga___assign+0x1f2): undefined reference to `__gnat_raise_from_controlled_operation'
vga.adb:(.text.vga___assign+0x201): undefined reference to `__gnat_raise_nodefer_with_msg'
vga.adb:(.text.vga___assign+0x21b): undefined reference to `__gnat_raise_nodefer_with_msg'
vga.adb:(.text.vga___assign+0x246): undefined reference to `system__soft_links__abort_undefer'
vga.adb:(.text.vga___assign+0x273): undefined reference to `__gnat_raise_from_controlled_operation'
vga.o: In function `vga__vgaSW':
vga.adb:(.text.vga__vgaSW+0x26): undefined reference to `system__stream_attributes__w_lu'
vga.adb:(.text.vga__vgaSW+0x34): undefined reference to `system__stream_attributes__w_u'
vga.adb:(.text.vga__vgaSW+0x4d): undefined reference to `system__stream_attributes__w_b'
vga.adb:(.text.vga__vgaSW+0x57): undefined reference to `system__stream_attributes__w_ssu'
vga.adb:(.text.vga__vgaSW+0xc2): undefined reference to `system__stream_attributes__w_c'
vga.o: In function `vga__vgaSR':
vga.adb:(.text.vga__vgaSR+0x26): undefined reference to `system__stream_attributes__i_lu'
vga.adb:(.text.vga__vgaSR+0x34): undefined reference to `system__stream_attributes__i_u'
vga.adb:(.text.vga__vgaSR+0x3e): undefined reference to `system__stream_attributes__i_b'
vga.adb:(.text.vga__vgaSR+0x48): undefined reference to `system__stream_attributes__i_ssu'
vga.adb:(.text.vga__vgaSR+0xbe): undefined reference to `system__stream_attributes__i_c'

Since all other parts of the runtime are explicitly created without threading support it should be removed from the secondary stack allocator, too. This should also allow an easier proof.

The following symbols are missing in the runtime:

__gl_default_stack_size
__gl_detect_blocking
__gl_interrupt_states
__gl_leap_seconds_support
__gl_locking_policy
__gl_main_cpu
__gl_main_priority
__gl_num_interrupt_states
__gl_num_specific_dispatching
__gl_priority_specific_dispatching
__gl_queuing_policy
__gl_task_dispatching_policy
__gl_time_slice_val
__gl_unreserve_all_interrupts
__gl_wc_encoding
__gnat_binder_ss_count
__gnat_default_ss_pool
__gnat_default_ss_size
__gnat_finalize
__gnat_finalize_library_objects
__gnat_initialize
__gnat_rcheck_CE_Access_Check
__gnat_runtime_finalize
__gnat_runtime_initialize
gnat_argc
gnat_argv
gnat_envp
gnat_exit_status
system__soft_links__get_gnat_exception
system__soft_links__get_jmpbuf_address_soft
system__standard_library__adafinal

To remove any dependency on a global Genode::Env the GNAT.IO terminal implementation will be replaced by an implementation with Genode::log that does not depend on Genode::Env.

Since the Genode Toolchain will be updated to GCC 8 we should update our runtime, too. This mainly means replacing the contrib files in this repository.

We should support 'Image/'Img for the most common integer types even in the SPARK runtime.
I'd suggest:

• s-imgboo.ads (Boolean'Image)
• s-imgint.ads (Integer'Image)
• s-imglli.ads (Long_Long_Integer'Image)
• s-imgllu.ads (Long_Long_Unsigned'Image)
• s-imguns.ads (Unsigned'Image)

The runtime should be tested automatically on all supported platforms by the CI.

Please change the license used for the runtime from AGPLv3 to AGPLv3-with-runtime-exception. This is the same as the files under contrib/gcc-6.3.0. For clarity, we should also add a license header to all the source files.

Right now, we cannot prove the runtime directly as gnatprove refuses to prove files that are part of the runtime (i.e. contained also in the runtime used by gnatprove).

We should check whether/how we can run gnatprove on the runtime directly.

Tagged types with dynamic dispatching are also supported in the ZFP runtime. Its complexy is feasible (350-400loc) and it enables the use of tagged and abstract types. Since the ZFP implementation lacks a linker exception in its license and uses access types heavily we want to have our own SPARK implementation.

Implement platform symbols for Muen.

Using the current version of the runtime leads to the following error:

Build Libraries
   [gprlib]       ada.lexch
   [bind SAL]     ada
   [Ada]          b__ada.adb
b__ada.adb:61:44: "Parameters" not declared in "System"
gprlib: invocation of /opt/gnat/bin/gcc failed
gprbuild: could not build library for project ada

The problem is that b__ada.ads does not contain the necessary context item: with System.Parameters;. It is not clear to me how gnatbind decides which with clauses will be added.

There's currently no global state information annotated. This makes proving global state for software that uses especially the drivers more difficult. We should introduce some runtime state.

I tried to add a test which tests the exception behaviour. The expected behaviour is a call to ada_raise_exception which prints the message and exits the program cleanly. Yet this isn't happening. I could track the issue down to Create_File_Line_String but not further. When omitting its call in Rcheck_CE_Explicit_Raise and issuing a constant message the behaviour above applies.