Skip to content

Commit 56bb816

Browse files
danielsndanielsn
authored
Hash table predefined hashes (#364)
* aws_hash_ptr + aws_hash_c_string * suppress undefined checks * check inputs to hash functions * turn on overflow checking, will work once diffblue/cbmc#4666 is merged * whitespace change to retrigger ci * Update bounds to aws_hash_c_string proof Signed-off-by: Felipe R. Monteiro <[email protected]> * Update bounds to aws_hash_string proof Signed-off-by: Felipe R. Monteiro <[email protected]> * Update cbmc-batch.yaml files Signed-off-by: Felipe R. Monteiro <[email protected]> * Disable pointers check on parts of hashlittle2 Signed-off-by: Felipe R. Monteiro <[email protected]> * Update bounds in aws_hash_c_string and aws_hash_string proofs Signed-off-by: Felipe R. Monteiro <[email protected]> * Improve documentation on the aws_hash_string proof Signed-off-by: Felipe R. Monteiro <[email protected]> * PR comments Signed-off-by: Felipe R. Monteiro <[email protected]> * Update cbmc-batch.yaml files Signed-off-by: Felipe R. Monteiro <[email protected]> * PR comments Signed-off-by: Felipe R. Monteiro <[email protected]> * Update proofs bounds Signed-off-by: Felipe R. Monteiro <[email protected]> * Guard CPROVER pragmas with CBMC macro Signed-off-by: Felipe R. Monteiro <[email protected]> * Update postconditions Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 0459e83 commit 56bb816

File tree

11 files changed

+258
-14
lines changed

11 files changed

+258
-14
lines changed

‎.cbmc-batch/jobs/aws_hash_c_string/Makefile

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
4+
# this file except in compliance with the License. A copy of the License is
5+
# located at
6+
#
7+
# http://aws.amazon.com/apache2.0/
8+
#
9+
# or in the "license" file accompanying this file. This file is distributed on an
10+
# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
11+
# implied. See the License for the specific language governing permissions and
12+
# limitations under the License.
13+
14+
###########
15+
#32: 4s
16+
#64: 5s
17+
#128 6s
18+
#256 11s
19+
#1024: 2m30s
20+
MAX_STRING_SIZE ?= 32
21+
DEFINES += -DMAX_STRING_SIZE=$(MAX_STRING_SIZE)
22+
23+
UNWINDSET += strlen.0:$(shell echo $$(( $(MAX_STRING_SIZE) + 1)))
24+
UNWINDSET += __CPROVER_file_local_lookup3_c_hashlittle2.0:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
25+
UNWINDSET += __CPROVER_file_local_lookup3_c_hashlittle2.1:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
26+
UNWINDSET += __CPROVER_file_local_lookup3_c_hashlittle2.2:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
27+
28+
CBMCFLAGS +=
29+
30+
DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
31+
DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
32+
DEPENDENCIES += $(HELPERDIR)/source/utils.c
33+
DEPENDENCIES += $(HELPERDIR)/stubs/error.c
34+
DEPENDENCIES += $(SRCDIR)/source/common.c
35+
DEPENDENCIES += $(SRCDIR)/source/hash_table.c
36+
37+
ENTRY = aws_hash_c_string_harness
38+
###########
39+
40+
include ../Makefile.common

‎.cbmc-batch/jobs/aws_hash_c_string/aws_hash_c_string_harness.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
/*
2+
* Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License"). You may not use
5+
* this file except in compliance with the License. A copy of the License is
6+
* located at
7+
*
8+
* http://aws.amazon.com/apache2.0/
9+
*
10+
* or in the "license" file accompanying this file. This file is distributed on an
11+
* "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
12+
* implied. See the License for the specific language governing permissions and
13+
* limitations under the License.
14+
*/
15+
16+
#include <aws/common/hash_table.h>
17+
#include <aws/common/private/hash_table_impl.h>
18+
#include <proof_helpers/make_common_data_structures.h>
19+
#include <proof_helpers/proof_allocators.h>
20+
#include <proof_helpers/utils.h>
21+
22+
void aws_hash_c_string_harness() {
23+
const char *str = make_arbitrary_c_str(MAX_STRING_SIZE);
24+
/* This function has no pre or post conditions */
25+
uint64_t rval = aws_hash_c_string(str);
26+
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
jobos: ubuntu16
2+
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:33,__CPROVER_file_local_lookup3_c_hashlittle2.0:3,__CPROVER_file_local_lookup3_c_hashlittle2.1:3,__CPROVER_file_local_lookup3_c_hashlittle2.2:3;--object-bits;8"
3+
goto: aws_hash_c_string_harness.goto
4+
expected: "SUCCESSFUL"

‎.cbmc-batch/jobs/aws_hash_ptr/Makefile

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
4+
# this file except in compliance with the License. A copy of the License is
5+
# located at
6+
#
7+
# http://aws.amazon.com/apache2.0/
8+
#
9+
# or in the "license" file accompanying this file. This file is distributed on an
10+
# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
11+
# implied. See the License for the specific language governing permissions and
12+
# limitations under the License.
13+
14+
###########
15+
16+
CBMCFLAGS +=
17+
18+
DEPENDENCIES += $(HELPERDIR)/source/utils.c
19+
DEPENDENCIES += $(HELPERDIR)/stubs/error.c
20+
DEPENDENCIES += $(SRCDIR)/source/common.c
21+
DEPENDENCIES += $(SRCDIR)/source/hash_table.c
22+
23+
ENTRY = aws_hash_ptr_harness
24+
###########
25+
26+
include ../Makefile.common

‎.cbmc-batch/jobs/aws_hash_ptr/aws_hash_ptr_harness.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
/*
2+
* Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License"). You may not use
5+
* this file except in compliance with the License. A copy of the License is
6+
* located at
7+
*
8+
* http://aws.amazon.com/apache2.0/
9+
*
10+
* or in the "license" file accompanying this file. This file is distributed on an
11+
* "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
12+
* implied. See the License for the specific language governing permissions and
13+
* limitations under the License.
14+
*/
15+
16+
#include <aws/common/hash_table.h>
17+
#include <aws/common/private/hash_table_impl.h>
18+
#include <proof_helpers/make_common_data_structures.h>
19+
#include <proof_helpers/proof_allocators.h>
20+
#include <proof_helpers/utils.h>
21+
22+
void aws_hash_ptr_harness() {
23+
void *ptr;
24+
/* This function has no pre or post conditions */
25+
uint64_t rval = aws_hash_ptr(ptr);
26+
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
jobos: ubuntu16
2+
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"
3+
goto: aws_hash_ptr_harness.goto
4+
expected: "SUCCESSFUL"

‎.cbmc-batch/jobs/aws_hash_string/Makefile

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
4+
# this file except in compliance with the License. A copy of the License is
5+
# located at
6+
#
7+
# http://aws.amazon.com/apache2.0/
8+
#
9+
# or in the "license" file accompanying this file. This file is distributed on an
10+
# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
11+
# implied. See the License for the specific language governing permissions and
12+
# limitations under the License.
13+
14+
###########
15+
#32: 4s
16+
#64: 5s
17+
#128 6s
18+
#256 11s
19+
#1024: 2m 30s
20+
MAX_STRING_SIZE ?= 32
21+
DEFINES += -DMAX_STRING_SIZE=$(MAX_STRING_SIZE)
22+
23+
UNWINDSET += __CPROVER_file_local_lookup3_c_hashlittle2.0:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
24+
UNWINDSET += __CPROVER_file_local_lookup3_c_hashlittle2.1:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
25+
UNWINDSET += __CPROVER_file_local_lookup3_c_hashlittle2.2:$(shell echo $$(( $$(( $(MAX_STRING_SIZE) / 12 )) +1 )) )
26+
27+
CBMCFLAGS +=
28+
29+
DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
30+
DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
31+
DEPENDENCIES += $(HELPERDIR)/source/utils.c
32+
DEPENDENCIES += $(HELPERDIR)/stubs/error.c
33+
DEPENDENCIES += $(SRCDIR)/source/common.c
34+
DEPENDENCIES += $(SRCDIR)/source/hash_table.c
35+
36+
ENTRY = aws_hash_string_harness
37+
###########
38+
39+
include ../Makefile.common

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

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/*
2+
* Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License"). You may not use
5+
* this file except in compliance with the License. A copy of the License is
6+
* located at
7+
*
8+
* http://aws.amazon.com/apache2.0/
9+
*
10+
* or in the "license" file accompanying this file. This file is distributed on an
11+
* "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
12+
* implied. See the License for the specific language governing permissions and
13+
* limitations under the License.
14+
*/
15+
16+
#include <aws/common/hash_table.h>
17+
#include <aws/common/private/hash_table_impl.h>
18+
#include <proof_helpers/make_common_data_structures.h>
19+
#include <proof_helpers/proof_allocators.h>
20+
#include <proof_helpers/utils.h>
21+
22+
void aws_hash_string_harness() {
23+
struct aws_string *str =
24+
make_arbitrary_aws_string_nondet_len_with_max(nondet_bool() ? NULL : can_fail_allocator(), MAX_STRING_SIZE);
25+
/*
26+
* aws_hash_string has no pre or post conditions. #TODO: Currently, CBMC is unable to
27+
* check all possible paths in these proof. aws_hash_string function calls hashlittle2
28+
* function, which calculates two 32-bit hash values. Internally, it contains two
29+
* conditions that test for alignment to 4 byte/2 byte boundaries, but CBMC is unable
30+
* to correctly evaluate such conditions, due to its pointer encoding. A potential
31+
* fix to this problem is under development.
32+
* For more details, see https://github.com/diffblue/cbmc/pull/1086.
33+
*/
34+
uint64_t rval = aws_hash_string(str);
35+
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
jobos: ubuntu16
2+
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;__CPROVER_file_local_lookup3_c_hashlittle2.0:3,__CPROVER_file_local_lookup3_c_hashlittle2.1:3,__CPROVER_file_local_lookup3_c_hashlittle2.2:3;--object-bits;8"
3+
goto: aws_hash_string_harness.goto
4+
expected: "SUCCESSFUL"

‎include/aws/common/private/lookup3.c

Lines changed: 48 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,11 @@ on 1 byte), but shoehorning those bytes into integers efficiently is messy.
5858
#pragma warning(disable:4127) /*Disable "conditional expression is constant" */
5959
#endif /* _MSC_VER */
6060

61+
#ifdef CBMC
62+
# pragma CPROVER check push
63+
# pragma CPROVER check disable "unsigned-overflow"
64+
#endif /* CBMC */
65+
6166
/*
6267
* My best guess at if you are big-endian or little-endian. This may
6368
* need adjustment.
@@ -322,12 +327,18 @@ static uint32_t hashlittle( const void *key, size_t length, uint32_t initval)
322327
* "k[2]&0xffffff" actually reads beyond the end of the string, but
323328
* then masks off the part it's not allowed to read. Because the
324329
* string is aligned, the masked-off tail is in the same word as the
325-
* rest of the string. Every machine with memory protection I've seen
326-
* does it on word boundaries, so is OK with this. But VALGRIND will
327-
* still catch it and complain. The masking trick does make the hash
328-
* noticably faster for short strings (like English words).
330+
* rest of the string. Every machine with memory protection I've seen
331+
* does it on word boundaries, so is OK with this. But VALGRIND and CBMC
332+
* will still catch it and complain. CBMC will ignore this type of error
333+
* in the code block between the pragmas "CPROVER check push" and
334+
* "CPROVER check pop". The masking trick does make the hash noticably
335+
* faster for short strings (like English words).
329336
*/
330337
#ifndef VALGRIND
338+
#ifdef CBMC
339+
# pragma CPROVER check push
340+
# pragma CPROVER check disable "pointer"
341+
#endif
331342
// changed in aws-c-common: fix unused variable warning
332343

333344
switch(length)
@@ -346,7 +357,9 @@ static uint32_t hashlittle( const void *key, size_t length, uint32_t initval)
346357
case 1 : a+=k[0]&0xff; break;
347358
case 0 : return c; /* zero length strings require no mixing */
348359
}
349-
360+
#ifdef CBMC
361+
# pragma CPROVER check pop
362+
#endif
350363
#else /* make valgrind happy */
351364

352365
const uint8_t *k8 = (const uint8_t *)k;
@@ -506,12 +519,18 @@ static void hashlittle2(
506519
* "k[2]&0xffffff" actually reads beyond the end of the string, but
507520
* then masks off the part it's not allowed to read. Because the
508521
* string is aligned, the masked-off tail is in the same word as the
509-
* rest of the string. Every machine with memory protection I've seen
510-
* does it on word boundaries, so is OK with this. But VALGRIND will
511-
* still catch it and complain. The masking trick does make the hash
512-
* noticably faster for short strings (like English words).
522+
* rest of the string. Every machine with memory protection I've seen
523+
* does it on word boundaries, so is OK with this. But VALGRIND and CBMC
524+
* will still catch it and complain. CBMC will ignore this type of error
525+
* in the code block between the pragmas "CPROVER check push" and
526+
* "CPROVER check pop". The masking trick does make the hash noticably
527+
* faster for short strings (like English words).
513528
*/
514529
#ifndef VALGRIND
530+
#ifdef CBMC
531+
# pragma CPROVER check push
532+
# pragma CPROVER check disable "pointer"
533+
#endif
515534
// changed in aws-c-common: fix unused variable warning
516535

517536
switch(length)
@@ -531,6 +550,9 @@ static void hashlittle2(
531550
case 0 : *pc=c; *pb=b; return; /* zero length strings require no mixing */
532551
}
533552

553+
#ifdef CBMC
554+
# pragma CPROVER check pop
555+
#endif
534556
#else /* make valgrind happy */
535557

536558
const uint8_t *k8 = (const uint8_t *)k;
@@ -682,12 +704,18 @@ static uint32_t hashbig( const void *key, size_t length, uint32_t initval)
682704
* "k[2]<<8" actually reads beyond the end of the string, but
683705
* then shifts out the part it's not allowed to read. Because the
684706
* string is aligned, the illegal read is in the same word as the
685-
* rest of the string. Every machine with memory protection I've seen
686-
* does it on word boundaries, so is OK with this. But VALGRIND will
687-
* still catch it and complain. The masking trick does make the hash
688-
* noticably faster for short strings (like English words).
707+
* rest of the string. Every machine with memory protection I've seen
708+
* does it on word boundaries, so is OK with this. But VALGRIND and CBMC
709+
* will still catch it and complain. CBMC will ignore this type of error
710+
* in the code block between the pragmas "CPROVER check push" and
711+
* "CPROVER check pop". The masking trick does make the hash noticably
712+
* faster for short strings (like English words).
689713
*/
690714
#ifndef VALGRIND
715+
#ifdef CBMC
716+
# pragma CPROVER check push
717+
# pragma CPROVER check disable "pointer"
718+
#endif
691719
// changed in aws-c-common: fix unused variable warning
692720

693721
switch(length)
@@ -706,7 +734,9 @@ static uint32_t hashbig( const void *key, size_t length, uint32_t initval)
706734
case 1 : a+=k[0]&0xff000000; break;
707735
case 0 : return c; /* zero length strings require no mixing */
708736
}
709-
737+
#ifdef CBMC
738+
# pragma CPROVER check pop
739+
#endif
710740
#else /* make valgrind happy */
711741

712742
const uint8_t *k8 = (const uint8_t *)k;
@@ -1017,3 +1047,7 @@ int main()
10171047
#if _MSC_VER
10181048
#pragma warning(pop)
10191049
#endif /* _MSC_VER */
1050+
1051+
#ifdef CBMC
1052+
# pragma CPROVER check pop
1053+
#endif /* CBMC */

‎source/hash_table.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -972,6 +972,7 @@ void aws_hash_table_clear(struct aws_hash_table *map) {
972972
}
973973

974974
uint64_t aws_hash_c_string(const void *item) {
975+
AWS_PRECONDITION(aws_c_string_is_valid(item));
975976
const char *str = item;
976977

977978
/* first digits of pi in hex */
@@ -982,26 +983,31 @@ uint64_t aws_hash_c_string(const void *item) {
982983
}
983984

984985
uint64_t aws_hash_string(const void *item) {
986+
AWS_PRECONDITION(aws_string_is_valid(item));
985987
const struct aws_string *str = item;
986988

987989
/* first digits of pi in hex */
988990
uint32_t b = 0x3243F6A8, c = 0x885A308D;
989991
hashlittle2(aws_string_bytes(str), str->len, &c, &b);
992+
AWS_POSTCONDITION(aws_string_is_valid(str));
990993

991994
return ((uint64_t)b << 32) | c;
992995
}
993996

994997
uint64_t aws_hash_byte_cursor_ptr(const void *item) {
998+
AWS_PRECONDITION(aws_byte_cursor_is_valid(item));
995999
const struct aws_byte_cursor *cur = item;
9961000

9971001
/* first digits of pi in hex */
9981002
uint32_t b = 0x3243F6A8, c = 0x885A308D;
9991003
hashlittle2(cur->ptr, cur->len, &c, &b);
1004+
AWS_POSTCONDITION(aws_byte_cursor_is_valid(cur));
10001005

10011006
return ((uint64_t)b << 32) | c;
10021007
}
10031008

10041009
uint64_t aws_hash_ptr(const void *item) {
1010+
/* Since the numeric value of the pointer is considered, not the memory behind it, 0 is an acceptable value */
10051011
/* first digits of e in hex
10061012
* 2.b7e 1516 28ae d2a6 */
10071013
uint32_t b = 0x2b7e1516, c = 0x28aed2a6;

0 commit comments

Comments
 (0)