From 97bb1bd47865719c1bc78e408b5581c568f49331 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 22 Dec 2020 16:58:50 +0100 Subject: [PATCH] Remove unneeded assumptions and use nondet values Replace precondition by false case in enc_request validator --- source/default_cmm.c | 3 ++- .../default_cmm_generate_enc_materials_harness.c | 4 ---- verification/cbmc/sources/make_common_data_structures.c | 2 +- verification/cbmc/stubs/on_encrypt_stub.c | 3 +-- 4 files changed, 4 insertions(+), 8 deletions(-) diff --git a/source/default_cmm.c b/source/default_cmm.c index 0d1930086..405b348ec 100644 --- a/source/default_cmm.c +++ b/source/default_cmm.c @@ -187,7 +187,8 @@ int aws_cryptosdk_default_cmm_set_alg_id(struct aws_cryptosdk_cmm *cmm, enum aws } bool aws_cryptosdk_default_cmm_is_valid(const struct aws_cryptosdk_cmm *cmm) { - AWS_PRECONDITION(cmm != NULL); + if (cmm == NULL) return false; + struct default_cmm *self = (struct default_cmm *)cmm; return aws_cryptosdk_cmm_base_is_valid(&self->base) && aws_allocator_is_valid(self->alloc) && aws_cryptosdk_keyring_is_valid(self->kr); diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c b/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c index dd833f53d..4c188d62c 100644 --- a/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c +++ b/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c @@ -41,14 +41,10 @@ void default_cmm_generate_enc_materials_harness() { struct aws_cryptosdk_enc_request *request = ensure_enc_request_attempt_allocation(MAX_TABLE_SIZE); /* Assumptions */ - __CPROVER_assume(cmm != NULL); __CPROVER_assume(aws_cryptosdk_default_cmm_is_valid(cmm)); __CPROVER_assume(output != NULL); - __CPROVER_assume(request != NULL); - __CPROVER_assume(aws_allocator_is_valid(request->alloc)); - __CPROVER_assume(request->enc_ctx != NULL); __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request)); /* Save current state of the data structures */ diff --git a/verification/cbmc/sources/make_common_data_structures.c b/verification/cbmc/sources/make_common_data_structures.c index 15d5e4045..22ef0415d 100644 --- a/verification/cbmc/sources/make_common_data_structures.c +++ b/verification/cbmc/sources/make_common_data_structures.c @@ -422,7 +422,7 @@ struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws struct default_cmm *self = NULL; if (cmm) { self = (struct default_cmm *)cmm; - self->alloc = can_fail_allocator(); + self->alloc = nondet_bool()? NULL : can_fail_allocator(); self->kr = keyring; } return (struct aws_cryptosdk_cmm *)self; diff --git a/verification/cbmc/stubs/on_encrypt_stub.c b/verification/cbmc/stubs/on_encrypt_stub.c index ac6759667..7438a8e6e 100644 --- a/verification/cbmc/stubs/on_encrypt_stub.c +++ b/verification/cbmc/stubs/on_encrypt_stub.c @@ -69,6 +69,5 @@ int on_encrypt( */ if (nondet_bool()) ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key); } - int ret; - return ret; + return nondet_int(); }