-
Notifications
You must be signed in to change notification settings - Fork 21
/
Copy pathMakefile
133 lines (96 loc) · 4.31 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
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
HOLBA_DIR = .
include $(HOLBA_DIR)/scripts/setup/env_base.mk
include $(HOLBA_DIR)/scripts/setup/env_check_hol4.mk
# set make's shell to bash
SHELL := /bin/bash
##########################################################
SRCDIR = src
EXSDIR = examples
EXAMPLES_BASE = $(SRCDIR)/shared/examples \
$(SRCDIR)/tools/cfg/examples \
$(SRCDIR)/tools/exec/examples \
$(SRCDIR)/tools/lifter/examples \
$(SRCDIR)/tools/wp/examples
EXAMPLES_ALL = $(EXAMPLES_BASE) \
$(EXSDIR)
BENCHMARKS = $(SRCDIR)/tools/lifter/benchmark \
$(SRCDIR)/tools/wp/benchmark
##########################################################
# recursive wildcard function
rwildcard=$(wildcard $1$2) $(foreach d,$(wildcard $1*),$(call rwildcard,$d/,$2))
HOLMAKEFILES = $(call rwildcard,$(SRCDIR)/,Holmakefile) \
$(call rwildcard,$(EXSDIR)/,Holmakefile)
ifdef HOLBA_HOLMAKE
HOLMAKEFILE_DIRS = $(patsubst %/,%,$(sort $(foreach file,$(HOLMAKEFILES),$(dir $(file)))))
HOLMAKEFILE_CLEANS = $(foreach holmfld,$(HOLMAKEFILE_DIRS),$(holmfld)_clean)
SML_RUNS = $(foreach sml,$(call rwildcard,$(SRCDIR)/,*.sml),$(sml)_run) \
$(foreach sml,$(call rwildcard,$(EXSDIR)/,*.sml),$(sml)_run)
TEST_SMLS = $(call rwildcard,$(SRCDIR)/,selftest.sml) $(call rwildcard,$(SRCDIR)/,selftest_*.sml) $(call rwildcard,$(SRCDIR)/,test-*.sml) \
$(call rwildcard,$(EXSDIR)/,selftest.sml) $(call rwildcard,$(EXSDIR)/,selftest_*.sml) $(call rwildcard,$(EXSDIR)/,test-*.sml)
TEST_EXES = $(TEST_SMLS:.sml=.exe)
TEST_SML_RUNQS = $(TEST_SMLS:.sml=.sml_runq)
TEST_DIRS = $(patsubst %/,%,$(sort $(foreach sml,$(TEST_SMLS),$(dir $(sml)))))
endif
##########################################################
.DEFAULT_GOAL := all
all: show-rules
@echo 'Please use sub-rules to build HolBA.'
show-rules:
@echo 'Available rules:'
ifdef HOLBA_HOLMAKE
@echo ' - theory: builds only src/theory/'
@echo ' - main: builds HolBA, but without the examples or documentation'
@echo ' - tests: builds HolBA and runs all the tests'
@echo ' - examples-base: builds HolBA and the examples for each tool'
@echo ' - examples-all: builds HolBA and all the examples (base + HolBA/examples/)'
@echo ' - benchmarks: builds HolBA and all the benchmarks'
endif
@echo ' - gendoc: generate the documentation'
@echo ' - cleanslate: removes all files that are .gitignore-d under src/ and examples/'
##########################################################
$(HOLMAKEFILE_DIRS): $(HOLMAKEFILES)
source ./scripts/setup/env_derive.sh && cd $@ && $(HOLBA_HOLMAKE) $(HOLBA_HOLMAKE_OPTS)
$(HOLMAKEFILE_CLEANS):
cd $(patsubst %_clean,%,$@) && $(HOLBA_HOLMAKE) clean && $(HOLBA_HOLMAKE) cleanAll
%.exe: %.sml $(HOLMAKEFILES)
@/usr/bin/env HOLBA_HOLMAKE="$(HOLBA_HOLMAKE)" ./scripts/mk-exe.sh $(@:.exe=.sml)
# this is a target for all sml files to run as scripts,
# it properly prepares first
# it also tries to find the undefined environment variables
$(SML_RUNS):
@make $(patsubst %/,%,$(dir $@))
@make $(@:.sml_run=.exe)
@source ./scripts/setup/env_derive.sh && ./scripts/run-test.sh $(@:.sml_run=.exe)
# this target is for quick running, mainly for the run-tests.sh
# (no environment preparation, it assumes that all
# TEST_DIRS are "made" and env.sh has been sourced)
%.sml_runq:
@./scripts/run-test.sh $(@:.sml_runq=.exe)
##########################################################
ifdef HOLBA_HOLMAKE
theory: $(SRCDIR)/theory
main: $(SRCDIR)
examples-base: main $(EXAMPLES_BASE)
examples-all: main $(EXAMPLES_ALL)
benchmarks: main $(BENCHMARKS)
riscv: main src/tools/symbexec/examples/riscv
tests: $(TEST_EXES) $(TEST_DIRS)
@source ./scripts/setup/env_derive.sh && ./scripts/run-tests.sh
# this target can be made with multiple jobs, the others cannot!
_run_tests: $(TEST_SML_RUNQS)
endif
gendoc:
cd doc/gen; ./dependencies.py
cleanslate:
git clean -fdX src
git clean -fdX examples
##########################################################
ifdef HOLBA_HOLMAKE
.PHONY: $(HOLMAKEFILE_DIRS)
.PHONY: $(SML_RUNS)
.PHONY: theory main
.PHONY: tests _run_tests
.PHONY: examples-base examples-all
.PHONY: benchmarks
endif
.PHONY: gendoc cleanslate