Stub out hdr_write. Use default CBMC_OBJECT_BITS value

verification/cbmc/proofs/sign_header/Makefile

@@ -18,9 +18,7 @@ include ../Makefile.local_default
 include ../Makefile.aws_byte_buf
 include ../Makefile.string
 
-
 PROOF_UID = sign_header
-
 HARNESS_ENTRY = $(PROOF_UID)_harness
 HARNESS_FILE = $(HARNESS_ENTRY).c
 
@@ -39,14 +37,6 @@ DEFINES += -DMAX_TRACE_LIST_ITEMS=$(MAX_TRACE_LIST_ITEMS)
 DEFINES += -DMAX_IV_LEN=$(MAX_IV_LEN)
 DEFINES += -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=array_list_item_generator
 
-# The maximum number of objects is set to 2^8 = 256. This option changes that to 2^9. 
-# Without this flag, running this proof causes the CBMC error of 
-# "too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8);
-# use the `--object-bits n` option to increase the maximum number"
-# The proof hits the error when the line "rv = aws_cryptosdk_hdr_write(&session->header,
-# &actual_size, session->header_copy, session->header_size);" is reached.
-CBMC_OBJECT_BITS = 9
-
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c
@@ -86,6 +76,7 @@ PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_sort_noop_stub.c
 PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c
 PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_hash_elems_array_init_stub.c
 PROOF_SOURCES += $(PROOF_STUB)/aws_default_allocator_stub.c
+PROOF_SOURCES += $(PROOF_STUB)/hdr_write_stub.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
 REMOVE_FUNCTION_BODY += aws_array_list_get_at_ptr

verification/cbmc/stubs/hdr_write_stub.c

@@ -0,0 +1,46 @@
+/*
+ * 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.
+ */
+
+#include <aws/cryptosdk/private/header.h>
+
+#include <proof_helpers/make_common_data_structures.h>
+
+/*
+ * Stub for aws_cryptosdk_hdr_write
+ * The original function declares an aws_byte_buf output variable where
+ * different components of the header get written, but the actual output
+ * of the function is bytes_written. Therefore, we assign a nondet. value
+ * to this variable in case of success or zero both outbuf and outlen in
+ * case of failure
+ */
+int aws_cryptosdk_hdr_write(
+    const struct aws_cryptosdk_hdr *hdr, size_t *bytes_written, uint8_t *outbuf, size_t outlen) {
+    assert(aws_cryptosdk_hdr_is_valid(hdr));
+    assert(hdr->iv.len <= UINT8_MAX);  // uint8_t max value
+    assert(outlen == 0 || AWS_MEM_IS_READABLE(outbuf, outlen));
+    assert(bytes_written != NULL);
+
+    if (nondet_bool()) {
+        size_t nondet_size;
+        __CPROVER_assume(nondet_size < MAX_BUFFER_SIZE);
+        *bytes_written = nondet_size;
+        return AWS_OP_SUCCESS;
+    } else {
+        int error = nondet_bool() ? AWS_CRYPTOSDK_ERR_BAD_STATE : AWS_ERROR_SHORT_BUFFER;
+        aws_secure_zero(outbuf, outlen);
+        *bytes_written = 0;
+        return aws_raise_error(error);
+    }
+}