blob: 01d518ed5b22834eadadd4a470318c1683ce956b (
plain)
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
|
default: report
# ____________________________________________________________________
# CBMC binaries
#
GOTO_CC = @GOTO_CC@
GOTO_INSTRUMENT = goto-instrument
GOTO_ANALYZER = goto-analyzer
VIEWER = cbmc-viewer
# ____________________________________________________________________
# Variables
#
# Naming scheme:
# ``````````````
# FOO is the concatenation of the following:
# FOO2: Set of command line
# C_FOO: Value of $FOO common to all harnesses, set in this file
# O_FOO: Value of $FOO specific to the OS we're running on, set in the
# makefile for the operating system
# H_FOO: Value of $FOO specific to a particular harness, set in the
# makefile for that harness
ENTRY = $(H_ENTRY)
OBJS = $(H_OBJS)
INC = \
$(INC2) \
$(C_INC) $(O_INC) $(H_INC) \
# empty
CFLAGS = \
$(CFLAGS2) \
$(C_DEF) $(O_DEF) $(H_DEF) $(DEF) \
$(C_OPT) $(O_OPT) $(H_OPT) $(OPT) \
-m32 \
# empty
CBMCFLAGS = \
$(CBMCFLAGS2) \
$(C_CBMCFLAGS) $(O_CBMCFLAGS) $(H_CBMCFLAGS) \
# empty
INSTFLAGS = \
$(INSTFLAGS2) \
$(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \
# empty
# ____________________________________________________________________
# Rules
#
# Rules for patching
patch:
cd $(PROOFS)/../patches && ./patch.py
unpatch:
cd $(PROOFS)/../patches && ./unpatch.py
# ____________________________________________________________________
# Rules
#
# Rules for building the CBMC harness
C_SOURCES = $(patsubst %.goto,%.c,$(H_OBJS_EXCEPT_HARNESS))
# Build each goto-binary out-of-source (i.e. in a 'gotos' directory
# underneath each proof directory, to make it safe to build all proofs
# in parallel
OOS_OBJS = $(patsubst %.c,gotos/%.goto,$(C_SOURCES))
CWD=$(abspath .)
gotos/%.goto: %.c
mkdir -p $(dir $@)
$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@
queue_datastructure.h: gotos/$(FREERTOS)/Source/queue.goto
python3 @TYPE_HEADER_SCRIPT@ --binary $(CWD)/gotos$(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c
$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER)
$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) $(ENTRY)_harness.c
$(ENTRY)1.goto: $(ENTRY)_harness.goto $(OOS_OBJS)
$(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness @RULE_INPUT@
$(ENTRY)2.goto: $(ENTRY)1.goto
$(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \
> $(ENTRY)2.txt 2>&1
$(ENTRY)3.goto: $(ENTRY)2.goto
$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
> $(ENTRY)3.txt 2>&1
$(ENTRY)4.goto: $(ENTRY)3.goto
$(GOTO_INSTRUMENT) $(INSTFLAGS) --slice-global-inits @RULE_INPUT@ @RULE_OUTPUT@ \
> $(ENTRY)4.txt 2>&1
# ____________________________________________________________________
# After running goto-instrument to remove function bodies the unused
# functions need to be dropped again.
$(ENTRY)5.goto: $(ENTRY)4.goto
$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
> $(ENTRY)5.txt 2>&1
$(ENTRY).goto: $(ENTRY)5.goto
@CP@ @RULE_INPUT@ @RULE_OUTPUT@
# ____________________________________________________________________
# Rules
#
# Rules for running CBMC
goto:
$(MAKE) patch
$(MAKE) -B $(ENTRY).goto
# Ignore the return code for CBMC, so that we can still generate the
# report if the proof failed. If the proof failed, we separately fail
# the entire job using the check-cbmc-result rule.
cbmc.txt: $(ENTRY).goto
-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1
property.xml: $(ENTRY).goto
cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
coverage.xml: $(ENTRY).goto
cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
cbmc: cbmc.txt
property: property.xml
coverage: coverage.xml
report: cbmc.txt property.xml coverage.xml
$(VIEWER) \
--goto $(ENTRY).goto \
--srcdir $(FREERTOS) \
--reportdir html \
--exclude "(.@FORWARD_SLASH@Demo)" \
--result cbmc.txt \
--property property.xml \
--coverage coverage.xml
# This rule depends only on cbmc.txt and has no dependents, so it will
# not block the report from being generated if it fails. This rule is
# intended to fail if and only if the CBMC safety check that emits
# cbmc.txt yielded a proof failure.
check-cbmc-result: cbmc.txt
grep -e "^VERIFICATION SUCCESSFUL" $^
# ____________________________________________________________________
# Rules
#
# Rules for cleaning up
clean:
@RM@ $(OBJS) $(ENTRY).goto
@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
@RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-*
@RM@ *~ \#*
@RM@ queue_datastructure.h
veryclean: clean
@RM_RECURSIVE@ html
@RM_RECURSIVE@ gotos
distclean: veryclean
cd $(PROOFS)/../patches && ./unpatch.py
cd $(PROOFS) && ./make-remove-makefiles.py
|
