check inputs to hash functions

Author: danielsn

.cbmc-batch/jobs/Makefile.common

@@ -37,7 +37,7 @@ CBMCFLAGS += --pointer-check
 CBMCFLAGS += --pointer-overflow-check
 CBMCFLAGS += --signed-overflow-check
 CBMCFLAGS += --undefined-shift-check
-CBMCFLAGS += --unsigned-overflow-check
+#CBMCFLAGS += --unsigned-overflow-check
 CBMCFLAGS += --unwind 1
 CBMCFLAGS += --unwinding-assertions
 CBMCFLAGS += $(CBMC_UNWINDSET)

.cbmc-batch/jobs/aws_hash_c_string/Makefile

@@ -12,11 +12,16 @@
 # limitations under the License.
 
 ###########
-MAX_STRING_SIZE ?= 4
+#32: 4s
+#64: 5s
+#128 6s
+#256 11s
+#1024: 2m 30s
+MAX_STRING_SIZE ?= 256
 DEFINES += -DMAX_STRING_SIZE=$(MAX_STRING_SIZE) 
 
 UNWINDSET += strlen.0:$(shell echo $$(( $(MAX_STRING_SIZE) + 1)))
-
+UNWINDSET += hashlittle2.2:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
 
 CBMCFLAGS +=
 

.cbmc-batch/jobs/aws_hash_c_string/cbmc-batch.yaml

@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;strlen.0:5;--object-bits;8"
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unwind;1;--unwinding-assertions;--unwindset;strlen.0:257,hashlittle2.2:22;--object-bits;8"
 goto: aws_hash_c_string_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_hash_ptr/cbmc-batch.yaml

@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unwind;1;--unwinding-assertions;--object-bits;8"
 goto: aws_hash_ptr_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_hash_string/Makefile

@@ -0,0 +1,37 @@
+# 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.
+
+###########
+#32: 4s
+#64: 5s
+#128 6s
+#256 11s
+#1024: 2m 30s
+MAX_STRING_SIZE ?= 256
+DEFINES += -DMAX_STRING_SIZE=$(MAX_STRING_SIZE) 
+
+UNWINDSET += hashlittle2.2:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+
+ENTRY = aws_hash_string_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_hash_string/aws_hash_string_harness.c

@@ -0,0 +1,27 @@
+/*
+ * Copyright 2019 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 <aws/common/hash_table.h>
+#include <aws/common/private/hash_table_impl.h>
+#include <proof_helpers/make_common_data_structures.h>
+#include <proof_helpers/proof_allocators.h>
+#include <proof_helpers/utils.h>
+
+void aws_hash_string_harness() {
+    struct aws_string *str =
+        make_arbitrary_aws_string_nondet_len_with_max(nondet_bool() ? NULL : can_fail_allocator(), MAX_STRING_SIZE);
+    /* This function has no pre or post conditions */
+    uint64_t rval = aws_hash_string(str);
+}

.cbmc-batch/jobs/aws_hash_string/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unwind;1;--unwinding-assertions;--unwindset;hashlittle2.2:22;--object-bits;8"
+goto: aws_hash_string_harness.goto
+expected: "SUCCESSFUL"

source/hash_table.c

@@ -972,16 +972,19 @@ void aws_hash_table_clear(struct aws_hash_table *map) {
 }
 
 uint64_t aws_hash_c_string(const void *item) {
+    AWS_PRECONDITION(aws_c_string_is_valid(item));
     const char *str = item;
 
     /* first digits of pi in hex */
     uint32_t b = 0x3243F6A8, c = 0x885A308D;
     hashlittle2(str, strlen(str), &c, &b);
 
+    AWS_POSTCONDITION(aws_c_string_is_valid(item));
     return ((uint64_t)b << 32) | c;
 }
 
 uint64_t aws_hash_string(const void *item) {
+    AWS_PRECONDITION(aws_string_is_valid(item));
     const struct aws_string *str = item;
 
     /* first digits of pi in hex */
@@ -992,16 +995,19 @@ uint64_t aws_hash_string(const void *item) {
 }
 
 uint64_t aws_hash_byte_cursor_ptr(const void *item) {
+    AWS_PRECONDITION(aws_byte_cursor_is_valid(item));
     const struct aws_byte_cursor *cur = item;
 
     /* first digits of pi in hex */
     uint32_t b = 0x3243F6A8, c = 0x885A308D;
     hashlittle2(cur->ptr, cur->len, &c, &b);
 
+    AWS_POSTCONDITION(aws_byte_cursor_is_valid(item));
     return ((uint64_t)b << 32) | c;
 }
 
 uint64_t aws_hash_ptr(const void *item) {
+    /* Since the numberic value of the pointer is considered, not the memory behind it, 0 is an acceptable value */
     /* first digits of e in hex
      * 2.b7e 1516 28ae d2a6 */
     uint32_t b = 0x2b7e1516, c = 0x28aed2a6;