1 /*
2  * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3  *
4  * Licensed under the Apache License, Version 2.0 (the "License").
5  * You may not use this file except in compliance with the License.
6  * A copy of the License is located at
7  *
8  *  http://aws.amazon.com/apache2.0
9  *
10  * or in the "license" file accompanying this file. This file is distributed
11  * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
12  * express or implied. See the License for the specific language governing
13  * permissions and limitations under the License.
14  */
15 
16 #include "crypto/s2n_fips.h"
17 #include "crypto/s2n_hash.h"
18 
19 #include <cbmc_proof/make_common_datastructures.h>
20 
s2n_hash_free_harness()21 void s2n_hash_free_harness()
22 {
23     /* Non-deterministic inputs. */
24     struct s2n_hash_state *state = cbmc_allocate_s2n_hash_state();
25 
26     /* Assumptions. */
27     __CPROVER_assume(s2n_result_is_ok(s2n_hash_state_validate(state)));
28 
29     struct rc_keys_from_hash_state saved_hash_state;
30     save_rc_keys_from_hash_state(state, &saved_hash_state);
31 
32     /* Operation under verification. */
33     assert(s2n_hash_free(state) == S2N_SUCCESS);
34     if (state != NULL) {
35         assert(state->hash_impl->free != NULL);
36         if (s2n_is_in_fips_mode()) {
37             assert(state->digest.high_level.evp.ctx == NULL);
38             assert(state->digest.high_level.evp_md5_secondary.ctx == NULL);
39             assert_rc_decrement_on_hash_state(&saved_hash_state);
40         } else {
41             assert_rc_unchanged_on_hash_state(&saved_hash_state);
42         }
43         assert(state->is_ready_for_input == 0);
44     }
45 
46     /* Cleanup after expected error cases, for memory leak check. */
47     if (state != NULL) {
48         /* 1. `free` leftover EVP_MD_CTX objects if `s2n_is_in_fips_mode`,
49               since `s2n_hash_free` is a NO-OP in that case. */
50         if (!s2n_is_in_fips_mode()) {
51             S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp.ctx);
52             S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp_md5_secondary.ctx);
53         }
54 
55         /* 2. `free` leftover reference-counted keys (i.e. those with non-zero ref-count),
56               since they are not automatically `free`d until their ref count reaches 0. */
57         free_rc_keys_from_hash_state(&saved_hash_state);
58     }
59     /* 3. free our heap-allocated `state` since `s2n_hash_free` only `free`s the contents. */
60     free(state);
61 }
62