custom parameters for log server

ref #165

src/log/gneiss-log.ads

@@ -46,14 +46,14 @@ is
    --  @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);
 
    --  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);
 
 private
 

src/log/linux/gneiss-log.adb

@@ -5,18 +5,20 @@ with Gneiss_Epoll;
 package body Gneiss.Log with
    SPARK_Mode
 is
-   use type Gneiss_Epoll.Epoll_Fd;
 
    function Initialized (Session : Client_Session) return Boolean is
       (Session.File_Descriptor > -1);
 
    function Initialized (Session : Dispatcher_Session) return Boolean is
       (Session.Broker_Fd > -1
-       and then Session.Epoll_Fd > -1
-       and then Session.Index.Valid);
+       and then Gneiss_Epoll.Valid_Fd (Session.Epoll_Fd)
+       and then Session.Index.Valid
+       and then (if Session.Registered then Session.Dispatch_Fd > -1));
 
    function Initialized (Session : Server_Session) return Boolean is
-      (Session.Fd >= 0 and then Gneiss_Platform.Is_Valid (Session.E_Cap));
+      (Session.Fd >= 0
+       and then Gneiss_Platform.Is_Valid (Session.E_Cap)
+       and then Session.Index.Valid);
 
    function Index (Session : Dispatcher_Session) return Session_Index_Option is
       (Session.Index);

src/log/linux/gneiss_internal-log.ads

@@ -29,6 +29,7 @@ is
       Epoll_Fd    : Gneiss_Epoll.Epoll_Fd       := -1;
       Index       : Gneiss.Session_Index_Option := Gneiss.Session_Index_Option'(Valid => False);
       Dispatch_Fd : Integer                     := -1;
+      Registered  : Boolean                     := False;
    end record;
 
    type Server_Session is limited record

src/log/server/gneiss-log-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/log/server/gneiss-log-server.ads

@@ -12,6 +12,7 @@
 generic
    pragma Warnings (Off, "* is not referenced");
    --  Supress unreferenced warnings since not every platform needs each subprogram
+   type Context is limited private;
 
    --  Called when data needs to be written
    --
@@ -23,19 +24,22 @@ generic
    --  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);
    --  Checks if the server implementation is ready
    --
    --  @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.Log.Server with
    SPARK_Mode

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

@@ -61,8 +61,12 @@ 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;
+         pragma Assert (Initialized (Session));  --  FIXME: This check should succeed
          Platform_Client.Dispatch (Session.Dispatch_Fd,
                                    Gneiss_Protocol.Session.Log,
                                    Name, Label, Fds);
@@ -96,7 +100,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, Fd, Ignore_Success);
          Gneiss_Syscall.Close (Integer (Session.Epoll_Fd));
       end if;
@@ -116,12 +123,17 @@ is
    is
       Ignore_Success : Integer;
    begin
+      if Session.Registered then
+         return;
+      end if;
       Platform_Client.Register (Session.Broker_Fd, Gneiss_Protocol.Session.Log, 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_Cap_Address (Session),
                            Ignore_Success);
+         pragma Assert (Initialized (Session));
       end if;
    end Register;
 
@@ -132,14 +144,21 @@ 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
+      pragma Assert (Server_S.Fd > -1);
+      pragma Assert (Server_S.Index.Valid);
+      pragma Assert (Gneiss_Platform.Is_Valid (Server_S.E_Cap));
+      pragma Assert (Initialized (Server_S));
+      --  FIXME: this assertion should prove,
+      --         it is equal to the three previous ones
+      Server_Instance.Initialize (Server_S, Ctx);
+      if not Server_Instance.Ready (Server_S, Ctx) then
          Gneiss_Syscall.Close (Server_S.Fd);
          Server_S.Index := Gneiss.Session_Index_Option'(Valid => False);
          Gneiss_Platform.Invalidate (Server_S.E_Cap);
@@ -148,8 +167,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, Event_Cap_Address (Server_S), Ignore_Success);
@@ -163,14 +184,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
          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);
          Session.Index := Gneiss.Session_Index_Option'(Valid => False);
          Gneiss_Platform.Invalidate (Server_S.E_Cap);
       end if;
@@ -180,14 +202,19 @@ is
                             Fd      :        Integer)
    is
       pragma Unreferenced (Fd);
+      Write_Buf : Gneiss_Internal.Log.Message_Buffer;
    begin
+      if not Initialized (Session) then
+         return;
+      end if;
       Read_Buffer (Session);
       for I in Session.Buffer'Range loop
          exit when Session.Buffer (I) = ASCII.NUL;
          Session.Cursor := I;
       end loop;
       if Session.Cursor > Session.Buffer'First then
