Generate tagged types for sessions

Ref. #768

defaults.adc

@@ -1,2 +1,3 @@
-pragma Restrictions (No_Elaboration_Code);
+-- pragma Restrictions (No_Elaboration_Code);
 pragma Restrictions (No_Secondary_Stack);
+-- pragma Restrictions (No_Tagged_Type_Registration);

examples/apps/dhcp_client/src/channel.adb

@@ -57,12 +57,11 @@ is
       SPARK_Mode => Off
    is
       Data : constant Ada.Streams.Stream_Element_Array (1 .. Buffer'Length) := To_Ada_Stream (Buffer);
-      Last : Ada.Streams.Stream_Element_Offset;
+      Unused_Last : Ada.Streams.Stream_Element_Offset;
    begin
-      pragma Unreferenced (Last);
       GNAT.Sockets.Send_Socket (Socket => Socket,
                                 Item => Data,
-                                Last => Last,
+                                Last => Unused_Last,
                                 To => GNAT.Sockets.Sock_Addr_Type'(Family => GNAT.Sockets.Family_Inet,
                                                                    Addr => GNAT.Sockets.Inet_Addr ("255.255.255.255"),
                                                                    Port => 67));

examples/apps/dhcp_client/src/dhcp_client.adb

@@ -2,87 +2,86 @@ pragma SPARK_Mode;
 
 with Ada.Text_IO;
 
-with GNAT.Sockets;
-
 with RFLX.RFLX_Types;
 with RFLX.RFLX_Builtin_Types;
 with RFLX.DHCP_Client.Session;
 
 with Channel;
+with Session;
 
 procedure DHCP_Client is
-   Socket : GNAT.Sockets.Socket_Type;
-
-   package Session is new RFLX.DHCP_Client.Session;
+   package DHCP_Client_Session renames RFLX.DHCP_Client.Session;
+   package Types renames RFLX.RFLX_Types;
 
-   procedure Read with
+   procedure Read (Ctx : in out Session.Context) with
       Pre =>
-         Session.Initialized
-         and then Session.Has_Data (Session.C_Channel),
+         DHCP_Client_Session.Initialized (Ctx)
+         and then DHCP_Client_Session.Has_Data (Ctx, DHCP_Client_Session.C_Channel),
       Post =>
-         Session.Initialized
+         DHCP_Client_Session.Initialized (Ctx)
    is
-      use type RFLX.RFLX_Types.Index;
-      use type RFLX.RFLX_Types.Length;
-      Buffer : RFLX.RFLX_Types.Bytes (RFLX.RFLX_Types.Index'First .. RFLX.RFLX_Types.Index'First + 4095)
+      use type Types.Index;
+      use type Types.Length;
+      Buffer : Types.Bytes (Types.Index'First .. Types.Index'First + 4095)
          := (others => 0);
+      Size : constant Types.Length := DHCP_Client_Session.Read_Buffer_Size (Ctx, DHCP_Client_Session.C_Channel);
    begin
