custom parameter and proof for message server

ref #165

src/message/gneiss-message.ads

@@ -53,21 +53,21 @@ is
    --  @param Session  Client session instance
    --  @return         Session index
    function Index (Session : Client_Session) return Session_Index_Option with
-      Post => Initialized (Session) = Index'Result.Valid;
+      Post => (if Initialized (Session) then Index'Result.Valid);
 
    --  Get the index value that has been set on initialization
    --
    --  @param Session  Server session instance
    --  @return         Session index
    function Index (Session : Server_Session) return Session_Index_Option with
-      Post => Initialized (Session) = Index'Result.Valid;
+      Post => (if Initialized (Session) then Index'Result.Valid);
 
    --  Get the index value that has been set on initialization
    --
    --  @param Session  Dispatcher session instance
    --  @return         Session index
    function Index (Session : Dispatcher_Session) return Session_Index_Option with
-      Post => Initialized (Session) = Index'Result.Valid;
+      Post => (if Initialized (Session) then Index'Result.Valid);
 
 private
 

src/message/linux/gneiss-message.adb

@@ -21,7 +21,8 @@ is
    function Initialized (Session : Dispatcher_Session) return Boolean is
       (Session.Broker_Fd >= 0
        and then Session.Epoll_Fd >= 0
-       and then Session.Index.Valid);
+       and then Session.Index.Valid
+       and then (if Session.Registered then Session.Dispatch_Fd > -1));
 
    function Index (Session : Client_Session) return Session_Index_Option is
       (Session.Index);

src/message/linux/gneiss_internal-message.ads

@@ -33,6 +33,7 @@ is
       Epoll_Fd         : Gneiss_Epoll.Epoll_Fd       := -1;
       Dispatch_Fd      : Integer                     := -1;
       Index            : Gneiss.Session_Index_Option := Gneiss.Session_Index_Option'(Valid => False);
+      Registered       : Boolean                     := False;
       E_Cap            : Gneiss_Platform.Event_Cap;
    end record;
 

src/message/server/gneiss-message-dispatcher.ads

@@ -69,10 +69,11 @@ is
    procedure Session_Initialize (Session  : in out Dispatcher_Session;
                                  Cap      :        Dispatcher_Capability;
                                  Server_S : in out Server_Session;
+                                 Ctx      : in out Server_Instance.Context;
                                  Idx      :        Session_Index := 1) with
       Pre  => Initialized (Session)
               and then Valid_Session_Request (Session, Cap)
-              and then not Server_Instance.Ready (Server_S)
+              and then not Server_Instance.Ready (Server_S, Ctx)
               and then not Initialized (Server_S),
       Post => Initialized (Session)
               and then Valid_Session_Request (Session, Cap);
@@ -84,13 +85,14 @@ is
    --  @param Server_S  Server session instance to handle client connection with
    procedure Session_Accept (Session  : in out Dispatcher_Session;
                              Cap      :        Dispatcher_Capability;
-                             Server_S : in out Server_Session) with
+                             Server_S : in out Server_Session;
+                             Ctx      :        Server_Instance.Context) with
       Pre  => Initialized (Session)
               and then Valid_Session_Request (Session, Cap)
-              and then Server_Instance.Ready (Server_S)
+              and then Server_Instance.Ready (Server_S, Ctx)
               and then Initialized (Server_S),
       Post => Initialized (Session)
-              and then Server_Instance.Ready (Server_S)
+              and then Server_Instance.Ready (Server_S, Ctx)
               and then Initialized (Server_S);
 
    --  Garbage collects disconnected sessions
@@ -104,7 +106,8 @@ is
    --  @param Server_S  Server session instance to check for removal
    procedure Session_Cleanup (Session  : in out Dispatcher_Session;
                               Cap      :        Dispatcher_Capability;
-                              Server_S : in out Server_Session) with
+                              Server_S : in out Server_Session;
+                              Ctx      : in out Server_Instance.Context) with
       Pre  => Initialized (Session),
       Post => Initialized (Session);
 

src/message/server/gneiss-message-server.ads

@@ -12,20 +12,23 @@
 generic
    pragma Warnings (Off, "* is not referenced");
    --  Supress unreferenced warnings since not every platform needs each subprogram
+   type Context is limited private;
 
    --  Custom initialization for the server,
    --  automatically called by Gneiss.Block.Dispatcher.Session_Accept
    --
    --  @param Session  Server session instance
