From 0bbf4088859569bec64a24b577057cd8929f8e7a Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Wed, 4 Aug 2021 23:32:12 +0000
Subject: [PATCH 01/19] Add CBMC-proofs infrastructure

---
 .gitmodules                               |   6 +
 test/cbmc/aws-templates-for-cbmc-proofs   |   1 +
 test/cbmc/litani                          |   1 +
 test/cbmc/proofs/Makefile-project-defines |  37 +
 test/cbmc/proofs/Makefile-project-targets |  10 +
 test/cbmc/proofs/Makefile-project-testing |  11 +
 test/cbmc/proofs/Makefile.common          | 862 ++++++++++++++++++++++
 test/cbmc/proofs/README.md                |  27 +
 test/cbmc/proofs/prepare.py               |  54 ++
 test/cbmc/proofs/run-cbmc-proofs.py       | 365 +++++++++
 10 files changed, 1374 insertions(+)
 create mode 160000 test/cbmc/aws-templates-for-cbmc-proofs
 create mode 160000 test/cbmc/litani
 create mode 100644 test/cbmc/proofs/Makefile-project-defines
 create mode 100644 test/cbmc/proofs/Makefile-project-targets
 create mode 100644 test/cbmc/proofs/Makefile-project-testing
 create mode 100644 test/cbmc/proofs/Makefile.common
 create mode 100644 test/cbmc/proofs/README.md
 create mode 100644 test/cbmc/proofs/prepare.py
 create mode 100755 test/cbmc/proofs/run-cbmc-proofs.py

diff --git a/.gitmodules b/.gitmodules
index 3bd7e7735..bfe815c15 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -8,3 +8,9 @@
 	path = test/unit-test/CMock
 	url = https://github.com/ThrowTheSwitch/CMock.git
 	update = none
