void aws_cryptosdk_keyring_on_decrypt_harness()

in verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/aws_cryptosdk_keyring_on_decrypt_harness.c [76:141]

• 54 lines of code
• 6 McCabe index (conditional complexity)

void aws_cryptosdk_keyring_on_decrypt_harness() {
    /* Non-deterministic inputs. */
    const struct aws_cryptosdk_keyring_vt vtable = { .vt_size    = sizeof(struct aws_cryptosdk_keyring_vt),
                                                     .name       = ensure_c_str_is_allocated(SIZE_MAX),
                                                     .destroy    = nondet_voidp(),
                                                     .on_encrypt = nondet_voidp(),
                                                     .on_decrypt = nondet_bool() ? NULL : on_decrypt };
    struct aws_cryptosdk_keyring keyring;
    ensure_cryptosdk_keyring_has_allocated_members(&keyring, &vtable);
    __CPROVER_assume(aws_cryptosdk_keyring_is_valid(&keyring));
    __CPROVER_assume(keyring.vtable != NULL);

    struct aws_allocator *request_alloc = can_fail_allocator();
    __CPROVER_assume(aws_allocator_is_valid(request_alloc));

    struct aws_array_list keyring_trace;
    __CPROVER_assume(
        aws_array_list_is_bounded(&keyring_trace, MAX_ITEM_SIZE, sizeof(struct aws_cryptosdk_keyring_trace_record)));
    __CPROVER_assume(keyring_trace.item_size == sizeof(struct aws_cryptosdk_keyring_trace_record));
    ensure_array_list_has_allocated_data_member(&keyring_trace);
    __CPROVER_assume(aws_array_list_is_valid(&keyring_trace));
    ensure_trace_has_allocated_records(&keyring_trace, MAX_STRING_LEN);
    __CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(&keyring_trace));

    struct aws_byte_buf unencrypted_data_key;
    if (nondet_bool()) {
        /* The caller could send an empty unencrypted_data_key. */
        unencrypted_data_key.buffer = NULL;
    } else {
        ensure_byte_buf_has_allocated_buffer_member(&unencrypted_data_key);
    }
    __CPROVER_assume(aws_byte_buf_is_valid(&unencrypted_data_key));

    struct aws_array_list edks;
    __CPROVER_assume(aws_cryptosdk_edk_list_is_bounded(&edks, NUM_ELEMS));
    ensure_cryptosdk_edk_list_has_allocated_list(&edks);
    __CPROVER_assume(aws_cryptosdk_edk_list_is_valid(&edks));
    __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_bounded(&edks, SIZE_MAX));
    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));
    if (enc_ctx != NULL) {
        ensure_allocated_hash_table(enc_ctx, MAX_TABLE_SIZE);
        __CPROVER_assume(aws_hash_table_is_valid(enc_ctx));
        ensure_hash_table_has_valid_destroy_functions(enc_ctx);
        size_t empty_slot_idx;
        __CPROVER_assume(aws_hash_table_has_an_empty_slot(enc_ctx, &empty_slot_idx));
    }

    enum aws_cryptosdk_alg_id alg;

    /* Operation under verification. */
    if (aws_cryptosdk_keyring_on_decrypt(
            &keyring, request_alloc, &unencrypted_data_key, &keyring_trace, &edks, enc_ctx, alg) == AWS_OP_SUCCESS) {
        assert(aws_byte_buf_is_valid(&unencrypted_data_key));
    }

    /* Post-conditions. */
    assert(aws_cryptosdk_keyring_is_valid(&keyring));
    assert(aws_allocator_is_valid(request_alloc));
    assert(aws_cryptosdk_keyring_trace_is_valid(&keyring_trace));
    assert(aws_cryptosdk_edk_list_is_valid(&edks));
    assert(aws_cryptosdk_edk_list_elements_are_valid(&edks));
    if (enc_ctx != NULL) assert(aws_hash_table_is_valid(enc_ctx));
}