Add DCCP example

Ref. eng/recordflux/RecordFlux#1362

examples/apps/dccp/.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "ada.projectFile": "build.gpr"
+}

examples/apps/dccp/Makefile

@@ -0,0 +1,11 @@
+.PHONY: test build prove generate clean
+
+test:
+
+build:
+
+prove:
+
+generate:
+
+clean:

examples/apps/dccp/README.md

@@ -0,0 +1,68 @@
+# DCCP
+
+## Getting started
+
+This project provides a simplified example set for a DCCP specification with a "client" and "server" application. Additional details about what each application does are described below.
+
+## DCCP Server
+
+This application acts as the "server," listening on a specific local port for messages in the DCCP format. It is able to receive a specific set of messages based on a small Wireshark sample data set. These messages include:
+
+- DCCP Request
+- DCCP Response
+- DCCP Ack
+- DCCP DataAck
+- DCCP Data
+- DCCP Close
+- DCCP Reset
+
+If one of the above messages is received in the expected format, the message information will be printed to the console window.
+
+This application constantly "listens" for a message and will provide no further indication of operation until a message is received.
+
+## DCCP Client
+
+This application acts as the "client," sending a specific set of DCCP messages to a local port. This specific set of messages was pulled from a Wireshark DCCP sample set ([Link to archive](https://wiki.wireshark.org/uploads/__moin_import__/attachments/SampleCaptures/dccp_trace.pcap.gz)).
+
+For simplicity, and to demonstrate how to write to/access message fields, these messages are hard-coded within the DCCP Client application.
+
+## Using the Applications
+
+The basic setup for these applications is simple. After compiling the code into an executable format:
+
+1. Run the DCCP Server
+2. Run the DCCP Client
+
+Once the client is running and prints out message status information, the server should start receiving the same respective information and print the results to the console. 
+
+## DCCP Specification
+
+RecordFlux was used to generate the "DCCP specification" for this project. Note that the DCCP protocol was **NOT** implemented in its entirety. The core of the protocol is the **Generic Header**; a fairly simple implementation of this is implemented in RecordFlux. A small portion of **Additional Fields** and **Options** are also implemented so as to align with the Wireshark sample data set. Additionally, the **Application Data Area** of the protocol is lightly implemented here based on Wireshark data.
+
+The DCCP Specification file is located in the **\specs** folder of each application.
+
+The message graph (generated from the specification file) is located in the **\out** folder of each application. This provides a visual graph of the message itself, which can be useful for understanding and/or message interpretation.
+
+## HOWTO: Generate a Message Graph
+
+To generate a message graph using RecordFlux, locate the message spec and enter the following into the terminal window:
+
+`rflx graph -d ./out dccp.rflx`
+
+For the above, **out** is the output directory for the graph and **dccp.rflx** is the spec file.
+
+## HOWTO: Generate Code Files from a Specification
+
+To generate code files for the RecordFlux specification, locate the message spec and enter the following into the terminal window:
+
+`rflx generate -d ./generated/ dccp.rflx`
+
+For the above, **generated** is the output directory for the generated code files and **dccp.rflx** is the spec file.
+
+## HOWTO: Validate the Specification
+
+RecordFlux provides the ability to validate a message specification with real world files in a RAW format. To run validate and generate a corresponding report, locate the message spec and enter the following into the terminal window:
+
+`rflx validate --coverage -v ./test/valid/ dccp.rflx DCCP::Header`
+
+For the above, **./test/valid** is the folder in which "valid" sample RAW files are located and **dccp.rflx** is the spec file.

examples/apps/dccp/build.gpr

@@ -0,0 +1,28 @@
+aggregate project Build is
+
+    for Project_Files use ("dccp_client/dccp_client.gpr", "dccp_server/dccp_server.gpr");
+    for Create_Missing_Dirs use "True";
+
+   Proof_Switches :=
+   (
+      "--prover=z3,cvc5,altergo,colibri",
+      "--steps=0",
+      "--timeout=300",
+      "--memlimit=5000",
+      "--checks-as-errors",
+      "--warnings=error",
+      "--function-sandboxing=off",
+      "--counterexamples=off",
+      "--output=oneline",
+      "-j0"
+   );
+
+   package Prove is
+      for Proof_Switches ("Ada") use Proof_Switches;
+   end Prove;
+
+   package Builder is
+      for Global_Configuration_Pragmas use "common.adc";
+   end Builder;
+
+end Build;

examples/apps/dccp/common.adc

@@ -0,0 +1 @@
+pragma SPARK_Mode (On);

examples/apps/dccp/common/socket.adb

@@ -0,0 +1,94 @@
+with Ada.Streams;
+
+package body Socket with
+  SPARK_Mode => Off
+is
+   function Is_Open (Chan : Channel) return Boolean is (Chan.Is_Open);
+
+   function Initialize
+     (Port : Natural; Server : Boolean := False) return Channel
+   is
+      Socket : GNAT.Sockets.Socket_Type;
+   begin
+      GNAT.Sockets.Create_Socket
+        (Socket => Socket, Mode => GNAT.Sockets.Socket_Datagram);
+
+      GNAT.Sockets.Set_Socket_Option
+        (Socket => Socket, Level => GNAT.Sockets.IP_Protocol_For_IP_Level,
+         Option => (GNAT.Sockets.Reuse_Address, True));
+
+      if Server then
+         GNAT.Sockets.Bind_Socket
+           (Socket  => Socket,
+            Address =>
+              (Family => GNAT.Sockets.Family_Inet,
+               Addr   => GNAT.Sockets.Inet_Addr ("127.0.0.1"),
+               Port   => GNAT.Sockets.Port_Type (Port)));
+      end if;
+
+      return
+        Channel'
+          (Socket  => Socket, Port => GNAT.Sockets.Port_Type (Port),
+           Is_Open => True);
+   end Initialize;
+
+   procedure Receive
+     (Chan :     Channel; Data : out RFLX.RFLX_Types.Bytes;
+      Last : out RFLX.RFLX_Types.Index; Success : out Boolean)
+   is
+      Recv_Data : Ada.Streams.Stream_Element_Array (1 .. 4_096);
+      Recv_Last : Ada.Streams.Stream_Element_Offset;
+      From      : GNAT.Sockets.Sock_Addr_Type;
+      use type Ada.Streams.Stream_Element_Offset;
+   begin
+      Success := False;
+
+      GNAT.Sockets.Receive_Socket
+        (Socket => Chan.Socket, Item => Recv_Data, Last => Recv_Last,
+         From   => From);
+
+      for I in Recv_Data'First .. Recv_Last loop
+         declare
+            J : constant RFLX.RFLX_Types.Index :=
+              Data'First + RFLX.RFLX_Types.Index (I) -
+              RFLX.RFLX_Types.Index (Recv_Data'First);
+         begin
+            if J not in Data'Range then
+               return;
+            end if;
+            Data (J) := RFLX.RFLX_Types.Byte (Recv_Data (I));
+         end;
+      end loop;
+
+      Last := Data'First + RFLX.RFLX_Types.Index (Recv_Last - Recv_Data'First);
+      Success := True;
+   end Receive;
+
+   procedure Close (Chan : in out Channel) is
+   begin
+      GNAT.Sockets.Close_Socket (Chan.Socket);
+      Chan.Is_Open := False;
+   end Close;
+
+   procedure Send (Chan : Channel; Data : RFLX.RFLX_Types.Bytes) is
+      Last      : Ada.Streams.Stream_Element_Offset;
+      Address   : GNAT.Sockets.Sock_Addr_Type;
+      Send_Data : Ada.Streams.Stream_Element_Array (1 .. Data'Length);
+      use type Ada.Streams.Stream_Element_Offset;
+   begin
+
+      for I in Data'Range loop
+         Send_Data
+           (Send_Data'First +
+            Ada.Streams.Stream_Element_Offset (I - Data'First)) :=
+           Ada.Streams.Stream_Element (Data (I));
+      end loop;
+
+      Address.Port := Chan.Port;
+      Address.Addr := GNAT.Sockets.Inet_Addr ("127.0.0.1");
+
+      GNAT.Sockets.Send_Socket
+        (Socket => Chan.Socket, Item => Send_Data, Last => Last,
+         To     => Address);
+   end Send;
+end Socket;

examples/apps/dccp/common/socket.ads

@@ -0,0 +1,40 @@
+with RFLX.RFLX_Types;
+private with GNAT.Sockets;
+
+package Socket with
+  SPARK_Mode
+is
+   type Channel is private with
+     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
+   use type RFLX.RFLX_Types.Index;
+
+   function Is_Open (Chan : Channel) return Boolean with
+     Ghost, Annotate => (GNATprove, Ownership, "Needs_Reclamation");
+
+   function Initialize
+     (Port : Natural; Server : Boolean := False) return Channel with
+     Post => Is_Open (Initialize'Result);
+
+   procedure Receive
+     (Chan :     Channel; Data : out RFLX.RFLX_Types.Bytes;
+      Last : out RFLX.RFLX_Types.Index; Success : out Boolean) with
+     Pre => Is_Open (Chan), Post => Data'First <= Last and Last <= Data'Last;
+
+   procedure Send (Chan : Channel; Data : RFLX.RFLX_Types.Bytes) with
+     Pre => Is_Open (Chan);
+
+   procedure Close (Chan : in out Channel) with
+     Pre     => Is_Open (Chan), Post => not Is_Open (Chan),
+     Depends => (Chan => null, null => Chan);
+
+private
+
+   pragma SPARK_Mode (Off);
+
+   type Channel is record
+      Socket  : GNAT.Sockets.Socket_Type;
+      Port    : GNAT.Sockets.Port_Type;
+      Is_Open : Boolean;
+   end record;
+
+end Socket;

examples/apps/dccp/dccp_client/.gitignore

@@ -0,0 +1 @@
+**/obj/**

examples/apps/dccp/dccp_client/dccp_client.gpr

@@ -0,0 +1,25 @@
+with "../defaults";
+
+project DCCP_Client is
+
+   for Languages use ("RecordFlux", "Ada");
+   for Source_Dirs use ("src", "../rflx/generated", "../rflx/specs", "../common");
+   for Object_Dir use "obj";
+   for Create_Missing_Dirs use "True";
+   for Main use ("dccp_client.adb");
+
+   package Compiler is
+      for Driver ("recordflux") use "";
+      for Default_Switches("Ada") use Defaults.Compiler_Switches;
+   end Compiler;
+
+   package Naming is
+      for Spec_Suffix ("recordflux") use ".rflx";
+   end Naming;
+
+   package Recordflux is
+      for Output_Dir use "../rflx/generated";
+   end Recordflux;
+
+end DCCP_Client;
+

examples/apps/dccp/dccp_client/src/dccp_client.adb

@@ -0,0 +1,18 @@
+with Socket;
+with Msg_Write;
+
+procedure DCCP_Client with
+  SPARK_Mode => On
+is
+   Channel : Socket.Channel := Socket.Initialize (1234);
+begin
+   Msg_Write.Send_Request (Channel);
+   Msg_Write.Send_Response (Channel);
+   Msg_Write.Send_Ack (Channel);
+   Msg_Write.Send_Data_Ack (Channel);
+   Msg_Write.Send_Data (Channel);
+   Msg_Write.Send_Close (Channel);
+   Msg_Write.Send_Reset (Channel);
+
+   Socket.Close (Channel);
+end DCCP_Client;