Update harness for aws_cryptosdk_enc_ctx_clone (aws#611)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Update enc_ctx_clone harness and Makefile, additional assumptions, needs new stubs from aws-c-common

* Updated harness to use malloc

* update time in Makefile and remove unneeded assumptions

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

.cbmc-batch/jobs/aws_cryptosdk_enc_ctx_clone/Makefile

@@ -20,8 +20,8 @@ include ../Makefile.local_default
 
 #########
 # Local vars
-MAX_NUM_ELEMS = 4
-# Time on my laptop: 4m50s
+MAX_TABLE_SIZE ?= 4
+# Time on my laptop: 5m10s
 #########
 #if we don't include the hash_table.c, we don't need to remove their function bodies
 ABSTRACTIONS += $(SRCDIR)/c-common-helper-stubs/aws_hash_table_no_slots_override.c
@@ -35,13 +35,14 @@ CBMCFLAGS +=
 
 DEFINES += -DHASH_ITER_ELEMENT_GENERATOR=hash_iterator_string_string_generator
 DEFINES += -DHASH_TABLE_FIND_ELEMENT_GENERATOR=hash_find_string_string_generator
-DEFINES += -DMAX_NUM_ELEMS=$(MAX_NUM_ELEMS)
+DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE)
 
 DEPENDENCIES += $(SRCDIR)/c-common-helper-src/make_common_data_structures.c
 DEPENDENCIES += $(SRCDIR)/c-common-helper-src/proof_allocators.c
 DEPENDENCIES += $(SRCDIR)/c-common-helper-src/utils.c
 DEPENDENCIES += $(SRCDIR)/c-common-src/byte_buf.c
 DEPENDENCIES += $(SRCDIR)/c-common-src/common.c
+DEPENDENCIES += $(SRCDIR)/c-common-src/hash_table.c
 DEPENDENCIES += $(SRCDIR)/c-common-src/math.c
 DEPENDENCIES += $(SRCDIR)/c-common-src/string.c
 DEPENDENCIES += $(SRCDIR)/c-enc-sdk-src/enc_ctx.c
@@ -51,8 +52,7 @@ ENTRY = aws_cryptosdk_enc_ctx_clone_harness
 REMOVE_FUNCTION_BODIES += --remove-function-body aws_string_destroy
 REMOVE_FUNCTION_BODIES += --remove-function-body aws_string_new_from_array
 
-UNWINDSET += aws_cryptosdk_enc_ctx_clone.0:$(shell echo $$(($(MAX_NUM_ELEMS) + 1)))
-UNWINDSET += aws_cryptosdk_enc_ctx_clone.1:$(shell echo $$(($(MAX_NUM_ELEMS) + 1)))
-
+UNWINDSET += aws_cryptosdk_enc_ctx_clone.0:$(shell echo $$((1 + $(MAX_TABLE_SIZE))))
+UNWINDSET += aws_cryptosdk_enc_ctx_clone.1:$(shell echo $$((1 + $(MAX_TABLE_SIZE))))
 ###########
 include ../Makefile.common

.cbmc-batch/jobs/aws_cryptosdk_enc_ctx_clone/aws_cryptosdk_enc_ctx_clone_harness.c

@@ -20,19 +20,22 @@
 #include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
-void make_hash_table_with_no_backing_store(struct aws_hash_table *map, size_t max_table_entries);
-
-/**
- * The actual proof
- */
 void aws_cryptosdk_enc_ctx_clone_harness() {
-    struct aws_hash_table dest;
-    make_hash_table_with_no_backing_store(&dest, MAX_NUM_ELEMS);
-    __CPROVER_assume(aws_hash_table_is_valid(&dest));
+    /* Nondet Input */
+    struct aws_hash_table *dest = malloc(sizeof(*dest));
+    struct aws_hash_table *src  = malloc(sizeof(*src));
+
+    /* Assumptions */
+    ensure_allocated_hash_table(dest, MAX_TABLE_SIZE);
+    __CPROVER_assume(aws_hash_table_is_valid(dest));
+    __CPROVER_assume(dest->p_impl->entry_count <= MAX_TABLE_SIZE);
+    ensure_hash_table_has_valid_destroy_functions(dest);
 
-    struct aws_hash_table src;
-    make_hash_table_with_no_backing_store(&src, MAX_NUM_ELEMS);
-    __CPROVER_assume(aws_hash_table_is_valid(&src));
+    ensure_allocated_hash_table(src, MAX_TABLE_SIZE);
+    __CPROVER_assume(aws_hash_table_is_valid(src));
+    __CPROVER_assume(src->p_impl->entry_count <= MAX_TABLE_SIZE);
+    ensure_hash_table_has_valid_destroy_functions(src);
 
-    int rval = aws_cryptosdk_enc_ctx_clone(can_fail_allocator(), &dest, &src);
+    /* Operation under verification */
+    int rval = aws_cryptosdk_enc_ctx_clone(can_fail_allocator(), dest, src);
 }