Added CBMC proof of stringBuilder function

test/cbmc/proofs/stringBuilder/Makefile

@@ -0,0 +1,28 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = stringBuilder_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 = stringBuilder
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+CBMC_FLAG_UNWINDING_ASSERTIONS =
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.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

test/cbmc/proofs/stringBuilder/README.md

@@ -0,0 +1,20 @@
+stringBuilder proof
+==============
+
+This directory contains a memory safety proof for stringBuilder.
+
+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`).

test/cbmc/proofs/stringBuilder/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

test/cbmc/proofs/stringBuilder/cbmc-viewer.json

@@ -0,0 +1,6 @@
+{ "expected-missing-functions":
+  [
+  ],
+  "proof-name": "<__FUNCTION_NAME__>",
+  "proof-root": "<__PATH_TO_PROOF_ROOT__>"
+}

test/cbmc/proofs/stringBuilder/stringBuilder_harness.c

@@ -0,0 +1,71 @@
+/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */
+/* SPDX-License-Identifier: Apache-2.0 */
+
+/**
+ * @file stringBuilder_harness.c
+ * @brief Implements the proof harness for stringBuilder function.
+ */
+#include "ota_mqtt_private.h"
+
+/* Declaration of the mangled name function generated by CBMC for static functions. */
+size_t __CPROVER_file_local_ota_mqtt_c_stringBuilder( char * pBuffer,
+                                                      size_t bufferSizeBytes,
+                                                      const char * strings[] );
+
+void stringBuilder_harness()
+{
+    char * pBuffer;
+    size_t bufferSizeBytes;
+    char ** strings;
+
+    size_t numStrings;
+    size_t stringSize;
+    size_t i;
+    size_t stringLength;
+
+    /* The pBuffer is statically allocated with a non-zero size before passing it to the stringBuilder function.*/
+    __CPROVER_assume( bufferSizeBytes > 0 );
+    pBuffer = ( char * ) malloc( bufferSizeBytes );
+
+    /* pBuffer can never be NULL since it it always initialized before passing it to the stringBuilder function. */
+    __CPROVER_assume( pBuffer != NULL );
+
+    /* The minimum and the maximum number of strings inside the numStrings are 0 and 11. */
+    __CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX );
+
+    /* Initializing an array of strings with size numStrings. */
+    strings = ( char ** ) malloc( numStrings * sizeof( char * ) );
+
+    /* The size of each string inside the strings array passed to the stringBuilder
+     * function is greater than 0. */
+    __CPROVER_assume( stringSize > 0 );
+
+    /* The strings array cannot be NULL as it is always initialized before
+     *  passing to the function. */
+    __CPROVER_assume( strings != NULL );
+
+    for( i = 0; i < numStrings - 1; ++i )
+    {
+        strings[ i ] = ( char * ) malloc( stringSize );
+
+        /* The strings inside the strings array are defined before passing it to
+         * the stringBuilder function. */
+        __CPROVER_assume( strings[ i ] != NULL );
+        strings[ i ][ stringSize - 1 ] = '\0';
+    }
+
+    /* Strings array is always passed with a NULL string at the end. */
+    __CPROVER_assume( strings[ numStrings - 1 ] == NULL );
+
+    __CPROVER_file_local_ota_mqtt_c_stringBuilder( pBuffer, bufferSizeBytes, strings );
+
+    /* Free the allocated memory. */
+    free( pBuffer );
+
+    for( i = 0; i < numStrings - 1; ++i )
+    {
+        free( strings[ i ] );
+    }
+
+    free( strings );
+}