forked from evdenis/verker
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
309 lines (232 loc) · 13 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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
export TIMEOUT ?= 10
export PROCESSES ?= 4
AV_WHY3_CONF := $(PWD)/astraver.why3.conf
CC := gcc
CFLAGS := -Wall -Werror
CLANG := clang
CLANGFLAGS := -g -O1
GEN_CFLAGS := -w
FUZZ_CFLAGS := -fsanitize=fuzzer,address -DFUZZ_MAIN
EXT_CFLAGS := -DDUMMY_MAIN
SPEC_CFLAGS := -DSPEC
BINDIR := bin
FUZZDIR := fzz
GENDIR := gen
EACSLDIR := $(GENDIR)/eacsl
RTEDIR := $(GENDIR)/rte
VALDIR := $(GENDIR)/val
GENBINDIR := $(BINDIR)/gen
EACSLBINDIR := $(GENBINDIR)/eacsl
EACSLFUZZDIR := $(FUZZDIR)/eacsl
OPAM_EVAL := eval $$(opam config env)
#FRAMAC := $(OPAM_EVAL); frama-c-gui -c11 -pp-annot -cpp-extra-args " -CC -E -x c $(SPEC_CFLAGS) " -machdep gcc_x86_64
FRAMAC := $(OPAM_EVAL); frama-c -c11 -pp-annot -cpp-extra-args " -CC -E -x c $(SPEC_CFLAGS) " -machdep gcc_x86_64
FRAMAC_NOHUP := $(OPAM_EVAL); nohup frama-c -c11 -pp-annot -cpp-extra-args " -CC -E -x c $(SPEC_CFLAGS) " -machdep gcc_x86_64
#FRAMAC_DFLAGS :=
#FRAMAC_DFLAGS := -wp
FRAMAC_DFLAGS := -av
FRAMAC_VFLAGS := -av-why3-opt " --extra-config $(AV_WHY3_CONF) "
FRAMAC_UFLAGS := -av -av-target update
FRAMAC_REPLAY := -av-target why3autoreplay
FRAMAC_SPROVE := -av-target why3sprove -av-why3-opt
SPROVE_EXTRA := --extra-config $(AV_WHY3_CONF) --strategy verker --theory-filter axiom
FRAMAC_EFLAGS := -e-acsl -main LLVMFuzzerTestOneInput -pp-annot -cpp-extra-args " -CC -E -x c -DFUZZ_MAIN "
FRAMAC_EGEN := -then-last -print -ocode
FRAMAC_RTEFLAGS := -rte -main LLVMFuzzerTestOneInput -pp-annot -cpp-extra-args " -CC -E -x c -DFUZZ_MAIN "
FRAMAC_VALFLAGS := -val -main LLVMFuzzerTestOneInput -pp-annot -cpp-extra-args " -CC -E -x c -DFUZZ_MAIN "
FRAMAC_RTEGEN := -print -ocode
FRAMAC_VALGEN := $(FRAMAC_RTEGEN)
FRAMAC_ESHARE := $(shell $(FRAMAC) -print-share-path)/e-acsl
FRAMAC_EMSHARE := $(shell $(FRAMAC) -print-share-path)/e-acsl/memory_model
FRAMAC_LIBPATH := $(shell $(FRAMAC) -print-lib-path)
FRAMAC_EACSL_LIB := -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_IDENTIFY -std=c99 -m64 -I$(FRAMAC_ESHARE) $(FRAMAC_ESHARE)/e_acsl_mmodel.c -lm -lpthread $(FRAMAC_LIBPATH)/../libeacsl-gmp.a $(FRAMAC_LIBPATH)/../libeacsl-jemalloc.a
SRCFILES := $(sort $(shell find ./src -maxdepth 1 -type f \! -name '*.pp.c' -name '*.c'))
SRCFILES_H := $(patsubst %.c, %.h, $(SRCFILES))
FZZAVAILFILES := $(sort $(shell grep -nre '|[[:space:]]\+[[:digit:]]\+[[:space:]]\+|' ./README.md | cut -d '|' -f 3,6 | grep yes | cut -d '|' -f 1 | tr -d ' \\' | sed -e 's/$$/.c/' -e 's!^!./src/!'))
BINAVAILFILES := $(sort $(shell grep -nre '|[[:space:]]\+[[:digit:]]\+[[:space:]]\+|' ./README.md | cut -d '|' -f 3 | tr -d ' \\' | sed -e 's/$$/.c/' -e 's!^!./src/!'))
PROVEDFILES := $(sort $(shell grep -nre '|[[:space:]]\+[[:digit:]]\+[[:space:]]\+|' ./README.md | cut -d '|' -f 3,4 | grep proved | cut -d '|' -f 1 | tr -d ' \\' | sed -e 's/$$/.c/' -e 's!^!./src/!'))
PROVEDFILES_H := $(patsubst %.c, %.h, $(PROVEDFILES))
BINFILES := $(patsubst ./src/%.c, $(BINDIR)/%, $(BINAVAILFILES))
FUZZFILES := $(patsubst ./src/%.c, $(FUZZDIR)/%, $(FZZAVAILFILES))
EACSLFILES := $(patsubst ./src/%.c, $(EACSLDIR)/%.c, $(BINAVAILFILES))
EACSLPROVEDFILES := $(patsubst ./src/%.c, $(EACSLDIR)/%.c, $(PROVEDFILES))
RTEFILES := $(patsubst ./src/%.c, $(RTEDIR)/%.c, $(SRCFILES))
VALFILES := $(patsubst ./src/%.c, $(VALDIR)/%.c, $(SRCFILES))
EACSLBINFILES := $(patsubst $(EACSLDIR)/%.c, $(EACSLBINDIR)/%, $(EACSLFILES))
EACSLBINPROVEDFILES := $(patsubst $(EACSLDIR)/%.c, $(EACSLBINDIR)/%, $(EACSLPROVEDFILES))
EACSLFUZZFILES := $(patsubst $(EACSLDIR)/%.c, $(EACSLFUZZDIR)/%, $(EACSLFILES))
EACSLFUZZPROVEDFILES := $(patsubst $(EACSLDIR)/%.c, $(EACSLFUZZDIR)/%, $(EACSLPROVEDFILES))
all: build ## Default target
build: $(BINDIR) $(BINFILES) ## Build each program.
fuzz: $(FUZZDIR) $(FUZZFILES) ## Fuzz each program.
eacsl: $(GENDIR) $(EACSLDIR) $(EACSLFILES) ## Generate E-ACSL programs.
eacsl-proved: $(GENDIR) $(EACSLDIR) $(EACSLPROVEDFILES) ## Generate E-ACSL for proved programs.
eacsl-build: eacsl $(GENBINDIR) $(EACSLBINDIR) $(EACSLBINFILES) ## Build generated E-ACSL programs.
eacsl-proved-build: eacsl-proved $(GENBINDIR) $(EACSLBINDIR) $(EACSLBINPROVEDFILES) ## Build E-ACSL proved programs.
eacsl-fuzz: eacsl $(EACSLDIR) $(FUZZDIR) $(EACSLFUZZDIR) $(EACSLFUZZFILES) ## Build generated E-ACSL programs with libfuzzer.
eacsl-proved-fuzz: eacsl-proved $(EACSLDIR) $(FUZZDIR) $(EACSLFUZZDIR) $(EACSLFUZZPROVEDFILES) ## Build E-ACSL proved programs with libfuzzer.
rte: $(GENDIR) $(RTEDIR) $(RTEFILES) ## Generate RTE specifications.
val: $(GENDIR) $(VALDIR) $(VALFILES) ## Run value analysis.
$(BINDIR):
@-mkdir -p $(BINDIR)
$(FUZZDIR):
@-mkdir -p $(FUZZDIR)
$(GENDIR):
@-mkdir -p $(GENDIR)
$(EACSLDIR):
@-mkdir -p $(EACSLDIR)
$(RTEDIR):
@-mkdir -p $(RTEDIR)
$(VALDIR):
@-mkdir -p $(VALDIR)
$(GENBINDIR):
@-mkdir -p $(GENBINDIR)
$(EACSLBINDIR):
@-mkdir -p $(EACSLBINDIR)
$(EACSLFUZZDIR):
@-mkdir -p $(EACSLFUZZDIR)
$(BINDIR)/skip_spaces: $(BINDIR)/ctype.o src/skip_spaces.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/strlcpy: $(BINDIR)/memcpy.o src/strlcpy.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/strim: $(BINDIR)/skip_spaces.o $(BINDIR)/ctype.o src/strim.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/_parse_integer_fixup_radix: $(BINDIR)/ctype.o src/_parse_integer_fixup_radix.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/strcasecmp: $(BINDIR)/ctype.o src/strcasecmp.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/strncasecmp: $(BINDIR)/ctype.o src/strncasecmp.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/strnstr: $(BINDIR)/memcmp.o $(BINDIR)/strlen.o src/strnstr.c
$(CC) $(CFLAGS) $(EXT_CFLAGS) $^ -o $@
$(BINDIR)/%.o: src/%.c src/%.h
$(CC) $(CFLAGS) -c $< -o $@
$(BINDIR)/%: src/%.c src/%.h
$(CC) $(CFLAGS) $(EXT_CFLAGS) $< -o $@
$(FUZZDIR)/%.o: src/%.c src/%.h
$(CLANG) $(CLANGFLAGS) -c $< -o $@
$(FUZZDIR)/skip_spaces: $(FUZZDIR)/ctype.o src/skip_spaces.c
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $^ -o $@
$(FUZZDIR)/_parse_integer_fixup_radix: $(FUZZDIR)/ctype.o src/_parse_integer_fixup_radix.c
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $^ -o $@
$(FUZZDIR)/strcasecmp: $(FUZZDIR)/ctype.o src/strcasecmp.c
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $^ -o $@
$(FUZZDIR)/strncasecmp: $(FUZZDIR)/ctype.o src/strncasecmp.c
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $^ -o $@
$(FUZZDIR)/strstr: $(FUZZDIR)/memcmp.o src/strstr.c
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $^ -o $@
$(FUZZDIR)/strnstr: $(FUZZDIR)/memcmp.o $(FUZZDIR)/strlen.o src/strnstr.c
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $^ -o $@
$(FUZZDIR)/%: src/%.c src/%.h
$(CLANG) $(CLANGFLAGS) $(FUZZ_CFLAGS) $< -o $@
$(EACSLDIR)/%.c: src/%.c
$(FRAMAC) $(FRAMAC_EFLAGS) $< $(FRAMAC_EGEN) $@
$(RTEDIR)/%.c: src/%.c
$(FRAMAC) $(FRAMAC_RTEFLAGS) $< $(FRAMAC_RTEGEN) $@
$(VALDIR)/%.c: src/%.c
$(FRAMAC) $(FRAMAC_VALFLAGS) $< $(FRAMAC_VALGEN) $@
$(GENBINDIR)/%: $(GENDIR)/%.c
$(CC) $(GEN_CFLAGS) $(FRAMAC_EACSL_LIB) $< -o $@
$(EACSLFUZZDIR)/%: $(EACSLDIR)/%.c
$(CLANG) $(CLANGFLAGS) $(GEN_CFLAGS) $(FUZZ_CFLAGS) $(FRAMAC_EACSL_LIB) $< -o $@
fuzz-%: $(FUZZDIR) $(FUZZDIR)/%
$(FUZZDIR)/$*
run: build ## Run each program. You can also type run-<target>.
@for i in $(BINFILES); do echo $$i; ./$$i; done
run-%: $(BINDIR) $(BINDIR)/%
$(BINDIR)/$*
eacsl-run: eacsl-build ## Run each E-ACSL program. You can also type eacsl-run-<target>.
@for i in $(GENBINFILES); do echo $$i; ./$$i; done
eacsl-run-%: $(GENDIR) $(GENBINDIR) $(GENBINDIR)/%
$(GENBINDIR)/$*
eacsl-fuzz-%: $(FUZZDIR) $(GENDIR) $(EACSLDIR) $(EACSLFUZZDIR) $(EACSLFUZZDIR)/%
$(EACSLFUZZDIR)/$*
verify: $(AV_WHY3_CONF) ## Run Frama-C on all files simultaneously. You can also type verify-<target>.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_VFLAGS) $(SRCFILES) $(SRCFILES_H) -av-out sessions/all.av
verify-separatedly: $(AV_WHY3_CONF) ## Run Frama-C on each file consequently.
@for i in $(SRCFILES); do i=$$(basename $$i .c); echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_VFLAGS) src/$$i.c src/$$i.h -av-out sessions/$$i.av; done
verify-proved: $(AV_WHY3_CONF) ## Run Frama-C on each file consequently. Only completely proved functions.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_VFLAGS) $(PROVEDFILES) $(PROVEDFILES_H) -av-out sessions/proved.av
verify-proved-separatedly: $(AV_WHY3_CONF) ## Run Frama-C on each file consequently. Only completely proved functions.
@for i in $(PROVEDFILES); do i=$$(basename $$i .c); echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_VFLAGS) src/$$i.c src/$$i.h -av-out sessions/$$i.av; done
verify-%: $(AV_WHY3_CONF)
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_VFLAGS) src/$*.c src/$*.h -av-out sessions/$*.av
update-%:
@$(FRAMAC) $(FRAMAC_UFLAGS) src/$*.c src/$*.h -av-out sessions/$*.av
replay: ## Replay proofs simultaiously. You can also type replay-<target>.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) $(SRCFILES) $(SRCFILES_H) -av-out sessions/all.av
replay-separatedly: ## Replay proofs consequently.
@for i in $(SRCFILES); do i=$$(basename $$i .c); echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) src/$$i.c src/$$i.h -av-out sessions/$$i.av; done
replay-proved: ## Replay proofs for completely proved functions.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) $(PROVEDFILES) $(PROVEDFILES_H) -av-out sessions/proved.av
replay-proved-separatedly: ## Replay proved functions consequently.
@FAIL=0; for i in $(PROVEDFILES); do i=$$(basename $$i .c); $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) src/$$i.c src/$$i.h -av-out sessions/$$i.av > /dev/null 2>&1 && echo "OK: $$i" || { echo "FAIL: $$i"; FAIL=1; }; done; if [ $$FAIL -eq 1 ]; then exit 1; fi
replay-%:
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) src/$*.c src/$*.h -av-out sessions/$*.av
define av_why3conf
[main]
running_provers_max = $(PROCESSES)
[strategy]
code = "
start:
c Alt-Ergo,, 2 2000
c CVC4,,noBV 2 2000
c CVC4,, 2 2000
c Eprover,, 2 2000
t split_goal_wp start
t introduce_premises next1
next1:
t inline_all next2
next2:
t eliminate_if next3
next3:
t remove_triggers start
c Alt-Ergo,, $(TIMEOUT) 8000
c CVC4,,noBV $(TIMEOUT) 8000
c CVC4,, $(TIMEOUT) 8000
c Eprover,, $(TIMEOUT) 8000"
desc = "Strategy for Verker examples"
name = "verker"
endef
export av_why3conf
$(AV_WHY3_CONF):
@if [ -f $@ ]; then \
tfile=$(shell mktemp); \
echo "$$av_why3conf" > $$tfile; \
diff -q $@ $$tfile > /dev/null || mv $$tfile $@; \
else echo "$$av_why3conf" > $@; fi
sprove: $(AV_WHY3_CONF) ## Replay proofs simultaiously. You can also type sprove-<target>.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_SPROVE) " $(SPROVE_EXTRA) --session $(PWD)/sessions/all.av/whole_program" $(SRCFILES) $(SRCFILES_H) -av-out sessions/all.av
sprove-separatedly: $(AV_WHY3_CONF) ## Replay proofs consequently.
@for i in $(SRCFILES); do i=$$(basename $$i .c); echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_SPROVE) " $(SPROVE_EXTRA) --session $(PWD)/sessions/$$i.av/whole_program" src/$$i.c src/$$i.h -av-out sessions/$$i.av; done
sprove-proved: $(AV_WHY3_CONF) ## Run sprove strategy on proved functions.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_SPROVE) " $(SPROVE_EXTRA) --session $(PWD)/sessions/proved.av/whole_program" $(PROVEDFILES) $(PROVEDFILES_H) -av-out sessions/proved.av
sprove-proved-separatedly: $(AV_WHY3_CONF) ## Run sprove strategy on proved functions separatedly.
@for i in $(PROVEDFILES); do i=$$(basename $$i .c); echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_SPROVE) " $(SPROVE_EXTRA) --session $(PWD)/sessions/$$i.av/whole_program" src/$$i.c src/$$i.h -av-out sessions/$$i.av; done
sprove-%: $(AV_WHY3_CONF)
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_SPROVE) " $(SPROVE_EXTRA) --session $(PWD)/sessions/$*.av/whole_program" src/$*.c src/$*.h -av-out sessions/$*.av
clean: ## Remove all binary and generated files.
-rm -fr $(AV_WHY3_CONF) $(GENBINDIR) $(RTEDIR) $(VALDIR) $(EACSLDIR) $(BINDIR) $(GENDIR) $(FUZZDIR) src/*.av src/*.o src/*.pp.c src/*.pp.h src/*.jessie
.PHONY: all build fuzz eacsl eacsl-build rte val run eacsl-run verify verify-separatedly verify-proved verify-proved-separatedly sprove-proved replay replay-separatedly replay-proved replay-proved-separatedly sprove sprove-separatedly clean $(AV_WHY3_CONF)
#COLORS
GREEN := $(shell tput -Txterm setaf 2)
WHITE := $(shell tput -Txterm setaf 7)
YELLOW := $(shell tput -Txterm setaf 3)
RESET := $(shell tput -Txterm sgr0)
# Add the following 'help' target to your Makefile
# And add help text after each target name starting with '\#\#'
# A category can be added with @category
HELP_FUN = \
%help; \
while(<>) { push @{$$help{$$2 // 'options'}}, [$$1, $$3] if /^([a-zA-Z\-]+)\s*:.*\#\#(?:@([a-zA-Z\-]+))?\s(.*)$$/ }; \
print "usage: make [target]\n\n"; \
for (sort keys %help) { \
print "${WHITE}$$_:${RESET}\n"; \
for (@{$$help{$$_}}) { \
$$sep = " " x (32 - length $$_->[0]); \
print " ${YELLOW}$$_->[0]${RESET}$$sep${GREEN}$$_->[1]${RESET}\n"; \
}; \
print "\n"; }
help: ## Show this help.
@perl -e '$(HELP_FUN)' $(MAKEFILE_LIST)
.PHONY: help