https://github.com/project-everest/hacl-star
Tip revision: 648dec91505e450c1d6e51640da624ce44b97adc authored by Aseem Rastogi on 17 November 2017, 13:48:19 UTC
adding gen1
adding gen1
Tip revision: 648dec9
Makefile
#
# Main HACL* Makefile
#
.PHONY: display verify test clean dependencies
all: display
display:
@echo "HACL* Makefile:"
@echo "If you want to run and test the C library:"
@echo "- 'make build' will generate a shared library from the hacl-c snapshot (no verification)"
@echo "- 'make unit-tests' will run tests on the library built rom the hacl-c snapshot (no verification)"
@echo "- 'make clean-build' will clean 'build' artifacts"
@echo ""
@echo "If you want to verify the F* code and regenerate the C library:"
@echo "- 'make prepare' will try to install F* and Kremlin (still has some prerequisites)"
@echo "- 'make verify' will run F* verification on all specs, code and secure-api directories"
@echo "- 'make extract' will generate all the C code into a snapshot and test it (no verification)"
@echo "- 'make test-all' will generate and test everything (no verification)"
@echo "- 'make world' will run everything (except make prepare)"
@echo "- 'make clean' will remove all artifacts created by other targets"
@echo ""
@echo "Specialized targets for Experts:"
@echo "- 'make verify-ct' will run F* verification of the code for the secret independance"
@echo "- 'make verify-specs' will run F* verification on the specifications"
@echo "- 'make verify-code' will run F* verification on the code against the specification"
@echo "- 'make verify-secure_api' will run F* verification of the secure_api directory"
@echo "- 'make extract-specs' will generate OCaml code for the specifications"
@echo "- 'make extract-all' will give you all versions of the C snapshots available"
@echo "- 'make extract-new' will remove and regenerate all versions of the C snapshots available"
@echo "- 'make extract-experimental' will generate C code for experimental primitives"
#
# Includes
#
ifneq ($(FSTAR_HOME),)
include Makefile.include
endif
include Makefile.build
include Makefile.prepare
#
# Verification
#
.verify-banner:
@echo $(CYAN)"# Verification of the HaCl*"$(NORMAL)
verify-ct:
$(MAKE) -C code ct
verify-specs: specs.dir-verify
verify-code: code.dir-verify
verify-secure_api: secure_api.dir-verify
verify: .verify-banner verify-ct verify-specs verify-code verify-secure_api
@echo $(CYAN)"\nDone ! Please check the verification output"$(NORMAL)
verify-nss:
@echo $(CYAN)"# Verification of the HaCl* algorithms used by NSS"$(NORMAL)
# Verify spec, code and ct
$(MAKE) ct -C code/curve25519
$(MAKE) verify -C code/curve25519
$(MAKE) Spec.Curve25519.fst-verify -C specs
#
# Code generation
#
.extract-banner:
@echo $(CYAN)"# Generation of the HaCl* verified C code"$(NORMAL)
@echo $(CYAN)" (This is not running formal verification)"$(NORMAL)
extract: .extract-banner
rm -rf snapshots/hacl-c snapshots/snapshot-gcc snapshots/snapshot-gcc-unrolled
$(MAKE) snapshots/hacl-c
@echo $(CYAN)"\nDone ! Generated code can be found in 'snapshots/hacl-c'."$(NORMAL)
extract-specs:
$(MAKE) -C specs
extract-all: snapshots-all
extract-new: snapshots-update
extract-experimental: extract-c-code-experimental
#
# Compilation of the library
#
.build-banner:
@echo $(CYAN)"# Compiling the HaCl* library"$(NORMAL)
build-make:
$(MAKE) build/libhacl.so
build-cmake:
mkdir -p build && cd build && CC=gcc cmake $(CMAKE_COMPILER_OPTION) .. && make
build: clean-build
$(MAKE) build-make
@echo $(CYAN)"\nDone ! Generated libraries can be found in 'build'."$(NORMAL)
#
# Test specification and code
#
unit-tests:
@echo $(CYAN)"# Testing the HaCl* shared library"$(NORMAL)
$(MAKE) -C snapshots/hacl-c unit-tests
test-all:
@echo $(CYAN)"# Testing the HaCl* code and specifications"$(NORMAL)
$(MAKE) -C test
#
# World
#
.base: verify extract-specs extract-all
world: .clean-banner .clean-git .clean-snapshots
$(MAKE) verify
$(MAKE) extract-specs
$(MAKE) extract-all
$(MAKE) build-make
$(MAKE) test-all
$(MAKE) package
#
# CI
#
ci: .clean-banner .clean-git .clean-snapshots
$(MAKE) .base
$(MAKE) build-make
$(MAKE) test-all
$(MAKE) package
#
# Clean
#
.clean-banner:
@echo $(CYAN)"# Clean HaCl*"$(NORMAL)
.clean-git:
git reset HEAD --hard
git clean -xfd
.clean-snapshots: snapshots-remove
clean-base:
rm -rf *~ *.tar.gz *.zip
rm -rf snapshots/hacl-c/*.o
rm -rf snapshots/hacl-c/libhacl*
clean-build:
rm -rf build
rm -rf build-experimental
clean-package: clean-base clean-build
clean: .clean-banner clean-base clean-build
$(MAKE) -C specs clean
$(MAKE) -C code clean
$(MAKE) -C secure_api clean
$(MAKE) -C apps clean
$(MAKE) -C test clean
#
# Packaging helper
#
.package-banner:
@echo $(CYAN)"# Packaging the HaCl* generated code"$(NORMAL)
@echo $(CYAN)" Make sure you have run verification before !"$(NORMAL)
package: .package-banner snapshots/hacl-c build
mkdir -p hacl
cp build/lib* hacl
cp -r snapshots/hacl-c/* hacl
tar -zcvf hacl-star.tar.gz hacl
rm -rf hacl
@echo $(CYAN)"\nDone ! Generated archive is 'hacl-star.tar.gz'. !"$(NORMAL)
#
# Undocumented targets
#
experimental:
@echo $(CYAN)"# Compiling the HaCl* library (with experimental features)"$(NORMAL)
mkdir -p build-experimental && cd build-experimental; \
cmake $(CMAKE_COMPILER_OPTION) -DExperimental=ON .. && make
@echo $(CYAN)"\nDone ! Generated libraries can be found in 'build-experimental'."$(NORMAL)
hints: code.dir-hints secure_api.dir-hints specs.dir-hints
# Colors
NORMAL="\\033[0;39m"
CYAN="\\033[1;36m"