chore: update aws-c-common dependency for CBMC proofs

CBMC proofs should use the same version of aws-c-common that customers
will use in their deployments. Stubs that had since been removed from
aws-c-common have now been moved into this repository.

Author: tautschnig

verification/cbmc/aws-c-common

@@ -21,7 +21,6 @@
 #include <aws/cryptosdk/private/header.h>
 #include <aws/cryptosdk/private/hkdf.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 #include <stdint.h>
 #include <stdlib.h>

verification/cbmc/include/make_common_data_structures.h

@@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 CBMCFLAGS +=
 
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
@@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
 PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/include/proof_allocators.h

@@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 CBMCFLAGS +=
 
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
@@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
 PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile

@@ -37,7 +37,6 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile

@@ -19,7 +19,6 @@
 #include <aws/cryptosdk/materials.h>
 #include <make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 void aws_cryptosdk_cmm_base_init_harness() {

verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile

@@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
 PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c

verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c

@@ -23,7 +23,6 @@
 #include <make_common_data_structures.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 // Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
@@ -52,7 +51,7 @@ int decrypt_materials(
     assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
     assert(aws_cryptosdk_dec_request_is_valid(request));
 
-    struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
+    struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
     if (materials == NULL) {
         *output = NULL;
         return AWS_OP_ERR;
@@ -92,15 +91,15 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
                                                  .decrypt_materials      = nondet_bool() ? decrypt_materials : NULL };
     __CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
 
-    struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
+    struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
     __CPROVER_assume(cmm);
     cmm->vtable = &vtable;
     __CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));
 
-    struct aws_cryptosdk_dec_request *request = can_fail_malloc(sizeof(*request));
+    struct aws_cryptosdk_dec_request *request = malloc(sizeof(*request));
     __CPROVER_assume(request);
-    request->alloc   = can_fail_allocator();
-    request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
+    request->alloc   = aws_default_allocator();
+    request->enc_ctx = malloc(sizeof(*request->enc_ctx));
     __CPROVER_assume(request->enc_ctx);
     ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
 
@@ -120,7 +119,7 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
     */
     __CPROVER_assume(aws_cryptosdk_dec_request_is_valid(request));
 
-    struct aws_cryptosdk_dec_materials **output = can_fail_malloc(sizeof(*output));
+    struct aws_cryptosdk_dec_materials **output = malloc(sizeof(*output));
     __CPROVER_assume(output);
 
     // Run the function under test.

verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile

@@ -51,8 +51,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
 PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c