Skip to content
This repository has been archived by the owner on May 22, 2023. It is now read-only.

Commit

Permalink
Unify duplicated helper functions
Browse files Browse the repository at this point in the history
ref #173
  • Loading branch information
jklmnn committed May 19, 2020
1 parent 21e035b commit 9918912
Show file tree
Hide file tree
Showing 5 changed files with 45 additions and 54 deletions.
21 changes: 3 additions & 18 deletions src/memory/client/linux/gneiss-memory-client.adb
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
with System;
with Gneiss_Internal.Syscall;
with Gneiss_Internal.Client;
with Gneiss_Internal.Util;
with Gneiss_Protocol.Session;

package body Gneiss.Memory.Client with
Expand All @@ -16,24 +17,8 @@ is
External_Name => "gneiss_memfd_create",
Global => (In_Out => Gneiss_Internal.Platform_State);

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;
function Get_First is new Gneiss_Internal.Util.Get_First (Buffer_Index);
function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);

procedure Initialize (Session : in out Client_Session;
Cap : Capability;
Expand Down
21 changes: 3 additions & 18 deletions src/memory/server/linux/gneiss-memory-server.adb
Original file line number Diff line number Diff line change
@@ -1,28 +1,13 @@

with Gneiss_Internal.Syscall;
with Gneiss_Internal.Util;

package body Gneiss.Memory.Server 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;
function Get_First is new Gneiss_Internal.Util.Get_First (Buffer_Index);
function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);

procedure Modify (Session : in out Server_Session;
Ctx : in out Context)
Expand Down
22 changes: 22 additions & 0 deletions src/platform/linux/gneiss_internal-util.adb
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@

package body Gneiss_Internal.Util with
SPARK_Mode
is

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;

end Gneiss_Internal.Util;
14 changes: 14 additions & 0 deletions src/platform/linux/gneiss_internal-util.ads
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@

package Gneiss_Internal.Util with
SPARK_Mode
is

generic
type Buffer_Index is range <>;
function Get_First (Length : Integer) return Buffer_Index;

generic
type Buffer_Index is range <>;
function Get_Last (Length : Integer) return Buffer_Index;

end Gneiss_Internal.Util;
21 changes: 3 additions & 18 deletions src/rom/client/linux/gneiss-rom-client.adb
Original file line number Diff line number Diff line change
Expand Up @@ -2,30 +2,15 @@
with System;
with Gneiss_Internal.Syscall;
with Gneiss_Internal.Client;
with Gneiss_Internal.Util;
with Gneiss_Protocol.Session;

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;
function Get_First is new Gneiss_Internal.Util.Get_First (Buffer_Index);
function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);

procedure Initialize (Session : in out Client_Session;
Cap : Gneiss.Capability;
Expand Down

0 comments on commit 9918912

Please sign in to comment.