-         Server_Instance.Write (Session, Session.Buffer (Session.Buffer'First .. Session.Cursor));
+         Write_Buf := Session.Buffer;
+         Server_Instance.Write (Session, Write_Buf (Session.Buffer'First .. Session.Cursor));
          --  FIXME: Copy buffer to fix aliasing
       end if;
    end Session_Event;

src/platform/linux/gneiss_platform.ads

@@ -24,7 +24,8 @@ is
                             Fd  :        Integer);
    function Create_Event_Cap (Ev_Ctx : Event_Context;
                               Er_Ctx : Error_Context;
-                              Fd     : Integer) return Event_Cap;
+                              Fd     : Integer) return Event_Cap with
+      Post => Is_Valid (Create_Event_Cap'Result);
 
    procedure Call (Cap : Event_Cap;
                    Ev  : Gneiss_Epoll.Event_Type);

test/linux_log_server/component.adb

@@ -14,27 +14,31 @@ is
       Newline : Boolean           := True;
    end record;
 
-   type Server_Reg is array (Gneiss.Session_Index range <>) of Gneiss.Log.Server_Session;
-   type Server_Meta is array (Gneiss.Session_Index range <>) of Server_Slot;
+   subtype Server_Index is Gneiss.Session_Index range 1 .. 10;
+   type Server_Reg is array (Server_Index'Range) of Gneiss.Log.Server_Session;
+   type Server_Meta is array (Server_Index'Range) of Server_Slot;
+
+   Dispatcher  : Gneiss.Log.Dispatcher_Session;
+   Capability  : Gneiss.Capability;
+   Servers     : Server_Reg;
+   Server_Data : Server_Meta;
 
    procedure Write (Session : in out Gneiss.Log.Server_Session;
                     Data    :        String);
-   procedure Initialize (Session : in out Gneiss.Log.Server_Session);
-   procedure Finalize (Session : in out Gneiss.Log.Server_Session);
-   function Ready (Session : Gneiss.Log.Server_Session) return Boolean;
+   procedure Initialize (Session : in out Gneiss.Log.Server_Session;
+                         Context : in out Server_Meta);
+   procedure Finalize (Session : in out Gneiss.Log.Server_Session;
+                       Context : in out Server_Meta);
+   function Ready (Session : Gneiss.Log.Server_Session;
+                   Context : Server_Meta) return Boolean;
    procedure Dispatch (Session : in out Gneiss.Log.Dispatcher_Session;
                        Cap     :        Gneiss.Log.Dispatcher_Capability;
                        Name    :        String;
                        Label   :        String);
 
-   package Log_Server is new Gneiss.Log.Server (Write, Initialize, Finalize, Ready);
+   package Log_Server is new Gneiss.Log.Server (Server_Meta, Write, Initialize, Finalize, Ready);
    package Log_Dispatcher is new Gneiss.Log.Dispatcher (Log_Server, Dispatch);
 
-   Dispatcher  : Gneiss.Log.Dispatcher_Session;
-   Capability  : Gneiss.Capability;
-   Servers     : Server_Reg (1 .. 10);
-   Server_Data : Server_Meta (Servers'Range);
-
    procedure Construct (Cap : Gneiss.Capability)
    is
    begin
@@ -83,25 +87,27 @@ is
       null;
    end Destruct;
 
-   procedure Initialize (Session : in out Gneiss.Log.Server_Session)
+   procedure Initialize (Session : in out Gneiss.Log.Server_Session;
+                         Context : in out Server_Meta)
    is
    begin
       if
          Gneiss.Log.Index (Session).Valid
-         and then Gneiss.Log.Index (Session).Value in Server_Data'Range
+         and then Gneiss.Log.Index (Session).Value in Context'Range
       then
-         Server_Data (Gneiss.Log.Index (Session).Value).Ready := True;
+         Context (Gneiss.Log.Index (Session).Value).Ready := True;
       end if;
    end Initialize;
 
-   procedure Finalize (Session : in out Gneiss.Log.Server_Session)
+   procedure Finalize (Session : in out Gneiss.Log.Server_Session;
+                       Context : in out Server_Meta)
    is
    begin
       if
          Gneiss.Log.Index (Session).Valid
-         and then Gneiss.Log.Index (Session).Value in Server_Data'Range
+         and then Gneiss.Log.Index (Session).Value in Context'Range
       then
-         Server_Data (Gneiss.Log.Index (Session).Value).Ready := False;
+         Context (Gneiss.Log.Index (Session).Value).Ready := False;
       end if;
    end Finalize;
 
@@ -113,27 +119,28 @@ is
    begin
       if Log_Dispatcher.Valid_Session_Request (Session, Cap) then
          for I in Servers'Range loop
-            if not Ready (Servers (I)) then
-               Log_Dispatcher.Session_Initialize (Session, Cap, Servers (I), I);
-               if Ready (Servers (I)) and then Gneiss.Log.Initialized (Servers (I)) then
+            if not Ready (Servers (I), Server_Data) then
+               Log_Dispatcher.Session_Initialize (Session, Cap, Servers (I), Server_Data, I);
+               if Ready (Servers (I), Server_Data) and then Gneiss.Log.Initialized (Servers (I)) then
                   Server_Data (I).Last := Name'Length + Label'Length + 1;
                   Server_Data (I).Ident (1 .. Server_Data (I).Last) := Name & ":" & Label;
-                  Log_Dispatcher.Session_Accept (Session, Cap, Servers (I));
+                  Log_Dispatcher.Session_Accept (Session, Cap, Servers (I), Server_Data);
                   exit;
                end if;
             end if;
          end loop;
       end if;
       for S of Servers loop
-         Log_Dispatcher.Session_Cleanup (Session, Cap, S);
+         Log_Dispatcher.Session_Cleanup (Session, Cap, S, Server_Data);
       end loop;
    end Dispatch;
 
-   function Ready (Session : Gneiss.Log.Server_Session) return Boolean is
+   function Ready (Session : Gneiss.Log.Server_Session;
+                   Context : Server_Meta) return Boolean is
       (if
           Gneiss.Log.Index (Session).Valid
-          and then Gneiss.Log.Index (Session).Value in Server_Data'Range
-       then Server_Data (Gneiss.Log.Index (Session).Value).Ready
+          and then Gneiss.Log.Index (Session).Value in Context'Range
+       then Context (Gneiss.Log.Index (Session).Value).Ready
        else False);
 
 end Component;