#
# General extraction
#
ifndef HACL_HOME
HACL_HOME:=$(abspath $(dir $(lastword $(MAKEFILE_LIST))))
HACL_HOME:=$(HACL_HOME:/=)
else
HACL_HOME:=$(abspath $(HACL_HOME))
HACL_HOME:=$(HACL_HOME:/=)
endif
#
# Compilers and tools
#
HAS_CL=$(shell which cl.exe >/dev/null 2>&1 && echo true || echo false)
HAS_CCOMP=$(shell which ccomp >/dev/null 2>&1 && echo true || echo false)
GFIND=$(shell which gfind >/dev/null 2>&1 && echo gfind || echo find)
ifeq ($(OS),Windows_NT)
GCC=x86_64-w64-mingw32-gcc.exe
MSVC=cl.exe
else
GCC=$(shell which gcc-7 >/dev/null 2>&1 && echo gcc-7 || (which gcc-6 >/dev/null 2>&1 && echo gcc-6 || echo gcc))
CMAKE_COMPILER_OPTION := -DCMAKE_C_COMPILER=$(GCC)
ENABLE_LTO=-flto
endif
GCC_OPTS=$(ENABLE_LTO) -std=c11 -D_GNU_SOURCE
#
# Targets
#
.PHONY: snapshot-collect snapshots-all snapshots-update snapshots-remove .%
#
# Extraction target for the stateful code
#
extract-c: extract-c-code extract-c-crypto # extract-c-apps
extract-c-code:
$(GFIND) code -name out.krml -exec touch {} \;
$(MAKE) -C code extract-c
extract-c-code-experimental:
$(MAKE) -C code/experimental extract-c
# Clean the code directories
clean-c-code:
$(MAKE) -C code clean-c
#
# Snapshot targets
#
SNAPSHOT_DIR = # Substituted by the correct value depending on the compiler
SNAPSHOT_FILES= \
$(KREMLIN_HOME)/include/* \
$(addprefix snapshots/api/, HACL.h) \
$(addprefix snapshots/api/, haclnacl.*) \
$(addprefix snapshots/makefiles/, Makefile) \
$(addprefix snapshots/common/, vec128.h) \
$(addprefix snapshots/experimental/, Hacl_Unverified_Random.*) \
$(KREMLIN_HOME)/kremlib/uint128/FStar_UInt128.* \
$(addprefix code/poly1305/poly-c/, Hacl_Poly1305_64.* AEAD_Poly1305_64.*) \
$(addprefix code/poly1305_32/poly-c/, Hacl_Poly1305_32.*) \
$(addprefix code/curve25519/x25519-c/, Hacl_Curve25519.*) \
$(addprefix code/salsa-family/chacha-c/, Hacl_Chacha20.*) \
$(addprefix code/salsa-family/salsa-c/, Hacl_Salsa20.*) \
$(addprefix code/api/aead-c/, Hacl_Chacha20Poly1305.*) \
$(addprefix code/api/box-c/, NaCl.*) \
$(addprefix code/api/policies-c/, Hacl_Policies.* ) \
$(addprefix code/ed25519/ed25519-c/, Hacl_Ed25519.*) \
$(addprefix code/hash/sha2-c/, Hacl_SHA2_256.*) \
$(addprefix code/hash/sha2-c/, Hacl_SHA2_384.*) \
$(addprefix code/hash/sha2-c/, Hacl_SHA2_512.*) \
$(addprefix code/hmac/hmac-sha256-c/, Hacl_HMAC_SHA2_256.*) \
$(addprefix code/hmac/hmac-sha384-c/, Hacl_HMAC_SHA2_384.*) \
$(addprefix code/hmac/hmac-sha512-c/, Hacl_HMAC_SHA2_512.*) \
$(addprefix code/salsa-family/chacha-vec128-c/, Hacl_Chacha20_Vec128.*)
snapshot-collect:
mkdir -p $(SNAPSHOT_DIR)
cp -r $(SNAPSHOT_FILES) $(SNAPSHOT_DIR)/
touch $(SNAPSHOT_DIR)/Prims.h
$(MAKE) -C $(SNAPSHOT_DIR) clean
snapshots/snapshot-gcc: clean-c-code
$(MAKE) extract-c-code extract-c-code-experimental KOPTS="-fparentheses" HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)"
$(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-gcc
snapshots/snapshot-gcc-unrolled: clean-c-code
$(MAKE) extract-c-code extract-c-code-experimental KOPTS="-funroll-loops 5 -fparentheses" HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)"
$(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-gcc-unrolled
snapshots/snapshot-compcert: clean-c-code
if $(HAS_CCOMP); then $(MAKE) extract-c-code extract-c-code-experimental KOPTS="-cc compcert -fparentheses -fnostruct-passing" HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)"; fi
if $(HAS_CCOMP); then $(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-compcert; fi
snapshots/snapshot-compcert-unrolled: clean-c-code
if $(HAS_CCOMP); then $(MAKE) extract-c-code extract-c-code-experimental KOPTS="-cc compcert -fparentheses -funroll-loops 5 -fnostruct-passing" HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)"; fi
if $(HAS_CCOMP); then $(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-compcert-unrolled; fi
snapshots/snapshot-msvc: clean-c-code
if $(HAS_CL); then $(MAKE) extract-c-code extract-c-code-experimental KOPTS="-cc msvc " HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)"; fi
if $(HAS_CL); then $(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-msvc; fi
snapshots/snapshot-msvc-unrolled: clean-c-code
if $(HAS_CL); then $(MAKE) extract-c-code extract-c-code-experimental KOPTS="-cc msvc -fparentheses -funroll-loops 5 " HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)"; fi
if $(HAS_CL); then $(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-msvc-unrolled; fi
#
# Production targets for C code
#
HACL_RELEASE=1
ifeq ($(shell uname -o),Cygwin)
HACL_LICENSE?=$(cygpath -a -m $(HACL_HOME)/snapshots/licenses/MIT)
else
HACL_LICENSE?=$(HACL_HOME)/snapshots/licenses/MIT
endif
HACL_LICENSE_NSS?=$(HACL_HOME)/snapshots/licenses/APACHE2
SNAPSHOT_HACL_C_FILES = $(addprefix snapshots/snapshot-gcc/, FStar_UInt128.* AEAD_Poly1305_64.* Hacl_Chacha20.* Hacl_Chacha20Poly1305.* Hacl_Chacha20_Vec128.* Hacl_Policies.* NaCl.* Hacl_Poly1305_64.* Hacl_Poly1305_32.* Hacl_Salsa20.* Hacl_SHA2_* Hacl_HMAC_SHA2_*) \
$(addprefix snapshots/snapshot-gcc-unrolled/, Hacl_Curve25519* Hacl_Ed25519*)
.snapshots/hacl-c/makefiles:
for f in CMakeLists.txt Makefile; do \
cp snapshots/makefiles/$$f snapshots/hacl-c/$$f ; \
done
.snapshots/hacl-c/common:
for f in vec128.h; do \
(cat $(HACL_LICENSE) snapshots/common/$$f ) > snapshots/hacl-c/$$f ; \
done
.snapshots/hacl-c/kremlib:
cp -r $(KREMLIN_HOME)/include/* snapshots/hacl-c
.snapshots/hacl-c/api:
for f in HACL.h haclnacl.h haclnacl.c; do \
(cat $(HACL_LICENSE) snapshots/api/$$f ) > snapshots/hacl-c/$$f ; \
done
.snapshots/hacl-c/experimental:
for f in Hacl_Unverified_Random.h Hacl_Unverified_Random.c; do \
(cat $(HACL_LICENSE) snapshots/experimental/$$f ) > snapshots/hacl-c/$$f ; \
done
snapshots/hacl-c: snapshots-remove-intermediates
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" snapshots/snapshot-gcc
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" snapshots/snapshot-gcc-unrolled
rm -rf snapshots/hacl-c
mkdir -p snapshots/hacl-c
cp $(SNAPSHOT_HACL_C_FILES) ./snapshots/hacl-c
$(MAKE) .snapshots/hacl-c/makefiles
$(MAKE) .snapshots/hacl-c/common
$(MAKE) .snapshots/hacl-c/kremlib
$(MAKE) .snapshots/hacl-c/api
$(MAKE) .snapshots/hacl-c/experimental
SNAPSHOT_NSS_FILES = \
$(addprefix snapshots/snapshot-gcc/, FStar_UInt128.* Hacl_Chacha20.* Hacl_Chacha20_Vec128.* Hacl_Poly1305_64.* Hacl_Poly1305_32.*) \
$(addprefix snapshots/snapshot-gcc-unrolled/, Hacl_Curve25519*)
.snapshots/nss/common:
for f in vec128.h; do \
(cat $(HACL_LICENSE_NSS) snapshots/common/$$f ) > snapshots/nss/$$f ; \
done
.snapshots/nss/kremlib:
cp -r snapshots/kremlib/* snapshots/nss
for f in kremlib.h kremlib.c kremdate.c kremstr.c; do \
(cat $(HACL_LICENSE_NSS) snapshots/kremlib/$$f ) > snapshots/nss/$$f ; \
done
.snapshots/nss/specs:
for f in Spec.Curve25519.fst Spec.CTR.fst Spec.Chacha20.fst Spec.Poly1305.fst; do \
(cat $(HACL_LICENSE_NSS) specs/$$f ) > snapshots/nss/specs/$$f ; \
done
snapshots/nss: snapshots-remove-intermediates
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE_NSS)" snapshots/snapshot-gcc
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE_NSS)" snapshots/snapshot-gcc-unrolled
rm -rf snapshots/nss
mkdir -p snapshots/nss
mkdir -p snapshots/nss/specs
cp $(SNAPSHOT_NSS_FILES) snapshots/nss
$(MAKE) .snapshots/nss/common
$(MAKE) .snapshots/nss/kremlib
$(MAKE) .snapshots/nss/specs
SNAPSHOT_RIOT_FILES = $(addprefix snapshots/snapshot-gcc/, FStar_UInt128.* AEAD_Poly1305_64.* Hacl_Chacha20.* Hacl_Chacha20Poly1305.* Hacl_Policies.* NaCl.* Hacl_Poly1305_64.* Hacl_Poly1305_32.* Hacl_Salsa20.* Hacl_SHA2_* Hacl_HMAC_SHA2_*) \
$(addprefix snapshots/snapshot-gcc-unrolled/, Hacl_Curve25519* Hacl_Ed25519*)
.snapshots/riot/kremlib:
cp -r snapshots/kremlib/* snapshots/riot
for f in kremlib.h kremlib.c kremdate.c kremstr.c; do \
(cat $(HACL_LICENSE) snapshots/kremlib/$$f ) > snapshots/riot/$$f ; \
done
snapshots/riot: snapshots-remove-intermediates
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" snapshots/snapshot-gcc
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" snapshots/snapshot-gcc-unrolled
rm -rf snapshots/riot
mkdir -p snapshots/riot
cp $(SNAPSHOT_RIOT_FILES) ./snapshots/riot
$(MAKE) .snapshots/riot/kremlib
SNAPSHOT_WIREGUARD_FILES = $(addprefix snapshots/snapshot-gcc-unrolled/, FStar_UInt128.* Hacl_Curve25519*)
.snapshots/wireguard/kremlib:
cp -r snapshots/kremlib/* snapshots/wireguard
for f in kremlib.h kremlib.c kremdate.c kremstr.c; do \
(cat $(HACL_LICENSE) snapshots/kremlib/$$f ) > snapshots/wireguard/$$f ; \
done
snapshots/wireguard: snapshots-remove-intermediates
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" KOPTS="$(KOPTS) -fc89" snapshots/snapshot-gcc-unrolled
rm -rf snapshots/wireguard
mkdir -p snapshots/wireguard
cp $(SNAPSHOT_WIREGUARD_FILES) snapshots/wireguard
$(MAKE) .snapshots/wireguard/kremlib
SNAPSHOT_TEZOS_FILES = $(addprefix snapshots/snapshot-gcc/, FStar_UInt128.* Hacl_Chacha20.* Hacl_Policies.* NaCl.* Hacl_Poly1305_64.* Hacl_Poly1305_32.* Hacl_Salsa20.* Hacl_SHA2_* Hacl_HMAC_SHA2_* AEAD_Poly1305_64.* Hacl_Chacha20Poly1305.*) \
$(addprefix snapshots/snapshot-gcc-unrolled/, Hacl_Curve25519* Hacl_Ed25519*)
.snapshots/tezos/makefiles:
for f in CMakeLists.Tezos.txt; do \
cp snapshots/makefiles/$$f snapshots/tezos/$$f ; \
done
.snapshots/tezos/haclnacl:
for f in haclnacl.h haclnacl.c; do \
(cat $(HACL_LICENSE) snapshots/api/$$f ) > snapshots/tezos/$$f ; \
done
.snapshots/tezos/kremlib:
cp -r snapshots/kremlib/* snapshots/tezos
for f in kremlib.h kremlib.c kremdate.c kremstr.c; do \
(cat $(HACL_LICENSE) snapshots/kremlib/$$f ) > snapshots/tezos/$$f ; \
done
.snapshots/tezos/experimental:
for f in Hacl_Unverified_Random.h Hacl_Unverified_Random.c; do \
(cat $(HACL_LICENSE) snapshots/experimental/$$f ) > snapshots/tezos/$$f ; \
done
snapshots/tezos: snapshots-remove-intermediates
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" snapshots/snapshot-gcc
$(MAKE) HACL_RELEASE="$(HACL_RELEASE)" HACL_LICENSE="$(HACL_LICENSE)" snapshots/snapshot-gcc-unrolled
rm -rf snapshots/tezos
mkdir -p snapshots/tezos
cp $(SNAPSHOT_TEZOS_FILES) ./snapshots/tezos
$(MAKE) .snapshots/tezos/makefiles
$(MAKE) .snapshots/tezos/kremlib
$(MAKE) .snapshots/tezos/experimental
mkdir -p snapshots/tezos/include
mv snapshots/tezos/*.h snapshots/tezos/include
$(MAKE) .snapshots/tezos/haclnacl
mv snapshots/tezos/CMakeLists.Tezos.txt snapshots/tezos/CMakeLists.txt
cp snapshots/api/HACL.Tezos.h snapshots/tezos/HACL.h
#
# Production target for Web Assembly
#
# Emscripten exported functions
define WASM_EXPORTED_FUNCTIONS
"_Hacl_Chacha20_chacha20", "_Hacl_Chacha20_chacha20_key_block", \
"_AEAD_Poly1305_64_mk_state", "_AEAD_Poly1305_64_mul_div_16", "_AEAD_Poly1305_64_pad_last", \
"_AEAD_Poly1305_64_poly1305_blocks_init", "_AEAD_Poly1305_64_poly1305_blocks_continue", \
"_AEAD_Poly1305_64_poly1305_blocks_finish_", "_AEAD_Poly1305_64_poly1305_blocks_finish", \
"_Hacl_Chacha20Poly1305_encode_length", "_Hacl_Chacha20Poly1305_aead_encrypt_", \
"_Hacl_Chacha20Poly1305_aead_encrypt", "_Hacl_Chacha20Poly1305_aead_decrypt", \
"_Hacl_Chacha20_Vec128_chacha20", "_Hacl_Curve25519_crypto_scalarmult", \
"_Hacl_Ed25519_sign", "_Hacl_Ed25519_verify", "_Hacl_Ed25519_secret_to_public", \
"_Hacl_HMAC_SHA2_256_hmac_core", "_Hacl_HMAC_SHA2_256_hmac", "_Hacl_Policies_declassify_u8", "_Hacl_Policies_declassify_u32", \
"_Hacl_Policies_declassify_u64", "_Hacl_Policies_declassify_u128", "_Hacl_Policies_cmp_bytes_", \
"_Hacl_Policies_cmp_bytes", "_Hacl_Poly1305_32_mk_state", "_Hacl_Poly1305_32_init", \
"_Hacl_Poly1305_32_update_block", "_Hacl_Poly1305_32_update", "_Hacl_Poly1305_32_update_last", \
"_Hacl_Poly1305_32_finish", "_Hacl_Poly1305_32_crypto_onetimeauth", "_Hacl_Poly1305_64_mk_state", \
"_Hacl_Poly1305_64_init", "_Hacl_Poly1305_64_update_block", "_Hacl_Poly1305_64_update", \
"_Hacl_Poly1305_64_update_last", "_Hacl_Poly1305_64_finish", "_Hacl_Poly1305_64_crypto_onetimeauth", \
"_Hacl_Salsa20_salsa20", "_Hacl_Salsa20_hsalsa20", "_Hacl_SHA2_256_init", "_Hacl_SHA2_256_update", \
"_Hacl_SHA2_256_update_multi", "_Hacl_SHA2_256_update_last", "_Hacl_SHA2_256_finish", \
"_Hacl_SHA2_256_hash", "_Hacl_SHA2_384_init", "_Hacl_SHA2_384_update", \
"_Hacl_SHA2_384_update_multi", "_Hacl_SHA2_384_update_last", "_Hacl_SHA2_384_finish", \
"_Hacl_SHA2_384_hash", "_Hacl_SHA2_512_init", "_Hacl_SHA2_512_update", \
"_Hacl_SHA2_512_update_multi", "_Hacl_SHA2_512_update_last", "_Hacl_SHA2_512_finish", \
"_Hacl_SHA2_512_hash", "_NaCl_crypto_secretbox_detached", "_NaCl_crypto_secretbox_open_detached", \
"_NaCl_crypto_secretbox_easy", "_NaCl_crypto_secretbox_open_easy", "_NaCl_crypto_box_beforenm", \
"_NaCl_crypto_box_detached_afternm", "NaCl_crypto_box_detached", "_NaCl_crypto_box_open_detached", \
"_NaCl_crypto_box_easy_afternm", "_NaCl_crypto_box_easy", "_NaCl_crypto_box_open_easy", \
"_NaCl_crypto_box_open_detached_afternm", "_NaCl_crypto_box_open_easy_afternm", \
"_malloc", "_free"
endef
snapshots/hacl-c-wasm: snapshots-remove-intermediates
$(MAKE) snapshots/hacl-c
rm -rf snapshots/hacl-c-wasm
mkdir -p snapshots/hacl-c-wasm/build
cp $(SNAPSHOT_HACL_C_FILES) snapshots/hacl-c-wasm/build
emcc -O3 -DKRML_NOUINT128 -Wno-implicit-function-declaration \
-Wno-bitwise-op-parentheses -Wno-shift-op-parentheses \
-s WASM=1 -s MODULARIZE=1 -s 'EXPORT_NAME="HaclLoader"' \
-o snapshots/hacl-c-wasm/HaclLoader.js \
-s EXPORTED_FUNCTIONS='[$(WASM_EXPORTED_FUNCTIONS)]' \
-I snapshots/hacl-c-wasm/build snapshots/hacl-c-wasm/build/*.c
rm -rf snapshots/hacl-c-wasm/build
#
# Build, refresh and clean targets for all snapshots
#
snapshots-intermediates:
$(MAKE) snapshots/snapshot-gcc
$(MAKE) snapshots/snapshot-gcc-unrolled
$(MAKE) snapshots/snapshot-compcert
$(MAKE) snapshots/snapshot-compcert-unrolled
$(MAKE) snapshots/snapshot-msvc
$(MAKE) snapshots/snapshot-msvc-unrolled
snapshots-production:
$(MAKE) snapshots/hacl-c
$(MAKE) snapshots/nss
$(MAKE) snapshots/riot
$(MAKE) snapshots/wireguard
$(MAKE) snapshots/tezos
snapshots-remove-intermediates:
rm -rf snapshots/snapshot*
snapshots-remove-production:
rm -rf snapshots/hacl-c
rm -rf snapshots/nss
rm -rf snapshots/riot
rm -rf snapshots/wireguard
rm -rf snapshots/tezos
#
# Building the shared library
#
snapshots/hacl-c/libhacl.so:
$(MAKE) -C snapshots/hacl-c libhacl.so
snapshots/hacl-c/libhacl.a:
$(MAKE) -C snapshots/hacl-c libhacl.a
snapshots/hacl-c/libhacl32.so:
$(MAKE) -C snapshots/hacl-c libhacl32.so
snapshots/hacl-c/libhacl32.a:
$(MAKE) -C snapshots/hacl-c libhacl32.a
build/libhacl.so:
mkdir -p build
$(MAKE) snapshots/hacl-c/libhacl.so
cp snapshots/hacl-c/libhacl.so build
build/libhacl.a:
mkdir -p build
$(MAKE) snapshots/hacl-c/libhacl.a
cp snapshots/hacl-c/libhacl.a build
build/libhacl32.so:
mkdir -p build
$(MAKE) snapshots/hacl-c/libhacl32.so
cp snapshots/hacl-c/libhacl32.so build
build/libhacl32.a:
mkdir -p build
$(MAKE) snapshots/hacl-c/libhacl32.a
cp snapshots/hacl-c/libhacl32.a build