diff --git a/.github/workflows/proof_ci.yaml b/.github/workflows/proof_ci.yaml index 8b593f558..88a4eaff0 100644 --- a/.github/workflows/proof_ci.yaml +++ b/.github/workflows/proof_ci.yaml @@ -152,10 +152,8 @@ jobs: echo "$(pwd)" >> $GITHUB_PATH - name: Run CBMC proofs shell: bash - env: - EXTERNAL_SAT_SOLVER: kissat working-directory: ${{ env.PROOFS_DIR }} - run: ${{ env.RUN_CBMC_PROOFS_COMMAND }} + run: ${{ env.RUN_CBMC_PROOFS_COMMAND }} --verbose --debug - name: Check repository visibility shell: bash run: | diff --git a/aws-encryption-sdk-specification b/aws-encryption-sdk-specification index 0d4d63c08..c35fbd91b 160000 --- a/aws-encryption-sdk-specification +++ b/aws-encryption-sdk-specification @@ -1 +1 @@ -Subproject commit 0d4d63c0859b4b7196777ff236f5f2624ce768c2 +Subproject commit c35fbd91b28303d69813119088c44b5006395eb4 diff --git a/verification/cbmc/aws-c-common b/verification/cbmc/aws-c-common index 70ed84b5e..24da21d2f 160000 --- a/verification/cbmc/aws-c-common +++ b/verification/cbmc/aws-c-common @@ -1 +1 @@ -Subproject commit 70ed84b5e4e167f906e665d1906cd0f0fcc1f676 +Subproject commit 24da21d2fc46c6e172496f17aade5683a32b76bb diff --git a/verification/cbmc/include/make_common_data_structures.h b/verification/cbmc/include/make_common_data_structures.h index abb390b95..c267ff3db 100644 --- a/verification/cbmc/include/make_common_data_structures.h +++ b/verification/cbmc/include/make_common_data_structures.h @@ -21,7 +21,6 @@ #include #include #include -#include #include #include #include diff --git a/verification/cbmc/include/proof_allocators.h b/verification/cbmc/include/proof_allocators.h deleted file mode 100644 index 478a3928e..000000000 --- a/verification/cbmc/include/proof_allocators.h +++ /dev/null @@ -1,23 +0,0 @@ -/* - * Copyright 2018 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. - */ - -#pragma once -#include "aws/common/common.h" - -/** - * The standard allocator in CBMC cannot fail. This one can, which allows us to - * nondeterministically find more bugs - */ -struct aws_allocator *can_fail_allocator(); diff --git a/verification/cbmc/proofs/Makefile.common b/verification/cbmc/proofs/Makefile.common index 1c05c2ef4..faaf4e3f5 100644 --- a/verification/cbmc/proofs/Makefile.common +++ b/verification/cbmc/proofs/Makefile.common @@ -307,8 +307,8 @@ COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) NONDET_STATIC ?= # Flags to pass to goto-cc for compilation and linking -COMPILE_FLAGS ?= -Wall -LINK_FLAGS ?= -Wall +COMPILE_FLAGS ?= -Wall -Werror +LINK_FLAGS ?= -Wall -Werror EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols # Preprocessor include paths -I... diff --git a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile index d416a8142..4de623308 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile @@ -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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile index 165297a0d..6a996b4e0 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile @@ -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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile index 3750ad1a4..1cb4c1720 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c index a7237001c..f8ad2f2bb 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void aws_cryptosdk_cmm_base_init_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile index 194c415a6..a8b8002ba 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/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 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c index e2c2508cc..f1750d427 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c @@ -23,7 +23,6 @@ #include #include #include -#include #include // 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. diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/Makefile b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/Makefile index cf33a8a37..e1a937119 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_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 diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c index 70e5c2270..8072ae8d4 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c @@ -23,7 +23,6 @@ #include #include #include -#include #include // Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed @@ -52,7 +51,7 @@ int generate_enc_materials( assert(AWS_OBJECT_PTR_IS_WRITABLE(output)); assert(aws_cryptosdk_enc_request_is_valid(request)); - struct aws_cryptosdk_enc_materials *materials = can_fail_malloc(sizeof(*materials)); + struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials)); if (materials == NULL) { *output = NULL; return AWS_OP_ERR; @@ -107,20 +106,20 @@ void aws_cryptosdk_cmm_generate_enc_materials_harness() { .decrypt_materials = nondet_voidp() }; __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_enc_request *request = can_fail_malloc(sizeof(*request)); + struct aws_cryptosdk_enc_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); __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request)); - struct aws_cryptosdk_enc_materials **output = can_fail_malloc(sizeof(*output)); + struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output)); __CPROVER_assume(output); // Run the function under test. diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile index 5bc9b93c1..13338574a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile @@ -36,7 +36,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c index 77129febe..103b22293 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void destroy(struct aws_cryptosdk_cmm *cmm) { @@ -36,7 +35,7 @@ void aws_cryptosdk_cmm_release_harness() { .decrypt_materials = nondet_voidp() }; __CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable)); - struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(struct aws_cryptosdk_cmm)); + struct aws_cryptosdk_cmm *cmm = malloc(sizeof(struct aws_cryptosdk_cmm)); if (cmm) { cmm->vtable = &vtable; diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile index cc0996e18..199b4e2b9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile @@ -38,7 +38,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c index 4377f49c4..6d97612dc 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void aws_cryptosdk_cmm_retain_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile b/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile index 5466baa64..c65235468 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile @@ -20,13 +20,13 @@ HARNESS_FILE = $(HARNESS_ENTRY).c CBMCFLAGS += +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/Makefile b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/Makefile index 29ff2c9be..a47490d43 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/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 diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c index 6b1dc3f20..e7aa1724c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c @@ -23,13 +23,12 @@ #include #include #include -#include #include void aws_cryptosdk_dec_materials_destroy_harness() { - struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials)); + struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials)); if (materials) { - materials->alloc = can_fail_allocator(); + materials->alloc = aws_default_allocator(); __CPROVER_assume(aws_allocator_is_valid(materials->alloc)); // Set up the signctx diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile index 72507b409..e93547a84 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile @@ -48,8 +48,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)/error.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c index 4e1bafed7..7648f910f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c @@ -20,11 +20,10 @@ #include #include #include -#include #include void aws_cryptosdk_dec_materials_new_harness() { - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); enum aws_cryptosdk_alg_id alg; struct aws_cryptosdk_dec_materials *rval = aws_cryptosdk_dec_materials_new(alloc, alg); diff --git a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile index 69debc662..449d5fd71 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile @@ -34,23 +34,23 @@ CBMCFLAGS += DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE) +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 PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/err_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.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 += $(COMMON_PROOF_UNINLINE)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c REMOVE_FUNCTION_BODY += EVP_EncryptUpdate REMOVE_FUNCTION_BODY += EVP_sha256 REMOVE_FUNCTION_BODY += EVP_sha384 -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += nondet_compare UNWINDSET += aws_cryptosdk_decrypt_body.0:$(call addone,$(MAX_BUFFER_SIZE)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c index ef654a746..3dd84c5ee 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c @@ -22,19 +22,19 @@ void aws_cryptosdk_decrypt_body_harness() { struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); - struct aws_byte_buf *outp = can_fail_malloc(sizeof(*outp)); + struct aws_byte_buf *outp = malloc(sizeof(*outp)); __CPROVER_assume(outp != NULL); __CPROVER_assume(aws_byte_buf_is_bounded(outp, MAX_BUFFER_SIZE)); ensure_byte_buf_has_allocated_buffer_member(outp); __CPROVER_assume(aws_byte_buf_is_valid(outp)); - struct aws_byte_cursor *inp = can_fail_malloc(sizeof(*inp)); + struct aws_byte_cursor *inp = malloc(sizeof(*inp)); __CPROVER_assume(inp != NULL); __CPROVER_assume(aws_byte_cursor_is_bounded(inp, MAX_BUFFER_SIZE)); ensure_byte_cursor_has_allocated_buffer_member(inp); __CPROVER_assume(aws_byte_cursor_is_valid(inp)); - struct aws_byte_buf *message_id = can_fail_malloc(sizeof(*message_id)); + struct aws_byte_buf *message_id = malloc(sizeof(*message_id)); __CPROVER_assume(message_id != NULL); __CPROVER_assume(aws_byte_buf_is_bounded(message_id, MAX_BUFFER_SIZE)); ensure_byte_buf_has_allocated_buffer_member(message_id); @@ -42,13 +42,13 @@ void aws_cryptosdk_decrypt_body_harness() { uint32_t seqno; - uint8_t *iv = can_fail_malloc(props->iv_len); + uint8_t *iv = malloc(props->iv_len); __CPROVER_assume(iv != NULL); struct content_key *content_key; /* Need to allocate tag_len bytes for writing the tag */ - uint8_t *tag = can_fail_malloc(props->tag_len); + uint8_t *tag = malloc(props->tag_len); __CPROVER_assume(tag != NULL); int body_frame_type; diff --git a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/Makefile b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/Makefile index 4cb169260..1d1134eb5 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/Makefile @@ -29,10 +29,11 @@ HARNESS_FILE = $(HARNESS_ENTRY).c CBMCFLAGS += PROJECT_SOURCES += $(SRCDIR)/source/default_cmm.c +PROJECT_SOURCES += $(SRCDIR)/source/header.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_STUB)/error.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c index 5fda0fd1c..8364a1bb7 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c @@ -35,7 +35,7 @@ void aws_cryptosdk_default_cmm_set_alg_id_harness() { __CPROVER_assume(aws_cryptosdk_keyring_is_valid(keyring)); /* Instantiate the default (non-caching) implementation of the Crypto MaterialsManager (CMM) */ - struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(can_fail_allocator(), keyring); + struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(aws_default_allocator(), keyring); /* Assumptions */ __CPROVER_assume(cmm != NULL); diff --git a/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/Makefile b/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/Makefile index 653cbe56e..9e09fe745 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/Makefile @@ -29,7 +29,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/framefmt.c PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c ########### diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/Makefile index 2a0e402e3..32cc03351 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/Makefile @@ -31,13 +31,13 @@ CBMCFLAGS += DEFINES += -DAWS_DEEP_CHECKS=1 +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/math.c PROJECT_SOURCES += $(SRCDIR)/source/edk.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/aws_cryptosdk_edk_clean_up_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/aws_cryptosdk_edk_clean_up_harness.c index 6c534b206..029da1a12 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/aws_cryptosdk_edk_clean_up_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/aws_cryptosdk_edk_clean_up_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void aws_cryptosdk_edk_clean_up_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/Makefile index e1f8a944b..613e75aca 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/Makefile @@ -31,16 +31,15 @@ CBMCFLAGS += DEFINES += -DAWS_DEEP_CHECKS=1 +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/math.c PROJECT_SOURCES += $(SRCDIR)/source/edk.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 += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/aws_cryptosdk_edk_eq_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/aws_cryptosdk_edk_eq_harness.c index 51307e3f2..d4c45ac8c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_eq/aws_cryptosdk_edk_eq_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_eq/aws_cryptosdk_edk_eq_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void aws_cryptosdk_edk_eq_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/Makefile index 70387dfdb..d24bb6888 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/Makefile @@ -36,8 +36,8 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c PROJECT_SOURCES += $(SRCDIR)/source/edk.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)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/aws_cryptosdk_edk_init_clone_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/aws_cryptosdk_edk_init_clone_harness.c index d09f83635..bcb3a7fc1 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/aws_cryptosdk_edk_init_clone_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/aws_cryptosdk_edk_init_clone_harness.c @@ -19,13 +19,12 @@ #include #include #include -#include #include void aws_cryptosdk_edk_init_clone_harness() { struct aws_array_list edk_list; - struct aws_allocator *alloc = can_fail_allocator(); // Precondition: valid allocator + struct aws_allocator *alloc = aws_default_allocator(); // Precondition: valid allocator __CPROVER_assume(aws_allocator_is_valid(alloc)); struct aws_cryptosdk_edk dest; // Precondition: non-null diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/Makefile index 4d4c400a4..064dc80ec 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/Makefile @@ -37,24 +37,22 @@ DEFINES += -DARRAY_LIST_TYPE_HEADER=\"aws/cryptosdk/edk.h\" DEFINES += -DAWS_NO_STATIC_IMPL DEFINES += -DNUM_ELEMS=$(NUM_ELEMS) +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/math.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c -PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(SRCDIR)/source/edk.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_array_list_defined_type.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c +PROOF_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c REMOVE_FUNCTION_BODY += aws_array_list_get_at_ptr -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += nondet_compare UNWINDSET += aws_cryptosdk_edk_list_clear.0:$(call addone,$(NUM_ELEMS)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/aws_cryptosdk_edk_list_clean_up_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/aws_cryptosdk_edk_list_clean_up_harness.c index 8edb69a72..fc9b94142 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/aws_cryptosdk_edk_list_clean_up_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/aws_cryptosdk_edk_list_clean_up_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void aws_cryptosdk_edk_list_clean_up_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/Makefile index 8b21dde42..c4bbf725c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/Makefile @@ -37,19 +37,17 @@ DEFINES += -DARRAY_LIST_TYPE_HEADER=\"aws/cryptosdk/edk.h\" DEFINES += -DAWS_NO_STATIC_IMPL DEFINES += -DNUM_ELEMS=$(NUM_ELEMS) +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/math.c +PROJECT_SOURCES += $(COMMON_PROOF_STUB)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c -PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(SRCDIR)/source/edk.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_array_list_defined_type.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/aws_cryptosdk_edk_list_clear_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/aws_cryptosdk_edk_list_clear_harness.c index 13b8b5dbb..74b60daa5 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/aws_cryptosdk_edk_list_clear_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/aws_cryptosdk_edk_list_clear_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include void aws_cryptosdk_edk_list_clear_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/Makefile index 4f24c6779..2899b4187 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/Makefile @@ -42,8 +42,8 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(SRCDIR)/source/list_utils.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)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c index 6b74aaa01..12a90d497 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c @@ -20,7 +20,6 @@ #include #include #include -#include #include /** @@ -131,7 +130,7 @@ void aws_cryptosdk_edk_list_copy_all_harness() { const struct aws_array_list old_src = *src; /* Operation under verification */ - if (aws_cryptosdk_edk_list_copy_all(can_fail_allocator(), dest, src) == AWS_OP_SUCCESS) { + if (aws_cryptosdk_edk_list_copy_all(aws_default_allocator(), dest, src) == AWS_OP_SUCCESS) { /* Post-conditions */ assert(src->length == old_src.length); assert(dest->length == old_dest.length + old_src.length); diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/Makefile index 5ce8800de..6f22070c6 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/Makefile @@ -36,8 +36,8 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c PROJECT_SOURCES += $(SRCDIR)/source/edk.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)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/aws_cryptosdk_edk_list_init_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/aws_cryptosdk_edk_list_init_harness.c index 79e2565a0..d3c124d1f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/aws_cryptosdk_edk_list_init_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_init/aws_cryptosdk_edk_list_init_harness.c @@ -15,13 +15,12 @@ #include #include -#include #include void aws_cryptosdk_edk_list_init_harness() { struct aws_array_list edk_list; - int rval = aws_cryptosdk_edk_list_init(can_fail_allocator(), &edk_list); + int rval = aws_cryptosdk_edk_list_init(aws_default_allocator(), &edk_list); if (rval == AWS_OP_SUCCESS) { assert(aws_cryptosdk_empty_edk_list_is_valid(&edk_list)); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/Makefile index fd0430845..61f49ca9f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/Makefile @@ -37,8 +37,8 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.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_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/aws_cryptosdk_enc_ctx_clean_up_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/aws_cryptosdk_enc_ctx_clean_up_harness.c index d31422dae..74085e650 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/aws_cryptosdk_enc_ctx_clean_up_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/aws_cryptosdk_enc_ctx_clean_up_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include /* @@ -30,7 +29,7 @@ void aws_cryptosdk_enc_ctx_clean_up_harness() { ensure_allocated_hash_table(&map, MAX_TABLE_SIZE); __CPROVER_assume(aws_hash_table_is_valid(&map)); ensure_hash_table_has_valid_destroy_functions(&map); - map.p_impl->alloc = can_fail_allocator(); + map.p_impl->alloc = aws_default_allocator(); struct hash_table_state *state = map.p_impl; size_t empty_slot_idx; diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/Makefile index 039df370f..5e6e50d68 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/Makefile @@ -39,15 +39,14 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.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_string_destroy_override.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memset_override_0.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_destroy REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c index 124188f74..4c79a8419 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_enc_ctx_clear_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/Makefile index 482098350..5d56cae0d 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/Makefile @@ -37,8 +37,8 @@ DEFINES += -DHASH_ITER_ELEMENT_GENERATOR=hash_iterator_string_string_generator DEFINES += -DHASH_TABLE_FIND_ELEMENT_GENERATOR=hash_find_string_string_generator DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) +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 #if we don't include the hash_table.c, we don't need to remove their function bodies PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c @@ -46,7 +46,7 @@ PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_new_from_array_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/hash_table_generators.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c +PROOF_SOURCES += $(PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/aws_cryptosdk_enc_ctx_clone_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/aws_cryptosdk_enc_ctx_clone_harness.c index dc1f153e2..e8ae5bad9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/aws_cryptosdk_enc_ctx_clone_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/aws_cryptosdk_enc_ctx_clone_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_enc_ctx_clone_harness() { @@ -37,5 +36,5 @@ void aws_cryptosdk_enc_ctx_clone_harness() { ensure_hash_table_has_valid_destroy_functions(src); /* Operation under verification */ - int rval = aws_cryptosdk_enc_ctx_clone(can_fail_allocator(), dest, src); + int rval = aws_cryptosdk_enc_ctx_clone(aws_default_allocator(), dest, src); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/Makefile index 8bbb8793b..903e584b9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/Makefile @@ -34,8 +34,8 @@ CBMCFLAGS += DEFINES += -DAWS_BYTE_CURSOR_READ_BE16_GENERATOR=aws_byte_cursor_read_be16_generator_for_enc_ctx_deserialize DEFINES += -DMAX_NUM_ELEMS=$(MAX_NUM_ELEMS) +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 #if we don't include the hash_table.c, we don't need to remove their function bodies PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_cursor_read_be16_override.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c index fb7f17bdd..c79773bdb 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c @@ -18,7 +18,6 @@ #include #include #include -#include #include void make_hash_table_with_no_backing_store(struct aws_hash_table *map, size_t max_table_entries); @@ -62,7 +61,7 @@ void aws_cryptosdk_enc_ctx_deserialize_harness() { __CPROVER_assume(aws_hash_table_is_valid(map)); /* Function under verification */ - int rval = aws_cryptosdk_enc_ctx_deserialize(can_fail_allocator(), map, cursor); + int rval = aws_cryptosdk_enc_ctx_deserialize(aws_default_allocator(), map, cursor); /* Post-conditions */ assert(aws_hash_table_is_valid(map)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/Makefile index a93f2b06a..387a16440 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/Makefile @@ -30,7 +30,7 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c +PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) ########### diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/aws_cryptosdk_enc_ctx_init_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/aws_cryptosdk_enc_ctx_init_harness.c index 783052f47..9758e2a61 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/aws_cryptosdk_enc_ctx_init_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/aws_cryptosdk_enc_ctx_init_harness.c @@ -14,11 +14,10 @@ */ #include -#include // This is a memory safety proof for aws_cryptosdk_enc_ctx_init void aws_cryptosdk_enc_ctx_init_harness() { - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_hash_table enc_ctx; aws_cryptosdk_enc_ctx_init(alloc, &enc_ctx); diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/Makefile index 90b081df3..b3efcee97 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/Makefile @@ -55,10 +55,9 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/string.c PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.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_byte_buf_write_stub.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_sort_noop_stub.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c index c64db09f2..c68c9b24f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c @@ -18,7 +18,6 @@ #include #include #include -#include #include // A generator function as described in the comment in aws_cryptosdk_hash_elems_array_init_stub.c. @@ -54,5 +53,5 @@ void aws_cryptosdk_enc_ctx_serialize_harness() { __CPROVER_assume(aws_hash_table_has_an_empty_slot(map, &empty_slot_idx)); /* Operation under verification */ - aws_cryptosdk_enc_ctx_serialize(can_fail_allocator(), output, map); + aws_cryptosdk_enc_ctx_serialize(aws_default_allocator(), output, map); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile index 8c5bc5e23..41a64d4d1 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/Makefile @@ -35,13 +35,13 @@ CBMCFLAGS += DEFINES += -DHASH_ITER_ELEMENT_GENERATOR=hash_iterator_generator2 DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.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_iter_overrides.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c index df20c7e64..105c1ef42 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c @@ -18,7 +18,6 @@ #include #include #include -#include #include void hash_iterator_generator(struct aws_hash_iter *new_iter, const struct aws_hash_iter *old_iter) { diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/Makefile index 07f09f0f6..42c95eefe 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/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 diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/aws_cryptosdk_enc_materials_destroy_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/aws_cryptosdk_enc_materials_destroy_harness.c index 74c68872a..53c41fb8a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/aws_cryptosdk_enc_materials_destroy_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/aws_cryptosdk_enc_materials_destroy_harness.c @@ -23,7 +23,6 @@ #include #include #include -#include #include // Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed @@ -35,9 +34,9 @@ void aws_cryptosdk_edk_list_clean_up(struct aws_array_list *encrypted_data_keys) } void aws_cryptosdk_enc_materials_destroy_harness() { - struct aws_cryptosdk_enc_materials *materials = can_fail_malloc(sizeof(*materials)); + struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials)); if (materials) { - materials->alloc = can_fail_allocator(); + materials->alloc = aws_default_allocator(); __CPROVER_assume(aws_allocator_is_valid(materials->alloc)); // Set up the signctx diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/Makefile b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/Makefile index bfadcee7e..367633d1e 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/Makefile @@ -43,8 +43,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)/error.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c index f62a063f0..5cfef69d1 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c @@ -20,12 +20,11 @@ #include #include #include -#include #include void aws_cryptosdk_enc_materials_new_harness() { /* Non-deterministic inputs. */ - struct aws_allocator *alloc = nondet_bool() ? NULL : can_fail_allocator(); + struct aws_allocator *alloc = nondet_bool() ? NULL : aws_default_allocator(); enum aws_cryptosdk_alg_id alg; /* Pre-condition. */ diff --git a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/Makefile b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/Makefile index 27ff2653b..c1152ac89 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/Makefile @@ -32,14 +32,15 @@ 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 +PROJECT_SOURCES += $(COMMON_PROOF_STUB)/error.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c @@ -48,7 +49,6 @@ REMOVE_FUNCTION_BODY += EVP_DecryptUpdate REMOVE_FUNCTION_BODY += EVP_sha256 REMOVE_FUNCTION_BODY += EVP_sha384 REMOVE_FUNCTION_BODY += EVP_sha512 -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += nondet_compare UNWINDSET += aws_cryptosdk_encrypt_body.0:$(call addone,$(MAX_BUFFER_SIZE)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/aws_cryptosdk_encrypt_body_harness.c b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/aws_cryptosdk_encrypt_body_harness.c index 5ff05e5d9..1b5d6543a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/aws_cryptosdk_encrypt_body_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_encrypt_body/aws_cryptosdk_encrypt_body_harness.c @@ -22,19 +22,19 @@ void aws_cryptosdk_encrypt_body_harness() { struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); - struct aws_byte_buf *outp = can_fail_malloc(sizeof(*outp)); + struct aws_byte_buf *outp = malloc(sizeof(*outp)); __CPROVER_assume(outp != NULL); __CPROVER_assume(aws_byte_buf_is_bounded(outp, MAX_BUFFER_SIZE)); ensure_byte_buf_has_allocated_buffer_member(outp); __CPROVER_assume(aws_byte_buf_is_valid(outp)); - struct aws_byte_cursor *inp = can_fail_malloc(sizeof(*inp)); + struct aws_byte_cursor *inp = malloc(sizeof(*inp)); __CPROVER_assume(inp != NULL); __CPROVER_assume(aws_byte_cursor_is_bounded(inp, MAX_BUFFER_SIZE)); ensure_byte_cursor_has_allocated_buffer_member(inp); __CPROVER_assume(aws_byte_cursor_is_valid(inp)); - struct aws_byte_buf *message_id = can_fail_malloc(sizeof(*message_id)); + struct aws_byte_buf *message_id = malloc(sizeof(*message_id)); __CPROVER_assume(message_id != NULL); __CPROVER_assume(aws_byte_buf_is_bounded(message_id, MAX_BUFFER_SIZE)); ensure_byte_buf_has_allocated_buffer_member(message_id); @@ -42,13 +42,13 @@ void aws_cryptosdk_encrypt_body_harness() { uint32_t seqno; - uint8_t *iv = can_fail_malloc(props->iv_len); + uint8_t *iv = malloc(props->iv_len); __CPROVER_assume(iv != NULL); struct content_key *content_key; /* Need to allocate tag_len bytes for writing the tag */ - uint8_t *tag = can_fail_malloc(props->tag_len); + uint8_t *tag = malloc(props->tag_len); __CPROVER_assume(tag != NULL); int body_frame_type; diff --git a/verification/cbmc/proofs/aws_cryptosdk_genrandom/Makefile b/verification/cbmc/proofs/aws_cryptosdk_genrandom/Makefile index 52d5f1200..fd9643c86 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_genrandom/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_genrandom/Makefile @@ -33,7 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_genrandom/aws_cryptosdk_genrandom_harness.c b/verification/cbmc/proofs/aws_cryptosdk_genrandom/aws_cryptosdk_genrandom_harness.c index b422ddc6e..5fe3734e0 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_genrandom/aws_cryptosdk_genrandom_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_genrandom/aws_cryptosdk_genrandom_harness.c @@ -19,7 +19,7 @@ void aws_cryptosdk_genrandom_harness() { size_t len; - uint8_t *buf = can_fail_malloc(len); + uint8_t *buf = malloc(len); __CPROVER_assume(buf != NULL); aws_cryptosdk_genrandom(buf, len); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/Makefile index 93a71e9f0..4f1801f14 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/Makefile @@ -28,6 +28,12 @@ CBMCFLAGS += DEFINES += -DAWS_NO_STATIC_IMPL +# 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" +CBMC_OBJECT_BITS ?= 9 + PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c @@ -36,8 +42,9 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_STUB)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOF_STUB)/aws_add_size_checked.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/aws_cryptosdk_hash_elems_array_init_harness.c b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/aws_cryptosdk_hash_elems_array_init_harness.c index 87a77ebf4..415b55b59 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/aws_cryptosdk_hash_elems_array_init_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/aws_cryptosdk_hash_elems_array_init_harness.c @@ -27,13 +27,13 @@ void aws_cryptosdk_hash_elems_array_init_harness() { /* Non-deterministic inputs. */ - struct aws_allocator *alloc = nondet_bool() ? NULL : can_fail_allocator(); + struct aws_allocator *alloc = nondet_bool() ? NULL : aws_default_allocator(); __CPROVER_assume(aws_allocator_is_valid(alloc)); - struct aws_array_list *list = can_fail_malloc(sizeof(*list)); + struct aws_array_list *list = malloc(sizeof(*list)); __CPROVER_assume(list != NULL); - struct aws_hash_table *map = can_fail_malloc(sizeof(*map)); + struct aws_hash_table *map = malloc(sizeof(*map)); __CPROVER_assume(map != NULL); ensure_allocated_hash_table(map, MAX_TABLE_SIZE); __CPROVER_assume(aws_hash_table_is_valid(map)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_size/Makefile b/verification/cbmc/proofs/aws_cryptosdk_hdr_size/Makefile index 7fcfd7086..a572df9c7 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hdr_size/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_hdr_size/Makefile @@ -35,6 +35,7 @@ DEFINES += -DARRAY_LIST_TYPE_HEADER=\"aws/cryptosdk/edk.h\" 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/hash_table.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c @@ -48,11 +49,9 @@ PROJECT_SOURCES += $(SRCDIR)/source/header.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override.c PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/Makefile b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/Makefile index 323ebe3d7..3c6262834 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/Makefile @@ -42,7 +42,15 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +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/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c @@ -57,19 +65,15 @@ PROJECT_SOURCES += $(SRCDIR)/source/header.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_array_list_defined_type.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_buf_write_stub.c +PROOF_SOURCES += $(PROOF_STUB)/aws_byte_buf_write_stub.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_iter_overrides.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override.c PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c 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 += $(PROOFDIR)/$(HARNESS_FILE) UNWINDSET += array_list_item_generator.0:$(call addone,$(MAX_TABLE_SIZE)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/aws_cryptosdk_hdr_write_harness.c b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/aws_cryptosdk_hdr_write_harness.c index 239e97b05..979644b91 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hdr_write/aws_cryptosdk_hdr_write_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_hdr_write/aws_cryptosdk_hdr_write_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include /** diff --git a/verification/cbmc/proofs/aws_cryptosdk_hkdf/Makefile b/verification/cbmc/proofs/aws_cryptosdk_hkdf/Makefile index c87c8032e..877e7d191 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hkdf/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_hkdf/Makefile @@ -25,6 +25,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 @@ -35,7 +36,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/Makefile index a75a5111e..1434cf226 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/Makefile @@ -30,7 +30,6 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/Makefile index 79d0faf30..45053714a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/Makefile @@ -57,10 +57,9 @@ 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_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/aws_cryptosdk_keyring_on_decrypt_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/aws_cryptosdk_keyring_on_decrypt_harness.c index f308097ed..cdd0eb29b 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/aws_cryptosdk_keyring_on_decrypt_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/aws_cryptosdk_keyring_on_decrypt_harness.c @@ -23,7 +23,6 @@ #include #include -#include #include /** @@ -85,7 +84,7 @@ void aws_cryptosdk_keyring_on_decrypt_harness() { __CPROVER_assume(aws_cryptosdk_keyring_is_valid(&keyring)); __CPROVER_assume(keyring.vtable != NULL); - struct aws_allocator *request_alloc = can_fail_allocator(); + struct aws_allocator *request_alloc = aws_default_allocator(); __CPROVER_assume(aws_allocator_is_valid(request_alloc)); struct aws_array_list keyring_trace; @@ -114,7 +113,7 @@ void aws_cryptosdk_keyring_on_decrypt_harness() { ensure_cryptosdk_edk_list_has_allocated_list_elements(&edks); __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_valid(&edks)); - struct aws_hash_table *enc_ctx = can_fail_malloc(sizeof(*enc_ctx)); + struct aws_hash_table *enc_ctx = malloc(sizeof(*enc_ctx)); if (enc_ctx != NULL) { ensure_allocated_hash_table(enc_ctx, MAX_TABLE_SIZE); __CPROVER_assume(aws_hash_table_is_valid(enc_ctx)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile index 1337fc535..d22b11ed6 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile @@ -56,10 +56,9 @@ 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_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c index 000c70771..440d7bcc2 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c @@ -23,7 +23,6 @@ #include #include -#include #include int on_encrypt( @@ -47,7 +46,7 @@ void aws_cryptosdk_keyring_on_encrypt_harness() { __CPROVER_assume(aws_cryptosdk_keyring_is_valid(&keyring)); __CPROVER_assume(keyring.vtable != NULL); - struct aws_allocator *request_alloc = can_fail_allocator(); + struct aws_allocator *request_alloc = aws_default_allocator(); __CPROVER_assume(aws_allocator_is_valid(request_alloc)); struct aws_array_list keyring_trace; @@ -76,7 +75,7 @@ void aws_cryptosdk_keyring_on_encrypt_harness() { ensure_cryptosdk_edk_list_has_allocated_list_elements(&edks); __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_valid(&edks)); - struct aws_hash_table *enc_ctx = can_fail_malloc(sizeof(*enc_ctx)); + struct aws_hash_table *enc_ctx = malloc(sizeof(*enc_ctx)); if (enc_ctx != NULL) { ensure_allocated_hash_table(enc_ctx, MAX_TABLE_SIZE); __CPROVER_assume(aws_hash_table_is_valid(enc_ctx)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_release/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_release/Makefile index da9c8f926..b5d7bd06b 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_release/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_release/Makefile @@ -27,11 +27,11 @@ CBMCFLAGS += PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c -PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.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_STUB)/error.c +PROOF_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c # aws_atomic_fetch_sub_explicit receives a volatile input, which is always model @@ -44,7 +44,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_atomics_gnu_inl_aws_atomic_fetch_su REMOVE_FUNCTION_BODY += aws_atomic_fetch_sub_explicit REMOVE_FUNCTION_BODY += aws_atomic_load_int REMOVE_FUNCTION_BODY += aws_atomic_priv_xlate_order -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += hash_proof_destroy_noop UNWINDSET += diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/Makefile index 5926c2fcf..2ebf73bfa 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_retain/Makefile @@ -31,7 +31,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c # aws_atomic_fetch_add_explicit receives a volatile input, which is always model diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/Makefile index e0a513471..bb0b2c80e 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/Makefile @@ -29,8 +29,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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)/memcpy_override_havoc.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/aws_cryptosdk_keyring_trace_add_record_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/aws_cryptosdk_keyring_trace_add_record_harness.c index 49844268e..2eaee93d4 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/aws_cryptosdk_keyring_trace_add_record_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/aws_cryptosdk_keyring_trace_add_record_harness.c @@ -24,7 +24,7 @@ void aws_cryptosdk_keyring_trace_add_record_harness() { /* data structure */ - struct aws_allocator *alloc = can_fail_allocator(); /* Precondition: valid allocator */ + struct aws_allocator *alloc = aws_default_allocator(); /* Precondition: valid allocator */ __CPROVER_assume(aws_allocator_is_valid(alloc)); struct aws_array_list trace; /* Precondition: trace must be non-null */ struct aws_string *namespace = diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/Makefile index 6050d2e95..7f2e06067 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/Makefile @@ -32,8 +32,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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)/memcpy_override_havoc.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/aws_cryptosdk_keyring_trace_add_record_buf_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/aws_cryptosdk_keyring_trace_add_record_buf_harness.c index 4f0d0f4d8..f1ca8ebc9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/aws_cryptosdk_keyring_trace_add_record_buf_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/aws_cryptosdk_keyring_trace_add_record_buf_harness.c @@ -23,7 +23,7 @@ void aws_cryptosdk_keyring_trace_add_record_buf_harness() { /* data structure */ - struct aws_allocator *alloc = can_fail_allocator(); /* Precondition: alloc must be non-null */ + struct aws_allocator *alloc = aws_default_allocator(); /* Precondition: alloc must be non-null */ struct aws_array_list trace; struct aws_byte_buf namespace; struct aws_byte_buf name; diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/Makefile index 61e9c29b0..feb0ed2b3 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/Makefile @@ -32,8 +32,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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)/memcpy_override_havoc.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/aws_cryptosdk_keyring_trace_add_record_c_str_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/aws_cryptosdk_keyring_trace_add_record_c_str_harness.c index 94268e500..d56acc9e2 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/aws_cryptosdk_keyring_trace_add_record_c_str_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/aws_cryptosdk_keyring_trace_add_record_c_str_harness.c @@ -28,7 +28,7 @@ void aws_cryptosdk_keyring_trace_add_record_c_str_harness() { /* data structure */ - struct aws_allocator *alloc = can_fail_allocator(); /* Precondition: alloc must be non-null */ + struct aws_allocator *alloc = aws_default_allocator(); /* Precondition: alloc must be non-null */ struct aws_array_list trace; const char *c_str_namespace = ensure_c_str_is_allocated(MAX_STRING_LEN); const char *c_str_name = ensure_c_str_is_allocated(MAX_STRING_LEN); diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/Makefile index ea327a2cc..bbb696e27 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/Makefile @@ -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 @@ -34,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/Makefile index c4c8f3ef1..15cf7b3a5 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/Makefile @@ -24,6 +24,7 @@ PROOF_UID = aws_cryptosdk_keyring_trace_clear HARNESS_ENTRY = $(PROOF_UID)_harness HARNESS_FILE = $(HARNESS_ENTRY).c +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 @@ -32,7 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile index bb9f6e03f..25cca06eb 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile @@ -48,8 +48,8 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c #PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c PROJECT_SOURCES += $(SRCDIR)/source/list_utils.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)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c index 76eb8c7b8..70cd4bb39 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c @@ -20,7 +20,6 @@ #include #include #include -#include #include // #include @@ -136,7 +135,7 @@ void aws_cryptosdk_keyring_trace_copy_all_harness() { const struct aws_array_list old_src = *src; /* Operation under verification */ - if (aws_cryptosdk_keyring_trace_copy_all(can_fail_allocator(), dest, src) == AWS_OP_SUCCESS) { + if (aws_cryptosdk_keyring_trace_copy_all(aws_default_allocator(), dest, src) == AWS_OP_SUCCESS) { /* Post-conditions */ assert(src->length == old_src.length); assert(dest->length == old_dest.length + old_src.length); diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile index 411b750f7..61765cce8 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/Makefile @@ -24,6 +24,7 @@ PROOF_UID = aws_cryptosdk_keyring_trace_eq HARNESS_ENTRY = $(PROOF_UID)_harness HARNESS_FILE = $(HARNESS_ENTRY).c +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 @@ -32,7 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/Makefile index 6f07660a3..56db31816 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/Makefile @@ -30,8 +30,8 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/aws_cryptosdk_keyring_trace_init_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/aws_cryptosdk_keyring_trace_init_harness.c index b22ae2264..60732bccc 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/aws_cryptosdk_keyring_trace_init_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/aws_cryptosdk_keyring_trace_init_harness.c @@ -20,8 +20,8 @@ void aws_cryptosdk_keyring_trace_init_harness() { /* data structure */ - struct aws_allocator *alloc = can_fail_allocator(); /* Precondition: alloc must be non-null */ - struct aws_array_list trace; /* Precondition: trace must be non-null */ + struct aws_allocator *alloc = aws_default_allocator(); /* Precondition: alloc must be non-null */ + struct aws_array_list trace; /* Precondition: trace must be non-null */ if (aws_cryptosdk_keyring_trace_init(alloc, &trace) == AWS_OP_SUCCESS) { /* assertions */ diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/Makefile index 01fa28011..641601bb9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/Makefile @@ -22,6 +22,7 @@ PROOF_UID = aws_cryptosdk_keyring_trace_record_clean_up HARNESS_ENTRY = $(PROOF_UID)_harness HARNESS_FILE = $(HARNESS_ENTRY).c +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 @@ -30,7 +31,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c ########### diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/Makefile index 1bbcb2073..fa66ff451 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/Makefile @@ -29,9 +29,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_STUB)/memcmp_override.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/aws_cryptosdk_keyring_trace_record_init_clone_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/aws_cryptosdk_keyring_trace_record_init_clone_harness.c index 4c495e78a..89feb0905 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/aws_cryptosdk_keyring_trace_record_init_clone_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/aws_cryptosdk_keyring_trace_record_init_clone_harness.c @@ -21,7 +21,7 @@ void aws_cryptosdk_keyring_trace_record_init_clone_harness() { /* data structure */ struct aws_cryptosdk_keyring_trace_record source_record; /* Precondition: record is non-null */ struct aws_cryptosdk_keyring_trace_record dest_record; /* Precondition: record is non-null */ - struct aws_allocator *alloc = can_fail_allocator(); /* Precondition: alloc must be non-null */ + struct aws_allocator *alloc = aws_default_allocator(); /* Precondition: alloc must be non-null */ source_record.wrapping_key_namespace = ensure_string_is_allocated_nondet_length(); __CPROVER_assume(aws_string_is_valid(source_record.wrapping_key_namespace)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_abort/Makefile b/verification/cbmc/proofs/aws_cryptosdk_md_abort/Makefile index 37e5a5d0f..f9e27e31d 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_abort/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_md_abort/Makefile @@ -27,13 +27,13 @@ HARNESS_FILE = $(HARNESS_ENTRY).c # But might as well do it when its easy CBMCFLAGS += --memory-leak-check +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/bn_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/ec_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_abort/aws_cryptosdk_md_abort_harness.c b/verification/cbmc/proofs/aws_cryptosdk_md_abort/aws_cryptosdk_md_abort_harness.c index 2bccb0624..3ec99aa5e 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_abort/aws_cryptosdk_md_abort_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_md_abort/aws_cryptosdk_md_abort_harness.c @@ -18,12 +18,11 @@ #include #include #include -#include /* Expected runtime: 40 seconds */ void aws_cryptosdk_md_abort_harness() { /* arguments */ - struct aws_cryptosdk_md_context *md_context = can_fail_malloc(sizeof(struct aws_cryptosdk_md_context)); + struct aws_cryptosdk_md_context *md_context = malloc(sizeof(struct aws_cryptosdk_md_context)); /* assumptions */ if (md_context) { diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_finish/Makefile b/verification/cbmc/proofs/aws_cryptosdk_md_finish/Makefile index 31222939a..4504e4f7c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_finish/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_md_finish/Makefile @@ -27,13 +27,13 @@ HARNESS_FILE = $(HARNESS_ENTRY).c # But might as well do it when its easy CBMCFLAGS += --memory-leak-check +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/bn_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/ec_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_finish/aws_cryptosdk_md_finish_harness.c b/verification/cbmc/proofs/aws_cryptosdk_md_finish/aws_cryptosdk_md_finish_harness.c index f341da0cd..581777285 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_finish/aws_cryptosdk_md_finish_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_md_finish/aws_cryptosdk_md_finish_harness.c @@ -17,17 +17,16 @@ #include #include #include -#include #include /* Expected runtime 1m20s */ void aws_cryptosdk_md_finish_harness() { /* arguments */ - struct aws_cryptosdk_md_context *md_context = can_fail_malloc(sizeof(struct aws_cryptosdk_md_context)); + struct aws_cryptosdk_md_context *md_context = malloc(sizeof(struct aws_cryptosdk_md_context)); size_t length; size_t buf_size; - void *buf = can_fail_malloc(buf_size); + void *buf = malloc(buf_size); /* assumptions */ __CPROVER_assume(md_context); diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_init/Makefile b/verification/cbmc/proofs/aws_cryptosdk_md_init/Makefile index 2ce4d6cde..6b15df4ff 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_init/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_md_init/Makefile @@ -33,7 +33,7 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/ec_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c +PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_init/aws_cryptosdk_md_init_harness.c b/verification/cbmc/proofs/aws_cryptosdk_md_init/aws_cryptosdk_md_init_harness.c index 841b4d904..7242135ac 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_init/aws_cryptosdk_md_init_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_md_init/aws_cryptosdk_md_init_harness.c @@ -28,7 +28,7 @@ void aws_cryptosdk_md_init_harness() { enum aws_cryptosdk_md_alg md_alg; /* assumptions */ - alloc = can_fail_allocator(); + alloc = aws_default_allocator(); /* operation under verification */ if (aws_cryptosdk_md_init(alloc, &md_context, md_alg) == AWS_OP_SUCCESS) { diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_update/Makefile b/verification/cbmc/proofs/aws_cryptosdk_md_update/Makefile index 736b1a28b..74b650a22 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_update/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_md_update/Makefile @@ -27,12 +27,12 @@ HARNESS_FILE = $(HARNESS_ENTRY).c # But might as well do it when its easy CBMCFLAGS += --memory-leak-check +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/bn_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/ec_override.c PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_md_update/aws_cryptosdk_md_update_harness.c b/verification/cbmc/proofs/aws_cryptosdk_md_update/aws_cryptosdk_md_update_harness.c index f87aac202..99150b288 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_md_update/aws_cryptosdk_md_update_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_md_update/aws_cryptosdk_md_update_harness.c @@ -18,15 +18,14 @@ #include #include #include -#include #include /* Expected runtime 1m30s */ void aws_cryptosdk_md_update_harness() { /* arguments */ - struct aws_cryptosdk_md_context *md_context = can_fail_malloc(sizeof(*md_context)); + struct aws_cryptosdk_md_context *md_context = malloc(sizeof(*md_context)); size_t length; - void *buf = can_fail_malloc(length); + void *buf = malloc(length); /* assumptions */ __CPROVER_assume(md_context); diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/Makefile b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/Makefile index 7aca06678..3ae65e7ac 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/Makefile @@ -27,8 +27,8 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(SRCDIR)/source/materials.c PROJECT_SOURCES += $(SRCDIR)/source/multi_keyring.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c index baf7fa640..76f0ceb98 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c @@ -18,7 +18,6 @@ #include #include -#include void aws_cryptosdk_multi_keyring_add_child_harness() { /* Non-deterministic inputs to initialize a multi_keyring object. */ @@ -31,7 +30,7 @@ void aws_cryptosdk_multi_keyring_add_child_harness() { ensure_cryptosdk_keyring_has_allocated_members(&generator, &vtable_generator); __CPROVER_assume(aws_cryptosdk_keyring_is_valid(&generator)); - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); /* * We inject non-deterministic parameters in aws_cryptosdk_multi_keyring_new to ensure diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/Makefile b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/Makefile index b78172ab9..e6e9dec48 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/Makefile @@ -28,7 +28,7 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c PROJECT_SOURCES += $(SRCDIR)/source/multi_keyring.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c +PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) ########### include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/MultiKeyringNew_harness.c b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/MultiKeyringNew_harness.c index dfd953336..d932a0fa9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/MultiKeyringNew_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/MultiKeyringNew_harness.c @@ -15,12 +15,11 @@ #include #include -#include "proof_helpers/proof_allocators.h" // This is a memory safety proof for aws_cryptosdk_multi_keyring() defined in // https://github.com/aws/aws-encryption-sdk-c/blob/master/source/multi_keyring.c void MultiKeyringNew_harness() { - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_cryptosdk_keyring generator; aws_cryptosdk_keyring_base_init(&generator, NULL); struct aws_cryptosdk_keyring *result = aws_cryptosdk_multi_keyring_new(alloc, &generator); diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/Makefile index bd6231947..0f001cc32 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/Makefile @@ -23,6 +23,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c CBMCFLAGS += +PROJECT_SOURCES += $(SRCDIR)/source/header.c PROJECT_SOURCES += $(SRCDIR)/source/session.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/Makefile index b4817165e..5bd298ff6 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/Makefile @@ -35,6 +35,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# The maximum number of objects is set to 2^8 = 256. This option changes that to 2^10. +# 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" +CBMC_OBJECT_BITS ?= 10 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -49,15 +56,14 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_cursor_read_be16_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_new_from_array_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c +PROOF_SOURCES += $(PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) @@ -69,7 +75,6 @@ REMOVE_FUNCTION_BODY += aws_string_new_from_array # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes UNWINDSET += aws_cryptosdk_edk_list_clear.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/aws_cryptosdk_priv_hdr_parse_aad_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/aws_cryptosdk_priv_hdr_parse_aad_harness.c index 7c7501b5e..992dcf214 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/aws_cryptosdk_priv_hdr_parse_aad_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/aws_cryptosdk_priv_hdr_parse_aad_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include static int flag = 0; diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/Makefile index 3d8602ab9..abb8f3c2a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/Makefile @@ -34,12 +34,20 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# The maximum number of objects is set to 2^8 = 256. This option changes that to 2^10. +# 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" +CBMC_OBJECT_BITS ?= 10 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.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/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/byte_order.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/string.c @@ -49,19 +57,15 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/aws_cryptosdk_priv_hdr_parse_alg_id_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/aws_cryptosdk_priv_hdr_parse_alg_id_harness.c index 7767a5281..d191bb2ff 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/aws_cryptosdk_priv_hdr_parse_alg_id_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/aws_cryptosdk_priv_hdr_parse_alg_id_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_alg_id_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/Makefile index 51e5626e0..ae9825470 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -49,19 +56,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/aws_cryptosdk_priv_hdr_parse_alg_suite_data_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/aws_cryptosdk_priv_hdr_parse_alg_suite_data_harness.c index 0940b18ae..7513e8efe 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/aws_cryptosdk_priv_hdr_parse_alg_suite_data_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/aws_cryptosdk_priv_hdr_parse_alg_suite_data_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_alg_suite_data_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/Makefile index f18ec5899..67e9b031d 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -49,19 +56,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/aws_cryptosdk_priv_hdr_parse_auth_tag_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/aws_cryptosdk_priv_hdr_parse_auth_tag_harness.c index cea4703ea..d6b187129 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/aws_cryptosdk_priv_hdr_parse_auth_tag_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/aws_cryptosdk_priv_hdr_parse_auth_tag_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_auth_tag_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/Makefile index 54b2293de..13b5ea677 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -49,19 +56,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/aws_cryptosdk_priv_hdr_parse_content_type_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/aws_cryptosdk_priv_hdr_parse_content_type_harness.c index 3d4cf1c20..899683575 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/aws_cryptosdk_priv_hdr_parse_content_type_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/aws_cryptosdk_priv_hdr_parse_content_type_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_content_type_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/Makefile index ff8f91180..b7696aa8b 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/Makefile @@ -33,6 +33,13 @@ DEFINES += -DAWS_NO_STATIC_IMPL DEFINES += -DMAX_EDK_LIST_ITEMS=$(MAX_EDK_LIST_ITEMS) DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) +# The maximum number of objects is set to 2^8 = 256. This option changes that to 2^10. +# 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" +CBMC_OBJECT_BITS ?= 10 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -47,13 +54,11 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_cursor_read_be16_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) @@ -63,7 +68,6 @@ REMOVE_FUNCTION_BODY += aws_byte_cursor_read_be16 # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/aws_cryptosdk_priv_hdr_parse_edks_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/aws_cryptosdk_priv_hdr_parse_edks_harness.c index 9ae627377..c00ef51ca 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/aws_cryptosdk_priv_hdr_parse_edks_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/aws_cryptosdk_priv_hdr_parse_edks_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include static bool flag = true; diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/Makefile index 3030fa636..d648c44b1 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/Makefile @@ -34,12 +34,20 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.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/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/byte_order.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/string.c @@ -49,19 +57,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/aws_cryptosdk_priv_hdr_parse_frame_len_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/aws_cryptosdk_priv_hdr_parse_frame_len_harness.c index e2a32aae0..ff4e21f10 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/aws_cryptosdk_priv_hdr_parse_frame_len_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/aws_cryptosdk_priv_hdr_parse_frame_len_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_frame_len_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/Makefile index bdb8b5ed3..c5dc33103 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -48,19 +55,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/aws_cryptosdk_priv_hdr_parse_header_version_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/aws_cryptosdk_priv_hdr_parse_header_version_harness.c index 2901fbddf..1a60f710a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/aws_cryptosdk_priv_hdr_parse_header_version_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/aws_cryptosdk_priv_hdr_parse_header_version_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_header_version_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/Makefile index b4a81925e..752d1a090 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -49,19 +56,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/aws_cryptosdk_priv_hdr_parse_iv_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/aws_cryptosdk_priv_hdr_parse_iv_harness.c index 6c94191e3..b9af97c58 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/aws_cryptosdk_priv_hdr_parse_iv_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/aws_cryptosdk_priv_hdr_parse_iv_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_iv_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/Makefile index f3a1d0ab9..6360f494d 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -49,19 +56,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/aws_cryptosdk_priv_hdr_parse_iv_len_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/aws_cryptosdk_priv_hdr_parse_iv_len_harness.c index f2da6881a..4b0e05265 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/aws_cryptosdk_priv_hdr_parse_iv_len_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/aws_cryptosdk_priv_hdr_parse_iv_len_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_iv_len_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/Makefile index 39d516817..f60f08e6f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -43,24 +50,22 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/string.c +PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/edk.c PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/aws_cryptosdk_priv_hdr_parse_message_id_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/aws_cryptosdk_priv_hdr_parse_message_id_harness.c index ccc4cd629..c982f5e4a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/aws_cryptosdk_priv_hdr_parse_message_id_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/aws_cryptosdk_priv_hdr_parse_message_id_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_message_id_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/Makefile index 6594fe482..24ffa1910 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/Makefile @@ -34,6 +34,13 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -48,19 +55,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/aws_cryptosdk_priv_hdr_parse_message_type_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/aws_cryptosdk_priv_hdr_parse_message_type_harness.c index b44c266c2..795609c8a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/aws_cryptosdk_priv_hdr_parse_message_type_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/aws_cryptosdk_priv_hdr_parse_message_type_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_message_type_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/Makefile index e32317b54..4785e55bf 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/Makefile @@ -34,12 +34,20 @@ DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) CBMCFLAGS += +# 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" +CBMC_OBJECT_BITS ?= 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.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/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/byte_order.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/string.c @@ -49,19 +57,16 @@ PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c PROJECT_SOURCES += $(SRCDIR)/source/header.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_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) # Functions removed for enc_ctx_clear REMOVE_FUNCTION_BODY += aws_hash_callback_string_destroy REMOVE_FUNCTION_BODY += aws_hash_string -REMOVE_FUNCTION_BODY += aws_raise_error_private REMOVE_FUNCTION_BODY += aws_string_bytes REMOVE_FUNCTION_BODY += aws_string_is_valid diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/aws_cryptosdk_priv_hdr_parse_reserved_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/aws_cryptosdk_priv_hdr_parse_reserved_harness.c index d3ea9441d..a730f09d2 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/aws_cryptosdk_priv_hdr_parse_reserved_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/aws_cryptosdk_priv_hdr_parse_reserved_harness.c @@ -17,7 +17,6 @@ #include #include #include -#include #include void aws_cryptosdk_priv_hdr_parse_reserved_harness() { diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index 84c8eab68..3f261a752 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -39,6 +39,12 @@ DEFINES += -DMAX_IV_LEN=$(MAX_IV_LEN) DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) DEFINES += -DMAX_TRACE_LIST_ITEMS=$(MAX_TRACE_LIST_ITEMS) +# 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" +CBMC_OBJECT_BITS ?= 9 + 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/hash_table.c @@ -66,15 +72,12 @@ PROJECT_SOURCES += $(SRCDIR)/source/session.c PROJECT_SOURCES += $(SRCDIR)/source/session_encrypt.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_array_list_defined_type.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_buf_write_stub.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_iter_overrides.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memset_override_havoc.c PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index 491079eee..d8daa2efc 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -22,7 +22,6 @@ #include #include #include -#include #include #include @@ -91,7 +90,7 @@ void aws_cryptosdk_priv_try_gen_key_harness() { session->keyring_trace = *keyring_trace; /* Set the allocators */ - session->alloc = can_fail_allocator(); + session->alloc = aws_default_allocator(); __CPROVER_assume(aws_allocator_is_valid(session->alloc)); /* This assumption is needed for build_header */ session->header.edk_list.alloc = session->alloc; diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/Makefile b/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/Makefile index 51a24fc85..926bd054c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/Makefile @@ -31,7 +31,6 @@ DEFINES += -DMSG_ID_LEN_V2=32 PROJECT_SOURCES += $(SRCDIR)/source/cipher.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/Makefile b/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/Makefile index 9d3565f6f..b5043de9c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/Makefile @@ -33,11 +33,11 @@ CBMCFLAGS += DEFINES += -DCOMMITMENT_BUF_SIZE=$(COMMITMENT_BUF_SIZE) +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/utils.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/Makefile index 212071794..64c48f3f0 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key/Makefile @@ -33,6 +33,7 @@ CBMCFLAGS += DEFINES += -DMSG_ID_LEN=16 DEFINES += -DMSG_ID_LEN_V2=32 +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 @@ -44,7 +45,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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/Makefile b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/Makefile index e49b56103..73fc99dce 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/Makefile @@ -31,6 +31,7 @@ CBMCFLAGS += # this is defined on cipher.c DEFINES += -DMSG_ID_LEN=16 +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 @@ -42,7 +43,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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/Makefile b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/Makefile index 6e074603c..eb962c781 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/Makefile @@ -28,6 +28,7 @@ CBMCFLAGS += # this is defined on cipher.c DEFINES += -DMSG_ID_LEN_V2=32 +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 @@ -39,7 +40,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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/Makefile index 0de1444e0..289193bfd 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/Makefile @@ -37,8 +37,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c PROJECT_SOURCES += $(SRCDIR)/source/hkdf.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)/error.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/aws_cryptosdk_rsa_decrypt_harness.c b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/aws_cryptosdk_rsa_decrypt_harness.c index b8050532d..464b5145d 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/aws_cryptosdk_rsa_decrypt_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/aws_cryptosdk_rsa_decrypt_harness.c @@ -23,7 +23,7 @@ void aws_cryptosdk_rsa_decrypt_harness() { /* Nondet Inputs */ struct aws_byte_buf plain; - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_byte_cursor cipher; struct aws_string *key = ensure_string_is_allocated_nondet_length(); enum aws_cryptosdk_rsa_padding_mode rsa_padding_mode; diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/Makefile index 32a2c907d..3d2948750 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/Makefile @@ -37,8 +37,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c PROJECT_SOURCES += $(SRCDIR)/source/hkdf.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)/error.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/aws_cryptosdk_rsa_encrypt_harness.c b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/aws_cryptosdk_rsa_encrypt_harness.c index f3592b3c2..5646b68e2 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/aws_cryptosdk_rsa_encrypt_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/aws_cryptosdk_rsa_encrypt_harness.c @@ -23,7 +23,7 @@ void aws_cryptosdk_rsa_encrypt_harness() { /* Nondet Inputs */ struct aws_byte_buf cipher; - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_byte_cursor plain; struct aws_string *key = ensure_string_is_allocated_nondet_length(); enum aws_cryptosdk_rsa_padding_mode rsa_padding_mode; diff --git a/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/Makefile b/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/Makefile index 243c255cf..ca22a5da9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_serialize_frame/Makefile @@ -22,6 +22,7 @@ PROOF_UID = aws_cryptosdk_serialize_frame HARNESS_ENTRY = $(PROOF_UID)_harness HARNESS_FILE = $(HARNESS_ENTRY).c +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 @@ -29,7 +30,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/framefmt.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/Makefile index 25a25b6d8..568e673d3 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/Makefile @@ -25,6 +25,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c # Added check for memory leaks CBMCFLAGS += --memory-leak-check +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 @@ -36,7 +37,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c PROJECT_SOURCES += $(SRCDIR)/source/framefmt.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/aws_cryptosdk_sig_abort_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/aws_cryptosdk_sig_abort_harness.c index 72baebcab..ce0555153 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_abort/aws_cryptosdk_sig_abort_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_abort/aws_cryptosdk_sig_abort_harness.c @@ -18,8 +18,6 @@ #include #include #include -#include -#include #include diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/Makefile index 5ed316847..8f76b7c80 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/Makefile @@ -35,8 +35,8 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/aws_cryptosdk_sig_get_privkey_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/aws_cryptosdk_sig_get_privkey_harness.c index 0fb545ddc..ed8c9bfbf 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/aws_cryptosdk_sig_get_privkey_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/aws_cryptosdk_sig_get_privkey_harness.c @@ -18,14 +18,13 @@ #include #include #include -#include #include void aws_cryptosdk_sig_get_privkey_harness() { /* Nondet Input */ struct aws_cryptosdk_sig_ctx *ctx = ensure_nondet_sig_ctx_has_allocated_members(); - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_string *priv_key = ensure_string_is_allocated_nondet_length(); /* Assumptions */ diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/Makefile index c29e5893a..32fa1cb70 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/Makefile @@ -36,7 +36,7 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c -PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c +PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/aws_cryptosdk_sig_get_pubkey_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/aws_cryptosdk_sig_get_pubkey_harness.c index 9c419bf96..5c91e8063 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/aws_cryptosdk_sig_get_pubkey_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/aws_cryptosdk_sig_get_pubkey_harness.c @@ -18,14 +18,13 @@ #include #include #include -#include #include void aws_cryptosdk_sig_get_pubkey_harness() { /* arguments */ struct aws_cryptosdk_sig_ctx *ctx = ensure_nondet_sig_ctx_has_allocated_members(); - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_string *pubkey; /* assumptions */ diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/Makefile index 983c1ceb4..a535e9165 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/Makefile @@ -36,8 +36,8 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/objects_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/aws_cryptosdk_sig_sign_finish_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/aws_cryptosdk_sig_sign_finish_harness.c index c922fa8b9..1c22de8e4 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/aws_cryptosdk_sig_sign_finish_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/aws_cryptosdk_sig_sign_finish_harness.c @@ -18,15 +18,13 @@ #include #include #include -#include -#include #include void aws_cryptosdk_sig_sign_finish_harness() { /* arguments */ struct aws_cryptosdk_sig_ctx *ctx = ensure_nondet_sig_ctx_has_allocated_members(); - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_string *signature; /* Max signature size is queried inside the function. This call initializes the value nondeterministically. */ initialize_max_signature_size(); diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/Makefile index b552dd4bd..058289069 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/Makefile @@ -36,8 +36,8 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/objects_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/aws_cryptosdk_sig_sign_start_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/aws_cryptosdk_sig_sign_start_harness.c index bb05cedbe..ced3767e6 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/aws_cryptosdk_sig_sign_start_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/aws_cryptosdk_sig_sign_start_harness.c @@ -18,14 +18,13 @@ #include #include #include -#include #include void aws_cryptosdk_sig_sign_start_harness() { /* Nondet Inputs */ struct aws_cryptosdk_sig_ctx *ctx = ensure_nondet_sig_ctx_has_allocated_members(); - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_string *pub_key; struct aws_string *priv_key = ensure_string_is_allocated_nondet_length(); enum aws_cryptosdk_alg_id alg_id; diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/Makefile index 9557d10f7..5a3c6d03a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/Makefile @@ -34,8 +34,8 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/objects_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/aws_cryptosdk_sig_sign_start_keygen_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/aws_cryptosdk_sig_sign_start_keygen_harness.c index 273335aa8..2db7c2694 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/aws_cryptosdk_sig_sign_start_keygen_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/aws_cryptosdk_sig_sign_start_keygen_harness.c @@ -18,14 +18,13 @@ #include #include #include -#include #include void aws_cryptosdk_sig_sign_start_keygen_harness() { /* arguments */ struct aws_cryptosdk_sig_ctx *pctx; - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_string *pub_key; enum aws_cryptosdk_alg_id alg_id; struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_update/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_update/Makefile index d2aa6f8b4..f817c2b50 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_update/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_update/Makefile @@ -25,6 +25,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c # Added check for memory leaks CBMCFLAGS += --memory-leak-check +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 @@ -35,7 +36,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_update/aws_cryptosdk_sig_update_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_update/aws_cryptosdk_sig_update_harness.c index 221b8c8ee..e05ed0512 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_update/aws_cryptosdk_sig_update_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_update/aws_cryptosdk_sig_update_harness.c @@ -18,8 +18,6 @@ #include #include #include -#include -#include #include diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/Makefile index cfede4f58..be8e501b9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/Makefile @@ -22,6 +22,7 @@ PROOF_UID = aws_cryptosdk_sig_verify_finish HARNESS_ENTRY = $(PROOF_UID)_harness HARNESS_FILE = $(HARNESS_ENTRY).c +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/encoding.c @@ -34,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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 += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/aws_cryptosdk_sig_verify_finish_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/aws_cryptosdk_sig_verify_finish_harness.c index 29d38649d..078bfb725 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/aws_cryptosdk_sig_verify_finish_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/aws_cryptosdk_sig_verify_finish_harness.c @@ -19,8 +19,6 @@ #include #include #include -#include -#include void aws_cryptosdk_sig_verify_finish_harness() { /* Nondet Input */ diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/Makefile index de03f880f..1eed12a30 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/Makefile @@ -34,8 +34,8 @@ PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/objects_override.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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)/memset_override_no_op.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/aws_cryptosdk_sig_verify_start_harness.c b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/aws_cryptosdk_sig_verify_start_harness.c index 1411e192b..160093581 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/aws_cryptosdk_sig_verify_start_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/aws_cryptosdk_sig_verify_start_harness.c @@ -19,13 +19,11 @@ #include #include #include -#include -#include void aws_cryptosdk_sig_verify_start_harness() { /* Nondet input */ struct aws_cryptosdk_sig_ctx *ctx; - struct aws_allocator *alloc = can_fail_allocator(); + struct aws_allocator *alloc = aws_default_allocator(); struct aws_string *pub_key = ensure_string_is_allocated_nondet_length(); enum aws_cryptosdk_alg_id alg_id; struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); diff --git a/verification/cbmc/proofs/aws_cryptosdk_sign_header/Makefile b/verification/cbmc/proofs/aws_cryptosdk_sign_header/Makefile index 32239728a..9aceaace2 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_sign_header/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_sign_header/Makefile @@ -24,6 +24,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 += $(PROOF_SOURCE)/openssl/bn_override.c @@ -33,7 +34,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_string_dup/Makefile b/verification/cbmc/proofs/aws_cryptosdk_string_dup/Makefile index 49480d9a6..b0e331cf0 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_string_dup/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_string_dup/Makefile @@ -28,9 +28,8 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_STUB)/memcmp_override.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_string_dup/aws_cryptosdk_string_dup_harness.c b/verification/cbmc/proofs/aws_cryptosdk_string_dup/aws_cryptosdk_string_dup_harness.c index e09dc83ee..8f487f4d7 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_string_dup/aws_cryptosdk_string_dup_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_string_dup/aws_cryptosdk_string_dup_harness.c @@ -22,7 +22,7 @@ void aws_cryptosdk_string_dup_harness() { /* data structure */ - struct aws_allocator *alloc = can_fail_allocator(); /* Precondition: alloc must be non-null */ + struct aws_allocator *alloc = aws_default_allocator(); /* Precondition: alloc must be non-null */ struct aws_string *str_a = ensure_string_is_allocated_nondet_length(); __CPROVER_assume(aws_string_is_valid(str_a)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/Makefile b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/Makefile index 199891480..c661033a9 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/Makefile @@ -38,6 +38,7 @@ DEFINES += -DAWS_NO_STATIC_IMPL DEFINES += -DITEM_SIZE=$(ITEM_SIZE) DEFINES += -DNUM_ELEMS=$(NUM_ELEMS) +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c @@ -48,7 +49,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(SRCDIR)/source/list_utils.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) diff --git a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c index f133bf88c..26b039b05 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c @@ -20,7 +20,6 @@ #include #include #include -#include #include /** @@ -57,13 +56,13 @@ bool aws_array_list_is_valid_deep(const struct aws_array_list *AWS_RESTRICT list } void aws_cryptosdk_transfer_list_harness() { - struct aws_array_list *dest = can_fail_malloc(sizeof(*dest)); + struct aws_array_list *dest = malloc(sizeof(*dest)); __CPROVER_assume(dest != NULL); __CPROVER_assume(aws_array_list_is_bounded(dest, NUM_ELEMS, ITEM_SIZE)); ensure_array_list_has_allocated_data_member(dest); __CPROVER_assume(aws_array_list_is_valid_deep(dest)); - struct aws_array_list *src = can_fail_malloc(sizeof(*src)); + struct aws_array_list *src = malloc(sizeof(*src)); __CPROVER_assume(src != NULL); __CPROVER_assume(aws_array_list_is_bounded(src, NUM_ELEMS, ITEM_SIZE)); ensure_array_list_has_allocated_data_member(src); diff --git a/verification/cbmc/proofs/aws_cryptosdk_verify_header/Makefile b/verification/cbmc/proofs/aws_cryptosdk_verify_header/Makefile index 4d79b1a38..7413d415b 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_verify_header/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_verify_header/Makefile @@ -24,6 +24,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 += $(PROOF_SOURCE)/openssl/bn_override.c @@ -34,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.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) diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile b/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile index 80474f858..f17e64dfc 100644 --- a/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile +++ b/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile @@ -32,6 +32,13 @@ CBMCFLAGS += DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) +# 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" +CBMC_OBJECT_BITS ?= 9 + +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/encoding.c @@ -51,7 +58,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.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)/aws_hash_table_no_slots_override.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c @@ -64,4 +70,4 @@ PROOF_SOURCES += $(PROOF_STUB)/on_encrypt_stub.c UNWINDSET += strcmp.0:$(call addone,$(PRIME_STRING_LEN)) ########### -include ../Makefile.common \ No newline at end of file +include ../Makefile.common diff --git a/verification/cbmc/proofs/derive_data_key/Makefile b/verification/cbmc/proofs/derive_data_key/Makefile index ec7287028..0ec117a6f 100644 --- a/verification/cbmc/proofs/derive_data_key/Makefile +++ b/verification/cbmc/proofs/derive_data_key/Makefile @@ -55,6 +55,7 @@ DEFINES += -DMSG_ID_LEN_V2=32 # use the `--object-bits n` option to increase the maximum number" CBMC_OBJECT_BITS ?= 9 +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/hash_table.c @@ -76,9 +77,7 @@ PROJECT_SOURCES += $(SRCDIR)/source/session.c PROJECT_SOURCES += $(SRCDIR)/source/session_decrypt.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_array_list_defined_type.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c diff --git a/verification/cbmc/proofs/list_copy_all/Makefile b/verification/cbmc/proofs/list_copy_all/Makefile index 460006575..540a14d43 100644 --- a/verification/cbmc/proofs/list_copy_all/Makefile +++ b/verification/cbmc/proofs/list_copy_all/Makefile @@ -44,8 +44,8 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c PROJECT_SOURCES += $(SRCDIR)/source/list_utils.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)/error.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) diff --git a/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c b/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c index 49168c7c1..ccc388edc 100644 --- a/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c +++ b/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c @@ -19,7 +19,6 @@ #include #include #include -#include #include /** @@ -86,13 +85,13 @@ void cleanup(void *p) { } void list_copy_all_harness() { - struct aws_array_list *dest = can_fail_malloc(sizeof(*dest)); + struct aws_array_list *dest = malloc(sizeof(*dest)); __CPROVER_assume(dest != NULL); __CPROVER_assume(aws_array_list_is_bounded(dest, NUM_ELEMS, ITEM_SIZE)); ensure_array_list_has_allocated_data_member(dest); __CPROVER_assume(aws_array_list_is_valid_deep(dest)); - struct aws_array_list *src = can_fail_malloc(sizeof(*src)); + struct aws_array_list *src = malloc(sizeof(*src)); __CPROVER_assume(src != NULL); __CPROVER_assume(aws_array_list_is_bounded(src, NUM_ELEMS, ITEM_SIZE)); ensure_array_list_has_allocated_data_member(src); @@ -102,7 +101,7 @@ void list_copy_all_harness() { const struct aws_array_list old_dest = *dest; const struct aws_array_list old_src = *src; // Name mangled version of static function - if (__CPROVER_file_local_list_utils_c_list_copy_all(can_fail_allocator(), dest, src, cloner, cleanup) == + if (__CPROVER_file_local_list_utils_c_list_copy_all(aws_default_allocator(), dest, src, cloner, cleanup) == AWS_OP_SUCCESS) { assert(src->length == old_src.length); assert(dest->length == old_dest.length + old_src.length); diff --git a/verification/cbmc/proofs/sign_header/Makefile b/verification/cbmc/proofs/sign_header/Makefile index 454cac3cf..8fdcab71e 100644 --- a/verification/cbmc/proofs/sign_header/Makefile +++ b/verification/cbmc/proofs/sign_header/Makefile @@ -37,6 +37,7 @@ 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 +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/hash_table.c @@ -62,13 +63,12 @@ PROJECT_SOURCES += $(SRCDIR)/source/session_encrypt.c PROJECT_SOURCES += $(SRCDIR)/source/utils.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_array_list_defined_type.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_buf_write_stub.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_defined_type.c +PROOF_SOURCES += $(PROOF_STUB)/aws_byte_buf_write_stub.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_iter_overrides.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c -PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override.c +PROOF_SOURCES += $(PROOF_STUB)/memcmp_override_no_op.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memset_override_havoc.c PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c diff --git a/verification/cbmc/sources/make_common_data_structures.c b/verification/cbmc/sources/make_common_data_structures.c index 55d4476c0..2b479af08 100644 --- a/verification/cbmc/sources/make_common_data_structures.c +++ b/verification/cbmc/sources/make_common_data_structures.c @@ -30,7 +30,6 @@ #include #include -#include struct default_cmm { struct aws_cryptosdk_cmm base; @@ -98,7 +97,7 @@ void ensure_trace_has_allocated_records(struct aws_array_list *trace, size_t max } void ensure_md_context_has_allocated_members(struct aws_cryptosdk_md_context *ctx) { - ctx->alloc = nondet_bool() ? NULL : can_fail_allocator(); + ctx->alloc = nondet_bool() ? NULL : aws_default_allocator(); ctx->evp_md_ctx = evp_md_ctx_nondet_alloc(); } @@ -107,7 +106,7 @@ struct aws_cryptosdk_sig_ctx *ensure_nondet_sig_ctx_has_allocated_members() { if (ctx == NULL) { return NULL; } - ctx->alloc = nondet_bool() ? NULL : can_fail_allocator(); + ctx->alloc = nondet_bool() ? NULL : aws_default_allocator(); enum aws_cryptosdk_alg_id alg_id; ctx->props = aws_cryptosdk_alg_props(alg_id); ctx->keypair = ec_key_nondet_alloc(); @@ -164,11 +163,11 @@ void ensure_cryptosdk_edk_list_has_allocated_list(struct aws_array_list *list) { if (list != NULL) { if (list->current_size == 0) { __CPROVER_assume(list->data == NULL); - list->alloc = can_fail_allocator(); + list->alloc = aws_default_allocator(); } else { size_t max_length = list->current_size / sizeof(struct aws_cryptosdk_edk); - list->data = bounded_malloc(sizeof(struct aws_cryptosdk_edk) * max_length); - list->alloc = nondet_bool() ? NULL : can_fail_allocator(); + list->data = malloc(sizeof(struct aws_cryptosdk_edk) * max_length); + list->alloc = nondet_bool() ? NULL : aws_default_allocator(); } } } @@ -184,7 +183,7 @@ void ensure_cryptosdk_edk_list_has_allocated_list_elements(struct aws_array_list void ensure_nondet_hdr_has_allocated_members_ref(struct aws_cryptosdk_hdr *hdr, const size_t max_table_size) { if (hdr) { - hdr->alloc = nondet_bool() ? NULL : can_fail_allocator(); + hdr->alloc = nondet_bool() ? NULL : aws_default_allocator(); ensure_byte_buf_has_allocated_buffer_member(&hdr->iv); ensure_byte_buf_has_allocated_buffer_member(&hdr->auth_tag); ensure_byte_buf_has_allocated_buffer_member(&hdr->message_id); @@ -197,7 +196,7 @@ void ensure_nondet_hdr_has_allocated_members_ref(struct aws_cryptosdk_hdr *hdr, struct aws_cryptosdk_hdr *ensure_nondet_hdr_has_allocated_members(const size_t max_table_size) { struct aws_cryptosdk_hdr *hdr = malloc(sizeof(*hdr)); if (hdr != NULL) { - hdr->alloc = nondet_bool() ? NULL : can_fail_allocator(); + hdr->alloc = nondet_bool() ? NULL : aws_default_allocator(); ensure_byte_buf_has_allocated_buffer_member(&hdr->iv); ensure_byte_buf_has_allocated_buffer_member(&hdr->auth_tag); ensure_byte_buf_has_allocated_buffer_member(&hdr->message_id); @@ -297,7 +296,7 @@ struct aws_cryptosdk_cmm *ensure_cmm_attempt_allocation(const size_t max_len) { struct aws_cryptosdk_session *ensure_nondet_session_has_allocated_members(const size_t max_table_size, size_t max_len) { struct aws_cryptosdk_session *session = malloc(sizeof(struct aws_cryptosdk_session)); if (session) { - session->alloc = nondet_bool() ? NULL : can_fail_allocator(); + session->alloc = nondet_bool() ? NULL : aws_default_allocator(); session->cmm = ensure_cmm_attempt_allocation(max_len); session->header_copy = malloc(sizeof(*(session->header_copy))); session->alg_props = ensure_alg_properties_attempt_allocation(max_len); @@ -360,7 +359,7 @@ bool aws_cryptosdk_dec_materials_members_are_bounded( struct aws_cryptosdk_dec_materials *ensure_dec_materials_attempt_allocation() { struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(struct aws_cryptosdk_dec_materials)); if (materials) { - materials->alloc = nondet_bool() ? NULL : can_fail_allocator(); + materials->alloc = nondet_bool() ? NULL : aws_default_allocator(); materials->signctx = ensure_nondet_sig_ctx_has_allocated_members(); ensure_byte_buf_has_allocated_buffer_member(&materials->unencrypted_data_key); ensure_array_list_has_allocated_data_member(&materials->keyring_trace); @@ -385,7 +384,7 @@ struct aws_cryptosdk_dec_materials *dec_materials_setup( struct aws_cryptosdk_enc_request *ensure_enc_request_attempt_allocation(const size_t max_table_size) { struct aws_cryptosdk_enc_request *request = malloc(sizeof(struct aws_cryptosdk_enc_request)); if (request) { - request->alloc = nondet_bool() ? NULL : can_fail_allocator(); + request->alloc = nondet_bool() ? NULL : aws_default_allocator(); request->enc_ctx = malloc(sizeof(struct aws_hash_table)); if (request->enc_ctx) { ensure_allocated_hash_table(request->enc_ctx, max_table_size); @@ -397,7 +396,7 @@ struct aws_cryptosdk_enc_request *ensure_enc_request_attempt_allocation(const si struct aws_cryptosdk_enc_materials *ensure_enc_materials_attempt_allocation() { struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(struct aws_cryptosdk_enc_materials)); if (materials) { - materials->alloc = nondet_bool() ? NULL : can_fail_allocator(); + materials->alloc = nondet_bool() ? NULL : aws_default_allocator(); materials->signctx = ensure_nondet_sig_ctx_has_allocated_members(); ensure_array_list_has_allocated_data_member(&materials->encrypted_data_keys); ensure_array_list_has_allocated_data_member(&materials->keyring_trace); @@ -424,7 +423,7 @@ struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation( struct default_cmm *self = NULL; if (cmm) { self = (struct default_cmm *)cmm; - self->alloc = nondet_bool() ? NULL : can_fail_allocator(); + self->alloc = nondet_bool() ? NULL : aws_default_allocator(); self->kr = keyring; } return (struct aws_cryptosdk_cmm *)self; diff --git a/verification/cbmc/sources/openssl/asn1_override.c b/verification/cbmc/sources/openssl/asn1_override.c index 42e7e3c84..04d6c29e6 100644 --- a/verification/cbmc/sources/openssl/asn1_override.c +++ b/verification/cbmc/sources/openssl/asn1_override.c @@ -61,7 +61,7 @@ ASN1_INTEGER *BN_to_ASN1_INTEGER(const BIGNUM *bn, ASN1_INTEGER *ai) { assert(bignum_is_valid(bn)); assert(!ai); // Assuming is always called with ai == NULL - ASN1_INTEGER *rv = can_fail_malloc(sizeof(ASN1_INTEGER)); + ASN1_INTEGER *rv = malloc(sizeof(ASN1_INTEGER)); if (rv) rv->is_valid = true; @@ -85,7 +85,7 @@ ASN1_INTEGER *d2i_ASN1_INTEGER(ASN1_INTEGER **a, unsigned char **ppin, long leng assert(*ppin); assert(AWS_MEM_IS_READABLE(*ppin, length)); - *a = can_fail_malloc(sizeof(ASN1_INTEGER)); + *a = malloc(sizeof(ASN1_INTEGER)); /* If *a is not NULL it might be in an invalid state */ if (*a == NULL || nondet_bool()) { @@ -112,7 +112,7 @@ int i2d_ASN1_INTEGER(ASN1_INTEGER *a, unsigned char **ppout) { int buf_size; __CPROVER_assume(0 < buf_size); - *ppout = can_fail_malloc(buf_size); + *ppout = malloc(buf_size); if (!*ppout) { int error_code; diff --git a/verification/cbmc/sources/openssl/bio_override.c b/verification/cbmc/sources/openssl/bio_override.c index 41a59129f..bbffe670d 100644 --- a/verification/cbmc/sources/openssl/bio_override.c +++ b/verification/cbmc/sources/openssl/bio_override.c @@ -15,7 +15,8 @@ #include #include -#include + +#include /* Abstraction of the BIO struct */ @@ -31,7 +32,7 @@ struct bio_st { * supplied area of memory must be unchanged until the BIO is freed. */ BIO *BIO_new_mem_buf(const void *buf, signed int len) { - BIO *bio = can_fail_malloc(sizeof(BIO)); + BIO *bio = malloc(sizeof(BIO)); if (bio) { bio->key_len = len; } diff --git a/verification/cbmc/sources/openssl/bn_override.c b/verification/cbmc/sources/openssl/bn_override.c index 36e542618..3bfc227fc 100644 --- a/verification/cbmc/sources/openssl/bn_override.c +++ b/verification/cbmc/sources/openssl/bn_override.c @@ -15,12 +15,14 @@ #include +#include #include - -#include +#include #include +#include + /* Abstraction of the BIGNUM struct */ struct bignum_st { bool is_initialized; @@ -32,7 +34,7 @@ struct bignum_st { * allocation fails, they return NULL and set an error code that can be obtained by ERR_get_error(3). */ BIGNUM *BN_new(void) { - BIGNUM *rv = can_fail_malloc(sizeof(BIGNUM)); + BIGNUM *rv = malloc(sizeof(BIGNUM)); if (rv) { rv->is_initialized = true; } @@ -94,5 +96,5 @@ bool bignum_is_valid(BIGNUM *a) { } BIGNUM *bignum_nondet_alloc() { - return can_fail_malloc(sizeof(BIGNUM)); + return malloc(sizeof(BIGNUM)); } diff --git a/verification/cbmc/sources/openssl/ec_override.c b/verification/cbmc/sources/openssl/ec_override.c index 0ce01997c..03bcebecc 100644 --- a/verification/cbmc/sources/openssl/ec_override.c +++ b/verification/cbmc/sources/openssl/ec_override.c @@ -13,6 +13,7 @@ * permissions and limitations under the License. */ +#include #include #include @@ -20,8 +21,8 @@ #include #include +#include #include -#include /* Abstraction of the EC_GROUP struct */ struct ec_group_st { @@ -38,7 +39,7 @@ struct ec_group_st { EC_GROUP *EC_GROUP_new_by_curve_name(int nid) { assert(nid == NID_X9_62_prime256v1 || nid == NID_secp384r1); - EC_GROUP *group = can_fail_malloc(sizeof(EC_GROUP)); + EC_GROUP *group = malloc(sizeof(EC_GROUP)); if (group) { group->curve_name = nid; @@ -94,7 +95,7 @@ struct ec_key_st { * EC_KEY_dup() return a pointer to the newly created EC_KEY object, or NULL on error. */ EC_KEY *EC_KEY_new() { - EC_KEY *key = can_fail_malloc(sizeof(EC_KEY)); + EC_KEY *key = malloc(sizeof(EC_KEY)); if (key) { key->references = 1; @@ -127,7 +128,7 @@ int EC_KEY_set_group(EC_KEY *key, const EC_GROUP *group) { if (!group || nondet_bool()) return 0; EC_GROUP_free(key->group); - key->group = can_fail_malloc(sizeof(EC_GROUP)); + key->group = malloc(sizeof(EC_GROUP)); if (!key->group) return 0; @@ -266,7 +267,7 @@ int i2o_ECPublicKey(const EC_KEY *key, unsigned char **out) { int buf_len; __CPROVER_assume(0 < buf_len); - *out = can_fail_malloc(buf_len); + *out = malloc(buf_len); if (*out == NULL) { int error_code; @@ -341,7 +342,7 @@ ECDSA_SIG *d2i_ECDSA_SIG(ECDSA_SIG **sig, const unsigned char **pp, long len) { assert(0 <= len); assert(AWS_MEM_IS_READABLE(*pp, len)); - *sig = can_fail_malloc(sizeof(ECDSA_SIG)); + *sig = malloc(sizeof(ECDSA_SIG)); if (*sig) { (*sig)->r = bignum_nondet_alloc(); @@ -389,7 +390,7 @@ bool ec_group_is_valid(EC_GROUP *group) { /* Helper function for CBMC proofs: allocates an EC_GROUP nondeterministically. */ EC_GROUP *ec_group_nondet_alloc() { - EC_GROUP *group = can_fail_malloc(sizeof(EC_GROUP)); + EC_GROUP *group = malloc(sizeof(EC_GROUP)); if (group) group->order = bignum_nondet_alloc(); @@ -404,7 +405,7 @@ bool ec_key_is_valid(EC_KEY *key) { /* Helper function for CBMC proofs: allocates an EC_KEY nondeterministically. */ EC_KEY *ec_key_nondet_alloc() { - EC_KEY *key = can_fail_malloc(sizeof(EC_KEY)); + EC_KEY *key = malloc(sizeof(EC_KEY)); if (key) { key->group = ec_group_nondet_alloc(); diff --git a/verification/cbmc/sources/openssl/evp_override.c b/verification/cbmc/sources/openssl/evp_override.c index 539a0d4ab..6b1d95899 100644 --- a/verification/cbmc/sources/openssl/evp_override.c +++ b/verification/cbmc/sources/openssl/evp_override.c @@ -30,7 +30,7 @@ * allocated EVP_PKEY structure or NULL if an error occurred. */ EVP_PKEY *EVP_PKEY_new() { - EVP_PKEY *pkey = can_fail_malloc(sizeof(EVP_PKEY)); + EVP_PKEY *pkey = malloc(sizeof(EVP_PKEY)); if (pkey) { pkey->references = 1; @@ -102,7 +102,7 @@ EVP_PKEY_CTX *EVP_PKEY_CTX_new(EVP_PKEY *pkey, ENGINE *e) { assert(evp_pkey_is_valid(pkey)); assert(!e); // Assuming is always called with e == NULL - EVP_PKEY_CTX *ctx = can_fail_malloc(sizeof(EVP_PKEY_CTX)); + EVP_PKEY_CTX *ctx = malloc(sizeof(EVP_PKEY_CTX)); if (ctx) { ctx->is_initialized_for_signing = false; @@ -125,7 +125,7 @@ EVP_PKEY_CTX *EVP_PKEY_CTX_new(EVP_PKEY *pkey, ENGINE *e) { EVP_PKEY_CTX *EVP_PKEY_CTX_new_id(int id, ENGINE *e) { // assert(!e); // Assuming is always called with e == NULL - EVP_PKEY_CTX *ctx = can_fail_malloc(sizeof(EVP_PKEY_CTX)); + EVP_PKEY_CTX *ctx = malloc(sizeof(EVP_PKEY_CTX)); if (ctx) { ctx->is_initialized_for_signing = false; @@ -451,7 +451,7 @@ struct evp_cipher_ctx_st { * EVP_CIPHER_CTX_new() creates a cipher context. */ EVP_CIPHER_CTX *EVP_CIPHER_CTX_new() { - EVP_CIPHER_CTX *cipher_ctx = can_fail_malloc(sizeof(EVP_CIPHER_CTX)); + EVP_CIPHER_CTX *cipher_ctx = malloc(sizeof(EVP_CIPHER_CTX)); if (cipher_ctx) { cipher_ctx->iv_len = DEFAULT_IV_LEN; cipher_ctx->iv_set = false; @@ -737,7 +737,7 @@ bool evp_md_ctx_is_valid(EVP_MD_CTX *ctx) { * Description: Allocates and returns a digest context. */ EVP_MD_CTX *EVP_MD_CTX_new() { - EVP_MD_CTX *ctx = can_fail_malloc(sizeof(EVP_MD_CTX)); + EVP_MD_CTX *ctx = malloc(sizeof(EVP_MD_CTX)); if (ctx) { ctx->is_initialized = false; @@ -905,7 +905,7 @@ int EVP_DigestVerifyFinal(EVP_MD_CTX *ctx, const unsigned char *sig, size_t sigl * Description: HMAC_CTX_init() initialises a HMAC_CTX before first use. It must be called. */ void HMAC_CTX_init(HMAC_CTX *ctx) { - HMAC_CTX *ctx_new = can_fail_malloc(sizeof(HMAC_CTX)); + HMAC_CTX *ctx_new = malloc(sizeof(HMAC_CTX)); __CPROVER_assume(ctx_new); // cannot be null ctx_new->is_initialized = true; ctx_new->md = malloc(sizeof(EVP_MD)); @@ -1011,7 +1011,7 @@ bool evp_pkey_is_valid(EVP_PKEY *pkey) { /* Helper function for CBMC proofs: allocates EVP_PKEY nondeterministically. */ EVP_PKEY *evp_pkey_nondet_alloc() { - EVP_PKEY *pkey = can_fail_malloc(sizeof(EVP_PKEY)); + EVP_PKEY *pkey = malloc(sizeof(EVP_PKEY)); return pkey; } @@ -1047,7 +1047,7 @@ bool evp_md_is_valid(EVP_MD *md) { /* Helper function for CBMC proofs: allocates EVP_MD_CTX nondeterministically. */ EVP_MD_CTX *evp_md_ctx_nondet_alloc() { - return can_fail_malloc(sizeof(EVP_MD_CTX)); + return malloc(sizeof(EVP_MD_CTX)); } /* Helper function for CBMC proofs: checks if EVP_MD_CTX is initialized. */ diff --git a/verification/cbmc/stubs/aws_array_list_defined_type.c b/verification/cbmc/stubs/aws_array_list_defined_type.c new file mode 100644 index 000000000..205d0b8bb --- /dev/null +++ b/verification/cbmc/stubs/aws_array_list_defined_type.c @@ -0,0 +1,29 @@ +/** + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0. + */ + +#include + +/** + * The array list implementation has a void* data field. This causes problems for CBMC, because it ends up needing to + * byte-extract everything from the data array, even if the array is only ever used for a single type. This + * dramatically slows down proofs (in one case, timing out after 90 minutes). If we know what the correct type is, we + * can do type-safe operations, and things are dramatically faster (2 minutes instead of timeout, on the proof mentioned + * above). + */ + +#include ARRAY_LIST_TYPE_HEADER + +int aws_array_list_get_at_ptr(const struct aws_array_list *AWS_RESTRICT list, void **val, size_t index) { + AWS_PRECONDITION(aws_array_list_is_valid(list)); + AWS_PRECONDITION(val != NULL); + if (list->length > index) { + ARRAY_LIST_TYPE *data = (ARRAY_LIST_TYPE *)(list->data); + *val = &(data[index]); + AWS_POSTCONDITION(aws_array_list_is_valid(list)); + return AWS_OP_SUCCESS; + } + AWS_POSTCONDITION(aws_array_list_is_valid(list)); + return aws_raise_error(AWS_ERROR_INVALID_INDEX); +} diff --git a/verification/cbmc/stubs/aws_byte_buf_write_stub.c b/verification/cbmc/stubs/aws_byte_buf_write_stub.c new file mode 100644 index 000000000..85234ca5a --- /dev/null +++ b/verification/cbmc/stubs/aws_byte_buf_write_stub.c @@ -0,0 +1,36 @@ +/** + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0. + */ + +#include +#include +#include +#include + +/** + * Stub for aws_byte_buf_write. + * Has the same behaviour as the actual function except it doesn't actually write the bytes. + * In order to use this function safely, the user must check that the byte_buf bytes are not actually + * used by the function under test. + * TODO: Once CBMC supports proper havocing, should havoc the bytes to get full soundness. + * + * On success, returns true and updates the buffer length accordingly. + * If there is insufficient space in the buffer, returns false, leaving the + * buffer unchanged. + */ +bool aws_byte_buf_write(struct aws_byte_buf *AWS_RESTRICT buf, const uint8_t *AWS_RESTRICT src, size_t len) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); + AWS_PRECONDITION(AWS_MEM_IS_WRITABLE(src, len), "Input array [src] must be readable up to [len] bytes."); + + if (buf->len > (SIZE_MAX >> 1) || len > (SIZE_MAX >> 1) || buf->len + len > buf->capacity) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(buf)); + return false; + } + + /* memcpy(buf->buffer + buf->len, src, len); */ + buf->len += len; + + AWS_POSTCONDITION(aws_byte_buf_is_valid(buf)); + return true; +} diff --git a/verification/cbmc/stubs/aws_cryptosdk_hash_elems_array_init_stub.c b/verification/cbmc/stubs/aws_cryptosdk_hash_elems_array_init_stub.c index 9c6f2b5e6..3803e05d3 100644 --- a/verification/cbmc/stubs/aws_cryptosdk_hash_elems_array_init_stub.c +++ b/verification/cbmc/stubs/aws_cryptosdk_hash_elems_array_init_stub.c @@ -22,7 +22,6 @@ #include #include -#include #include /* If the consumer of the list doesn't use the elements in the list, we can just leave it undef @@ -48,7 +47,7 @@ int aws_cryptosdk_hash_elems_array_init( elems->item_size = sizeof(struct aws_hash_element); elems->length = entry_count; __CPROVER_assume(elems->current_size >= elems->length * elems->item_size); - elems->data = bounded_malloc(elems->current_size); + elems->data = malloc(elems->current_size); /* Malloc can return NULL, assume that elems->data (which would come from map) isn't NULL */ __CPROVER_assume(elems->data != NULL); diff --git a/verification/cbmc/stubs/aws_default_allocator_stub.c b/verification/cbmc/stubs/aws_default_allocator_stub.c deleted file mode 100644 index f88f7c413..000000000 --- a/verification/cbmc/stubs/aws_default_allocator_stub.c +++ /dev/null @@ -1,20 +0,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. - */ - -#include - -struct aws_allocator *aws_default_allocator() { - return can_fail_allocator(); -} diff --git a/verification/cbmc/stubs/memcmp_override_no_op.c b/verification/cbmc/stubs/memcmp_override_no_op.c new file mode 100644 index 000000000..ed99dc6f0 --- /dev/null +++ b/verification/cbmc/stubs/memcmp_override_no_op.c @@ -0,0 +1,15 @@ +/** + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0. + */ + +#include + +/** Abstract memcmp to check that pointers are valid, and then return nondet */ + +int memcmp(const void *s1, const void *s2, size_t n) { + __CPROVER_precondition(__CPROVER_r_ok(s1, n), "memcmp region 1 readable"); + __CPROVER_precondition(__CPROVER_r_ok(s2, n), "memcpy region 2 readable"); + + return nondet_int(); +}