chore: Compile libsodium reference implementation with compcert.

This ensures that we're able to generate a guaranteed semantically
correct binary with all of toxcore and libsodium. We don't currently
compile libvpx and opus with compcert. Probably not worth the effort.

Author: iphydf

other/docker/compcert/Makefile

@@ -1,26 +1,39 @@
-SOURCES := $(wildcard auto_tests/auto_test_support.c \
-		   auto_tests/send_message_test.c \
-		   testing/misc_tools.c \
-		   toxav/*.c \
-		   toxcore/*.c \
-		   toxcore/*/*.c \
-		   toxencryptsave/*.c \
-		   third_party/cmp/*.c)
+CC := ccomp
+CFLAGS := -Wall \
+	  -Wno-c11-extensions \
+	  -Wno-unknown-pragmas \
+	  -Wno-unused-variable \
+	  -fstruct-passing -fno-unprototyped -g \
+	  -Ilibsodium/src/libsodium/include \
+	  $(shell pkg-config --cflags opus vpx)
+LDFLAGS := -lpthread $(shell pkg-config --libs opus vpx)
 
-OBJECTS := $(SOURCES:.c=.o)
+libsodium_SOURCES := $(shell find libsodium/src/libsodium -name "*.c")
+libsodium_OBJECTS := $(libsodium_SOURCES:.c=.o)
 
-CC := ccomp
-CFLAGS := -Wall -Werror \
-		  -Wno-c11-extensions \
-		  -Wno-unknown-pragmas \
-		  -Wno-unused-variable \
-		  -fstruct-passing -fno-unprototyped -g \
-		  -D__COMPCERT__ \
-		  -DDISABLE_VLA \
-		  -DMIN_LOGGER_LEVEL=LOGGER_LEVEL_TRACE \
-		  -Dinline= \
-		  $(shell pkg-config --cflags libsodium opus vpx)
-LDFLAGS := -lpthread $(shell pkg-config --libs libsodium opus vpx)
+$(libsodium_OBJECTS): CFLAGS += \
+	-DDEV_MODE \
+	-DCONFIGURED \
+	-D_DEFAULT_SOURCE \
+	-Ilibsodium/builds/msvc \
+	-Ilibsodium/src/libsodium/include/sodium
+
+toxcore_SOURCES := $(wildcard \
+	   auto_tests/auto_test_support.c \
+	   auto_tests/send_message_test.c \
+	   testing/misc_tools.c \
+	   toxav/*.c \
+	   toxcore/*.c \
+	   toxcore/*/*.c \
+	   toxencryptsave/*.c \
+	   third_party/cmp/*.c)
+toxcore_OBJECTS := $(toxcore_SOURCES:.c=.o)
+$(toxcore_OBJECTS): CFLAGS += \
+	-Werror \
+	-D__COMPCERT__ \
+	-DDISABLE_VLA \
+	-DMIN_LOGGER_LEVEL=LOGGER_LEVEL_TRACE \
+	-Dinline= \
 
-send_message_test: $(OBJECTS)
+send_message_test: $(libsodium_OBJECTS) $(toxcore_OBJECTS)
 	$(CC) -o $@ $+ $(LDFLAGS)

other/docker/compcert/compcert.Dockerfile

@@ -13,6 +13,7 @@ COPY --from=sources /src/ /work/
 
 SHELL ["/bin/bash", "-o", "pipefail", "-c"]
 
+RUN git clone --depth=1 https://github.com/jedisct1/libsodium /work/libsodium
 COPY other/docker/compcert/Makefile /work/
 RUN make "-j$(nproc)"
 RUN ./send_message_test | grep 'tox clients connected'