forked from vigor-nf/vigor
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMakefile.dpdk
346 lines (292 loc) · 13.4 KB
/
Makefile.dpdk
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
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
# This Makefile expects to be included from the shared one
# Skeleton Makefile for Vigor NFs
# Variables that should be defined by inheriting Makefiles:
# - NF_DEVICES := <number of devices during verif-time, default 2>
# - NF_ARGS := <arguments to pass to the NF>
# -----------------------------------------------------------------------
# get current dir, see https://stackoverflow.com/a/8080530
SELF_DIR := $(abspath $(dir $(lastword $(MAKEFILE_LIST))))
# needs to be defined, see shared Makefile
NF_PROCESS_NAME := nf
# Default value for arguments
NF_DEVICES ?= 2
# DPDK stuff
include $(RTE_SDK)/mk/rte.vars.mk
# Same name for everyone, makes it easier to run them all with the same script
APP := nf
# allow the use of advanced globs in paths
SHELL := /bin/bash -O extglob -O globstar -c
# NF base source;
# somehow because of DPDK makefile magic wildcards mess up everything here,
# so we ask echo to expand those
SRCS-y := $(shell echo $(SELF_DIR)/nf*.c \
$(SELF_DIR)/libvig/verified/*.c)
SRCS-y += $(NF_FILES)
# Compiler flags
CFLAGS += -I $(SELF_DIR)
CFLAGS += -std=gnu99
CFLAGS += -DCAPACITY_POW2
CFLAGS += -O3
#CFLAGS += -O0 -g -rdynamic -DENABLE_LOG -Wfatal-errors
# It seems the DPDK makefiles really don't like being recursively invoked -
# and benchmarking invokes make run;
# so we just don't include the DPDK makefile if we're benchmarking
ifeq (,$(findstring benchmark-,$(MAKECMDGOALS)))
include $(RTE_SDK)/mk/rte.extapp.mk
endif
# ========
# VeriFast
# ========
LIBVIG_SRC_ARITH := $(SELF_DIR)/libvig/verified/arith.c \
$(SELF_DIR)/libvig/verified/modulo.c
LIBVIG_SRC_Z3 := $(subst .c,.o,$(LIBVIG_SRC_ARITH)) \
$(SELF_DIR)/libvig/verified/bitopsutils.c \
$(SELF_DIR)/libvig/verified/mod-pow2.c \
$(SELF_DIR)/libvig/verified/lpm-dir-24-8-lemmas.c \
$(SELF_DIR)/libvig/verified/lpm-dir-24-8.c
LIBVIG_SRC := $(subst .c,.o,$(LIBVIG_SRC_Z3)) \
$(SELF_DIR)/libvig/verified/double-chain-impl.c \
$(SELF_DIR)/libvig/verified/double-chain.c \
$(SELF_DIR)/libvig/verified/map-impl.c \
$(SELF_DIR)/libvig/verified/map-impl-pow2.c \
$(SELF_DIR)/libvig/verified/double-map.c \
$(SELF_DIR)/libvig/verified/prime.c \
$(SELF_DIR)/libvig/verified/listutils-lemmas.c \
$(SELF_DIR)/libvig/verified/vector.c \
$(SELF_DIR)/libvig/verified/transpose-lemmas.c \
$(SELF_DIR)/libvig/verified/permutations.c \
$(SELF_DIR)/libvig/verified/cht.c \
$(SELF_DIR)/libvig/verified/packet-io.c \
$(SELF_DIR)/libvig/verified/map.c \
$(SELF_DIR)/libvig/verified/coherence.c \
$(SELF_DIR)/libvig/verified/expirator.c \
$(SELF_DIR)/libvig/verified/boilerplate-assumptions.c \
$(SELF_DIR)/libvig/verified/ether.c
VERIFAST_COMMAND := verifast -I $(SELF_DIR) \
-I $(SELF_DIR)/libvig/models/dpdk \
-allow_assume -shared
VERIFAST_CLEAN_COMMAND := rm -rf $(SELF_DIR)/**/*.vfmanifest
verifast: autogen
@printf '\n\n!!!\n\n'
@printf 'This is gonna take a while, go make a nice cup of tea...\n\n'
@printf 'Note that we are verifying the code twice,\n'
@printf 'once with the pow2 optimization for the map and once without.\n'
@printf 'Also, some parts of the proof can only be verified\n'
@printf 'with Z3 and some with the standard VeriFast solver,\n'
@printf 'so we split the verification in parts...\n'
@printf '\n!!!\n\n'
@$(VERIFAST_CLEAN_COMMAND)
@$(VERIFAST_COMMAND) -emit_vfmanifest $(LIBVIG_SRC_ARITH)
@$(VERIFAST_COMMAND) -prover="Z3v4.5" -emit_vfmanifest $(LIBVIG_SRC_Z3)
@$(VERIFAST_COMMAND) -emit_vfmanifest $(LIBVIG_SRC)
@$(VERIFAST_COMMAND) -emit_vfmanifest -D CAPACITY_POW2 $(LIBVIG_SRC)
# =========================================
# Verification general commands and targets
# =========================================
# Cleanup
CLEAN_BUILD_ARTIFACTS_COMMAND := rm -rf *.bc *.os *.ll
CLEAN_ALL_COMMAND := $(CLEAN_BUILD_ARTIFACTS_COMMAND) && rm -rf {loop,state}.{c,h} *.gen.{c,h}
# Compilation
COMPILE_COMMAND := clang
# Linking with klee-uclibc, but without some methods we are modeling
# (not sure why they're in klee-uclibc.bca);
# also purge the pointless GNU linker warnings
# so KLEE doesn't warn about module asm
LINK_COMMAND := llvm-ar x $(KLEE_BUILD_PATH)/Release+Debug+Asserts/lib/klee-uclibc.bca && \
rm -f sleep.os vfprintf.os socket.os exit.os fflush_unlocked.os fflush.os && \
llvm-link -o nf_raw.bc *.os *.bc && \
llvm-dis -o nf_raw.ll nf_raw.bc && \
sed -i -e 's/module asm ".section .gnu.warning.*"//g' \
-e 's/module asm "\\09.previous"//g' \
-e 's/module asm ""//g' \
nf_raw.ll && \
llvm-as -o nf_raw.bc nf_raw.ll
# Optimization; analyze and remove as much provably dead code as possible
# (exceptions are models;
# also, mem* functions, not sure why it DCEs them since they are used...
# maybe related to LLVM having intrinsics for them?)
# We tried adding '-constprop -ipconstprop -ipsccp -correlated-propagation
# -loop-deletion -dce -die -dse -adce -deadargelim -instsimplify';
# this works but the traced prefixes seem messed up :(
OPT_EXCEPTIONS := memset,memcpy,memmove,stub_abort,stub_free,stub_hardware_read,stub_hardware_write,stub_prefetch,stub_rdtsc,stub_socket,stub_strerror,stub_delay
OPT_COMMAND := opt -basicaa -basiccg -internalize \
-internalize-public-api-list=main,$(OPT_EXCEPTIONS) \
-globaldce nf_raw.bc \
> nf.bc
# KLEE verification;
# if something takes longer than expected,
# try --max-solver-time=3 --debug-report-symbdex (to avoid symbolic indices)
VERIF_COMMAND := /usr/bin/time -v \
klee -no-externals -allocate-determ \
-allocate-determ-start-address=0x00040000000 \
-allocate-determ-size=1000 -dump-call-traces \
-dump-call-trace-prefixes -solver-backend=z3 \
-exit-on-error -max-memory=750000 -search=dfs \
-condone-undeclared-havocs --debug-report-symbdex \
nf.bc
# Cleanup after ourselves, but don't shadow the existing DPDK target
clean-vigor:
@$(CLEAN_ALL_COMMAND)
clean: clean-vigor
# Built-in DPDK default target, make it aware of autogen,
# and make it clean every time because our dependency tracking is nonexistent...
all: clean autogen
# =======================
# Symbex with DPDK models
# =======================
# Basic flags: only compile, emit debug code, in LLVM format,
# with checks for overflows (but not unsigned overflows -
# they're not UB and DPDK depends on them)
# also no unused-value, DPDK triggers that...
VERIF_FLAGS := -c -g -emit-llvm -fsanitize=signed-integer-overflow -Wno-unused-value
# Basic includes: NF root, KLEE, DPDK cmdline
VERIF_INCLUDES := -I $(SELF_DIR) -I $(KLEE_INCLUDE) -I $(RTE_SDK)/lib/librte_cmdline
# Basic defines
VERIF_DEFS := -D_GNU_SOURCE -DKLEE_VERIFICATION
# Number of devices
VERIF_DEFS += -DSTUB_DEVICES_COUNT=$(NF_DEVICES)
# NF base
VERIF_FILES := $(SELF_DIR)/nf*.c
# Specific NF
VERIF_FILES += $(NF_FILES) loop.c
# Models
VERIF_FILES += $(SELF_DIR)/libvig/models/verified/*.c \
$(SELF_DIR)/libvig/models/externals/*.c
# DPDK cmdline parsing library, always included,
# we don't want/need to model it... and the string function it uses
VERIF_FILES += $(RTE_SDK)/lib/librte_cmdline/*.c \
$(RTE_SDK)/lib/librte_eal/common/eal_common_string_fns.c
# The only thing we don't put in variables is the DPDK model headers,
# since we don't want to use those for the other symbex targets
symbex: clean autogen
@$(COMPILE_COMMAND) $(VERIF_DEFS) $(VERIF_INCLUDES) \
-I $(SELF_DIR)/libvig/models/dpdk \
$(VERIF_FILES) $(VERIF_FLAGS)
@$(LINK_COMMAND)
@$(OPT_COMMAND)
@$(VERIF_COMMAND) $(NF_ARGS)
@$(CLEAN_BUILD_ARTIFACTS_COMMAND)
# ==================================
# Symbex with hardware and OS models
# ==================================
# CPUFLAGS is set to a sentinel value;
# usually it's passed from the DPDK build system
VERIF_WITHDPDK_DEFS := -DRTE_COMPILE_TIME_CPUFLAGS=424242
# Let hardware models know we want them
VERIF_WITHDPDK_DEFS += -DVIGOR_MODEL_HARDWARE
# We need librte_eal/common because eal_private.h is in there,
# required by eal_thread.c...
# We need bus/pci because the linuxapp PCI stuff requires a private.h file in there...
# net/ixgbe is for model hardware (the ixgbe driver)
VERIF_WITHDPDK_INCLUDES := -I $(RTE_SDK)/$(RTE_TARGET)/include \
-I $(RTE_SDK)/lib/librte_eal/common \
-I $(RTE_SDK)/drivers/bus/pci \
-I $(RTE_SDK)/drivers/net/ixgbe
# And then some special DPDK includes: builtin models for built-ins DPDK uses,
# rte_config.h because many files forget to include it
VERIF_WITHDPDK_INCLUDES += --include=libvig/models/builtin.h \
--include=rte_config.h
# Platform-independent and Linux-specific EAL
DPDK_FILES += $(RTE_SDK)/lib/librte_eal/common/*.c \
$(RTE_SDK)/lib/librte_eal/linuxapp/eal/*.c
# Default ring mempool driver
DPDK_FILES += $(RTE_SDK)/drivers/mempool/ring/rte_mempool_ring.c
# Other libraries, except acl and distributor
# which use CPU intrinsics (there is a generic version of distributor,
# but we don't need it)
# and power has been broken for a while:
# http://dpdk.org/ml/archives/dev/2016-February/033152.html
DPDK_FILES += $(RTE_SDK)/lib/!(librte_acl|librte_distributor|librte_power)/*.c
# PCI driver support (for ixgbe driver)
DPDK_FILES += $(RTE_SDK)/drivers/bus/pci/*.c $(RTE_SDK)/drivers/bus/pci/linux/*.c
# ixgbe driver
IXGBE_FILES := $(RTE_SDK)/drivers/net/ixgbe/ixgbe_{fdir,flow,ethdev,ipsec,pf,rxtx,tm}.c \
$(RTE_SDK)/drivers/net/ixgbe/base/ixgbe_{api,common,phy,82599}.c
# DPDK, ixgbe, hardware models
VERIF_WITHDPDK_FILES := $(DPDK_FILES) $(IXGBE_FILES) \
$(SELF_DIR)/libvig/models/hardware.c
# Low-level models for specific functions
VERIF_WITHDPDK_FILES += $(SELF_DIR)/libvig/models/dpdk-low-level.c
symbex-withdpdk: clean autogen
@$(COMPILE_COMMAND) $(VERIF_DEFS) $(VERIF_WITHDPDK_DEFS) $(VERIF_INCLUDES) \
$(VERIF_WITHDPDK_INCLUDES) $(VERIF_FILES) \
$(VERIF_WITHDPDK_FILES) $(VERIF_FLAGS)
@$(LINK_COMMAND)
@$(OPT_COMMAND)
@$(VERIF_COMMAND) $(NF_ARGS)
@$(CLEAN_BUILD_ARTIFACTS_COMMAND)
# ====================================
# Symbex with hardware models and NFOS
# ====================================
# Convert the bash-style NF arguments (nf --no-shconf -- -n 3 -m 6) into
# C-style char*[] comma separated list
# of c-strings ("nf","--no-shconf","--","-n","3","-m","6") for NFOS to put
# into argv at compilation time.
dquote := \"
space := $(null) #
comma := ,
NF_ARGUMENTS_MACRO := -DNF_ARGUMENTS=\"$(subst $(space),$(dquote)$(comma)$(dquote),nf.bc $(NF_ARGS))\"
symbex-withnfos: clean autogen
@$(COMPILE_COMMAND) $(VERIF_DEFS) $(VERIF_WITHDPDK_DEFS) \
$(NF_ARGUMENTS_MACRO) -DNFOS $(VERIF_INCLUDES) \
$(VERIF_WITHDPDK_INCLUDES) $(VERIF_FILES) \
$(VERIF_WITHDPDK_FILES) $(SELF_DIR)/libvig/kernel/*.c \
$(VERIF_FLAGS) -mssse3 -msse2 -msse4.1
@$(LINK_COMMAND)
@$(OPT_COMMAND)
@$(VERIF_COMMAND) $(NF_ARGS)
@$(CLEAN_BUILD_ARTIFACTS_COMMAND)
# ==========
# Validation
# ==========
validate: autogen
@cd $(SELF_DIR)/validator && make $(notdir $(shell pwd))
# =======
# Running
# =======
run: all
@sudo ./build/app/nf $(NF_ARGS) || true
# ======================
# Counting lines of code
# ======================
# cloc instead of sloccount because the latter does not report comments,
# and all VeriFast annotations are comments
count-loc:
@cloc -q $(NF_FILES) $(subst .c,.h,$(NF_FILES)) $(NF_AUTOGEN_SRCS) \
$(SELF_DIR)/nf*.{c,h} 2>/dev/null
count-spec-loc:
@cloc -q spec.py
count-libvig-loc:
@# Bit of a hack for this one,
@# cloc can\'t be given a custom language but for some reason
@# it knows about Pig Latin, which is never gonna happen in our codebase, so...
@cloc --quiet --force-lang 'Pig Latin',gh \
$(SELF_DIR)/libvig/verified/*.{c,h,gh} | \
sed 's/Pig Latin/VeriFast /g'
@echo "NOTE: Annotations == VeriFast code + C comments - \
$$(grep '//[^@]' $(SELF_DIR)/libvig/verified/*.{c,h} | wc -l) \
(that last number is the non-VeriFast C comments)"
@if grep -F '/*' $(SELF_DIR)/libvig/verified/*.{c,h} | grep -vF '/*@'; then \
echo 'ERROR: There are multiline non-VeriFast comments in the C code, \
the total above is wrong!'; \
fi
count-dpdk-loc:
@cloc -q $(DPDK_FILES) $(subst .c,.h,$(DPDK_FILES)) 2>/dev/null
count-ixgbe-loc:
@cloc -q $(IXGBE_FILES) $(subst .c,.h,$(IXGBE_FILES)) 2>/dev/null
# This is a horrible hack - we get the files included in the build process by...
# running make -n
count-uclibc-loc:
@cd $(VIGOR_DIR)/klee-uclibc; \
make clean >> /dev/null 2>&1; \
cloc $$(for f in $$(make -n | grep --null -oh '[_a-zA-Z0-9][_a-zA-Z0-9]*\.[ch]'); \
do find . -name $$f; done); \
make -j >> /dev/null 2>&1
# =============
# Create new NF
# =============
new-nf:
@read -p 'NF short name, e.g. "nat": ' name; \
mkdir vig$${name}; \
cp template/* vig$${name}/.; \
echo "Go to the vig$${name} folder, and check out the comments in each file."