+[submodule "test/cbmc/aws-templates-for-cbmc-proofs"]
+	path = test/cbmc/aws-templates-for-cbmc-proofs
+	url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git
+[submodule "test/cbmc/litani"]
+	path = test/cbmc/litani
+	url = https://github.com/awslabs/aws-build-accumulator.git
diff --git a/test/cbmc/aws-templates-for-cbmc-proofs b/test/cbmc/aws-templates-for-cbmc-proofs
new file mode 160000
index 000000000..0bfb2d7b1
--- /dev/null
+++ b/test/cbmc/aws-templates-for-cbmc-proofs
@@ -0,0 +1 @@
+Subproject commit 0bfb2d7b1aad0fedd39a1d7a5006a3f84d264175
diff --git a/test/cbmc/litani b/test/cbmc/litani
new file mode 160000
index 000000000..bba4c8248
--- /dev/null
+++ b/test/cbmc/litani
@@ -0,0 +1 @@
+Subproject commit bba4c8248e9b62f8e99998268571d3e0acb5a0ee
diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines
new file mode 100644
index 000000000..f6f7681f7
--- /dev/null
+++ b/test/cbmc/proofs/Makefile-project-defines
@@ -0,0 +1,37 @@
+# -*- 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...
+# Consider adding
+#     INCLUDES += -I$(CBMC_ROOT)/include
+# You will want to decide what order that comes in relative to the other
+# include directories in your project.
+#
+# INCLUDES =
+
+# Preprocessor definitions -D...
+# DEFINES =
+
+# Path to arpa executable
+# ARPA =
+
+# Flags to pass to cmake for building the project
+# ARPA_CMAKE_FLAGS =
diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets
new file mode 100644
index 000000000..2d4d4602a
--- /dev/null
+++ b/test/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.
+################################################################
diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing
new file mode 100644
index 000000000..dc0c20971
--- /dev/null
+++ b/test/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
+################################################################
diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common
new file mode 100644
index 000000000..fb0844b70
--- /dev/null
+++ b/test/cbmc/proofs/Makefile.common
@@ -0,0 +1,862 @@
+# -*- 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
+
+################################################################
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+#
+# Licensed under the Apache License, Version 2.0 (the "License"). You
+# may not use this file except in compliance with the License. A copy
+# of the License is located at
+#
+#     http://aws.amazon.com/apache2.0/
+#
+# or in the "license" file accompanying this file. This file is
+# distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF
+# ANY KIND, either express or implied. See the License for the
+# specific language governing permissions and limitations under the
+# License.
+
+################################################################
+# This file Makefile.common defines the basic work flow for cbmc proofs.
+#
+# The intention is that the goal of your project is to write proofs
+# for a collection of functions in a source tree.
+#
+# To use this file
+#   1. Edit the variable definitions in Section I below as appropriate for
+#      your project, your proofs, and your source tree.
+#   2. For each function for which you are writing a proof,
+#      a. Create a subdirectory <DIR>.
+#      b. Write a proof harness (a function) with the name <HARNESS_ENTRY>
+#         in a file with the name <DIR>/<HARNESS_FILE>.c
+#      c. Write a makefile with the name <DIR>/Makefile that looks
+#         something like
+#
+#         HARNESS_FILE=<HARNESS_FILE>
+#         HARNESS_ENTRY=<HARNESS_ENTRY>
+#         PROOF_UID=<PROOF_UID>
+#
+#         PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c
+#         PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c
+#
+#         PROOF_SOURCES += $(PROOFDIR)/harness.c
+#         PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c
+#         PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c
+#
+#         UNWINDSET += foo.0:3
+#         UNWINDSET += bar.1:6
+#
+#         REMOVE_FUNCTION_BODY += api_stub_a
+#         REMOVE_FUNCTION_BODY += api_stub_b
+#
+#         DEFINES = -DDEBUG=0
+#
+#         include ../Makefile.common
+#
+#      d. Change directory to <DIR> and run make
+#
+# Dependency handling in this file may not be perfect. Consider
+# running "make clean" or "make veryclean" before "make report" if you
+# get results that are hard to explain.
+
+SHELL=/bin/bash
+
+default: report
+
+################################################################
+################################################################
+## Section I: This section gives common variable definitions.
+##
+## Feel free to edit these definitions for your project.
+##
+## Definitions specific to a proof (generally definitions defined
+## below with ?= like PROJECT_SOURCES listing the project source files
+## required by the proof) should be defined in the proof Makefile.
+##
+## Remember that this Makefile is intended to be included from the
+## Makefile in your proof directory, so all relative pathnames should
+## be relative to your proof directory.
+##
+
+# Absolute path to the directory containing this Makefile.common
+# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html
+#
+# Note: We compute the absolute paths to the makefiles in MAKEFILE_LIST
+# before we filter the list of makefiles for %/Makefile.common.
+# Otherwise an invocation of the form "make -f Makefile.common" will set
+# MAKEFILE_LIST to "Makefile.common" which will fail to match the
+# pattern %/Makefile.common.
+#
+MAKEFILE_PATHS = $(foreach makefile,$(MAKEFILE_LIST),$(abspath $(makefile)))
+PROOF_ROOT = $(dir $(filter %/Makefile.common,$(MAKEFILE_PATHS)))
+
+CBMC_ROOT = $(shell dirname $(PROOF_ROOT))
+PROOF_STUB = $(CBMC_ROOT)/stubs
+PROOF_SOURCE = $(CBMC_ROOT)/sources
+
+# Project-specific definitions to override default definitions below
+#   * Makefile-project-defines will never be overwritten
+#   * Makefile-template-defines will be overwritten each time the
+#     proof templates are updated
+sinclude $(PROOF_ROOT)/Makefile-project-defines
+sinclude $(PROOF_ROOT)/Makefile-template-defines
+
+# SRCDIR is the path to the root of the source tree
+SRCDIR ?= $(abspath ../..)
+
+# PROOFDIR is the path to the directory containing the proof harness
+PROOFDIR ?= $(abspath .)
+
+# Path to the root of the cbmc project.
+#
+# Projects generally have a directory $(CBMCDIR) with subdirectories
+# $(CBMCDIR)/proofs containing the proofs and maybe $(CBMCDIR)/stubs
+# containing the stubs used in the proof.  This Makefile is generally
+# at $(CBMCDIR)/proofs/Makefile.common.
+CBMCDIR ?= $(PROOF_ROOT)/cbmc
+
+# Default CBMC flags used for property checking and coverage checking
+CBMCFLAGS += --unwind 1 $(CBMC_UNWINDSET) --flush
+
+# Do property checking with the external SAT solver given by
+# EXTERNAL_SAT_SOLVER.  Do coverage checking with the default solver,
+# since coverage checking requires the use of an incremental solver.
+# The EXTERNAL_SAT_SOLVER variable is typically set (if it is at all)
+# as an environment variable or as a makefile variable in
+# Makefile-project-defines.
+#
+# For a particular proof, if the default solver is faster, do property
+# checking with the default solver by including this definition in the
+# proof Makefile:
+#         USE_EXTERNAL_SAT_SOLVER =
+#
+ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),)
+   USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver $(EXTERNAL_SAT_SOLVER)
+endif
+CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
+
+# Job pools
+# For version of Litani that are new enough (where `litani print-capabilities`
+# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a
+# "job pool" that restricts how many expensive proofs are run at a time. All
+# other proofs will be built in parallel as usual.
+#
+# In more detail: all compilation, instrumentation, and report jobs are run with
+# full parallelism as usual, even for expensive proofs. The CBMC jobs for
+# non-expensive proofs are also run in parallel. The only difference is that the
+# CBMC safety checks and coverage checks for expensive proofs are run with a
+# restricted parallelism level. At any one time, only N of these jobs are run at
+# once, amongst all the proofs.
+#
+# To configure N, Litani needs to be initialized with a pool called "expensive".
+# For example, to only run two CBMC safety/coverage jobs at a time from amongst
+# all the proofs, you would initialize litani like
+#         litani init --pools expensive:2
+# The run-cbmc-proofs.py script takes care of this initialization through the
+# --expensive-jobs-parallelism flag.
+#
+# To enable this feature, set
+# the ENABLE_POOLS variable when running Make, like
+#         `make ENABLE_POOLS=true report`
+# The run-cbmc-proofs.py script takes care of this through the
+# --restrict-expensive-jobs flag.
+
+ifeq ($(strip $(ENABLE_POOLS)),)
+  POOL =
+else ifeq ($(strip $(EXPENSIVE)),)
+  POOL =
+else
+  POOL = --pool expensive
+endif
+
+# Similar to the pool feature above. If Litani is new enough, enable
+# profiling CBMC's memory use.
+ifeq ($(strip $(ENABLE_MEMORY_PROFILING)),)
+  MEMORY_PROFILING =
+else
+  MEMORY_PROFILING = --profile-memory
+endif
+
+# Property checking flags
+#
+# Each variable below controls a specific property checking flag
+# within CBMC. If desired, a property flag can be disabled within
+# a particular proof by nulling the corresponding variable. For
+# instance, the following line:
+#
+#     CHECK_FLAG_POINTER_CHECK =
+#
+# would disable the --pointer-check CBMC flag within:
+#   * an entire project when added to Makefile-project-defines
+#   * a specific proof when added to the harness Makefile
+
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
+CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
+CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
+CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
+CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
+CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
+CBMC_FLAG_NAN_CHECK ?= --nan-check
+CBMC_FLAG_POINTER_CHECK ?= --pointer-check
+CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
+CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
+CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
+CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
+CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
+CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
+
+# CBMC flags used for property checking
+
+CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
+CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
+CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_FLOAT_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_NAN_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_POINTER_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_POINTER_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+
+# CBMC flags used for coverage checking
+
+COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
+COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
+
+# Additional CBMC flag to CBMC control verbosity.
+#
+# Meaningful values are
+# 0 none
+# 1 only errors
+# 2 + warnings
+# 4 + results
+# 6 + status/phase information
+# 8 + statistical information
+# 9 + progress information
+# 10 + debug info
+#
+# Uncomment the following line or set in Makefile-project-defines
+# CBMC_VERBOSITY ?= --verbosity 4
+
+# Additional CBMC flag to control how CBMC treats static variables.
+#
+# NONDET_STATIC is a list of flags of the form --nondet-static
+# and --nondet-static-exclude VAR.  The --nondet-static flag causes
+# CBMC to initialize static variables with unconstrained value
+# (ignoring initializers and default zero-initialization).  The
+# --nondet-static-exclude VAR excludes VAR for the variables
+# initialized with unconstrained values.
+NONDET_STATIC ?= ""
+
+# Flags to pass to goto-cc for compilation and linking
+COMPILE_FLAGS ?=
+LINK_FLAGS ?=
+
+# Preprocessor include paths -I...
+INCLUDES ?=
+
+# Preprocessor definitions -D...
+DEFINES ?=
+
+# CBMC object model
+#
+# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for
+# the id of the object to which a pointer is pointing.  CBMC uses 8
+# bits for the object id by default. The remaining bits in the pointer
+# are used for offset into the object.  This limits the size of the
+# objects that CBMC can model.  This Makefile defines this bound on
+# object size to be CBMC_MAX_OBJECT_SIZE.  You are likely to get
+# unexpected results if you try to malloc an object larger than this
+# bound.
+CBMC_OBJECT_BITS ?= 8
+
+# CBMC loop unwinding (Normally set in the proof Makefile)
+#
+# UNWINDSET is a list of pairs of the form foo.1:4 meaning that
+# CBMC should unwind loop 1 in function foo no more than 4 times.
+# For historical reasons, the number 4 is one more than the number
+# of times CBMC actually unwinds the loop.
+UNWINDSET ?=
+
+# CBMC function removal (Normally set set in the proof Makefile)
+#
+# REMOVE_FUNCTION_BODY is a list of function names.  CBMC will "undefine"
+# the function, and CBMC will treat the function as having no side effects
+# and returning an unconstrained value of the appropriate return type.
+# The list should include the names of functions being stubbed out.
+REMOVE_FUNCTION_BODY ?=
+
+# The project source files (Normally set set in the proof Makefile)
+#
+# PROJECT_SOURCES is the list of project source files to compile,
+# including the source file defining the function under test.
+PROJECT_SOURCES ?=
+
+# The proof source files (Normally set in the proof Makefile)
+#
+# PROOF_SOURCES is the list of proof source files to compile, including
+# the proof harness, and including any function stubs being used.
+PROOF_SOURCES ?=
+
+# The number of seconds that CBMC should be allowed to run for before
+# being forcefully terminated. Currently, this is set to be less than
+# the time limit for a CodeBuild job, which is eight hours. If a proof
+# run takes longer than the time limit of the CI environment, the
+# environment will halt the proof run without updating the Litani
+# report, making the proof run appear to "hang".
+CBMC_TIMEOUT ?= 21600
+
+# Proof writers could add function contracts in their source code.
+# These contracts are ignored by default, but may be enabled in two distinct
+# contexts using the following two variables:
+# 1. To check whether one or more function contracts are sound with respect to
+#    the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of
+#    function names.
+# 2. To replace calls to certain functions with their correspondent function
+#    contracts, USE_FUNCTION_CONTRACTS should be a list of function names.
+#    One must check separately whether a function contract is sound before
+#    replacing it in calling contexts.
+CHECK_FUNCTION_CONTRACTS ?= ""
+CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS))
+
+USE_FUNCTION_CONTRACTS ?= ""
+CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS))
+
+# Similarly, proof writers could also add loop contracts in their source code
+# to obtain unbounded correctness proofs. Unlike function contracts, loop
+# contracts are not reusable and thus are checked and used simultaneously.
+# These contracts are also ignored by default, but may be enabled by setting
+# the APPLY_LOOP_CONTRACTS variable to 1.
+APPLY_LOOP_CONTRACTS ?= 0
+
+################################################################
+################################################################
+## Section II: This section is for project-specific definitions
+
+
+################################################################
+################################################################
+## Section II: This section defines the process of running a proof
+##
+## There should be no reason to edit anything below this line.
+
+################################################################
+# Paths
+
+CBMC ?= cbmc
+GOTO_ANALYZER ?= goto-analyzer
+GOTO_CC ?= goto-cc
+GOTO_INSTRUMENT ?= goto-instrument
+VIEWER ?= cbmc-viewer
+MAKE_SOURCE ?= make-source
+VIEWER2 ?= cbmc-viewer
+CMAKE ?= cmake
+ARPA ?= @echo "You must set ARPA in Makefile-project-defines to run arpa in this project"; false
+
+GOTODIR ?= $(PROOFDIR)/gotos
+LOGDIR ?= $(PROOFDIR)/logs
+
+PROJECT ?= project
+PROOF ?= proof
+
+HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE)
+PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT)
+PROOF_GOTO ?= $(GOTODIR)/$(PROOF)
+
+ARPA_BLDDIR ?= $(abspath $(PROOFDIR)/arpa_cmake)
+ARPA_COMP_CMDS ?= $(ARPA_BLDDIR)/compile_commands.json
+
+################################################################
+# Useful macros for values that are hard to reference
+SPACE :=$() $()
+COMMA :=,
+
+################################################################
+# Set C compiler defines
+
+CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
+
+DEFINES += -DCBMC=1
+DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
+DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
+
+# CI currently assumes cbmc invocation has at most one --unwindset
+ifdef UNWINDSET
+  ifneq ($(strip $(UNWINDSET)),"")
+    CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
+  endif
+endif
+CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY))
+
+################################################################
+# Build targets that make the relevant .goto files
+
+# Compile project sources
+$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES)
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_CC) $(CBMC_VERBOSITY) --export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES) $^ -o $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/project_sources-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): building project binary"
+
+# Compile proof sources
+$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_CC) $(CBMC_VERBOSITY) --export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES) $^ -o $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/proof_sources-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): building proof binary"
+
+# Optionally remove function bodies from project sources
+$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
+ifeq ($(REMOVE_FUNCTION_BODY),"")
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not removing function bodies from project sources"
+else
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/remove_function_body-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): removing function bodies from project sources"
+endif
+
+# Link project and proof sources into the proof harness
+$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
+	$(LITANI) add-job \
+	  --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ -o $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/link_proof_project-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): linking project to proof"
+
+# Optionally check function contracts
+$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
+ifeq ($(CHECK_FUNCTION_CONTRACTS),"")
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not checking function contracts"
+else
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): checking function contracts"
+endif
+
+# Optionally replace function calls with function contracts
+$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
+ifeq ($(USE_FUNCTION_CONTRACTS),"")
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not replacing function calls with function contracts"
+else
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/use_function_contracts-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): replacing function calls with function contracts"
+endif
+
+# Optionally apply loop contracts
+$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
+ifneq ($(APPLY_LOOP_CONTRACTS),1)
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not applying loop contracts"
+else
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --apply-loop-contracts $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): applying loop contracts"
+endif
+
+# Optionally fill static variable with unconstrained values
+$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
+ifeq ($(NONDET_STATIC),"")
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not setting static variables to nondet"
+else
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/nondet_static-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): setting static variables to nondet"
+endif
+
+# Omit unused functions (sharpens coverage calculations)
+$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): dropping unused functions"
+
+# Omit initialization of unused global variables (reduces problem size)
+$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): slicing global initializations"
+
+# Final name for proof harness
+$(HARNESS_GOTO).goto: $(HARNESS_GOTO)7.goto
+	$(LITANI) add-job \
+	  --command 'cp $< $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): copying final goto-binary"
+
+################################################################
+# Targets to run Arpa
+
+$(ARPA_BLDDIR):
+	$(CMAKE) $(ARPA_CMAKE_FLAGS) \
+	  -DCMAKE_EXPORT_COMPILE_COMMANDS=1 \
+	  -B $(ARPA_BLDDIR) \
+	  -S $(SRCDIR)
+
+arpa: $(ARPA_BLDDIR)
+	$(ARPA) run -cc $(ARPA_COMP_CMDS) -r $(SRCDIR)
+
+################################################################
+# Targets to run the analysis commands
+
+$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --trace $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:safety checks" \
+	  --stderr-file $(LOGDIR)/result-err-log.txt \
+	  --description "$(PROOF_UID): checking safety properties"
+
+$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --trace --xml-ui $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:safety checks" \
+	  --stderr-file $(LOGDIR)/result-err-log.txt \
+	  --description "$(PROOF_UID): checking safety properties"
+
+$(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --show-properties --xml-ui $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  --ignore-returns 10 \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --stderr-file $(LOGDIR)/property-err-log.txt \
+	  --description "$(PROOF_UID): printing safety properties"
+
+$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:coverage computation" \
+	  --stderr-file $(LOGDIR)/coverage-err-log.txt \
+	  --description "$(PROOF_UID): calculating coverage"
+
+define VIEWER_CMD
+  $(VIEWER) \
+    --result $(LOGDIR)/result.txt \
+    --block $(LOGDIR)/coverage.xml \
+    --property $(LOGDIR)/property.xml \
+    --srcdir $(SRCDIR) \
+    --goto $(HARNESS_GOTO).goto \
+    --htmldir $(PROOFDIR)/html
+endef
+export VIEWER_CMD
+
+$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
+	$(LITANI) add-job \
+	  --command "$$VIEWER_CMD" \
+	  --inputs $^ \
+	  --outputs $(PROOFDIR)/html \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage report \
+	  --stdout-file $(LOGDIR)/viewer-log.txt \
+	  --interleave-stdout-stderr \
+	  --description "$(PROOF_UID): generating report"
+
+
+# Caution: run make-source before running property and coverage checking
+# The current make-source script removes the goto binary
+$(LOGDIR)/source.json:
+	mkdir -p $(dir $@)
+	$(RM) -r $(GOTODIR)
+	$(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@
+	$(RM) -r $(GOTODIR)
+
+define VIEWER2_CMD
+  $(VIEWER2) \
+    --result $(LOGDIR)/result.xml \
+    --coverage $(LOGDIR)/coverage.xml \
+    --property $(LOGDIR)/property.xml \
+    --srcdir $(SRCDIR) \
+    --goto $(HARNESS_GOTO).goto \
+    --reportdir $(PROOFDIR)/report
+endef
+export VIEWER2_CMD
+
+# Omit logs/source.json from report generation until make-sources
+# works correctly with Makefiles that invoke the compiler with
+# mutliple source files at once.
+$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
+	$(LITANI) add-job \
+	  --command "$$VIEWER2_CMD" \
+	  --inputs $^ \
+	  --outputs $(PROOFDIR)/report \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --stdout-file $(LOGDIR)/viewer-log.txt \
+	  --interleave-stdout-stderr \
+	  --ci-stage report \
+	  --description "$(PROOF_UID): generating report"
+
+litani-path:
+	@echo $(LITANI)
+
+# ##############################################################
+# Phony Rules
+#
+#	These rules provide a convenient way to run a single proof up to a
+#	certain stage. Users can browse into a proof directory and run
+#	"make -Bj 3 report" to generate a report for just that proof, or
+#	"make goto" to build the goto binary. Under the hood, this runs litani
+#	for just that proof.
+
+_goto: $(HARNESS_GOTO).goto
+goto:
+	$(LITANI) init --project $(PROJECT_NAME)
+	$(MAKE) -B _goto
+	$(LITANI) run-build
+
+_result: $(LOGDIR)/result.txt
+result:
+	$(LITANI) init --project $(PROJECT_NAME)
+	$(MAKE) -B _result
+	$(LITANI) run-build
+
+_property: $(LOGDIR)/property.xml
+property:
+	$(LITANI) init --project $(PROJECT_NAME)
+	$(MAKE) -B _property
+	$(LITANI) run-build
+
+_coverage: $(LOGDIR)/coverage.xml
+coverage:
+	$(LITANI) init --project $(PROJECT_NAME)
+	$(MAKE) -B _coverage
+	$(LITANI) run-build
+
+_report: $(PROOFDIR)/html
+report:
+	$(LITANI) init --project $(PROJECT_NAME)
+	$(MAKE) -B _report
+	$(LITANI) run-build
+
+_report2: $(PROOFDIR)/report
+report2:
+	$(LITANI) init --project $(PROJECT_NAME)
+	$(MAKE) -B _report2
+	$(LITANI) run-build
+
+
+################################################################
+# Targets to clean up after ourselves
+clean:
+	-$(RM) $(DEPENDENT_GOTOS)
+	-$(RM) TAGS*
+	-$(RM) *~ \#*
+	-$(RM) Makefile.arpa
+	-$(RM) -r $(ARPA_BLDDIR)
+
+veryclean: clean
+	-$(RM) -r html report
+	-$(RM) -r $(LOGDIR) $(GOTODIR)
+
+.PHONY: \
+  _coverage \
+  _goto \
+  _property \
+  _report \
+  _report2 \
+  _result \
+  arpa \
+  clean \
+  coverage \
+  goto \
+  litani-path \
+  property \
+  report \
+  report2 \
+  result \
+  setup_dependencies \
+  testdeps \
+  veryclean \
+  #
+
+################################################################
+
+# Rule for generating cbmc-batch.yaml, used by the CI at
+# https://github.com/awslabs/aws-batch-cbmc/
+
+JOB_OS ?= ubuntu16
+JOB_MEMORY ?= 32000
+
+# Proofs that are expected to fail should set EXPECTED to
+# "FAILED" in their Makefile. Values other than SUCCESSFUL
+# or FAILED will cause a CI error.
+EXPECTED ?= SUCCESSFUL
+
+define yaml_encode_options
+	"$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
+endef
+
+CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS)
+
+cbmc-batch.yaml:
+	@$(RM) $@
+	@echo 'build_memory: $(JOB_MEMORY)' > $@
+	@echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@
+	@echo 'coverage_memory: $(JOB_MEMORY)' >> $@
+	@echo 'expected: $(EXPECTED)' >> $@
+	@echo 'goto: $(HARNESS_GOTO).goto' >> $@
+	@echo 'jobos: $(JOB_OS)' >> $@
+	@echo 'property_memory: $(JOB_MEMORY)' >> $@
+	@echo 'report_memory: $(JOB_MEMORY)' >> $@
+
+.PHONY: cbmc-batch.yaml
+
+################################################################
+
+# Run "make echo-proof-uid" to print the proof ID of a proof. This can be
+# used by scripts to ensure that every proof has an ID, that there are
+# no duplicates, etc.
+
+.PHONY: echo-proof-uid
+echo-proof-uid:
+	@echo $(PROOF_UID)
+
+.PHONY: echo-project-name
+echo-project-name:
+	@echo $(PROJECT_NAME)
+
+################################################################
+
+# Project-specific targets requiring values defined above
+sinclude $(PROOF_ROOT)/Makefile-project-targets
+
+# CI-specific targets to drive cbmc in CI
+sinclude $(PROOF_ROOT)/Makefile-project-testing
+
+################################################################
diff --git a/test/cbmc/proofs/README.md b/test/cbmc/proofs/README.md
new file mode 100644
index 000000000..5e22aa01a
--- /dev/null
+++ b/test/cbmc/proofs/README.md
@@ -0,0 +1,27 @@
+CBMC proofs
+===========
+
+This directory contains the CBMC proofs.  Each proof is in its own
+directory.
+
+This directory includes four Makefiles.
+
+One Makefile describes the basic workflow for building and running proofs:
+
+* Makefile.common:
+    * make: builds the goto binary, does the cbmc property checking
+	  and coverage checking, and builds the final report.
+	* make goto: builds the goto binary
+	* make result: does cbmc property checking
+	* make coverage: does cbmc coverage checking
+	* make report: builds the final report
+
+Three included Makefiles describe project-specific settings and can override
+definitions in Makefile.common:
+
+* Makefile-project-defines: definitions like compiler flags
+  required to build the goto binaries, and definitions to override
+  definitions in Makefile.common.
+* Makefile-project-targets: other make targets needed for the project
+* Makefile-project-testing: other definitions and targets needed for
+  unit testing or continuous integration.
diff --git a/test/cbmc/proofs/prepare.py b/test/cbmc/proofs/prepare.py
new file mode 100644
index 000000000..d58805cad
--- /dev/null
+++ b/test/cbmc/proofs/prepare.py
@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+
+"""Prepare the source tree for proofs in continuous integration."""
+
+
+import os
+import subprocess
+
+
+MAKEFILE = "Makefile"
+CBMC_BATCH_YAML = "cbmc-batch.yaml"
+
+
+def create_cbmc_batch_yaml(folder):
+    """Run make to create cbmc-batch.yaml in folder."""
+
+    try:
+        subprocess.run(
+            ["make", "-B", CBMC_BATCH_YAML],
+            cwd=folder,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.PIPE,
+            universal_newlines=True,
+            check=True
+        )
+    except subprocess.CalledProcessError as error:
+        raise UserWarning("Failed to create {} in {}: "
+                          "command was '{}': "
+                          "error was '{}'"
+                          .format(CBMC_BATCH_YAML, folder,
+                                  ' '.join(error.cmd),
+                                  error.stderr.strip())) from None
+
+
+def create_cbmc_batch_yaml_files(root='.'):
+    """Create cbmc-batch.yaml in all directories under root."""
+
+    for folder, _, files in os.walk(root):
+        if CBMC_BATCH_YAML in files and MAKEFILE in files:
+            create_cbmc_batch_yaml(folder)
+
+
+def prepare():
+    """Prepare the source tree for proofs in continuous integration."""
+
+    create_cbmc_batch_yaml_files()
+
+
+if __name__ == "__main__":
+    prepare()
diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py
new file mode 100755
index 000000000..33d0f778f
--- /dev/null
+++ b/test/cbmc/proofs/run-cbmc-proofs.py
@@ -0,0 +1,365 @@
+#!/usr/bin/env python3
+#
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+
+import argparse
+import asyncio
+import json
+import logging
+import math
+import os
+import pathlib
+import re
+import subprocess
+import sys
+
+
+DESCRIPTION = "Configure and run all CBMC proofs in parallel"
+
+# Keep the epilog hard-wrapped at 70 characters, as it gets printed
+# verbatim in the terminal. 70 characters stops here --------------> |
+EPILOG = """
+This tool automates the process of running `make report` in each of
+the CBMC proof directories. The tool calculates the dependency graph
+of all tasks needed to build, run, and report on all the proofs, and
+executes these tasks in parallel.
+
+The tool is roughly equivalent to doing this:
+
+        litani init --project "my-cool-project";
+
+        find . -name cbmc-proof.txt | while read -r proof; do
+            pushd $(dirname ${proof});
+
+            # The `make _report` rule adds a single proof to litani
+            # without running it
+            make _report;
+
+            popd;
+        done
+
+        litani run-build;
+
+except that it is much faster and provides some convenience options.
+The CBMC CI runs this script with no arguments to build and run all
+proofs in parallel. The value of "my-cool-project" is taken from the
+PROJECT_NAME variable in Makefile-project-defines.
+
+The --no-standalone argument omits the `litani init` and `litani
+run-build`; use it when you want to add additional proof jobs, not
+just the CBMC ones. In that case, you would run `litani init`
+yourself; then run `run-cbmc-proofs --no-standalone`; add any
+additional jobs that you want to execute with `litani add-job`; and
+finally run `litani run-build`.
+
+The litani dashboard will be written under the `output` directory; the
+cbmc-viewer reports remain in the `$PROOF_DIR/report` directory. The
+HTML dashboard from the latest Litani run will always be symlinked to
+`output/latest/html/index.html`, so you can keep that page open in
+your browser and reload the page whenever you re-run this script.
+"""
+# 70 characters stops here ----------------------------------------> |
+
+
+def get_project_name():
+    cmd = [
+        "make",
+        "-f", "Makefile.common",
+        "echo-project-name",
+    ]
+    logging.debug(" ".join(cmd))
+    proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE)
+    if proc.returncode:
+        logging.critical("could not run make to determine project name")
+        sys.exit(1)
+    if not proc.stdout.strip():
+        logging.warning(
+            "project name has not been set; using generic name instead. "
+            "Set the PROJECT_NAME value in Makefile-project-defines to "
+            "remove this warning")
+        return "<PROJECT NAME HERE>"
+    return proc.stdout.strip()
+
+
+def get_args():
+    pars = argparse.ArgumentParser(
+        description=DESCRIPTION, epilog=EPILOG,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    for arg in [{
+            "flags": ["-j", "--parallel-jobs"],
+            "type": int,
+            "metavar": "N",
+            "help": "run at most N proof jobs in parallel",
+    }, {
+            "flags": ["--no-standalone"],
+            "action": "store_true",
+            "help": "only configure proofs: do not initialize nor run",
+    }, {
+            "flags": ["-p", "--proofs"],
+            "nargs": "+",
+            "metavar": "DIR",
+            "help": "only run proof in directory DIR (can pass more than one)",
+    }, {
+            "flags": ["--project-name"],
+            "metavar": "NAME",
+            "default": get_project_name(),
+            "help": "project name for report. Default: %(default)s",
+    }, {
+            "flags": ["--proof-marker"],
+            "metavar": "FILE",
+            "default": "cbmc-proof.txt",
+            "help": (
+                "name of file that marks proof directories. Default: "
+                "%(default)s"),
+    }, {
+            "flags": ["--no-memory-profile"],
+            "action": "store_true",
+            "help": "disable memory profiling, even if Litani supports it"
+    }, {
+            "flags": ["--no-expensive-limit"],
+            "action": "store_true",
+            "help": "do not limit parallelism of 'EXPENSIVE' jobs",
+    }, {
+            "flags": ["--expensive-jobs-parallelism"],
+            "metavar": "N",
+            "default": 1,
+            "type": int,
+            "help": (
+                "how many proof jobs marked 'EXPENSIVE' to run in parallel. "
+                "Default: %(default)s"),
+    }, {
+            "flags": ["--verbose"],
+            "action": "store_true",
+            "help": "verbose output",
+    }]:
+        flags = arg.pop("flags")
+        pars.add_argument(*flags, **arg)
+    return pars.parse_args()
+
+
+def set_up_logging(verbose):
+    if verbose:
+        level = logging.DEBUG
+    else:
+        level = logging.WARNING
+    logging.basicConfig(
+        format="run-cbmc-proofs: %(message)s", level=level)
+
+
+def task_pool_size():
+    ret = os.cpu_count()
+    if ret is None or ret < 3:
+        return 1
+    return ret - 2
+
+
+def print_counter(counter):
+    print(
+        "\rConfiguring CBMC proofs: "
+        "{complete:{width}} / {total:{width}}".format(
+            **counter), end="", file=sys.stderr)
+
+
+def get_proof_dirs(proof_root, proof_list, proof_marker):
+    if proof_list is not None:
+        proofs_remaining = list(proof_list)
+    else:
+        proofs_remaining = []
+
+    for root, _, fyles in os.walk(proof_root):
+        proof_name = str(pathlib.Path(root).name)
+        if proof_list and proof_name not in proof_list:
+            continue
+        if proof_list and proof_name in proofs_remaining:
+            proofs_remaining.remove(proof_name)
+        if proof_marker in fyles:
+            yield root
+
+    if proofs_remaining:
+        logging.critical(
+            "The following proofs were not found: %s",
+            ", ".join(proofs_remaining))
+        sys.exit(1)
+
+
+def run_build(litani, jobs):
+    cmd = [str(litani), "run-build"]
+    if jobs:
+        cmd.extend(["-j", str(jobs)])
+
+    logging.debug(" ".join(cmd))
+    proc = subprocess.run(cmd)
+    if proc.returncode:
+        logging.critical("Failed to run litani run-build")
+        sys.exit(1)
+
+
+def get_litani_path(proof_root):
+    cmd = [
+        "make",
+        "PROOF_ROOT=%s" % proof_root,
+        "-f", "Makefile.common",
+        "litani-path",
+    ]
+    logging.debug(" ".join(cmd))
+    proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE)
+    if proc.returncode:
+        logging.critical("Could not determine path to litani")
+        sys.exit(1)
+    return proc.stdout.strip()
+
+
+def get_litani_capabilities(litani_path):
+    cmd = [litani_path, "print-capabilities"]
+    proc = subprocess.run(
+        cmd, text=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL)
+    if proc.returncode:
+        return []
+    try:
+        return json.loads(proc.stdout)
+    except RuntimeError:
+        logging.warning("Could not load litani capabilities: '%s'", proc.stdout)
+        return []
+
+
+def check_uid_uniqueness(proof_dir, proof_uids):
+    with (pathlib.Path(proof_dir) / "Makefile").open() as handle:
+        for line in handle:
+            m = re.match(r"^PROOF_UID\s*=\s*(?P<uid>\w+)", line)
+            if not m:
+                continue
+            if m["uid"] not in proof_uids:
+                proof_uids[m["uid"]] = proof_dir
+                return
+
+            logging.critical(
+                "The Makefile in directory '%s' should have a different "
+                "PROOF_UID than the Makefile in directory '%s'",
+                proof_dir, proof_uids[m["uid"]])
+            sys.exit(1)
+
+    logging.critical(
+        "The Makefile in directory '%s' should contain a line like", proof_dir)
+    logging.critical("PROOF_UID = ...")
+    logging.critical("with a unique identifier for the proof.")
+    sys.exit(1)
+
+
+def should_enable_memory_profiling(litani_caps, args):
+    if args.no_memory_profile:
+        return False
+    return "memory_profile" in litani_caps
+
+
+def should_enable_pools(litani_caps, args):
+    if args.no_expensive_limit:
+        return False
+    return "pools" in litani_caps
+
+
+async def configure_proof_dirs(
+    queue, counter, proof_uids, enable_pools, enable_memory_profiling):
+    while True:
+        print_counter(counter)
+        path = str(await queue.get())
+
+        check_uid_uniqueness(path, proof_uids)
+
+        pools = ["ENABLE_POOLS=true"] if enable_pools else []
+        profiling = [
+            "ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else []
+
+        proc = await asyncio.create_subprocess_exec(
+            # Allow interactive tasks to preempt proof configuration
+            "nice", "-n", "15", "make", *pools, *profiling, "-B", "--quiet",
+            "_report", cwd=path)
+        await proc.wait()
+        counter["fail" if proc.returncode else "pass"].append(path)
+        counter["complete"] += 1
+
+        print_counter(counter)
+        queue.task_done()
+
+
+async def main():
+    args = get_args()
+    set_up_logging(args.verbose)
+
+    proof_root = pathlib.Path(__file__).resolve().parent
+    litani = get_litani_path(proof_root)
+
+    litani_caps = get_litani_capabilities(litani)
+    enable_pools = should_enable_pools(litani_caps, args)
+    init_pools = [
+        "--pools", f"expensive:{args.expensive_jobs_parallelism}"
+    ] if enable_pools else []
+
+    if not args.no_standalone:
+        cmd = [str(litani), "init", *init_pools, "--project", args.project_name]
+
+        if "output_directory_flags" in litani_caps:
+            out_prefix = proof_root / "output"
+            out_symlink = out_prefix / "latest"
+            out_index = out_symlink / "html" / "index.html"
+            cmd.extend([
+                "--output-prefix", str(out_prefix),
+                "--output-symlink", str(out_symlink),
+            ])
+            print(
+                "\nFor your convenience, the output of this run will be "
+                "symbolically linked to %s\n" % str(out_index))
+
+        logging.debug(" ".join(cmd))
+        proc = subprocess.run(cmd)
+        if proc.returncode:
+            logging.critical("Failed to run litani init")
+            sys.exit(1)
+
+    proof_dirs = list(get_proof_dirs(
+        proof_root, args.proofs, args.proof_marker))
+    if not proof_dirs:
+        logging.critical("No proof directories found")
+        sys.exit(1)
+
+    proof_queue = asyncio.Queue()
+    for proof_dir in proof_dirs:
+        proof_queue.put_nowait(proof_dir)
+
+    counter = {
+        "pass": [],
+        "fail": [],
+        "complete": 0,
+        "total": len(proof_dirs),
+        "width": int(math.log10(len(proof_dirs))) + 1
+    }
+
+    proof_uids = {}
+    tasks = []
+
+    enable_memory_profiling = should_enable_memory_profiling(litani_caps, args)
+
+    for _ in range(task_pool_size()):
+        task = asyncio.create_task(configure_proof_dirs(
+            proof_queue, counter, proof_uids, enable_pools,
+            enable_memory_profiling))
+        tasks.append(task)
+
+    await proof_queue.join()
+
+    print_counter(counter)
+    print("", file=sys.stderr)
+
+    if counter["fail"]:
+        logging.critical(
+            "Failed to configure the following proofs:\n%s", "\n".join(
+                [str(f) for f in counter["fail"]]))
+        sys.exit(1)
+
+    if not args.no_standalone:
+        run_build(litani, args.parallel_jobs)
+
+
+if __name__ == "__main__":
+    asyncio.run(main())

From 21ee448b512bfe648bf7d8ba5323221111363e4e Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 10:30:48 +0000
Subject: [PATCH 02/19] Added value to not update the submodule

---
 .gitmodules | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitmodules b/.gitmodules
index bfe815c15..de2986481 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -11,6 +11,8 @@
 [submodule "test/cbmc/aws-templates-for-cbmc-proofs"]
 	path = test/cbmc/aws-templates-for-cbmc-proofs
 	url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git
+	update = none
 [submodule "test/cbmc/litani"]
 	path = test/cbmc/litani
 	url = https://github.com/awslabs/aws-build-accumulator.git
+	update = none
\ No newline at end of file

From 4b189aa8bc35bcce0420f9418ca5845e82854301 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 11:08:25 +0000
Subject: [PATCH 03/19] Added Include paths and preprocessor defines

---
 test/cbmc/proofs/Makefile.common | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common
index fb0844b70..3e9c0b05d 100644
--- a/test/cbmc/proofs/Makefile.common
+++ b/test/cbmc/proofs/Makefile.common
@@ -260,10 +260,10 @@ COMPILE_FLAGS ?=
 LINK_FLAGS ?=
 
 # Preprocessor include paths -I...
-INCLUDES ?=
+INCLUDES += -I$(SRCDIR)/source/include/
 
 # Preprocessor definitions -D...
-DEFINES ?=
+DEFINES += -DOTA_DO_NOT_USE_CUSTOM_CONFIG
 
 # CBMC object model
 #
@@ -860,3 +860,4 @@ sinclude $(PROOF_ROOT)/Makefile-project-targets
 sinclude $(PROOF_ROOT)/Makefile-project-testing
 
 ################################################################
+

From ae17c099ef0158df7b75a9f33d9dec08f8b0fa05 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 11:29:02 +0000
Subject: [PATCH 04/19] Added template define file

---
 test/cbmc/proofs/Makefile-template-defines | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test/cbmc/proofs/Makefile-template-defines

diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines
new file mode 100644
index 000000000..5b09353ac
--- /dev/null
+++ b/test/cbmc/proofs/Makefile-template-defines
@@ -0,0 +1,11 @@
+
+# Absolute path to the root of the source tree.
+#
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
+
+
+# Absolute path to the litani script.
+#
+LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani)
+PROJECT_NAME = "AWS IoT Over-the-air Update Library"
+

