-
Notifications
You must be signed in to change notification settings - Fork 160
/
Makefile.include
134 lines (108 loc) · 3.79 KB
/
Makefile.include
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
UNAME := $(shell uname)
.DEFAULT_GOAL=all
ifndef HACL_HOME
HACL_HOME:=$(abspath $(dir $(lastword $(MAKEFILE_LIST)))/..)
else
HACL_HOME:=$(abspath $(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=$(KREMLIN_HOME)/krml
KREMLIN_ARGS?=
# Pass parameters to kremlin from the command-line
KREMLIN_ARGS+=$(KOPTS)
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
# Linux specific compilation instruction for PneuTube
ifeq ($(UNAME), Linux)
KREMLIN_ARGS+=-ccopt -D_GNU_SOURCE
endif
KREMLIB=$(KREMLIN_HOME)/kremlib
KREMTEST=$(KREMLIN_HOME)/test
KREMLIN_ARGS+=-I $(HACL_KREMLIN) -I $(KREMLIB) -I $(HACL_HOME)/specs -I .
KREMLIN_TESTLIB=-add-include '"testlib.h"' $(KREMLIB)/testlib.c
FSTAR_LIB=$(FSTAR_HOME)/ulib
HINTS_ENABLED?=--use_hints
FSTAR_INCLUDES+=--include $(HACL_KREMLIN) --include $(KREMLIB) --include $(HACL_HOME)/specs
ifndef CLOUD_VERIFY
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(HINTS_ENABLED) $(OTHERFLAGS) $(FSTAR_INCLUDES)
export BATCH_ID_FILE:=
else
export BATCH_ID_FILE:=$(HACL_HOME)/batch_id.tmp
EABC=python /mnt/f/dev/sec/eabc/eabc.py
CURRENT_SUBDIR:=$(subst $(HACL_HOME)/,,$(abspath $(shell pwd)))
$(BATCH_ID_FILE):
$(info CREATING)
$(EABC) create > $@
BATCH_JOB_ID=$(subst job-id:,,$(filter job-id:%, $(shell cat $(BATCH_ID_FILE))))
FSTAR=$(EABC) -j $(BATCH_JOB_ID) -d 'hacl-star/$(CURRENT_SUBDIR)' $(EABC_EXTRA) add -- \$$H/FStar/bin/fstar.exe $(HINTS_ENABLED) $(OTHERFLAGS) $(FSTAR_INCLUDES)
KREMLIN=$(EABC) -j $(BATCH_JOB_ID) -d 'hacl-star/$(CURRENT_SUBDIR)' $(EABC_EXTRA) add -- \$$H/kremlin/krml
# $(info goals: $(MAKECMDGOALS))
# $(MAKECMDGOALS): $(BATCH_ID_FILE)
# .PHONY: BATCH_CLEANUP
# BATCH_CLEANUP: $(MAKECMDGOALS)
# $(info CLEANUP)
endif
include $(FSTAR_HOME)/ulib/ml/Makefile.include
OCAMLOPT:=$(OCAMLOPT) -thread -package batteries,zarith,stdint -w -20-26-3-8-58
OCAML_OPTIONS=-fsopt "--lax" -fsopt "--codegen OCaml" -fsopt "--no_location_info"
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 $(BATCH_ID_FILE)
$(FSTAR) $< 2>&1
%.fsti-verify: %.fsti $(BATCH_ID_FILE)
$(FSTAR) $< 2>&1
%.fst.hints: %.fst $(BATCH_ID_FILE)
$(FSTAR) --record_hints $< 2>&1
%.fsti.hints: %.fsti $(BATCH_ID_FILE)
$(FSTAR) --record_hints $< 2>&1
# Custom verification targets for re-located hint files
%.fst-reloc-verify: %.fst $(BATCH_ID_FILE)
$(FSTAR) --hint_file $(subst -reloc-verify,,$(@F)).hints $^ 2>&1
%.fsti-reloc-verify: %.fsti $(BATCH_ID_FILE)
$(FSTAR) --hint_file $(subst -reloc-verify,,$(@F)).hints $^ 2>&1
%.fst.reloc.hints: %.fst $(BATCH_ID_FILE)
$(FSTAR) --hint_file $(subst .reloc,,$(@F)) --record_hints $^ 2>&1
%.fsti.reloc.hints: %.fsti $(BATCH_ID_FILE)
$(FSTAR) --hint_file $(subst .reloc,,$(@F)) --record_hints $^ 2>&1