-      if Buffer'Length >= Session.Read_Buffer_Size (Session.C_Channel) then
-         Session.Read
-            (Session.C_Channel,
-             Buffer
-                (Buffer'First
-                 .. Buffer'First - 2 + RFLX.RFLX_Types.Index (Session.Read_Buffer_Size (Session.C_Channel) + 1)));
-         Channel.Send
-            (Socket,
-             Buffer
-                (Buffer'First
-                 .. Buffer'First - 2 + RFLX.RFLX_Types.Index (Session.Read_Buffer_Size (Session.C_Channel) + 1)));
-      else
-         Ada.Text_IO.Put_Line ("Error: read buffer too small");
+      if Size = 0 then
+         Ada.Text_IO.Put_Line ("Error: read buffer size is 0");
+         return;
       end if;
+      if Buffer'Length < Size then
+         Ada.Text_IO.Put_Line ("Error: buffer too small");
+         return;
+      end if;
+      DHCP_Client_Session.Read
+         (Ctx,
+          DHCP_Client_Session.C_Channel,
+          Buffer (Buffer'First .. Buffer'First - 2 + Types.Index (Size + 1)));
+      Channel.Send
+         (Ctx.Socket,
+          Buffer (Buffer'First .. Buffer'First - 2 + Types.Index (Size + 1)));
    end Read;
 
-   procedure Write with
+   procedure Write (Ctx : in out Session.Context) with
       Pre =>
-         Session.Initialized
-         and then Session.Needs_Data (Session.C_Channel),
+         DHCP_Client_Session.Initialized (Ctx)
+         and then DHCP_Client_Session.Needs_Data (Ctx, DHCP_Client_Session.C_Channel),
       Post =>
-         Session.Initialized
+         DHCP_Client_Session.Initialized (Ctx)
    is
-      use type RFLX.RFLX_Types.Index;
-      use type RFLX.RFLX_Types.Length;
-      Buffer : RFLX.RFLX_Types.Bytes (RFLX.RFLX_Types.Index'First .. RFLX.RFLX_Types.Index'First + 4095);
+      use type Types.Index;
+      use type Types.Length;
+      Buffer : Types.Bytes (Types.Index'First .. Types.Index'First + 4095);
       Length : RFLX.RFLX_Builtin_Types.Length;
    begin
-      Channel.Receive (Socket, Buffer, Length);
+      Channel.Receive (Ctx.Socket, Buffer, Length);
       if
          Length > 0
-         and Length <= Session.Write_Buffer_Size (Session.C_Channel)
+         and Length <= DHCP_Client_Session.Write_Buffer_Size (Ctx, DHCP_Client_Session.C_Channel)
       then
-         Session.Write
-            (Session.C_Channel,
+         DHCP_Client_Session.Write
+            (Ctx,
+             DHCP_Client_Session.C_Channel,
              Buffer (Buffer'First .. Buffer'First +  RFLX.RFLX_Builtin_Types.Index (Length) - 1));
       end if;
    end Write;
+
+   Ctx : Session.Context;
 begin
-   Channel.Initialize (Socket);
-   Session.Initialize;
-   while Session.Active loop
-      pragma Loop_Invariant (Session.Initialized);
-      for C in Session.Channel'Range loop
-         pragma Loop_Invariant (Session.Initialized);
-         if Session.Has_Data (C) then
-            Read;
+   Channel.Initialize (Ctx.Socket);
+   DHCP_Client_Session.Initialize (Ctx);
+   while DHCP_Client_Session.Active (Ctx) loop
+      pragma Loop_Invariant (DHCP_Client_Session.Initialized (Ctx));
+      for C in DHCP_Client_Session.Channel'Range loop
+         pragma Loop_Invariant (DHCP_Client_Session.Initialized (Ctx));
+         if DHCP_Client_Session.Has_Data (Ctx, C) then
+            Read (Ctx);
          end if;
-         if Session.Needs_Data (C) then
-            Write;
+         if DHCP_Client_Session.Needs_Data (Ctx, C) then
+            Write (Ctx);
          end if;
       end loop;
-      Session.Run;
+      DHCP_Client_Session.Run (Ctx);
    end loop;
-   --  ISSUE: Componolit/Workarounds#32
-   pragma Warnings (Off, """*"" is set by ""Finalize"" but not used after the call");
-   Session.Finalize;
-   pragma Warnings (On, """*"" is set by ""Finalize"" but not used after the call");
 end DHCP_Client;

examples/apps/dhcp_client/src/session.ads

@@ -1,5 +1,14 @@
-pragma SPARK_Mode;
+with GNAT.Sockets;
 
 with RFLX.DHCP_Client.Session;
 
-package Session is new RFLX.DHCP_Client.Session;
+package Session with
+  SPARK_Mode
+is
+
+   type Context is new RFLX.DHCP_Client.Session.Context with
+      record
+         Socket : GNAT.Sockets.Socket_Type;
+      end record;
+
+end Session;

rflx/ada.py

@@ -1,5 +1,7 @@
 # pylint: disable=too-many-lines
 
+from __future__ import annotations
+
 import itertools
 import os
 from abc import abstractmethod
@@ -413,6 +415,10 @@ class Image(Attribute):
     pass
 
 
+class Class(Attribute):
+    pass
+
+
 class UnrestrictedAccess(Attribute):
     @property
     def _representation(self) -> str:
@@ -945,6 +951,32 @@ def definition(self) -> str:
         return str(self.expr)
 
 
+class ClassPrecondition(Aspect):
+    def __init__(self, expr: Expr) -> None:
+        self.expr = expr
+
+    @property
+    def mark(self) -> str:
+        return "Pre'Class"
+
+    @property
+    def definition(self) -> str:
+        return str(self.expr)
+
+
+class ClassPostcondition(Aspect):
+    def __init__(self, expr: Expr) -> None:
+        self.expr = expr
+
+    @property
+    def mark(self) -> str:
+        return "Post'Class"
+
+    @property
+    def definition(self) -> str:
+        return str(self.expr)
+
+
 class ContractCases(Aspect):
     def __init__(self, *cases: Tuple[Expr, Expr]) -> None:
         self.cases = cases
@@ -1069,6 +1101,7 @@ def definition(self) -> str:
 
 class Annotate(Aspect):
     def __init__(self, *args: str) -> None:
+        assert len(args) > 0
         self.args = args
 
     @property
@@ -1081,6 +1114,16 @@ def definition(self) -> str:
         return f"({args})"
 
 
+class ElaborateBody(Aspect):
+    @property
+    def mark(self) -> str:
+        return "Elaborate_Body"
+
+    @property
+    def definition(self) -> str:
+        return ""
+
+
 class FormalDeclaration(Base):
     @abstractmethod
     def __str__(self) -> str:
@@ -1365,13 +1408,32 @@ def type_definition(self) -> str:
 
 
 class DerivedType(TypeDeclaration):
-    def __init__(self, identifier: StrID, type_identifier: StrID) -> None:
+    def __init__(
+        self,
+        identifier: StrID,
+        type_identifier: StrID,
+        record_extension: Sequence[Component] = None,
+    ) -> None:
         super().__init__(identifier)
         self.type_identifier = ID(type_identifier)
+        self.record_extension = record_extension
 
     @property
     def type_definition(self) -> str:
-        return f" new {self.type_identifier}"
+        extension = ""
+
+        if self.record_extension is not None:
+            if len(self.record_extension) == 0:
+                extension = " with null record"
+            else:
+                components = (
+                    (indent("\n".join(map(str, self.record_extension)), 6) + "\n")
+                    if self.record_extension
+                    else ""
+                )
+                extension = f" with\n   record\n{components}   end record"
+
+        return f" new {self.type_identifier}{extension}"
 
 
 class PrivateType(TypeDeclaration):
@@ -1415,17 +1477,23 @@ def type_definition(self) -> str:
 
 class Component(Base):
     def __init__(
-        self, identifier: StrID, type_identifier: Union[StrID, Expr], default: Expr = None
+        self,
+        identifier: StrID,
+        type_identifier: Union[StrID, Expr],
+        default: Expr = None,
+        aliased: bool = False,
     ) -> None:
         self.identifier = ID(identifier)
         self.type_identifier = (
             type_identifier if isinstance(type_identifier, Expr) else Variable(type_identifier)
         )
         self.default = default
+        self.aliased = aliased
 
     def __str__(self) -> str:
         default = f" := {self.default}" if self.default else ""
-        return f"{self.identifier} : {self.type_identifier}{default};"
+        aliased = "aliased " if self.aliased else ""
+        return f"{self.identifier} : {aliased}{self.type_identifier}{default};"
 
 
 class NullComponent(Component):
@@ -1458,26 +1526,39 @@ def __str__(self) -> str:
 
 
 class RecordType(TypeDeclaration):
-    def __init__(
+    def __init__(  # pylint: disable = too-many-arguments
         self,
         identifier: StrID,
         components: List[Component],
         discriminants: Sequence[Discriminant] = None,
         variant_part: VariantPart = None,
         aspects: Sequence[Aspect] = None,
+        abstract: bool = False,
+        tagged: bool = False,
     ) -> None:
+        assert tagged if abstract else True
         super().__init__(identifier, discriminants, aspects)
         self.components = components
         self.discriminants = discriminants or []
         self.variant_part = variant_part
+        self.abstract = abstract
+        self.tagged = tagged
 
     @property
     def type_definition(self) -> str:
-        components = (
-            (indent("\n".join(map(str, self.components)), 6) + "\n") if self.components else ""
-        )
-        variant_part = indent(str(self.variant_part), 6) if self.variant_part else ""
-        return f"\n" f"   record\n" f"{components}" f"{variant_part}" f"   end record"
+        abstract = " abstract" if self.abstract else ""
+        tagged = " tagged" if self.tagged else ""
+
+        if self.components or self.variant_part:
+            components = (
+                (indent("\n".join(map(str, self.components)), 6) + "\n") if self.components else ""
+            )
+            variant_part = indent(str(self.variant_part), 6) if self.variant_part else ""
+            definition = f"\n   record\n{components}{variant_part}   end record"
+        else:
+            definition = " null record"
+
+        return f"{abstract}{tagged}{definition}"
 
 
 class Statement(Base):
@@ -1808,15 +1889,18 @@ def __init__(
         specification: SubprogramSpecification,
         aspects: Sequence[Aspect] = None,
         formal_parameters: Sequence[FormalDeclaration] = None,
+        abstract: bool = False,
     ) -> None:
         super().__init__(specification)
         self.aspects = aspects or []
         self.formal_parameters = formal_parameters
+        self.abstract = abstract
 
     def __str__(self) -> str:
+        abstract = " is abstract" if self.abstract else ""
         return (
             f"{generic_formal_part(self.formal_parameters)}"
-            f"{self.specification}{aspect_specification(self.aspects)};"
+            f"{self.specification}{abstract}{aspect_specification(self.aspects)};"
         )