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

Commit

Permalink
prove broker with only low checks missing
Browse files Browse the repository at this point in the history 
ref #161
  • Loading branch information
@jklmnn
jklmnn committed Apr 24, 2020
1 parent 1e81735 commit 1867325
Show file tree
Hide file tree
Showing 11 changed files with 199 additions and 80 deletions.
4 changes: 4 additions & 0 deletions init/gneiss-broker-lookup.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,9 @@ is
pragma Loop_Invariant (SXML.Query.Is_Valid (Query_State, Document));
pragma Loop_Invariant (SXML.Query.Is_Open (Query_State, Document)
or else SXML.Query.Is_Content (Query_State, Document));
pragma Loop_Invariant (Default_State = SXML.Query.Invalid_State
or else (SXML.Query.State_Result (Default_State) = SXML.Result_OK
and then SXML.Query.Is_Valid (Default_State, Document)));
Query_State := SXML.Query.Find_Sibling (Query_State, Document, "service", "name", Kind);
exit when SXML.Query.State_Result (Query_State) /= SXML.Result_OK;
SXML.Query.Attribute (Query_State, Document, "label", Result, Buffer, Last);
Expand Down Expand Up @@ -50,6 +53,7 @@ is
return;
end if;
for I in State.Components'Range loop
pragma Loop_Invariant (not Valid);
if State.Components (I).Fd > -1 then
SXML.Query.Attribute (State.Components (I).Node, State.Xml, "name", Result, XML_Buf, Last);
Valid := Result = SXML.Result_OK and then Compare (XML_Buf, Last, Name);
Expand Down
7 changes: 7 additions & 0 deletions init/gneiss-broker-lookup.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ with Gneiss_Protocol.Session;
package Gneiss.Broker.Lookup with
SPARK_Mode
is
use type SXML.Query.State_Type;

procedure Match_Service (Document : SXML.Document_Type;
Comp : SXML.Query.State_Type;
Expand All @@ -14,6 +15,9 @@ is
Dest : out SXML.Query.State_Type) with
Pre => SXML.Query.Is_Valid (Comp, Document)
and then SXML.Query.State_Result (Comp) = SXML.Result_OK,
Post => Dest = SXML.Query.Invalid_State
or else (SXML.Query.State_Result (Dest) = SXML.Result_OK
and then SXML.Query.Is_Valid (Dest, Document)),
Global => null;

procedure Lookup_Request (State : Broker_State;
Expand All @@ -32,6 +36,8 @@ is
Index : out Positive;
Valid : out Boolean) with
Pre => Is_Valid (State.Xml, State.Components),
Post => (if Valid then (Index in State.Components'Range
and then State.Components (Index).Fd > -1)),
Global => null;