-   with procedure Initialize (Session : in out Server_Session);
+   with procedure Initialize (Session : in out Server_Session;
+                              Ctx     : in out Context);
 
    --  Custom finalization for the server
    --
    --  Is automatically called by Gneiss.Block.Dispatcher.Session_Cleanup
    --  when the connected client disconnects.
    --
    --  @param S  Server session instance
-   with procedure Finalize (Session : in out Server_Session);
+   with procedure Finalize (Session : in out Server_Session;
+                            Ctx     : in out Context);
 
    --  Called when a message is recieved
    --
@@ -38,7 +41,8 @@ generic
    --
    --  @param S  Server session instance
    --  @return   True if the server implementation is ready
-   with function Ready (Session : Server_Session) return Boolean;
+   with function Ready (Session : Server_Session;
+                        Ctx     : Context) return Boolean;
    pragma Warnings (On, "* is not referenced");
 package Gneiss.Message.Server with
    SPARK_Mode
@@ -50,10 +54,11 @@ is
    --  @param Session  Server session instance
    --  @param Data     Message
    procedure Send (Session : in out Server_Session;
-                   Data    :        Message_Buffer) with
-      Pre  => Ready (Session)
+                   Data    :        Message_Buffer;
+                   Ctx     :        Context) with
+      Pre  => Ready (Session, Ctx)
               and then Initialized (Session),
-      Post => Ready (Session)
+      Post => Ready (Session, Ctx)
               and then Initialized (Session);
 
 end Gneiss.Message.Server;

src/message/server/linux/gneiss-message-dispatcher.adb

@@ -31,10 +31,13 @@ is
                                                                   Dispatch_Error);
 
    function Available (Session : Server_Session) return Boolean is
-      (Gneiss_Internal.Message_Syscall.Peek (Session.Fd) >= Message_Buffer'Size * 8);
+      (Gneiss_Internal.Message_Syscall.Peek (Session.Fd) >= Message_Buffer'Size * 8) with
+         Pre => Initialized (Session);
 
    procedure Read (Session : in out Server_Session;
-                   Data    :    out Message_Buffer);
+                   Data    :    out Message_Buffer) with
+      Pre  => Initialized (Session),
+      Post => Initialized (Session);
 
    procedure Read (Session : in out Server_Session;
                    Data    :    out Message_Buffer) with
@@ -50,6 +53,9 @@ is
       pragma Unreferenced (Fd);
       Buffer : Message_Buffer;
    begin
+      if not Initialized (Session) then
+         return;
+      end if;
       if Available (Session) then
          Read (Session, Buffer);
          Server_Instance.Receive (Session, Buffer);
@@ -77,6 +83,9 @@ is
       Name  : Gneiss_Internal.Session_Label;
       Label : Gneiss_Internal.Session_Label;
    begin
+      if not Initialized (Session) then
+         return;
+      end if;
       if Fd = Session.Dispatch_Fd then
          Session.Accepted := False;
          Platform_Client.Dispatch (Session.Dispatch_Fd, RFLX.Session.Message,
@@ -111,7 +120,10 @@ is
    is
       Ignore_Success : Integer;
    begin
-      if Fd = Session.Dispatch_Fd then
+      if not Initialized (Session) then
+         return;
+      end if;
+      if Fd = Session.Dispatch_Fd and then Session.Registered then
          Gneiss_Epoll.Remove (Session.Epoll_Fd, Session.Dispatch_Fd, Ignore_Success);
       end if;
    end Dispatch_Error;
@@ -132,7 +144,8 @@ is
    begin
       Platform_Client.Register (Session.Broker_Fd, RFLX.Session.Message, Session.Dispatch_Fd);
       if Session.Dispatch_Fd > -1 then
-         Session.E_Cap := Dispatch_Cap (Session, Session, Session.Dispatch_Fd);
+         Session.Registered := True;
+         Session.E_Cap      := Dispatch_Cap (Session, Session, Session.Dispatch_Fd);
          Gneiss_Epoll.Add (Session.Epoll_Fd, Session.Dispatch_Fd,
                            Dispatch_Event_Address (Session), Ignore_Success);
       end if;
@@ -145,14 +158,15 @@ is
    procedure Session_Initialize (Session  : in out Dispatcher_Session;
                                  Cap      :        Dispatcher_Capability;
                                  Server_S : in out Server_Session;
+                                 Ctx      : in out Server_Instance.Context;
                                  Idx      :        Session_Index := 1)
    is
    begin
       Server_S.Fd       := Cap.Server_Fd;
       Server_S.Index    := Gneiss.Session_Index_Option'(Valid => True, Value => Idx);
       Server_S.E_Cap    := Event_Cap (Server_S, Session, Server_S.Fd);
-      Server_Instance.Initialize (Server_S);
-      if not Server_Instance.Ready (Server_S) then
+      Server_Instance.Initialize (Server_S, Ctx);
+      if not Server_Instance.Ready (Server_S, Ctx) then
          Server_S.Index := Gneiss.Session_Index_Option'(Valid => False);
          Gneiss_Syscall.Close (Server_S.Fd);
          Gneiss_Platform.Invalidate (Server_S.E_Cap);
@@ -161,8 +175,10 @@ is
 
    procedure Session_Accept (Session  : in out Dispatcher_Session;
                              Cap      :        Dispatcher_Capability;
-                             Server_S : in out Server_Session)
+                             Server_S : in out Server_Session;
+                             Ctx      :        Server_Instance.Context)
    is
+      pragma Unreferenced (Ctx);
       Ignore_Success : Integer;
    begin
       Gneiss_Epoll.Add (Session.Epoll_Fd, Server_S.Fd, Server_Event_Address (Server_S), Ignore_Success);
@@ -176,14 +192,15 @@ is
 
    procedure Session_Cleanup (Session  : in out Dispatcher_Session;
                               Cap      :        Dispatcher_Capability;
-                              Server_S : in out Server_Session)
+                              Server_S : in out Server_Session;
+                              Ctx      : in out Server_Instance.Context)
    is
       Ignore_Success : Integer;
    begin
