https://github.com/project-everest/hacl-star
Tip revision: abe760c66f85d0a1db1ec028c157486ac3ada695 authored by Santiago Zanella-Beguelin on 10 October 2018, 17:13:02 UTC
Tweaks
Tweaks
Tip revision: abe760c
Makefile.include
UNAME := $(shell uname)
.DEFAULT_GOAL=all
ifndef HACL_HOME
HACL_HOME:=$(abspath $(dir $(lastword $(MAKEFILE_LIST))))
HACL_HOME:=$(HACL_HOME:/=)
endif
ifndef FSTAR_HOME
FSTAR_HOME:=$(HACL_HOME)/../FStar
endif
ifndef KREMLIN_HOME
KREMLIN_HOME:=$(HACL_HOME)/../kremlin
endif
export HACL_HOME
export FSTAR_HOME
export KREMLIN_HOME
# $(info $(HACL_HOME))
# $(info $(FSTAR_HOME))
# $(info $(KREMLIN_HOME))
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 $(KREMLIN_HOME)/kremlib/compat -I $(HACL_KREMLIN) -I $(KREMLIB) -I $(HACL_HOME)/specs -I .
ifneq (,$(EVEREST_WINDOWS))
KREMLIN_ARGS+=-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
# BB. Check if this is necessary
# Release mode (includes testlib if not release)
ifdef HACL_RELEASE
KREMLIN_TESTLIB=
else
KREMLIN_TESTLIB=-add-include '"extracted/TestLib.h"' $(KREMLIB)/c/testlib.c
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_HOME)/lib \
--include $(HACL_HOME)/lib/fst \
--include $(HACL_HOME)/specs \
--query_stats
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(HINTS_ENABLED) $(OTHERFLAGS) $(FSTAR_INCLUDES)
include $(FSTAR_HOME)/ulib/ml/Makefile.include
#
# OCaml
#
OCAMLOPT:=$(OCAMLOPT) -thread -package batteries,zarith,stdint -w -20-26-3-8-58
#
# 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-8 >/dev/null 2>&1 && echo gcc-8 || (which gcc-7 >/dev/null 2>&1 && echo gcc-7 || 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-verify: %.fst
$(FSTAR) $<
%.fsti-verify: %.fsti
$(FSTAR) $<
%.fst-in:
@echo --hint_info \
$(HINTS_ENABLED) \
$(OTHERFLAGS) \
$(FSTAR_INCLUDES)
%.fsti-in:
@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 $<
# 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"