From 4a2ed43c36c1b18be3adb9d51097c7ea6c569c80 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 11:36:42 +0000
Subject: [PATCH 05/19] Updated to ignore the output files on git push

---
 test/cbmc/.gitignore | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test/cbmc/.gitignore

diff --git a/test/cbmc/.gitignore b/test/cbmc/.gitignore
new file mode 100644
index 000000000..1e5826a7b
--- /dev/null
+++ b/test/cbmc/.gitignore
@@ -0,0 +1,24 @@
+# Emitted when running CBMC proofs
+proofs/**/logs
+proofs/**/gotos
+proofs/**/report
+proofs/**/html
+proofs/output
+
+# Emitted by CBMC Viewer
+TAGS-*
+
+# Emitted by Arpa
+arpa_cmake/
+arpa-validation-logs/
+Makefile.arpa
+
+# Emitted by litani
+.ninja_deps
+.ninja_log
+.litani_cache_dir
+
+# These files should be overwritten whenever prepare.py runs
+cbmc-batch.yaml
+
+__pycache__/

From 6c5d6f5c547fd0188c8b6ab2d59d375c7744a8b6 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 11:47:15 +0000
Subject: [PATCH 06/19] Added words

---
 tools/lexicon.txt | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/tools/lexicon.txt b/tools/lexicon.txt