-      if Cap.Clean_Fd > -1 and then Cap.Clean_Fd = Server_S.Fd then
+      if Cap.Clean_Fd > -1 and then Cap.Clean_Fd = Server_S.Fd and then Initialized (Server_S) then
          Gneiss_Epoll.Remove (Session.Epoll_Fd, Server_S.Fd, Ignore_Success);
+         Server_Instance.Finalize (Server_S, Ctx);
          Gneiss_Syscall.Close (Server_S.Fd);
-         Server_Instance.Finalize (Server_S);
          Server_S.Index := Gneiss.Session_Index_Option'(Valid => False);
          Gneiss_Platform.Invalidate (Server_S.E_Cap);
       end if;

src/message/server/linux/gneiss-message-server.adb

@@ -6,9 +6,11 @@ package body Gneiss.Message.Server with
 is
 
    procedure Send (Session : in out Server_Session;
-                   Data    :        Message_Buffer) with
+                   Data    :        Message_Buffer;
+                   Ctx     :        Context) with
       SPARK_Mode => Off
    is
+      pragma Unreferenced (Ctx);
    begin
       Gneiss_Internal.Message_Syscall.Write (Session.Fd, Data'Address, Data'Size * 8);
    end Send;

test/message_server/component.adb

@@ -17,25 +17,27 @@ is
       Ready : Boolean := False;
    end record;
 
