Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit f32eef1

Browse files
dbeyerdbeyer
authored
Merge pull request #1187 from smackers/fix-memcmp
Cleaned up definitions of memcmp function
2 parents 3e24028 + 19b6e0a commit f32eef1

19 files changed

+59
-306
lines changed

‎c/aws-c-common/aws_array_eq_c_str_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_array_eq_c_str_ignore_case_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_array_eq_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_array_eq_ignore_case_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_byte_buf_cat_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_byte_buf_eq_c_str_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_byte_buf_eq_c_str_ignore_case_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_byte_buf_eq_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_byte_buf_eq_ignore_case_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

‎c/aws-c-common/aws_byte_cursor_compare_lexical_harness.i‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7395,23 +7395,10 @@ int aws_last_error(void) {
73957395

73967396

73977397

7398-
int memcmp(const void *s1, const void *s2, size_t n) {
7399-
7400-
int res = 0;
7398+
int memcmp_safe(const void *s1, const void *s2, size_t n) {
74017399
assume_abort_if_not((((n) == 0) || (s1)));
74027400
assume_abort_if_not((((n) == 0) || (s2)));
7403-
7404-
7405-
const unsigned char *sc1 = s1, *sc2 = s2;
7406-
for (; n != 0; n--) {
7407-
res = (*sc1++) - (*sc2++);
7408-
if (res != 0)
7409-
return res;
7410-
}
7411-
return res;
7412-
7413-
7414-
7401+
return memcmp(s1, s2, n);
74157402
}
74167403
size_t aws_nospec_mask(size_t index, size_t bound);
74177404
int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) {
@@ -8255,7 +8242,7 @@ int aws_byte_cursor_compare_lexical(const struct aws_byte_cursor *lhs, const str
82558242
comparison_length = rhs->len;
82568243
}
82578244

8258-
int result = memcmp(lhs->ptr, rhs->ptr, comparison_length);
8245+
int result = memcmp_safe(lhs->ptr, rhs->ptr, comparison_length);
82598246

82608247
__VERIFIER_assert((aws_byte_cursor_is_valid(lhs)));
82618248
__VERIFIER_assert((aws_byte_cursor_is_valid(rhs)));

0 commit comments

Comments
 (0)