Merge pull request #8606 from mgrojo/feature/alire-usability

Ada: preparation for Alire index and fixes detected by GNATprove

wrapper/Ada/README.md

@@ -13,10 +13,11 @@ code to zero-out stack frames used by subprograms.
 Unfortunately this works well for the primary stack but not
 for the secondary stack. The GNAT User's Guide recommends
 avoiding the secondary stack using the restriction
-No_Secondary_Stack (see the GNAT configuration file gnat.adc
+No_Secondary_Stack (see the GNAT configuration file restricted.adc
 which instructs compilation of the WolfSSL Ada binding under
 this restriction). Note, however, that the examples do make use of the
-secondary stack.
+secondary stack and the Alire project does not include this restriction, for
+letting users of the library to define it at their level.
 
 Portability: The WolfSSL Ada binding makes no usage of controlled types
 and has no dependency upon the Ada.Finalization package.
@@ -25,11 +26,11 @@ the restriction No_Finalization. The WolfSSL Ada binding has
 been developed with maximum portability in mind.
 
 Not only can the WolfSSL Ada binding be used in Ada applications but
-also SPARK applications (a subset of the Ada language suitable
+also SPARK applications (a subset of the Ada language suitable for
 formal verification). To formally verify the Ada code in this repository
-open the client.gpr with GNAT Studio and then select
+open the examples.gpr with GNAT Studio and then select
 SPARK -> Prove All Sources and use Proof Level 2. Or when using the command
-line, use `gnatprove -Pclient.gpr --level=4 -j12` (`-j12` is there in
+line, use `gnatprove -Pexamples.gpr --level=4 -j12` (`-j12` is there in
 order to instruct the prover to use 12 CPUs if available).
 
 ```
@@ -83,7 +84,7 @@ and use gprbuild to build the source code.
 cd wrapper/Ada
 gprclean
 gprbuild default.gpr
-gprbuild client.gpr
+gprbuild examples.gpr
 
 cd obj/
 ./tls_server_main &
@@ -93,7 +94,7 @@ cd obj/
 On Windows, build the executables with:
 ```sh
 gprbuild -XOS=Windows default.gpr
-gprbuild -XOS=Windows client.gpr
+gprbuild -XOS=Windows examples.gpr
 ```
 
 ## Files

wrapper/Ada/alire.toml

@@ -9,3 +9,6 @@ licenses = "GPL-2.0-only"
 website = "https://www.wolfssl.com/"
 project-files = ["wolfssl.gpr"]
 tags = ["ssl", "tls", "embedded", "spark"]
+
+[configuration.variables]
+STATIC_PSK = {type = "Boolean", default = false}

wrapper/Ada/default.gpr

@@ -11,21 +11,27 @@ project Default is
                         "../../src",
                         "../../wolfcrypt/src");
 
-   --  Don't build the tls client application because it makes use
+   --  Don't build the tls application examples because they make use
    --  of the Secondary Stack due to usage of the Ada.Command_Line
    --  package. All other Ada source code does not use the secondary stack.
-   for Excluded_Source_Files use ("tls_client_main.adb",
-                                  "tls_client.ads",
-                                  "tls_client.adb");
+   for Excluded_Source_Files use
+     ("tls_client_main.adb",
+      "tls_client.ads",
+      "tls_client.adb",
+      "tls_server_main.adb",
+      "tls_server.ads",
+      "tls_server.adb");
 
    for Object_Dir use "obj";
 
-   for Main use ("tls_server_main.adb");
-
    package Naming is
       for Spec_Suffix ("C") use ".h";
    end Naming;
 
+   package Builder is
+      for Global_Configuration_Pragmas use "restricted.adc";
+   end Builder;
+
    package Compiler is
       for Switches ("C") use
          ("-DWOLFSSL_USER_SETTINGS", --  Use the user_settings.h file.

wrapper/Ada/examples.gpr

@@ -1,4 +1,4 @@
-project Client is
+project Examples is
    type OS_Kind is ("Windows", "Linux_Or_Mac");
 
    OS : OS_Kind := external ("OS", "Linux_Or_Mac");
@@ -12,7 +12,7 @@ project Client is
 
    for Object_Dir use "obj";
 
-   for Main use ("tls_client_main.adb");
+   for Main use ("tls_server_main.adb", "tls_client_main.adb");
 
    package Naming is
       for Spec_Suffix ("C") use ".h";
@@ -75,4 +75,4 @@ project Client is
       for Switches ("Ada") use ("-Es");  --  To include stack traces.
    end Binder;
 
-end Client;
+end Examples;

wrapper/Ada/include.am

@@ -4,7 +4,7 @@
 
 EXTRA_DIST+= wrapper/Ada/README.md
 EXTRA_DIST+= wrapper/Ada/default.gpr
-EXTRA_DIST+= wrapper/Ada/gnat.adc
+EXTRA_DIST+= wrapper/Ada/restricted.adc
 EXTRA_DIST+= wrapper/Ada/ada_binding.c
 EXTRA_DIST+= wrapper/Ada/tls_client_main.adb
 EXTRA_DIST+= wrapper/Ada/tls_client.adb

wrapper/Ada/tls_client.adb

@@ -204,8 +204,8 @@ package body Tls_Client with SPARK_Mode is
       Output : WolfSSL.Write_Result;
 
       Result : WolfSSL.Subprogram_Result;
-      DTLS   : Boolean;
-      PSK    : Boolean;
+      DTLS   : Boolean := False;
+      PSK    : Boolean := False;
    begin
       Result := WolfSSL.Initialize;
       if Result /= Success then

wrapper/Ada/tls_server.adb

@@ -122,10 +122,10 @@ package body Tls_Server with SPARK_Mode is
       Identity_String : constant String := "Client_identity";
       --  Test key in hex is 0x1a2b3c4d, in decimal 439,041,101
       Key_String : constant String :=
-        Character'Val   (26)
-        & Character'Val (43)
-        & Character'Val (60)
-        & Character'Val (77);
+        (Character'Val (26),
+         Character'Val (43),
+         Character'Val (60),
+         Character'Val (77));
       --  These values are aligned with test values in wolfssl/wolfssl/test.h
       --  and wolfssl-examples/psk/server-psk.c for testing interoperability.
 
@@ -139,10 +139,6 @@ package body Tls_Server with SPARK_Mode is
          return 0;
       end if;
 
-      put_line (Interfaces.C.Strings.Value
-        (Item   => Identity,
-         Length => Identity_String'Length) );
-
       Interfaces.C.Strings.Update
         (Item   => Key,
          Offset => 0,
@@ -162,7 +158,7 @@ package body Tls_Server with SPARK_Mode is
       Ch : Character;
 
       Result : WolfSSL.Subprogram_Result;
-      DTLS, PSK : Boolean;
+      DTLS, PSK : Boolean := True;
       Shall_Continue : Boolean := True;
 
       Input  : WolfSSL.Read_Result;
@@ -261,13 +257,15 @@ package body Tls_Server with SPARK_Mode is
       if not PSK then
          --  Require mutual authentication.
          WolfSSL.Set_Verify
-            (Context => Ctx,
+           (Context => Ctx,
             Mode    => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert);
 
          --  Check verify is set correctly (GitHub #7461)
          if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then
-               Put ("Error: Verify does not match requested");
-               New_Line;
+               Put_Line ("Error: Verify does not match requested");
+               SPARK_Sockets.Close_Socket (L);
+               WolfSSL.Free (Context => Ctx);
+               Set (Exit_Status_Failure);
                return;
          end if;
 

wrapper/Ada/wolfssl.gpr

@@ -1,10 +1,8 @@
+with "config/wolfssl_config.gpr";
+
 library project WolfSSL is
 
    for Library_Name use "wolfssl";
-   --  for Library_Version use Project'Library_Name & ".so";
-   type OS_Kind is ("Windows", "Linux_Or_Mac");
-
-   OS : OS_Kind := external ("OS", "Linux_Or_Mac");
 
    for Languages use ("C", "Ada");
 
@@ -15,12 +13,13 @@ library project WolfSSL is
 
    --  Don't build the tls client or server application.
    --  They are not needed in order to build the library.
-   for Excluded_Source_Files use ("tls_client_main.adb",
-                                  "tls_client.ads",
-                                  "tls_client.adb",
-				  "tls_server_main.adb",
-				  "tls_server.ads",
-				  "tls_server.adb");
+   for Excluded_Source_Files use
+      ("tls_client_main.adb",
+      "tls_client.ads",
+      "tls_client.adb",
+      "tls_server_main.adb",
+      "tls_server.ads",
+      "tls_server.adb");
 
    for Object_Dir use "obj";
    for Library_Dir use "lib";
@@ -34,12 +33,19 @@ library project WolfSSL is
       for Spec_Suffix ("C") use ".h";
    end Naming;
 
-   package Builder is
-      for Global_Configuration_Pragmas use "gnat.adc";
-   end Builder;
+   C_Compiler_Config := ();
+
+   case Wolfssl_Config.STATIC_PSK is
+   when "True" => 
+      C_Compiler_Config := 
+         ("-DWOLFSSL_STATIC_PSK" -- Enable the static PSK cipher support
+         );
+   when others =>
+      C_Compiler_Config := ();
+   end case;
 
    package Compiler is
-      for Switches ("C") use
+      for Switches ("C") use C_Compiler_Config &
          ("-DWOLFSSL_USER_SETTINGS", --  Use the user_settings.h file.
           "-Wno-pragmas",
           "-Wall",
@@ -81,16 +87,5 @@ library project WolfSSL is
    package Binder is
       for Switches ("Ada") use ("-Es");  --  To include stack traces.
    end Binder;
- 
---     case OS is
---        when "Windows" =>
---           for Library_Options use ("-lm",  --  To include the math library (used by WolfSSL).
---  		                  "-lcrypt32");  --  Needed on Windows.
---        when "Linux_Or_Mac" =>
---  	 for Library_Options use ("-lm");  --  To include the math library (used by WolfSSL).
---     end case;
---  
---     --  Put user options in front, for options like --as-needed.
---     for Leading_Library_Options use External_As_List ("LDFLAGS", " ");
 
 end WolfSSl;