-   type Server_Reg is array (Gneiss.Session_Index range <>) of Message.Server_Session;
-   type Server_Meta is array (Gneiss.Session_Index range <>) of Server_Slot;
+   subtype Server_Index is Gneiss.Session_Index range 1 .. 2;
+   type Server_Reg is array (Server_Index'Range) of Message.Server_Session;
+   type Server_Meta is array (Server_Index'Range) of Server_Slot;
 
-   procedure Initialize (Session : in out Message.Server_Session) with
+   procedure Initialize (Session : in out Message.Server_Session;
+                         Context : in out Server_Meta) with
       Pre  => Message.Initialized (Session),
       Post => Message.Initialized (Session);
 
-   procedure Finalize (Session : in out Message.Server_Session) with
+   procedure Finalize (Session : in out Message.Server_Session;
+                       Context : in out Server_Meta) with
       Pre  => Message.Initialized (Session),
       Post => Message.Initialized (Session);
 
    procedure Recv (Session : in out Message.Server_Session;
                    Data    :        Message_Buffer) with
-      Pre  => Message.Initialized (Session)
-              and then Ready (Session),
-      Post => Message.Initialized (Session)
-              and then Ready (Session);
+      Pre  => Message.Initialized (Session),
+      Post => Message.Initialized (Session);
 
-   function Ready (Session : Message.Server_Session) return Boolean;
+   function Ready (Session : Message.Server_Session;
+                   Context : Server_Meta) return Boolean;
 
    procedure Dispatch (Session  : in out Message.Dispatcher_Session;
                        Disp_Cap :        Message.Dispatcher_Capability;
@@ -44,13 +46,13 @@ is
       Pre  => Message.Initialized (Session),
       Post => Message.Initialized (Session);
 
-   package Message_Server is new Message.Server (Initialize, Finalize, Recv, Ready);
+   package Message_Server is new Message.Server (Server_Meta, Initialize, Finalize, Recv, Ready);
    package Message_Dispatcher is new Message.Dispatcher (Message_Server, Dispatch);
 
    Dispatcher  : Message.Dispatcher_Session;
    Capability  : Gneiss.Capability;
-   Servers     : Server_Reg (1 .. 2);
-   Server_Data : Server_Meta (Servers'Range);
+   Servers     : Server_Reg;
+   Server_Data : Server_Meta;
 
    procedure Construct (Cap : Gneiss.Capability)
    is
@@ -74,22 +76,26 @@ is
                    Data    :        Message_Buffer)
    is
    begin
-      Message_Server.Send (Session, Data);
+      if Ready (Session, Server_Data) then
+         Message_Server.Send (Session, Data, Server_Data);
+      end if;
    end Recv;
 
-   procedure Initialize (Session : in out Message.Server_Session)
+   procedure Initialize (Session : in out Message.Server_Session;
+                         Context : in out Server_Meta)
    is
    begin
-      if Message.Index (Session).Value in Server_Data'Range then
-         Server_Data (Message.Index (Session).Value).Ready := True;
+      if Message.Index (Session).Value in Context'Range then
+         Context (Message.Index (Session).Value).Ready := True;
       end if;
    end Initialize;
 
-   procedure Finalize (Session : in out Message.Server_Session)
+   procedure Finalize (Session : in out Message.Server_Session;
+                       Context : in out Server_Meta)
    is
    begin
-      if Message.Index (Session).Value in Server_Data'Range then
-         Server_Data (Message.Index (Session).Value).Ready := False;
+      if Message.Index (Session).Value in Context'Range then
+         Context (Message.Index (Session).Value).Ready := False;
       end if;
    end Finalize;
 
@@ -102,32 +108,33 @@ is
       if Message_Dispatcher.Valid_Session_Request (Session, Disp_Cap) then
          for I in Servers'Range loop
             if
-               not Ready (Servers (I))
+               not Ready (Servers (I), Server_Data)
                and then not Message.Initialized (Servers (I))
                and then Name'Length < Server_Data (I).Ident'Last
                and then Label'Length < Server_Data (I).Ident'Last
                and then Name'Length + Label'Length + 1 <= Server_Data (I).Ident'Last
                and then Name'First < Positive'Last - Server_Data (I).Ident'Length
             then
-               Message_Dispatcher.Session_Initialize (Session, Disp_Cap, Servers (I), I);
-               if Ready (Servers (I)) and then Message.Initialized (Servers (I)) then
+               Message_Dispatcher.Session_Initialize (Session, Disp_Cap, Servers (I), Server_Data, I);
+               if Ready (Servers (I), Server_Data) and then Message.Initialized (Servers (I)) then
                   Server_Data (I).Ident (1 .. Name'Length + Label'Length + 1) := Name & ":" & Label;
-                  Message_Dispatcher.Session_Accept (Session, Disp_Cap, Servers (I));
+                  Message_Dispatcher.Session_Accept (Session, Disp_Cap, Servers (I), Server_Data);
                   exit;
                end if;
             end if;
          end loop;
       end if;
       for S of Servers loop
-         Message_Dispatcher.Session_Cleanup (Session, Disp_Cap, S);
+         Message_Dispatcher.Session_Cleanup (Session, Disp_Cap, S, Server_Data);
       end loop;
    end Dispatch;
 
-   function Ready (Session : Message.Server_Session) return Boolean is
+   function Ready (Session : Message.Server_Session;
+                   Context : Server_Meta) return Boolean is
       (if
           Message.Index (Session).Valid
-          and then Message.Index (Session).Value in Server_Data'Range
-       then Server_Data (Message.Index (Session).Value).Ready
+          and then Message.Index (Session).Value in Context'Range
+       then Context (Message.Index (Session).Value).Ready
        else False);
 
 end Component;