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
|
#!/usr/bin/make -f
# trap ... ERR isn't supported by dash, which is used on some systems
SHELL = /bin/bash
# building the source code
ifeq ($(filter-out cpachecker.%,$(CONFIG)),)
COMPILER ?= cpbm cillify -D__CPROVER_assert=__assert_fail -Dassert=__assert_fail
SUFFIX ?= i
endif
ifeq ($(filter-out blast.%,$(CONFIG)),)
COMPILER ?= cpbm cillify --blast
SUFFIX ?= i
endif
ifeq ($(filter-out llvm.%,$(CONFIG)),)
COMPILER ?= clang -emit-llvm -c
SUFFIX ?= s
endif
COMPILER ?= goto-cc --32
SUFFIX ?= bin
build:
test -d cprover
$(MAKE) -f cprover/rules cprover/binaries.$(CONFIG)
cprover/binaries.$(CONFIG): $(addsuffix .$(SUFFIX), $(addprefix build/, $(BENCHMARKS)))
$(RM) $@
set -e ; trap '$(RM) $@' ERR ; \
for f in $^ ; do \
echo $$f >> $@ ; \
done
build/%.$(SUFFIX): %.c
mkdir -p $(dir $@)
cd $(dir $<) ; $(COMPILER) -o $(abspath $@) $(realpath $<)
# verification rules
verify: build
test -d cprover
$(MAKE) -f cprover/rules cprover/verified.$(CONFIG)
cprover/verified.$(CONFIG): $(addsuffix .vr, $(addprefix results.$(CONFIG)/, $(BENCHMARKS)))
set -e ; trap '$(RM) $@' ERR ; \
cat $^ > $@
results.$(CONFIG)/%vr: build/%$(SUFFIX)
mkdir -p $(dir $@)
set -e ; trap '$(RM) $(abspath $@)' ERR ; \
tool="$(TOOL)" ; if [ "x$$tool" = "x" ] ; then tool="$(basename $(CONFIG))" ; fi ; \
timeout="$(TIMEOUT)" ; if [ "x$$timeout" != "x" ] ; then timeout="--timeout $(TIMEOUT)" ; fi ; \
maxmem="$(MAXMEM)" ; if [ "x$$maxmem" != "x" ] ; then maxmem="--maxmem $(MAXMEM)" ; fi ; \
cd $(dir $@) ; \
claims=`cpbm list-claims --cmd $$tool $(realpath $<) -- $(TOOL_OPTS)` ; \
for c in $$claims ; do \
cl=`echo $$c | cut -f1 -d:` ; \
st=`echo $$c | cut -f2 -d:` ; \
if [ "$$st" = "TRUE" ] ; then st="--valid" ; else st="--unknown" ; fi ; \
cpbm run --claim $$cl $$st $$timeout $$maxmem --cmd $$tool $(realpath $<) -- $(TOOL_OPTS) ; \
done | tee $(abspath $@) ; \
exit $${PIPESTATUS[0]}
# statistics collection
csv: verify
test -d cprover
$(MAKE) -f cprover/rules cprover/results.$(CONFIG).csv
cprover/results.$(CONFIG).csv: cprover/verified.$(CONFIG)
set -e ; trap '$(RM) $@' ERR ; \
parser="$(PARSER)" ; if [ "x$$parser" = "x" ] ; then parser="$(basename $(CONFIG))" ; fi ; \
cpbm csv $$parser $^ > $@
table: csv
test -d cprover
cpbm table cprover/results.$(CONFIG).csv Benchmark Result usertime maxmem
graph: csv
test -d cprover
cpbm graph cprover/results.$(CONFIG).csv
web: csv
test -d cprover
cpbm web cprover/results.$(CONFIG).csv cprover/results.$(CONFIG).web
# cleanup
clean:
test -d cprover
rm -rf results.* build
rm -f cprover/binaries.* cprover/verified.*
rm -rf cprover/results.*
.PHONY: clean build verify csv table graph web
|