index df311aafa..c9252ccc3 100644
--- a/tools/lexicon.txt
+++ b/tools/lexicon.txt
@@ -28,6 +28,7 @@ bitmaplen
 bitmask
 blockbitmapmaxsize
 blockbitmapsize
+blockid
 blockindex
 blockindex
 blockoffset
@@ -47,6 +48,7 @@ bytestosend
 c89
 c90
 ca
+cbmc
 cbor
 cborarray
 cborerror
@@ -98,6 +100,7 @@ cwd
 datablock
 datacallback
 datalength
+decodeandstoredatablock
 decodemem
 decodememmaxsize
 decodememorysize
@@ -113,6 +116,7 @@ destlen
 destoffset
 developerguide
 didn
+div
 dns
 docmodel
 docparam
@@ -548,6 +552,7 @@ pfilepath
 pfinalfile
 pformat
 phostname
+phttp
 pjobdocjson
 pjobid
 pjobname
@@ -702,6 +707,7 @@ sendtimeout
 sendtimeoutms
 serverfileid
 serverinfo
+setcontrolinterface
 setdatainterface
 setimagestate
 setplatformimagestate
@@ -715,6 +721,7 @@ snihostname
 sockaddr
 sockets_invalid_parameter
 socketstatus
+spdx
 srand
 src
 ssl