procedure Find_Resource_By_Name (State : Broker_State;
Expand All @@ -52,6 +58,7 @@ is
and then SXML.Query.Is_Open (Serv, State.Xml)
and then Location'Length > 0
and then Location'Last <= Natural'Last - SXML.Chunk_Length,
Post => (if Valid then Last in Location'Range),
Global => null;

private
Expand Down
9 changes: 7 additions & 2 deletions init/gneiss-broker-main.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is
Status := 1;
return;
end if;
State.Resources := (others => (Fd => -1,
Node => SXML.Query.Invalid_State));
Startup.Parse_Resources (State.Resources, State.Xml, Query);
State.Components := (others => (Fd => -1,
Node => SXML.Query.Initial_State,
Expand All @@ -80,12 +82,13 @@ is
Status := 1;
loop
pragma Loop_Invariant (Is_Valid (B_State.Xml, B_State.Components));
pragma Loop_Invariant (Is_Valid (B_State.Xml, B_State.Resources));
pragma Loop_Invariant (Gneiss_Epoll.Valid_Fd (B_State.Epoll_Fd));
Gneiss_Epoll.Wait (B_State.Epoll_Fd, Ev, Fd);
Index := Get_Dest (B_State, Fd);
if Index in B_State.Components'Range and then B_State.Components (Index).Fd > -1 then
SXML.Query.Attribute (B_State.Components (Index).Node, B_State.Xml, "name", Result, XML_Buf, Last);
if Ev.Epoll_In then
if Ev.Epoll_In and then Fd > -1 then
Message.Read_Message (B_State, Index, Fd);
end if;
if Ev.Epoll_Hup or else Ev.Epoll_Rdhup then
Expand All @@ -101,7 +104,9 @@ is
& " exited with status "
& Basalt.Strings.Image (Success));
end if;
Gneiss_Epoll.Remove (B_State.Epoll_Fd, B_State.Components (Index).Fd, Success);
if B_State.Components (Index).Fd > -1 then
Gneiss_Epoll.Remove (B_State.Epoll_Fd, B_State.Components (Index).Fd, Success);
end if;
Gneiss_Syscall.Close (B_State.Components (Index).Fd);
B_State.Components (Index).Node := SXML.Query.Init (B_State.Xml);
B_State.Components (Index).Pid := -1;
Expand Down
3 changes: 2 additions & 1 deletion init/gneiss-broker-main.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ private
procedure Event_Loop (B_State : in out Broker_State;
Status : out Return_Code) with
Pre => Gneiss_Epoll.Valid_Fd (B_State.Epoll_Fd)
and then Is_Valid (B_State.Xml, B_State.Components);
and then Is_Valid (B_State.Xml, B_State.Components)
and then Is_Valid (B_State.Xml, B_State.Resources);

end Gneiss.Broker.Main;
135 changes: 87 additions & 48 deletions init/gneiss-broker-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,41 +16,45 @@ is
when Gneiss_Protocol.Session.Rom => "Rom",
when Gneiss_Protocol.Session.Timer => "Timer");

procedure Setup_Service (State : in out Broker_State;
procedure Setup_Service (State : in out Service_List;
Kind : Gneiss_Protocol.Session.Kind_Type;
Index : Positive);
Efd : Gneiss_Epoll.Epoll_Fd;
Valid : out Boolean) with
Pre => Gneiss_Epoll.Valid_Fd (Efd),
Post => (if Valid then (State (Kind).Broker > -1 and then State (Kind).Disp > -1));

procedure Setup_Service (State : in out Broker_State;
procedure Setup_Service (State : in out Service_List;
Kind : Gneiss_Protocol.Session.Kind_Type;
Index : Positive)
Efd : Gneiss_Epoll.Epoll_Fd;
Valid : out Boolean)
is
Ignore_Success : Integer;
Success : Integer;
begin
if
State.Components (Index).Serv (Kind).Broker > -1
and then State.Components (Index).Serv (Kind).Disp > -1
then
Valid := False;
if State (Kind).Broker > -1 and then State (Kind).Disp > -1 then
Valid := True;
return;
end if;
Gneiss_Syscall.Socketpair (State.Components (Index).Serv (Kind).Broker,
State.Components (Index).Serv (Kind).Disp);
if
State.Components (Index).Serv (Kind).Broker < 0
or else State.Components (Index).Serv (Kind).Disp < 0
then
Gneiss_Syscall.Socketpair (State (Kind).Broker, State (Kind).Disp);
if State (Kind).Broker < 0 or else State (Kind).Disp < 0 then
Gneiss_Log.Error ("Failed to create service fds");
Gneiss_Syscall.Close (State.Components (Index).Serv (Kind).Broker);
Gneiss_Syscall.Close (State.Components (Index).Serv (Kind).Disp);
Gneiss_Syscall.Close (State (Kind).Broker);
Gneiss_Syscall.Close (State (Kind).Disp);
return;
end if;
Gneiss_Epoll.Add (Efd, State (Kind).Broker, State (Kind).Broker, Success);
if Success /= 0 then
Gneiss_Log.Error ("Failed to register broker callback");
Gneiss_Syscall.Close (State (Kind).Broker);
Gneiss_Syscall.Close (State (Kind).Disp);
return;
end if;
Gneiss_Epoll.Add (State.Epoll_Fd, State.Components (Index).Serv (Kind).Broker,
State.Components (Index).Serv (Kind).Broker, Ignore_Success);
Valid := True;
end Setup_Service;

function Convert_Message (S : String) return Gneiss_Protocol_String
is
use type Gneiss_Protocol.Session.Length_Type;
R : Gneiss_Protocol_String (1 .. Gneiss_Protocol.Session.Length_Type (S'Length));
R : Gneiss_Protocol_String (1 .. RFLX.Session.Length_Type (S'Length));
begin
for I in R'Range loop
R (I) := S (S'First + Natural (I - R'First));
Expand Down Expand Up @@ -129,14 +133,14 @@ is
Source_Name : String (1 .. 255);
Last : Natural;
Result : SXML.Result_Type;
Fds_Out : Gneiss_Syscall.Fd_Array (1 .. 4) := (others => -1);
Fds_Out : Gneiss_Syscall.Fd_Array (1 .. 4);
begin
if State.Components (Source).Fd < 0 then
Gneiss_Log.Warning ("Cannot process invalid source");
return;
end if;
Lookup.Match_Service (State.Xml, State.Components (Source).Node, Image (Kind), Label, Serv_State);
if Serv_State = SXML.Query.Invalid_State then
if Serv_State = SXML.Query.Invalid_State or else not SXML.Query.Is_Open (Serv_State, State.Xml) then
Gneiss_Log.Error ("No service found");
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
Expand All @@ -155,17 +159,28 @@ is
end if;
case Kind is
when Gneiss_Protocol.Session.Message | Gneiss_Protocol.Session.Log =>
if Destination not in State.Components'Range then
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
end if;
Process_Message_Request (Fds_Out, Valid);
if Valid and then Destination in State.Components'Range then
Setup_Service (State, Kind, Destination);
Send_Request (State.Components (Destination).Serv (Kind).Broker,
Kind,
Source_Name (Source_Name'First .. Last),
Label,
Fds_Out (Fds_Out'First .. Fds_Out'First + 1));
else
if not Valid then
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
end if;
Setup_Service (State.Components (Destination).Serv, Kind, State.Epoll_Fd, Valid);
if not Valid then
for Fd of Fds_Out loop
Gneiss_Syscall.Close (Fd);
end loop;
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
end if;
Send_Request (State.Components (Destination).Serv (Kind).Broker,
Kind,
Source_Name (Source_Name'First .. Last),
Label,
Fds_Out (Fds_Out'First .. Fds_Out'First + 1));
when Gneiss_Protocol.Session.Rom =>
if Destination in State.Components'Range then
Gneiss_Log.Warning ("Rom server currently not supported");
Expand All @@ -178,17 +193,28 @@ is
end if;
end if;
when Gneiss_Protocol.Session.Memory =>
if Destination not in State.Components'Range or else Fds'Length < 1 then
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
end if;
Process_Memory_Request (Fds, Fds_Out, Valid);
if Valid and then Destination in State.Components'Range then
Setup_Service (State, Kind, Destination);
Send_Request (State.Components (Destination).Serv (Kind).Broker,
Kind,
Source_Name (Source_Name'First .. Last),
Label,
Fds_Out (Fds_Out'First .. Fds_Out'First + 2));
else
if not Valid then
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
end if;
Setup_Service (State.Components (Destination).Serv, Kind, State.Epoll_Fd, Valid);
if not Valid then
for Fd of Fds_Out loop
Gneiss_Syscall.Close (Fd);
end loop;
Send_Reject (State.Components (Source).Fd, Kind, Label);
return;
end if;
Send_Request (State.Components (Destination).Serv (Kind).Broker,
Kind,
Source_Name (Source_Name'First .. Last),
Label,
Fds_Out (Fds_Out'First .. Fds_Out'First + 2));
when Gneiss_Protocol.Session.Timer =>
Process_Timer_Request (Fds_Out, Valid);
if Valid then
Expand All @@ -202,21 +228,26 @@ is
procedure Process_Message_Request (Fds : out Gneiss_Syscall.Fd_Array;
Valid : out Boolean)
is
Fd1 : Integer;
Fd2 : Integer;
begin
Fds := (others => -1);
Gneiss_Syscall.Socketpair (Fds (Fds'First), Fds (Fds'First + 1));
Valid := Fds (Fds'First) > -1 and then Fds (Fds'First + 1) > -1;
Gneiss_Syscall.Socketpair (Fd1, Fd2);
Valid := Fd1 > -1 and then Fd2 > -1;
if not Valid then
Gneiss_Syscall.Close (Fds (Fds'First));
Gneiss_Syscall.Close (Fds (Fds'First + 1));
Gneiss_Syscall.Close (Fd1);
Gneiss_Syscall.Close (Fd2);
end if;
Fds (Fds'First .. Fds'First + 1) := (Fd1, Fd2);
end Process_Message_Request;

procedure Process_Memory_Request (Fds_In : Gneiss_Syscall.Fd_Array;
Fds_Out : out Gneiss_Syscall.Fd_Array;
Valid : out Boolean)
is
Success : Integer;
Fd1 : Integer;
Fd2 : Integer;
begin
Valid := False;
Fds_Out := (others => -1);
Expand All @@ -229,7 +260,8 @@ is
Gneiss_Syscall.Close (Fds_Out (Fds_Out'First + 2));
return;
end if;
Gneiss_Syscall.Socketpair (Fds_Out (Fds_Out'First), Fds_Out (Fds_Out'First + 1));
Gneiss_Syscall.Socketpair (Fd1, Fd2);
Fds_Out (Fds_Out'First .. Fds_Out'First + 1) := (Fd1, Fd2);
Valid := Fds_Out (Fds_Out'First) > -1 and then Fds_Out (Fds_Out'First + 1) > -1;
if not Valid then
Gneiss_Syscall.Close (Fds_Out (Fds_Out'First));
Expand Down Expand Up @@ -258,6 +290,7 @@ is
Valid : out Boolean)
is
begin
Fds := (others => -1);
Gneiss_Syscall.Timerfd_Create (Fds (Fds'First));
Valid := Fds (Fds'First) > -1;
end Process_Timer_Request;
Expand All @@ -275,7 +308,7 @@ is
if Valid then
case Kind is
when Gneiss_Protocol.Session.Message | Gneiss_Protocol.Session.Log | Gneiss_Protocol.Session.Memory =>
if Fds (Fds'First) >= 0 then
if Fds'Length > 0 and then Fds (Fds'First) >= 0 then
Send_Confirm (State.Components (Destination).Fd, Kind, Label, Fds (Fds'First .. Fds'First));
else
Gneiss_Log.Warning ("Invalid Fd, rejecting");
Expand Down Expand Up @@ -309,11 +342,17 @@ is
Source : Positive;
Kind : Gneiss_Protocol.Session.Kind_Type)
is
Fds : Gneiss_Syscall.Fd_Array (1 .. 1);
Fds : Gneiss_Syscall.Fd_Array (1 .. 1);
Valid : Boolean;
begin
Setup_Service (State, Kind, Source);
pragma Assert (if State.Components (Source).Fd > -1
then SXML.Query.State_Result (State.Components (Source).Node) = SXML.Result_OK
and then SXML.Query.Is_Valid (State.Components (Source).Node, State.Xml)
and then SXML.Query.Is_Open (State.Components (Source).Node, State.Xml));
Setup_Service (State.Components (Source).Serv, Kind, State.Epoll_Fd, Valid);
pragma Assert (Is_Valid (State.Xml, State.Components));
Fds := (1 => State.Components (Source).Serv (Kind).Disp);
if Fds (Fds'First) > -1 then
if Valid then
Send_Confirm (State.Components (Source).Fd, Kind, "", Fds);
else
Send_Reject (State.Components (Source).Fd, Kind, "");
Expand Down
Loading

0 comments on commit 1867325

Please sign in to comment.