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
KREMLIN=$(KREMLIN_HOME)/krml
KREMTEST=$(KREMLIN_HOME)/test


# Default Kremlin arguments
KREMLIN_ARGS?=
KREMLIN_ARGS+=$(KOPTS)
KREMLIN_ARGS+=-I $(HACL_KREMLIN) -I $(KREMLIB)/compat -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)/compat --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"