@@ -801,6 +808,7 @@ urlsize
 useraborthandler
 ustopiclen
 utils
+validateandstartjob
 validatedatablock
 valuelength
 verifyactivejobstatus

From b4a774c19cfd4342e4584d880ee64f56bc745cee Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 12:00:06 +0000
Subject: [PATCH 07/19] Updated Project Name

---
 test/cbmc/proofs/Makefile-template-defines | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines
index 5b09353ac..a9e99859d 100644
--- a/test/cbmc/proofs/Makefile-template-defines
+++ b/test/cbmc/proofs/Makefile-template-defines
@@ -1,11 +1,19 @@
 
 # Absolute path to the root of the source tree.
 #
-SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-emebedded-sdk)
 
 
 # Absolute path to the litani script.
 #
 LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani)
+
+
+# Name of this proof project, displayed in proof reports. For example,
+# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots,
+# this may be overridden on the command-line to Make, for example
+#
+# 	  make PROJECT_NAME="FreeRTOS MQTT" report
+#
 PROJECT_NAME = "AWS IoT Over-the-air Update Library"
 

From db409b71cef47072f2382862d55178c0da22d13b Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 12:31:55 +0000
Subject: [PATCH 08/19] Updated source directory path

---
 test/cbmc/proofs/Makefile-template-defines | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines
