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 = \
  --flush \
  $(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)/freertos_kernel/queue.goto
	python3 @TYPE_HEADER_SCRIPT@ --binary $(CWD)/gotos$(FREERTOS)/freertos_kernel/queue.goto --c-file $(FREERTOS)/freertos_kernel/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) -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.xml: $(ENTRY).goto
	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @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.xml

property: property.xml

coverage: coverage.xml

report: cbmc.xml property.xml coverage.xml
	$(VIEWER) \
	--goto $(ENTRY).goto \
	--srcdir $(FREERTOS_PLUS_TCP) \
	--reportdir report \
	--result cbmc.xml \
	--property property.xml \
	--coverage coverage.xml

# This rule depends only on cbmc.xml 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.xml yielded a proof failure.
check-cbmc-result: cbmc.xml
	grep '<cprover-status>SUCCESS</cprover-status>' $^

# ____________________________________________________________________
# Rules
#
# Rules for cleaning up

clean:
	@RM@ $(OBJS) $(ENTRY).goto
	@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
	@RM@ cbmc.xml 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