prove global state of rom client

ref #164
Componolit · Apr 24, 2020 · 22115db · 22115db
1 parent cc6d8aa
commit 22115db
Show file tree

Hide file tree

Showing 4 changed files with 55 additions and 18 deletions.
diff --git a/src/rom/client/gneiss-rom-client.ads b/src/rom/client/gneiss-rom-client.ads
@@ -8,6 +8,7 @@
 --  This file is part of Gneiss, which is distributed under the terms of the
 --  GNU Affero General Public License version 3.
 --
+with Gneiss_Internal;
 
 generic
    pragma Warnings (Off, "* is not referenced");
@@ -33,7 +34,8 @@ is
    procedure Initialize (Session : in out Client_Session;
                          Cap     :        Gneiss.Capability;
                          Label   :        String;
-                         Idx     :        Session_Index := 1);
+                         Idx     :        Session_Index := 1) with
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Update the rom and call Read
    --
@@ -42,15 +44,17 @@ is
       with function Contract (Ctx : Context) return Boolean;
    procedure Update (Session : in out Client_Session;
                      Ctx     : in out Context) with
-      Pre  => Initialized (Session)
-              and then Contract (Ctx),
-      Post => Initialized (Session)
-              and then Contract (Ctx);
+      Pre    => Initialized (Session)
+                and then Contract (Ctx),
+      Post   => Initialized (Session)
+                and then Contract (Ctx),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Close the session
    --
    --  @param Session  Client session
    procedure Finalize (Session : in out Client_Session) with
-      Post => not Initialized (Session);
+      Post   => not Initialized (Session),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
 end Gneiss.Rom.Client;
diff --git a/src/rom/client/linux/gneiss-rom-client.adb b/src/rom/client/linux/gneiss-rom-client.adb
@@ -1,6 +1,5 @@
 
 with System;
-with Gneiss_Internal;
 with Gneiss_Internal.Syscall;
 with Gneiss_Internal.Client;
 with Gneiss_Protocol.Session;
@@ -9,6 +8,25 @@ package body Gneiss.Rom.Client with
    SPARK_Mode
 is
 
+   function Get_First (Length : Integer) return Buffer_Index;
+   function Get_Last (Length : Integer) return Buffer_Index;
+
+   function Get_First (Length : Integer) return Buffer_Index is
+      (if Length < 1 then Buffer_Index'First + 1 else Buffer_Index'First);
+
+   function Get_Last (Length : Integer) return Buffer_Index
+   is
+   begin
+      if Length < 1 then
+         return Buffer_Index'First;
+      end if;
+      if Long_Integer (Length) < Long_Integer (Buffer_Index'Last - Buffer_Index'First + 1) then
+         return Buffer_Index (Long_Integer (Buffer_Index'First) + Long_Integer (Length) - 1);
+      else
+         return Buffer_Index'Last;
+      end if;
+   end Get_Last;
+
    procedure Initialize (Session : in out Client_Session;
                          Cap     :        Gneiss.Capability;
                          Label   :        String;
@@ -18,7 +36,7 @@ is
       use type Gneiss_Internal.File_Descriptor;
       Fds : Gneiss_Internal.Fd_Array (1 .. 1) := (others => -1);
    begin
-      if Initialized (Session) then
+      if Initialized (Session) or else Label'Length > 255 then
          return;
       end if;
       Gneiss_Internal.Client.Initialize (Cap.Broker_Fd, Gneiss_Protocol.Session.Rom, Fds, Label);
@@ -39,10 +57,10 @@ is
    procedure Update (Session : in out Client_Session;
                      Ctx     : in out Context)
    is
-      Size  : constant Integer      := Gneiss_Internal.Syscall.Stat_Size (Session.Fd);
-      First : constant Buffer_Index := Buffer_Index'First;
-      Last  : constant Buffer_Index := Buffer_Index (Long_Integer (First) + Long_Integer (Size - 1));
-      Buf   : Buffer (First .. Last) with
+      Length : constant Integer      := Gneiss_Internal.Syscall.Stat_Size (Session.Fd);
+      Last   : constant Buffer_Index := Get_Last (Length);
+      First  : constant Buffer_Index := Get_First (Length);
+      Buf    : Buffer (First .. Last) with
          Import,
          Address => Session.Map;
    begin

diff --git a/test/rom/component.adb b/test/rom/component.adb
@@ -5,7 +5,9 @@ with Gneiss.Log;
 with Gneiss.Log.Client;
 
 package body Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Refined_State => (Component_State => C,
+                     Platform_State  => (Log, Config))
 is
 
    package Gneiss_Log is new Gneiss.Log;
@@ -19,8 +21,11 @@ is
    procedure Read (Session : in out Rom.Client_Session;
                    Data    :        String;
                    Ctx     : in out Gneiss_Log.Client_Session) with
-      Pre  => Gneiss_Log.Initialized (Ctx),
-      Post => Gneiss_Log.Initialized (Ctx);
+      Pre    => Rom.Initialized (Session)
+                and then Gneiss_Log.Initialized (Ctx),
+      Post   => Rom.Initialized (Session)
+                and then Gneiss_Log.Initialized (Ctx),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    package Rom_Client is new Rom.Client (Gneiss_Log.Client_Session, Read);
    procedure Update is new Rom_Client.Update (Gneiss_Log.Initialized);

diff --git a/test/rom/component.ads b/test/rom/component.ads
@@ -1,13 +1,23 @@
 
 with Gneiss;
 with Gneiss.Component;
+with Gneiss_Internal;
 
 package Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Abstract_State => (Component_State, Platform_State),
+   Initializes    => (Main.Platform, Platform_State)
 is
 
-   procedure Construct (Capability : Gneiss.Capability);
-   procedure Destruct;
+   procedure Construct (Capability : Gneiss.Capability) with
+      Global => (Output => Component_State,
+                 In_Out => (Platform_State,
+                            Main.Platform,
+                            Gneiss_Internal.Platform_State));
+
+   procedure Destruct with
+      Global => (In_Out => (Platform_State,
+                            Gneiss_Internal.Platform_State));
 
    package Main is new Gneiss.Component (Construct, Destruct);