index a9e99859d..0c8a3c391 100644
--- a/test/cbmc/proofs/Makefile-template-defines
+++ b/test/cbmc/proofs/Makefile-template-defines
@@ -1,7 +1,7 @@
 
 # Absolute path to the root of the source tree.
 #
-SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-emebedded-sdk)
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-embedded-sdk/)
 
 
 # Absolute path to the litani script.

From 62ddec4f502b2d27278d2f889252792828f6bd25 Mon Sep 17 00:00:00 2001
From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu, 5 Aug 2021 09:26:17 -0700
Subject: [PATCH 09/19] Add checks on the branch

---
 .github/workflows/ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8b98744ef..383b68fd5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -7,6 +7,7 @@ on:
     branches:
       - main
       - development
+      - cbmc-proof
   workflow_dispatch:
 
 jobs:

From 67ad6b0fb286e263992d7658abd9e94483f5710c Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 16:33:53 +0000
Subject: [PATCH 10/19] Updated Submodule update value

---
 .gitmodules | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.gitmodules b/.gitmodules
index de2986481..04bdf5d8e 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -15,4 +15,3 @@
 [submodule "test/cbmc/litani"]
 	path = test/cbmc/litani
 	url = https://github.com/awslabs/aws-build-accumulator.git
-	update = none
\ No newline at end of file

