1default: report
2
3# ____________________________________________________________________
4# CBMC binaries
5#
6
7GOTO_CC = @GOTO_CC@
8GOTO_INSTRUMENT = goto-instrument
9GOTO_ANALYZER = goto-analyzer
10VIEWER = cbmc-viewer
11
12# ____________________________________________________________________
13# Variables
14#
15# Naming scheme:
16# ``````````````
17# FOO is the concatenation of the following:
18# FOO2: Set of command line
19# C_FOO: Value of $FOO common to all harnesses, set in this file
20# O_FOO: Value of $FOO specific to the OS we're running on, set in the
21#        makefile for the operating system
22# H_FOO: Value of $FOO specific to a particular harness, set in the
23#        makefile for that harness
24
25ENTRY = $(H_ENTRY)
26OBJS = $(H_OBJS)
27
28INC = \
29  $(INC2) \
30  $(C_INC) $(O_INC) $(H_INC) \
31  # empty
32
33CFLAGS = \
34  $(CFLAGS2) \
35  $(C_DEF) $(O_DEF) $(H_DEF) $(DEF) \
36  $(C_OPT) $(O_OPT) $(H_OPT) $(OPT) \
37  -m32 \
38  # empty
39
40CBMCFLAGS = \
41  --flush \
42  $(CBMCFLAGS2) \
43  $(C_CBMCFLAGS) $(O_CBMCFLAGS) $(H_CBMCFLAGS) \
44  # empty
45
46INSTFLAGS = \
47  $(INSTFLAGS2) \
48  $(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \
49  # empty
50
51# ____________________________________________________________________
52# Rules
53#
54# Rules for patching
55
56patch:
57	cd $(PROOFS)/../patches && ./patch.py
58
59unpatch:
60	cd $(PROOFS)/../patches && ./unpatch.py
61
62# ____________________________________________________________________
63# Rules
64#
65# Rules for building the CBMC harness
66
67C_SOURCES = $(patsubst %.goto,%.c,$(H_OBJS_EXCEPT_HARNESS))
68
69# Build each goto-binary out-of-source (i.e. in a 'gotos' directory
70# underneath each proof directory, to make it safe to build all proofs
71# in parallel
72OOS_OBJS = $(patsubst %.c,gotos/%.goto,$(C_SOURCES))
73
74CWD=$(abspath .)
75
76gotos/%.goto: %.c
77	mkdir -p $(dir $@)
78	$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@
79
80queue_datastructure.h: gotos/$(FREERTOS)/freertos_kernel/queue.goto
81	python3 @TYPE_HEADER_SCRIPT@ --binary $(CWD)/gotos$(FREERTOS)/freertos_kernel/queue.goto --c-file $(FREERTOS)/freertos_kernel/queue.c
82
83$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER)
84	$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) $(ENTRY)_harness.c
85
86$(ENTRY)1.goto: $(ENTRY)_harness.goto $(OOS_OBJS)
87	$(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness @RULE_INPUT@
88
89$(ENTRY)2.goto: $(ENTRY)1.goto
90	 $(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \
91		> $(ENTRY)2.txt 2>&1
92
93$(ENTRY)3.goto: $(ENTRY)2.goto
94	$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
95		> $(ENTRY)3.txt 2>&1
96
97$(ENTRY)4.goto: $(ENTRY)3.goto
98	$(GOTO_INSTRUMENT) $(INSTFLAGS) --slice-global-inits @RULE_INPUT@ @RULE_OUTPUT@ \
99		> $(ENTRY)4.txt 2>&1
100# ____________________________________________________________________
101# After running goto-instrument to remove function bodies the unused
102# functions need to be dropped again.
103
104$(ENTRY)5.goto: $(ENTRY)4.goto
105	$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
106		> $(ENTRY)5.txt 2>&1
107
108$(ENTRY).goto: $(ENTRY)5.goto
109	@CP@ @RULE_INPUT@ @RULE_OUTPUT@
110
111# ____________________________________________________________________
112# Rules
113#
114# Rules for running CBMC
115
116goto:
117	$(MAKE) -B $(ENTRY).goto
118
119# Ignore the return code for CBMC, so that we can still generate the
120# report if the proof failed. If the proof failed, we separately fail
121# the entire job using the check-cbmc-result rule.
122cbmc.xml: $(ENTRY).goto
123	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1
124
125property.xml: $(ENTRY).goto
126	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
127
128coverage.xml: $(ENTRY).goto
129	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
130
131cbmc: cbmc.xml
132
133property: property.xml
134
135coverage: coverage.xml
136
137report: cbmc.xml property.xml coverage.xml
138	$(VIEWER) \
139	--goto $(ENTRY).goto \
140	--srcdir $(FREERTOS_PLUS_TCP) \
141	--reportdir report \
142	--result cbmc.xml \
143	--property property.xml \
144	--coverage coverage.xml
145
146# This rule depends only on cbmc.xml and has no dependents, so it will
147# not block the report from being generated if it fails. This rule is
148# intended to fail if and only if the CBMC safety check that emits
149# cbmc.xml yielded a proof failure.
150check-cbmc-result: cbmc.xml
151	grep '<cprover-status>SUCCESS</cprover-status>' $^
152
153# ____________________________________________________________________
154# Rules
155#
156# Rules for cleaning up
157
158clean:
159	@RM@ $(OBJS) $(ENTRY).goto
160	@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
161	@RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-*
162	@RM@ *~ \#*
163	@RM@ queue_datastructure.h
164
165
166veryclean: clean
167	@RM_RECURSIVE@ html
168	@RM_RECURSIVE@ gotos
169
170distclean: veryclean
171	cd $(PROOFS)/../patches && ./unpatch.py
172	cd $(PROOFS) && ./make-remove-makefiles.py
173