Merge pull request #7303 from Irvise/master

[Ada] Initial library support

.gitignore

@@ -442,6 +442,12 @@ debian/changelog
 debian/control
 *.deb
 
+# Ada/Alire files
+wrapper/Ada/alire/
+wrapper/Ada/config/
+wrapper/Ada/lib/
+wrapper/Ada/obj/
+
 # PlatformIO
 /**/.pio
 /**/.vscode/.browse.c_cpp.db*

wrapper/Ada/README.md

@@ -28,7 +28,9 @@ Not only can the WolfSSL Ada binding be used in Ada applications but
 also SPARK applications (a subset of the Ada language suitable
 formal verification). To formally verify the Ada code in this repository
 open the client.gpr with GNAT Studio and then select
-SPARK -> Prove All Sources and use Proof Level 2.
+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
+order to instruct the prover to use 12 CPUs if available).
 
 ```
 Summary of SPARK analysis
@@ -53,19 +55,31 @@ Total                           172    17 (10%)          .                     1
 
 ## Compiler and Build System installation
 
-### GNAT Community Edition 2021
-Download and install the GNAT community Edition 2021 compiler and studio:
-https://www.adacore.com/download
+### Recommended: [Alire](https://alire.ada.dev)
+[Alire](https://alire.ada.dev) is a modern package manager for the Ada
+ecosystem.  The latest version is available for Windows, OSX, Linux and FreeBSD
+systems.  It can install a complete Ada toolchain if needed, see `alr install`
+for more information.
 
-Linux Install:
+In order to use WolfSSL in a project, just add WolfSSL as a dependency by
+running `alr with wolfssl` within your project's directory.
 
-```sh
-chmod +x gnat-2021-20210519-x86_64-linux-bin
-./gnat-2021-20210519-x86_64-linux-bin
-```
+If the project is to be verified with SPARK, just add `gnatprove` as a
+dependency by running `alr with gnatprove` and then running `alr gnatprove`,
+which will execute the SPARK solver. If you get warnings, it is recommended to
+increase the prove level: `alr gnatprove --level=4`.
+
+### GNAT FSF Compiler and GPRBuild manual installation
+In May 2022 AdaCore announced the end of the GNAT Community releases.
+Pre-built binaries for the GNAT FSF compiler and GPRBuild can be
+downloaded and manually installed from here:
+https://github.com/alire-project/GNAT-FSF-builds/releases
+Make sure the executables for the compiler and GPRBuild are on the PATH
+and use gprbuild to build the source code.
+
+#### Manual build of the project
 
 ```sh
-export PATH="/opt/GNAT/2021/bin:$PATH"
 cd wrapper/Ada
 gprclean
 gprbuild default.gpr
@@ -82,15 +96,6 @@ gprbuild -XOS=Windows default.gpr
 gprbuild -XOS=Windows client.gpr
 ```
 
-
-### GNAT FSF Compiler and GPRBuild manual installation
-In May 2022 AdaCore announced the end of the GNAT Community releases.
-Pre-built binaries for the GNAT FSF compiler and GPRBuild can be
-downloaded and manually installed from here:
-https://github.com/alire-project/GNAT-FSF-builds/releases
-Make sure the executables for the compiler and GPRBuild are on the PATH
-and use gprbuild to build the source code.
-
 ## Files
 The (D)TLS v1.3 client example in the Ada/SPARK programming language
 using the WolfSSL library can be found in the files:
@@ -103,15 +108,3 @@ using the WolfSSL library can be found in the files:
 tls_server_main.adb
 tls_server.ads
 tls_server.adb
-
-A feature of the Ada language that is not part of SPARK is exceptions.
-Some packages of the Ada standard library and GNAT specific packages
-provided by the GNAT compiler can therefore not be used directly but
-need to be put into wrapper packages that does not raise exceptions.
-The packages that provide access to sockets and command line arguments
-to applications implemented in the SPARK programming language can be
-found in the files:
-spark_sockets.ads
-spark_sockets.adb
-spark_terminal.ads
-spark_terminal.adb

wrapper/Ada/alire.toml

@@ -0,0 +1,11 @@
+name = "wolfssl"
+description = "WolfSSL encryption library and its Ada bindings"
+version = "5.7.0"
+
+authors = ["Fernando Oleo Blanco"]
+maintainers = ["Fernando Oleo Blanco <irvise@irvise.xyz>"]
+maintainers-logins = ["Irvise"]
+licenses = "GPL-2.0-only"
+website = "https://www.wolfssl.com/"
+project-files = ["wolfssl.gpr"]
+tags = ["ssl", "tls", "embedded", "spark"]

wrapper/Ada/user_settings.h

@@ -37,6 +37,9 @@ extern "C" {
 /* Usually comes from configure -> config.h */
 #define HAVE_SYS_TIME_H
 
+/* Explicitly define NETDB support */
+#define HAVE_NETDB_H
+
 /* Features */
 #define SINGLE_THREADED
 #define WOLFSSL_IGNORE_FILE_WARN /* Ignore *.c include warnings */

wrapper/Ada/wolfssl.gpr

@@ -0,0 +1,96 @@
+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");
+
+   for Source_Dirs use (".",
+                        "../../",
+                        "../../src",
+                        "../../wolfcrypt/src");
+
+   --  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 Object_Dir use "obj";
+   for Library_Dir use "lib";
+   for Create_Missing_Dirs use "True";
+
+   type Library_Type_Type is ("relocatable", "static", "static-pic");
+   Library_Type : Library_Type_Type := external("LIBRARY_TYPE", "static");
+   for Library_Kind use Library_Type;
+
+   package Naming is
+      for Spec_Suffix ("C") use ".h";
+   end Naming;
+
+   package Builder is
+      for Global_Configuration_Pragmas use "gnat.adc";
+   end Builder;
+
+   package Compiler is
+      for Switches ("C") use
+         ("-DWOLFSSL_USER_SETTINGS", --  Use the user_settings.h file.
+          "-Wno-pragmas",
+          "-Wall",
+          "-Wextra",
+          "-Wunknown-pragmas",
+          "--param=ssp-buffer-size=1",
+          "-Waddress",
+          "-Warray-bounds",
+          "-Wbad-function-cast",
+          "-Wchar-subscripts",
+          "-Wcomment",
+          "-Wfloat-equal",
+          "-Wformat-security",
+          "-Wformat=2",
+          "-Wmaybe-uninitialized",
+          "-Wmissing-field-initializers",
+          "-Wmissing-noreturn",
+          "-Wmissing-prototypes",
+          "-Wnested-externs",
+          "-Wnormalized=id",
+          "-Woverride-init",
+          "-Wpointer-arith",
+          "-Wpointer-sign",
+          "-Wshadow",
+          "-Wsign-compare",
+          "-Wstrict-overflow=1",
+          "-Wstrict-prototypes",
+          "-Wswitch-enum",
+          "-Wundef",
+          "-Wunused",
+          "-Wunused-result",
+          "-Wunused-variable",
+          "-Wwrite-strings",
+          "-fwrapv") & External_As_List ("CFLAGS", " ");
+
+      for Switches ("Ada") use ("-g") & External_As_List ("ADAFLAGS", " ");
+   end Compiler;
+
+   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;