Makefile

# attempts to run CN frontend on alloc.c, via an explicit cpp and direct

CC = clang

# includes adapted from _build/compile_commands.json
INCLUDES= -Isrc -Iinclude

# KM version
INCLUDES= -I$(OPAM_SWITCH_PREFIX)/lib/cerberus-lib/runtime/libc/include/ -Isrc -Iinclude
CPP=$(CC) -std=c11 -E -P -CC -Werror -Wno-builtin-macro-redefined -nostdinc -undef -D__cerb__

# Fulminate
RUNTIME_PREFIX = $(OPAM_SWITCH_PREFIX)/lib/cn/runtime
RUNTIME_LIB = $(RUNTIME_PREFIX)
# RUNTIME_INCLUDES= -Isrc -Iinclude
# RUNTIME_CPP = $(CC) -std=gnu11 -E -P -CC -Werror -Wno-builtin-macro-redefined -undef -D__x86_64__ -D__GNUC__="5" -D__cerb__ 
# RUNTIME_CPP = $(CC) -std=gnu11 -E -P -CC -Werror -Wno-builtin-macro-redefined -nostdinc -undef -D__cerb__ 
RUNTIME_CPP = $(CC) -std=gnu11 -E -P -CC -isystem$(OPAM_SWITCH_PREFIX)/lib/cerberus-lib/runtime/libc/include/ -Werror -Wno-builtin-macro-redefined -D__cerb__  -undef -fkeep-system-includes  -Isrc -Iinclude  -DSTANDALONE -DNO_STATEMENT_EXPRS

tmp-alloc.c: src/alloc.c
	$(CPP) -DSTANDALONE -DNO_STATEMENT_EXPRS $(INCLUDES) src/alloc.c > tmp-alloc.c

.PHONY: with-cerb
with-cerb:
	cerberus -DSTANDALONE -DNO_STATEMENT_EXPRS $(INCLUDES) src/alloc.c

.PHONY: ninja
ninja:
	ninja -C _build/

.PHONY: cn-verify-via-cpp
cn-verify-via-cpp: tmp-alloc.c
	cn verify tmp-alloc.c

.PHONY: cn-verify
cn-verify: src/alloc.c
	cn verify --incremental-solving=false --disable-multiclause-predicate-unfolding --no-vip $(if $(OPT), $(OPT)) $(if $(ONLY),--only=$(ONLY)) -DSTANDALONE -DNO_STATEMENT_EXPRS $(INCLUDES) src/alloc.c

cn-verify-par: src/alloc.c
	./verify.sh "$(shell nproc)"

main.pp.c: src/main.c src/alloc.c specs/spec.c
	$(RUNTIME_CPP) $< > $@

main.pp.exec.c: main.pp.c
	cn instrument --exec-c-locs-mode --insert-curly-braces $<

main.pp.exec.o: main.pp.exec.c
	$(CC) -g -c -O0 -std=gnu11 -I$(RUNTIME_PREFIX)/include -Isrc -Iinclude -Wno-builtin-macro-redefined -Wno-unused-value -D__cerb__ -DSTANDALONE -DNO_STATEMENT_EXPRS -include fulminate2.h $<

main.exe: main.pp.exec.o $(RUNTIME_LIB)/libcn_exec.a
	$(CC) $^ -L $(RUNTIME_LIB) -lcn_exec -o $@

.PHONY: cn-instrument
cn-instrument: main.exe
	./main.exe || lldb -S lldb_config_for_fulminate.lldb

.PHONY: cn-test-random
cn-test-random: src/alloc.c ./test-random.sh
	./test-random.sh --cc=$(CC)

.PHONY: cn-test-symbolic
cn-test-symbolic: src/alloc.c ./test-symbolic.sh
	./test-symbolic.sh --cc=$(CC) \
		--skip=hyp_alloc

.PHONY: cn-test-symbolic-lite
cn-test-symbolic-lite: src/alloc.c
	./test-symbolic.sh --cc=$(CC) \
		--skip=my_list_is_last,chunk_list_del \
		--skip=chunk_list_insert \
		--skip=LemmaCreateNewChunk \
		--skip=LemmaCnChunkHdrsRevToCnChunkHdrs \
		--skip=LemmaConcatCnChunkHdrsRev \
		--skip=LemmaNextChunk \
		--skip=LemmaPrevChunk \
		--skip=chunk_install \
		--skip=chunk_reclaimable \
		--skip=chunk_destroyable \
		--skip=LemmaLsegToChunkHdrs \
		--skip=chunk_recycle \
		--skip=LemmaGetLastChunk \
		--skip=get_free_chunk \
		--skip=setup_first_chunk \
		--skip=LemmaCnChunkHdrsRevToCnHypAllocator \
		--skip=chunk_merge \
		--skip=chunk_inc_map \
		--skip=chunk_can_split \
		--skip=brain_exploding_calculation \
		--skip=hyp_alloc \
		--skip=hyp_free

.PHONY: collect-pbt-comparison
collect-pbt-comparison:
	./pbt_bench/collect_comparison.py

.PHONY: collect-pbt-bug-finding
collect-pbt-bug-finding:
	./pbt_bench/collect_bugfinding.py

.PHONY: collect-pbt-bug-finding-buggy
collect-pbt-bug-finding-buggy:
	./pbt_bench/collect_bugfinding.py --only-buggy

.PHONY: collect-pbt-sizing
collect-pbt-sizing:
	./pbt_bench/collect_sizing.py

.PHONY: analyze-pbt-comparison
analyze-pbt-comparison:
	./pbt_bench/analyze_comparison.py

.PHONY: fulm-bench
fulm-bench:
	./fulm_bench/fulm_bench.py

.PHONY: clean
clean:
	rm -f tmp-alloc.c
	rm -f *~
	rm -f *.pp.c
	rm -f *.exec.c
	rm -f *.exec.o
	rm -f *.exe
	rm -rf _test_symbolic
	rm -rf _test_random