-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathMakefile
95 lines (64 loc) · 3.27 KB
/
Makefile
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
# Paths inside docker container
FSTAR_HOME ?= /home/build/FStar
DY_HOME ?= /home/build/dolev-yao-star
CACHE_DIR ?= $(DY_HOME)/.cache/symbolic
HINT_DIR ?= $(DY_HOME)/.hints/symbolic
.PHONY: all verify clean
all:
rm -f .depend.symbolic && $(MAKE) .depend.symbolic
$(MAKE) verify
COMPARSE_LIB_FILES = Comparse.Bytes.Typeclass Comparse.Utils Comparse.Parser.Builtins Comparse.Parser.Typeclass Comparse.Parser.Derived
COMPARSE_LIB_FST_FILES=$(addprefix $(DY_HOME)/comparse/,$(addsuffix .fst,$(COMPARSE_LIB_FILES)))
COMPARSE_LIB_CMX_FILES = $(addprefix ocaml-symbolic/,$(addsuffix .cmx,$(subst .,_,$(COMPARSE_LIB_FILES))))
LIB_BASE_FST_FILES = $(COMPARSE_LIB_FST_FILES) $(addprefix $(DY_HOME)/,Ord.fst SecrecyLabels.fst CryptoEffect.fst GlobalRuntimeLib.fst LabeledRuntimeAPI.fst LabeledPKI.fst AttackerAPI.fst SerializationHelpers.fst RelaxLabels.fst ComparseGlue.fst SecurityLemmas.fst) $(addprefix $(DY_HOME)/symbolic/,CryptoLib.fst LabeledCryptoAPI.fst)
LIB_BASE_CMX_FILES = $(COMPARSE_LIB_CMX_FILES) ocaml-symbolic/Ord.cmx ocaml-symbolic/SecrecyLabels.cmx ocaml-symbolic/CryptoLib.cmx ocaml-symbolic/CryptoEffect.cmx ocaml-symbolic/GlobalRuntimeLib.cmx ocaml-symbolic/LabeledCryptoAPI.cmx ocaml-symbolic/LabeledRuntimeAPI.cmx ocaml-symbolic/LabeledPKI.cmx ocaml-symbolic/AttackerAPI.cmx ocaml-symbolic/SerializationHelpers.cmx ocaml-symbolic/RelaxLabels.cmx ocaml-symbolic/ComparseGlue.cmx ocaml-symbolic/SecurityLemmas.cmx
FSTAR_INCLUDE_DIRS = $(DY_HOME) $(DY_HOME)/symbolic $(DY_HOME)/comparse
FSTAR_FLAGS = --cmi \
--warn_error -331 \
--cache_checked_modules --cache_dir $(CACHE_DIR) \
--already_cached "+Prims +FStar +LowStar +C +Spec.Loops +TestLib" \
$(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
ALL_SOURCES = $(wildcard *.fst) $(wildcard *.fsti)
ROOTS = $(filter-out $(FIXME),$(ALL_SOURCES))
.depend.symbolic: $(HINT_DIR) $(CACHE_DIR)
$(info $(ROOTS))
$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
include .depend.symbolic
$(HINT_DIR):
mkdir -p $@
$(CACHE_DIR):
mkdir -p $@
$(CACHE_DIR)/%.checked: | .depend.symbolic $(HINT_DIR) $(CACHE_DIR)
$(FSTAR) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
# Targets for interactive mode
%.fst-in:
$(info $(FSTAR_FLAGS) \
$(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
%.fsti-in:
$(info $(FSTAR_FLAGS) \
$(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
#OCaml extraction
CODEGEN=OCaml
ifeq ($(OS),Windows_NT)
export OCAMLPATH := $(FSTAR_HOME)/lib;$(OCAMLPATH)
else
export OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
endif
OCAMLOPT = ocamlfind opt -package fstar.lib -thread -linkpkg -g -I ocaml-symbolic -w -8-20-26
OCAMLSHARED = ocamlfind opt -shared -package fstar.lib -g -I ocaml-symbolic -w -8-20-26
.PRECIOUS: %.ml
%.ml:
$(FSTAR) --codegen $(CODEGEN) \
--include .. --odir ocaml-symbolic --extract_module $(basename $(notdir $(subst _,.,$@))) \
$(notdir $(subst _,.,$(subst .ml,.fst,$@)))
%.cmx: %.ml
$(OCAMLOPT) -c $< -o $@
# Clean targets
SHELL=/bin/bash
clean:
rm -rf ocaml-symbolic *~
distclean: clean
rm -rf .cache/*