File: rules.cpbm.generic

package info (click to toggle)
bmt 0.6-1
  • links: PTS
  • area: main
  • in suites: buster, stretch
  • size: 324 kB
  • sloc: perl: 1,711; sh: 828; makefile: 90
file content (97 lines) | stat: -rw-r--r-- 2,700 bytes parent folder | download | duplicates (2)
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