From 3bda16abcd0cf4719896abcb16c3d36285ead9f2 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 16:46:47 +0000
Subject: [PATCH 11/19] Added litani submodule update

---
 .gitmodules | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitmodules b/.gitmodules
index 04bdf5d8e..de2986481 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -15,3 +15,4 @@
 [submodule "test/cbmc/litani"]
 	path = test/cbmc/litani
 	url = https://github.com/awslabs/aws-build-accumulator.git
+	update = none
\ No newline at end of file

From 2c7f2eee2df4b4e072e58f2ecfccc7aec647c12f Mon Sep 17 00:00:00 2001
From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com>
Date: Thu, 5 Aug 2021 09:51:09 -0700
Subject: [PATCH 12/19] Update Project name

Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
---
 test/cbmc/proofs/Makefile-template-defines | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines
index 0c8a3c391..a4fcaa007 100644
--- a/test/cbmc/proofs/Makefile-template-defines
+++ b/test/cbmc/proofs/Makefile-template-defines
@@ -13,7 +13,6 @@ LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani)
 # "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots,
 # this may be overridden on the command-line to Make, for example
 #
-# 	  make PROJECT_NAME="FreeRTOS MQTT" report
+# 	  make PROJECT_NAME="AWS IoT Over-the-air Update Library" report
 #
 PROJECT_NAME = "AWS IoT Over-the-air Update Library"
-

From e88c8c02d940e62bee9919b1870622e84c23f4d4 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 16:52:43 +0000
Subject: [PATCH 13/19] Added new line in the end of the file

---
 .gitmodules | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitmodules b/.gitmodules
index de2986481..a53db1696 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -15,4 +15,5 @@
 [submodule "test/cbmc/litani"]
 	path = test/cbmc/litani
 	url = https://github.com/awslabs/aws-build-accumulator.git
-	update = none
\ No newline at end of file
+	update = none
+	
\ No newline at end of file

From d274f81a503e530b3b1251f1223b408c4660a40d Mon Sep 17 00:00:00 2001
From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu, 5 Aug 2021 09:54:41 -0700
Subject: [PATCH 14/19] Remove whitespace

---
 .gitmodules | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.gitmodules b/.gitmodules
index a53db1696..89f9e83c9 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -16,4 +16,3 @@
 	path = test/cbmc/litani
 	url = https://github.com/awslabs/aws-build-accumulator.git
 	update = none
-	
\ No newline at end of file

From f54e3bd902795c27c1a6247bd3ab02e1b40b4ea6 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Thu, 5 Aug 2021 17:14:52 +0000
Subject: [PATCH 15/19] Added CBMC proof for setDataInterface function

---
 test/cbmc/proofs/setDataInterface/Makefile    | 25 +++++++++
 test/cbmc/proofs/setDataInterface/README.md   | 20 +++++++
 .../proofs/setDataInterface/cbmc-proof.txt    |  2 +
 .../proofs/setDataInterface/cbmc-viewer.json  |  7 +++
 .../setDataInterface_harness.c                | 55 +++++++++++++++++++
 5 files changed, 109 insertions(+)
 create mode 100644 test/cbmc/proofs/setDataInterface/Makefile
 create mode 100644 test/cbmc/proofs/setDataInterface/README.md
 create mode 100644 test/cbmc/proofs/setDataInterface/cbmc-proof.txt
 create mode 100644 test/cbmc/proofs/setDataInterface/cbmc-viewer.json
 create mode 100644 test/cbmc/proofs/setDataInterface/setDataInterface_harness.c

