Revision eb73f5e87fdf4e25d82bb7ac0b8868c4cae124d0 authored by Konrad Kohbrok on 19 April 2018, 06:56:09 UTC, committed by Konrad Kohbrok on 19 April 2018, 06:56:09 UTC
1 parent c596c6b
Makefile.build
#
# General extraction
#
.PHONY: snapshot-collect snapshots-all snapshots-update snapshots-remove
#
# Extraction target for the stateful code
#
# BB: Add extract-c-apps to extract-c when libsodium is on the build machine
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
#
# Snapshot targets
#
SNAPSHOT_DIR = # Substituted by the correct value depending on the compiler
SNAPSHOT_FILES= $(addprefix snapshots/kremlib/, kremlib.* testlib.* gcc_compat.h FStar.h Makefile) \
$(addprefix code/poly1305/poly-c/, Poly1305_64.* AEAD_Poly1305_64.*) \
./code/curve25519/x25519-c/Curve25519.* \
./code/salsa-family/chacha-c/Chacha20.* \
./code/salsa-family/salsa-c/Salsa20.* \
$(addprefix code/api/aead-c/, Chacha20Poly1305.*) \
$(addprefix code/api/box-c/, NaCl.*) \
$(addprefix code/api/policies-c/, Hacl_Policies.* ) \
$(addprefix code/ed25519/ed25519-c/, Ed25519.*) \
$(addprefix code/hash/sha2-c/, SHA2_256.*) \
$(addprefix code/hash/sha2-c/, SHA2_384.*) \
$(addprefix code/hash/sha2-c/, SHA2_512.*) \
$(addprefix code/hmac/hmac-c/, HMAC_SHA2_256.*) \
$(addprefix code/salsa-family/chacha-vec128-c/, Chacha20_Vec128.* ../vec128.h)
SNAPSHOT_CCOMP_FILES=$(KREMLIN_HOME)/kremlib/kremlib.c $(KREMLIN_HOME)/kremlib/kremlib.h \
code/lib/kremlin/ccomp-c/FStar.c code/lib/kremlin/ccomp-c/FStar.h
snapshot-collect:
mkdir -p $(SNAPSHOT_DIR)
cp $(SNAPSHOT_FILES) $(SNAPSHOT_DIR)/
ifeq ($(SNAPSHOT_DIR),snapshots/hacl-c-compcert)
cp $(SNAPSHOT_CCOMP_FILES) $(SNAPSHOT_DIR)/
else
endif
$(MAKE) -C $(SNAPSHOT_DIR) clean
snapshots/hacl-c-compcert:
$(MAKE) -C code clean
if $(HAS_CCOMP); then $(MAKE) -B extract-c-code extract-c-code-experimental KOPTS="-cc compcert -funroll-loops 10 -fnouint128 -fnostruct-passing"; fi
if $(HAS_CCOMP); then $(MAKE) -B snapshot-collect SNAPSHOT_DIR=snapshots/hacl-c-compcert; fi
snapshots/snapshot-msvc:
$(MAKE) -C code clean
if $(HAS_CL); then $(MAKE) extract-c-code extract-c-code-experimental KOPTS="-cc msvc -drop FStar"; fi
if $(HAS_CL); then $(MAKE) snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-msvc; fi
snapshots/snapshot-gcc:
$(MAKE) -C code clean
$(MAKE) -B extract-c-code extract-c-code-experimental KOPTS="-drop FStar"
$(MAKE) -B snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-gcc
snapshots/snapshot-gcc-unrolled:
$(MAKE) -C code clean
$(MAKE) -B extract-c-code extract-c-code-experimental KOPTS="-funroll-loops 5 -drop FStar"
$(MAKE) -B snapshot-collect SNAPSHOT_DIR=snapshots/snapshot-gcc-unrolled
# BB: This requires to have up-to-date snapshot-gcc and snapshot-gcc-unrolled
# Maybe we should call 'snapshot-remove' before to enforce it (at the cost of two more extractions) ?
snapshots/hacl-c:
$(MAKE) snapshots/snapshot-gcc
$(MAKE) snapshots/snapshot-gcc-unrolled
mkdir -p snapshots/hacl-c
cp $(addprefix snapshots/snapshot-gcc/, AEAD_Poly1305_64.* Chacha20.* Chacha20Poly1305.* Chacha20_Vec128.* Hacl_Policies.* NaCl.* Poly1305_64.* Salsa20.* SHA2_* HMAC_SHA2_* vec128.h) \
$(addprefix snapshots/snapshot-gcc-unrolled/, Curve25519* Ed25519*) \
$(addprefix snapshots/kremlib/, kremlib.* testlib.* gcc_compat.h FStar.h Makefile) \
./snapshots/hacl-c
snapshots-all:
$(MAKE) snapshots/snapshot-gcc
$(MAKE) snapshots/snapshot-gcc-unrolled
$(MAKE) snapshots/snapshot-msvc
$(MAKE) snapshots/hacl-c-compcert
$(MAKE) snapshots/hacl-c
snapshots-remove:
rm -rf snapshots/hacl-c
rm -rf snapshots/snapshot*
snapshots-update:
$(MAKE) snapshots-remove
$(MAKE) snapshots-all
#
# Building the shared library
#
snapshots/hacl-c/libhacl.so: snapshots/hacl-c
$(MAKE) -C snapshots/hacl-c CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl.so
snapshots/hacl-c/libhacl32.so: snapshots/hacl-c
$(MAKE) -C snapshots/hacl-c CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl32.so
snapshots/snapshot-gcc/libhacl.so: snapshots/snapshot-gcc
$(MAKE) -C snapshots/snapshot-gcc CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl.so
snapshots/snapshot-gcc/libhacl32.so: snapshots/snapshot-gcc
$(MAKE) -C snapshots/snapshot-gcc CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl32.so
snapshots/snapshot-gcc-unrolled/libhacl.so: snapshots/snapshot-gcc-unrolled
$(MAKE) -C snapshots/snapshot-gcc-unrolled CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl.so
snapshots/snapshot-gcc-unrolled/libhacl32.so: snapshots/snapshot-gcc-unrolled
$(MAKE) -C snapshots/snapshot-gcc-unrolled CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl32.so
# BB: The options for Compcert and MSVC must be adjusted here
snapshots/hacl-c-compcert/libhacl.so: snapshots/hacl-c-compcert
$(MAKE) -C snapshots/hacl-c-compcert CC="$(CCOMP) $(CCOMP_OPTS) -fPIC" libhacl.so
snapshots/hacl-c-compcert/libhacl32.so: snapshots/hacl-c-compcert
$(MAKE) -C snapshots/hacl-c-compcert CC="$(CCOMP) $(CCOMP_OPTS) -fPIC" libhacl32.so
snapshots/snapshot-msvc/libhacl.so: snapshots/snapshot-msvc
$(MAKE) -C snapshots/snapshot-msvc CC="$(MSVC) $(MSVC_OPTS) -fPIC" libhacl.so
snapshots/snapshot-msvc/libhacl32.so: snapshots/snapshot-msvc
$(MAKE) -C snapshots/snapshot-msvc CC="$(MSVC) $(MSVC_OPTS) -fPIC" libhacl32.so
build/libhacl.so:
mkdir -p build
$(MAKE) snapshots/hacl-c/libhacl.so
cp snapshots/hacl-c/libhacl.so build
build/libhacl32.so:
mkdir -p build
$(MAKE) snapshots/hacl-c/libhacl32.so
cp snapshots/hacl-c/libhacl32.so build
#
# 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
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
Computing file changes ...