Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Issue 10: Prove ping component (w/o globals) #13

Merged
merged 2 commits into from
Jun 23, 2020
Merged

Issue 10: Prove ping component (w/o globals) #13

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fb4f99a
Prove ping component (w/o globals)
jklmnn Jun 15, 2020
1b55353
Prove buffer length
jklmnn Jun 19, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 37 additions & 19 deletions components/common/ping/ping-component.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,15 +88,13 @@ is
Identifier : ICMP.Identifier;
Sequence_Number : ICMP.Sequence_Number;
Length : Natural;
Latency : Duration;
procedure Process_Data (Buffer : Types.Bytes);
procedure Process_Data (Buffer : Types.Bytes)
is
begin
Packet_Checksum := Checksum.Echo_Request_Reply_Checksum (ICMP.Echo_Reply,
0,
Identifier,
Sequence_Number,
Buffer);
Packet_Checksum := Checksum.Echo_Request_Reply_Checksum
(ICMP.Echo_Reply, 0, Identifier, Sequence_Number, Buffer);
end Process_Data;
procedure Generate_Checksum is new Echo.Get_Data (Process_Data);
begin
Expand All @@ -106,16 +104,28 @@ is
or else not Packet.Initialized (Client)
or else ICMP_Buf.Ptr = null
or else ICMP_Buf.Ptr'Length /= Buffer_Size
or else ICMP_Buf.Ptr'First /= 1
then
return;
end if;
Received := Timer_Client.Clock (Trigger);
if
Received > Sent_Time
and Then (if Sent_Time < 0.0 then Received < Gneiss_Timer.Time'Last + Sent_Time)
then
Latency := Duration (Received - Sent_Time);
else
Latency := 0.0;
end if;
Timer_Client.Set_Timeout (Trigger, 1.0);
Packet_Client.Receive (Client, ICMP_Buf.Ptr.all, Length);
if Length > ICMP_Buf.Ptr'Length then
Log_Client.Warning (Log, "Receive truncated packet.");
Length := ICMP_Buf.Ptr'Length;
end if;
if Length < 1 then
return;
end if;
Echo.Initialize (Context, ICMP_Buf.Ptr,
RFLX_Types.First_Bit_Index (ICMP_Buf.Ptr'First),
RFLX_Types.Last_Bit_Index (ICMP_Buf.Ptr'First + Types.Length (Length) - 1));
Expand All @@ -127,40 +137,46 @@ is
then
Identifier := Echo.Get_Identifier (Context);
Sequence_Number := Echo.Get_Sequence_Number (Context);
Generate_Checksum (Context);
if Echo.Present (Context, Echo.F_Data) then
Generate_Checksum (Context);
else
Packet_Checksum := Checksum.Echo_Request_Reply_Checksum
(ICMP.Echo_Reply, 0, Identifier, Sequence_Number, (1 .. 0 => 0));
end if;
Log_Client.Info (Log, "seq="
& Image (Sequence_Number)
& " time="
& Basalt.Strings.Image (Duration (Received - Sent_Time))
& Basalt.Strings.Image (Latency)
& " checksum="
& Image (Echo.Get_Checksum (Context), 16)
& " ("
& Image (Packet_Checksum, 16)
& ")");
end if;
pragma Warnings (Off, "unused assignment to ""Context""");
Echo.Take_Buffer (Context, ICMP_Buf.Ptr);
pragma Warnings (On, "unused assignment to ""Context""");
end Event;

procedure Timer_Event
is
use type ICMP.Sequence_Number;
use type Types.Length;
use type Types.Bytes_Ptr;
use type Types.Bit_Length;
Context : Echo.Context;
Packet_Checksum : ICMP.Checksum;
Success : Boolean;
procedure Process_Data (Buffer : out Types.Bytes);
Data : constant Types.Bytes (1 .. 8) := (others => 65);
function Valid_Length (L : Types.Length) return Boolean is
(L = Data'Length);
procedure Process_Data (Buffer : out Types.Bytes) with
Pre => Valid_Length (Buffer'Length);
procedure Process_Data (Buffer : out Types.Bytes)
is
begin
Buffer := (others => 16#65#);
Packet_Checksum := Checksum.Echo_Request_Reply_Checksum (ICMP.Echo_Request,
0,
16#0#,
Seq,
Buffer);
Buffer := Data;
end Process_Data;
procedure Set_Data is new Echo.Set_Bounded_Data (Process_Data);
procedure Set_Data is new Echo.Set_Bounded_Data (Process_Data, Valid_Length);
begin
if
not Gneiss_Timer.Initialized (Trigger)
Expand All @@ -176,12 +192,14 @@ is
Echo.Initialize (Context, ICMP_Buf.Ptr);
Echo.Set_Tag (Context, ICMP.Echo_Request);
Echo.Set_Code_Zero (Context, 0);
Echo.Set_Checksum (Context, 16#0#);
Echo.Set_Checksum (Context, Checksum.Echo_Request_Reply_Checksum
(ICMP.Echo_Request, 0, 16#0#, Seq, Data));
Echo.Set_Identifier (Context, 16#0#);
Echo.Set_Sequence_Number (Context, Seq);
Set_Data (Context, 64);
Echo.Set_Checksum (Context, Packet_Checksum);
Set_Data (Context, Data'Length * Types.Byte'Size);
pragma Warnings (Off, "unused assignment to ""Context""");
Echo.Take_Buffer (Context, ICMP_Buf.Ptr);
pragma Warnings (On, "unused assignment to ""Context""");
Packet_Client.Send (Client, ICMP_Buf.Ptr.all (ICMP_Buf.Ptr'First .. ICMP_Buf.Ptr'First + 15), Success);
if not Success then
Log_Client.Warning (Log, "Failed to send packet.");
Expand Down