Simplify code generation caused by generic buffer type

[treiher]

Context and Problem Statement

In #46 we added a generic package Types to allow the use of custom buffer types in the generated SPARK code. Types must be a formal parameter of all packages which use the buffer type. Also all packages which depend on Types and are used by another package depending on Types must be also passed as formal parameter. This leads to complex dependencies between this packages and instantiating them can be very cumbersome. Here is an example related to sessions (cf. #650):

A session S has a function F1 with message M1 as return type. M1 contains a sequence S1 with message M2 as sequence element. The generic packages need the following formal parameters:

• S
  • Types
  • M2
    • Types
  • S1
    • Types
    • M2
      • Types
  • M1
    • Types
    • M2
      • Types
    • S1
      • Types
      • M2
        • Types
  • F1
    • M1
      • Types
      • M2
        • Types
      • S1
        • Types
        • M2
          • Types

Each indentation level represents the formal parameters required to instantiate the corresponding package (e.g, M1 has the formal parameters Types, M2 and S1). Even this relatively simple example requires a user to instantiate five generic packages to instantiate the generic session package S. In realistic cases, the number is likely to be much higher.

Considered Options

O1 Use just one instantiation of Types

All generated code could expect to find an instantiation of Types at a specified place (e.g., {PREFIX}.RFLX_Types) instead of getting it as formal parameter. A user could customize this instantiation by additional arguments for rflx or by editing the generated source code directly ({PREFIX}.RFLX_Types is already generated with predefined types). As a consequence generic packages would not be needed for messages anymore. Generic packages for sessions would only need formal parameters for channels and external functions.

+ Much simpler code; no need for many formal parameters and generic packages anymore
− Generated code is fixed to one buffer type, using two different buffer types in one application would not be possible anymore (without duplicating generated code)
− Derived messages cannot be realized by message instantiation when message is not generic package

Decision Outcome

O1

[treiher]

After the refactoring I get a bug box now:

+===========================GNAT BUG DETECTED==============================+
| Community 2020 (20200429-93) (x86_64-pc-linux-gnu) GCC error:            |
| in gnat_to_gnu_entity, at ada/gcc-interface/decl.c:456                   |
| Error detected at rflx-ethernet-frame.ads:168:32                         |

The error points to the Fld attribute of a function in a precondition:

   function Path_Condition (Ctx : Context; Fld : Field) return Boolean with
     Pre =>
       Valid_Predecessor (Ctx, Fld);

There were no direct changes related to Field or this function, so the root cause is unclear to me and it would probably take some time to find it. The bug is already fixed in later versions of GNAT, so we could also just wait for the Community 2021 release (which should be released soon) and drop the support for Community 2020 afterwards.