UNAME := $(shell uname)
.DEFAULT_GOAL=all
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
ifndef FSTAR_HOME
FSTAR_HOME:=$(abspath $(HACL_HOME)/dependencies/FStar)
else
FSTAR_HOME:=$(abspath $(FSTAR_HOME))
endif
ifndef KREMLIN_HOME
KREMLIN_HOME:=$(abspath $(HACL_HOME)/dependencies/kremlin)
else
KREMLIN_HOME:=$(abspath $(KREMLIN_HOME))
endif
export HACL_HOME
export FSTAR_HOME
export KREMLIN_HOME
# $(info $(HACL_HOME))
# $(info $(FSTAR_HOME))
# $(info $(KREMLIN_HOME))
HACL_LIB=$(HACL_HOME)/code/lib
HACL_FILES=Hacl.UInt8.fst Hacl.UInt16.fst Hacl.UInt32.fst Hacl.UInt64.fst Hacl.UInt128.fst Hacl.Cast.fst Hacl.Types.fst Hacl.Policies.fst
HACL_LIB_FILES=$(addprefix $(HACL_LIB)/, $(HACL_FILES))
HACL_KREMLIN=$(HACL_LIB)/kremlin
HACL_KREMLIN_FILES=$(addprefix $(HACL_KREMLIN)/, $(HACL_FILES))
HACL_API=$(HACL_HOME)/code/api
HACL_CRYPTO_UTILS=$(HACL_HOME)/code/lib
ifeq ($(CI),true)
VERBOSE=
else
VERBOSE=-verbose
endif
#
# Kremlin
#
KREMLIB=$(KREMLIN_HOME)/kremlib/compat
KREMLIN=$(KREMLIN_HOME)/krml
KREMTEST=$(KREMLIN_HOME)/test
# Default Kremlin arguments
KREMLIN_ARGS?=
KREMLIN_ARGS+=$(KOPTS)
KREMLIN_ARGS+=-I $(HACL_KREMLIN) -I $(KREMLIB) -I $(HACL_HOME)/specs -I $(HACL_HOME)/specs/old -I .
ifneq (,$(EVEREST_WINDOWS))
KREMLIN_ARGS+=-fparentheses -falloca -ftail-calls
endif
# Compiler options
ifdef USE_CCOMP
KREMLIN_ARGS+=-cc compcert $(VERBOSE)
else ifdef USE_CL
KREMLIN_ARGS+=-cc msvc $(VERBOSE)
else
KREMLIN_ARGS+=-ccopt -march=native $(VERBOSE) -ldopt -flto
endif
# License header
ifdef HACL_LICENSE
KREMLIN_ARGS+=-header $(HACL_LICENSE)
endif
#
# FStar
#
FSTAR_LIB=$(FSTAR_HOME)/ulib
HINTS_ENABLED?=--use_hints
FSTAR_INCLUDES+=--include $(HACL_KREMLIN) --include $(KREMLIB) --include $(HACL_HOME)/specs --include $(HACL_HOME)/specs/old
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(HINTS_ENABLED) $(OTHERFLAGS) $(FSTAR_INCLUDES)
#
# Azure cloud verification
#
ifdef CLOUD_VERIFY
BATCH_JOB_ID=$(subst job-id:,,$(filter job-id:%, $(shell cat $(BATCH_ID_FILE))))
BATCH_OUTPUT_SAS=$(subst output-sas:,,$(filter output-sas:%, $(shell cat $(BATCH_ID_FILE))))
EABC=python /mnt/f/dev/sec/eabc/eabc.py
CURRENT_SUBDIR:=$(subst $(HACL_HOME)/,,$(abspath $(shell pwd)))
BATCH_ADD_CMD=$(EABC) add -d "hacl-star/$(CURRENT_SUBDIR)" $(EABC_EXTRA) "$(BATCH_OUTPUT_SAS)" $(BATCH_JOB_ID)
BATCH_RUN_CMD=$(EABC) run -d "hacl-star/$(CURRENT_SUBDIR)" $(EABC_EXTRA) "$(BATCH_OUTPUT_SAS)" $(BATCH_JOB_ID)
BATCH_CMD=$(BATCH_ADD_CMD)
FSTAR_RELATIVIZED=$(subst $(abspath $(HACL_HOME)/..),\$$H,$(HINTS_ENABLED) $(OTHERFLAGS) $(FSTAR_INCLUDES))
FSTAR=$(BATCH_CMD) \$$H/FStar/bin/fstar.exe $(FSTAR_RELATIVIZED)
KREMLIN=$(BATCH_CMD) \$$H/kremlin/krml
endif
include $(FSTAR_HOME)/ulib/ml/Makefile.include
#
# OCaml
#
OCAMLOPT:=$(OCAMLOPT) -thread -package batteries,zarith,stdint -w -20-26-3-8-58
OCAML_OPTIONS=-fsopt "--lax" -fsopt "--codegen OCaml" -fsopt "--no_location_info"
#
# 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
#
# HACL* generalized targets
#
ml-lib:
$(MAKE) -C $(ULIB_ML)
import-lib:
@cp $(HACL_LIB_FILES) .
import-kremlin:
@cp $(HACL_KREMLIN_FILES)) .
%.fst-lax: %.fst
$(FSTAR) --lax $^
%.fsti-lax: %.fsti
$(FSTAR) --lax $^
%.fst-krml: %.fst
$(KREMLIN) $(KREMLIN_ARGS) $(KREMLIN_INCLUDES) $<
%.fst-verify: %.fst
$(FSTAR) $<
%.fsti-verify: %.fsti
$(FSTAR) $<
%.fst-in: %.fst
@echo --hint_info \
$(HINTS_ENABLED) \
$(OTHERFLAGS) \
$(FSTAR_INCLUDES)
%.fsti-in: %.fsti
@echo --hint_info \
$(HINTS_ENABLED) \
$(OTHERFLAGS) \
$(FSTAR_INCLUDES)
%.fst.hints: %.fst
$(FSTAR) --record_hints --z3rlimit_factor 5 $<
%.fsti.hints: %.fsti
$(FSTAR) --record_hints --z3rlimit_factor 5 $<
# Custom verification targets for re-located hint files
%.fst-reloc-verify: %.fst
$(FSTAR) --hint_file $(subst -reloc-verify,,$(@F)).hints $<
%.fsti-reloc-verify: %.fsti
$(FSTAR) --hint_file $(subst -reloc-verify,,$(@F)).hints $<
%.fst.reloc.hints: %.fst
$(FSTAR) --hint_file $(subst .reloc,,$(@F)) --record_hints $<
%.fsti.reloc.hints: %.fsti
$(FSTAR) --hint_file $(subst .reloc,,$(@F)) --record_hints $<
# Interactive verification
%.fst-in: %.fst
@echo --hint_info \
$(HINTS_ENABLED) \
$(OTHERFLAGS) \
$(FSTAR_INCLUDES)
%.fsti-in: %.fsti
@echo --hint_info \
$(HINTS_ENABLED) \
$(OTHERFLAGS) \
$(FSTAR_INCLUDES)
# Directories
%.dir-verify: %
$(MAKE) -C $^ verify
%.dir-extract-c: %
$(MAKE) -C $^ extract-c
%.dir-hints: %
$(MAKE) -C $^ hints
# Colors
NORMAL="\\033[0;39m"
CYAN="\\033[1;36m"