Enable CBMC proofs to run in CI

This commit introduces the Litani submodule for running CBMC proofs in
parallel locally and in CI.

Author: karkhaz

.gitmodules

@@ -6,3 +6,7 @@
 	path = test/FreeRTOS-Kernel
 	url = https://github.com/FreeRTOS/FreeRTOS-Kernel
 	update = none
+[submodule "test/cbmc/aws-build-accumulator"]
+	path = test/litani
+	url = https://github.com/awslabs/aws-build-accumulator
+	update = none

test/cbmc/proofs/Makefile.template

@@ -47,16 +47,6 @@ INSTFLAGS = \
   $(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \
   # empty
 
-# ____________________________________________________________________
-# Rules
-#
-# Rules for building a:FR object files. These are not harness-specific,
-# and several harnesses might depend on a particular a:FR object, so
-# define them all once here.
-
-@RULE_GOTO@
-	$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@
-
 # ____________________________________________________________________
 # Rules
 #
@@ -73,14 +63,27 @@ unpatch:
 #
 # Rules for building the CBMC harness
 
-#queue_datastructure.h: $(H_OBJS_EXCEPT_HARNESS)
-#	python3 @TYPE_HEADER_SCRIPT@ --binary $(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c
+C_SOURCES = $(patsubst %.goto,%.c,$(H_OBJS_EXCEPT_HARNESS))
 
-$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER)
+# 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@
 
-$(ENTRY)1.goto: $(OBJS)
-	$(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness $(OBJS)
+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@ \
@@ -110,17 +113,16 @@ $(ENTRY).goto: $(ENTRY)5.goto
 # Rules for running CBMC
 
 goto:
-	$(MAKE) patch
-	$(MAKE) $(ENTRY).goto
+	$(MAKE) -B $(ENTRY).goto
 
 cbmc.txt: $(ENTRY).goto
-	- cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1
+	cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ 2>&1 | tee $@
 
 property.xml: $(ENTRY).goto
-	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
+	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ 2>&1 | tee $@
 
 coverage.xml: $(ENTRY).goto
-	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
+	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ 2>&1 | tee $@
 
 cbmc: cbmc.txt
 
@@ -133,7 +135,7 @@ report: cbmc.txt property.xml coverage.xml
 	--goto $(ENTRY).goto \
 	--srcdir $(FREERTOS_PLUS_TCP) \
 	--blddir $(FREERTOS_PLUS_TCP) \
-	--htmldir html \
+	--htmldir $(CWD)/html \
 	--srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \
 	--result cbmc.txt \
 	--property property.xml \