Use unified Makefile template for CBMC proofs (aws#2080)

* Add aws-templates-for-cbmc-proofs submodule

This commit submodules in this repository and begins the process of
integrating it into the CBMC proof directory.

  https://github.com/awslabs/aws-templates-for-cbmc-proofs

That repository contains a standardized Makefile and associated data
that are used for CBMC proofs at AWS. As well as submoduling it into the
s2n repository, this commit changes some of the files that run the
proofs to be symbolic links into the submodule, and changes the
directory structure to be conformat to the templates-for-cbmc-proofs
layout. Future commits will update the proof Makefiles so that they
correctly run with the new files.

* Add s2n inclusions to CBMC proofs

* Patch proof makefiles to use makefile template

This commit changes the variable names in the individual proof Makefiles
so that they conform to the naming scheme used in the
aws-templates-for-cbmc-proofs submodule. Here is a list of the changes:

* `DEPENDENCIES` that are s2n source files are now added to
  `PROJECT_SOURCES`
* `DEPENDENCIES` that are CBMC helper functions are now added to
  `PROOF_SOURCES` and listed as under the `PROOF_SOURCE` directory
* `DEPENDENCIES` that are overrides of s2n functions are now added to
  `PROOF_SOURCES` and listed as under the `PROOF_STUB` directory
* `ENTRY` -> `HARNESS_ENTRY`
* The name of the proof harness is the value of `HARNESS_FILE`
* `HARNESS_FILE` is added to `PROOF_SOURCES`
* `UNWINDSET` -> `CBMC_UNWINDSET`
* `REMOVE_FUNCTION_BODY` -> `CBMC_REMOVE_FUNCTION_BODY`

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "tests/cbmc/aws-templates-for-cbmc-proofs"]
+	path = tests/cbmc/aws-templates-for-cbmc-proofs
+	url = https://github.com/awslabs/aws-templates-for-cbmc-proofs

tests/cbmc/include/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md

tests/cbmc/proofs/Makefile-project-defines

@@ -0,0 +1,45 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to give project-specific definitions of the command
+# line arguments to pass to CBMC tools like goto-cc to build the goto
+# binaries and cbmc to do the property and coverage checking.
+#
+# Use this file to override most default definitions of variables in
+# Makefile.common.
+################################################################
+
+# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
+# COMPILE_FLAGS =
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Preprocessor include paths -I...
+INCLUDES += -I$(CBMC_ROOT)/include
+INCLUDES += -I$(SRCDIR)
+INCLUDES += -I$(SRCDIR)/api
+
+# Preprocessor definitions -D...
+
+# Whether a proof needs these checks should be decided on a proof by proof basis.
+# Checks can be enabled by setting AWS_DEEP_CHECKS to 1 in the makefile
+# of the proof that requires them
+AWS_DEEP_CHECKS ?= 0
+DEFINES += -DAWS_DEEP_CHECKS=$(AWS_DEEP_CHECKS)
+
+################################################################
+# Remove function bodies that are not used in the proofs.
+# Removing the function from the goto program helps CBMC's
+# function pointer analysis
+
+# We override abort() to be assert(0)
+PROOF_SOURCES += $(PROOF_STUB)/abort_override_assert_false.c
+REMOVE_FUNCTION_BODY += abort
+
+# Useful for setting unwind limits to one more than some value.
+addone = $(shell echo $$(( $(1) + 1)))

tests/cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,10 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

tests/cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,11 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to define project-specific targets and definitions for
+# unit testing or continuous integration that may depend on targets
+# defined in Makefile.common
+################################################################

tests/cbmc/proofs/Makefile-template-defines

@@ -0,0 +1 @@
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)

tests/cbmc/proofs/Makefile.common

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common

tests/cbmc/proofs/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md