diff --git a/test/cbmc/proofs/setDataInterface/Makefile b/test/cbmc/proofs/setDataInterface/Makefile
new file mode 100644
index 000000000..5c1616df7
--- /dev/null
+++ b/test/cbmc/proofs/setDataInterface/Makefile
@@ -0,0 +1,25 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = setDataInterface_harness
+HARNESS_FILE = $(HARNESS_ENTRY)
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = setDataInterface
+
+DEFINES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/ota_interface.c
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+include ../Makefile.common
diff --git a/test/cbmc/proofs/setDataInterface/README.md b/test/cbmc/proofs/setDataInterface/README.md
new file mode 100644
index 000000000..bfc464cd6
--- /dev/null
+++ b/test/cbmc/proofs/setDataInterface/README.md
@@ -0,0 +1,20 @@
+setDataaInterface proof
+==============
+
+This directory contains a memory safety proof for setDataInterface.
+
+To run the proof.
+-------------
+
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open html/index.html in a web browser.
+
+To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles.
+-------------
+
+* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
+* Use Makefile.arpa as the starting point for your proof Makefile by:
+  1. Modifying Makefile.arpa (if required).
+  2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).
diff --git a/test/cbmc/proofs/setDataInterface/cbmc-proof.txt b/test/cbmc/proofs/setDataInterface/cbmc-proof.txt
new file mode 100644
index 000000000..0639406e3
--- /dev/null
+++ b/test/cbmc/proofs/setDataInterface/cbmc-proof.txt
@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory.
\ No newline at end of file
diff --git a/test/cbmc/proofs/setDataInterface/cbmc-viewer.json b/test/cbmc/proofs/setDataInterface/cbmc-viewer.json
new file mode 100644
index 000000000..a9cb231ec
--- /dev/null
+++ b/test/cbmc/proofs/setDataInterface/cbmc-viewer.json
@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "setDataInterface",
+  "proof-root": "test/cbmc/proofs"
+}
diff --git a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
new file mode 100644
index 000000000..5c55fb24c
--- /dev/null
+++ b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
@@ -0,0 +1,55 @@
+/*
+ * AWS IoT Over-the-air Update v3.0.0
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file setDataInterface_harness.c
+ * @brief Implements the proof harness for setDataInterface function.
+ */
+/* Ota interface includes. */
+#include "ota_interface_private.h"
+
+void setDataInterface_harness()
+{
+    OtaDataInterface_t * pDataInterface;
+    OtaDataInterface_t dataInterface;
+    OtaErr_t err;
+
+    uint8_t * pProtocol;
+    size_t protocolBufferSize;
+
+    /* The maximum size of the protocol buffer is defined by OTA_PROTOCOL_BUFFER_SIZE
+     *  and thus size variable cannot exceed OTA_PROTOCOL_BUFFER_SIZE. */
+    __CPROVER_assume( protocolBufferSize <= OTA_PROTOCOL_BUFFER_SIZE );
+
+    pProtocol = ( uint8_t * ) malloc( protocolBufferSize );
+    pDataInterface = &dataInterface;
+
+    err = setDataInterface( pDataInterface, pProtocol );
+
+    /* The function return can only be either of two values i.e OtaErrNone or
+     *  OtaErrInvalidDataProtocol. */
+    __CPROVER_assert( ( err == OtaErrInvalidDataProtocol ) || ( err == OtaErrNone ),
+                      "The function return can be either of those values." );
+
+    /* Free variables. */
+    free( pProtocol );
+}

From 6584e87f79a86a2e5943af583d8daa258dd66ee5 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Fri, 6 Aug 2021 00:25:23 +0000
Subject: [PATCH 16/19] removed unnecessary variables

---
 .../setDataInterface/setDataInterface_harness.c     | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
index 5c55fb24c..0fd51af49 100644
--- a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
+++ b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
@@ -33,14 +33,11 @@ void setDataInterface_harness()
     OtaDataInterface_t dataInterface;
     OtaErr_t err;
 
-    uint8_t * pProtocol;
-    size_t protocolBufferSize;
+    /* The input to the setDataInterface is a buffer statically initialized in the 
+        source code with its size defined by OTA_PROTOCOL_BUFFER_SIZE. This macro is 
+        not user configurable and thus the input does not require any constraint. */
+    uint8_t pProtocol[OTA_PROTOCOL_BUFFER_SIZE];
 
-    /* The maximum size of the protocol buffer is defined by OTA_PROTOCOL_BUFFER_SIZE
-     *  and thus size variable cannot exceed OTA_PROTOCOL_BUFFER_SIZE. */
-    __CPROVER_assume( protocolBufferSize <= OTA_PROTOCOL_BUFFER_SIZE );
-
-    pProtocol = ( uint8_t * ) malloc( protocolBufferSize );
     pDataInterface = &dataInterface;
 
     err = setDataInterface( pDataInterface, pProtocol );
@@ -50,6 +47,4 @@ void setDataInterface_harness()
     __CPROVER_assert( ( err == OtaErrInvalidDataProtocol ) || ( err == OtaErrNone ),
                       "The function return can be either of those values." );
 
-    /* Free variables. */
-    free( pProtocol );
 }

From 00c584ff56af2ffd29297de27a527a4687706687 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Fri, 6 Aug 2021 00:26:20 +0000
Subject: [PATCH 17/19] Updated documentation

---
 test/cbmc/proofs/Makefile-template-defines         | 2 +-
 test/cbmc/proofs/setDataInterface/README.md        | 2 +-
 test/cbmc/proofs/setDataInterface/cbmc-viewer.json | 1 -
 3 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines
index a4fcaa007..31eddd08c 100644
--- a/test/cbmc/proofs/Makefile-template-defines
+++ b/test/cbmc/proofs/Makefile-template-defines
@@ -1,7 +1,7 @@
 
 # Absolute path to the root of the source tree.
 #
-SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-embedded-sdk/)
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../)
 
 
 # Absolute path to the litani script.
diff --git a/test/cbmc/proofs/setDataInterface/README.md b/test/cbmc/proofs/setDataInterface/README.md
index bfc464cd6..48169f993 100644
--- a/test/cbmc/proofs/setDataInterface/README.md
+++ b/test/cbmc/proofs/setDataInterface/README.md
@@ -1,4 +1,4 @@
-setDataaInterface proof
+setDataInterface proof
 ==============
 
 This directory contains a memory safety proof for setDataInterface.
diff --git a/test/cbmc/proofs/setDataInterface/cbmc-viewer.json b/test/cbmc/proofs/setDataInterface/cbmc-viewer.json
index a9cb231ec..13f4418c3 100644
--- a/test/cbmc/proofs/setDataInterface/cbmc-viewer.json
+++ b/test/cbmc/proofs/setDataInterface/cbmc-viewer.json
@@ -1,6 +1,5 @@
 { "expected-missing-functions":
   [
-
   ],
   "proof-name": "setDataInterface",
   "proof-root": "test/cbmc/proofs"

From 11e33e5c9df4bd77f0842150f3e852ab895a4e49 Mon Sep 17 00:00:00 2001
From: bujain <bujain@amazon.com>
Date: Fri, 6 Aug 2021 00:37:51 +0000
Subject: [PATCH 18/19] Uncrustified

---
 .../proofs/setDataInterface/setDataInterface_harness.c   | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
index 0fd51af49..db4baf63a 100644
--- a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
+++ b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
@@ -33,10 +33,10 @@ void setDataInterface_harness()
     OtaDataInterface_t dataInterface;
     OtaErr_t err;
 
-    /* The input to the setDataInterface is a buffer statically initialized in the 
-        source code with its size defined by OTA_PROTOCOL_BUFFER_SIZE. This macro is 
-        not user configurable and thus the input does not require any constraint. */
-    uint8_t pProtocol[OTA_PROTOCOL_BUFFER_SIZE];
+    /* The input to the setDataInterface is a buffer statically initialized in the
+     *  source code with its size defined by OTA_PROTOCOL_BUFFER_SIZE. This macro is
+     *  not user configurable and thus the input does not require any constraint. */
+    uint8_t pProtocol[ OTA_PROTOCOL_BUFFER_SIZE ];
 
     pDataInterface = &dataInterface;
 
@@ -46,5 +46,4 @@ void setDataInterface_harness()
      *  OtaErrInvalidDataProtocol. */
     __CPROVER_assert( ( err == OtaErrInvalidDataProtocol ) || ( err == OtaErrNone ),
                       "The function return can be either of those values." );
-
 }

From 2d459eee2d0d7b6ca903000a2bd07a8b690139c6 Mon Sep 17 00:00:00 2001
From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com>
Date: Fri, 6 Aug 2021 16:19:00 -0700
Subject: [PATCH 19/19] Updated year in copyright notice

---
 test/cbmc/proofs/setDataInterface/setDataInterface_harness.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
index db4baf63a..445d40130 100644
--- a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
+++ b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c
@@ -1,6 +1,6 @@
 /*
  * AWS IoT Over-the-air Update v3.0.0
- * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in