Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds proof harnesses for aws_byte_cursor_eq* functions #386

Merged
merged 4 commits into from
May 30, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 32 additions & 0 deletions .cbmc-batch/jobs/aws_byte_cursor_eq/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
# 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 ../Makefile.aws_byte_buf

UNWINDSET += memcmp.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 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 += $(HELPERDIR)/stubs/memcmp_override.c
DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
DEPENDENCIES += $(SRCDIR)/source/common.c

ENTRY = aws_byte_cursor_eq_harness
###########

include ../Makefile.common
62 changes: 62 additions & 0 deletions .cbmc-batch/jobs/aws_byte_cursor_eq/aws_byte_cursor_eq_harness.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
/*
* 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/byte_buf.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>

void aws_byte_cursor_eq_harness() {
/* parameters */
struct aws_byte_cursor lhs;
struct aws_byte_cursor rhs;

/* assumptions */
__CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE));
ensure_byte_cursor_has_allocated_buffer_member(&lhs);
__CPROVER_assume(aws_byte_cursor_is_valid(&lhs));
if (nondet_bool()) {
rhs = lhs;
} else {
__CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE));
ensure_byte_cursor_has_allocated_buffer_member(&rhs);
__CPROVER_assume(aws_byte_cursor_is_valid(&rhs));
}

/* save current state of the data structure */
struct aws_byte_cursor old_lhs = lhs;
struct store_byte_from_buffer old_byte_from_lhs;
save_byte_from_array(lhs.ptr, lhs.len, &old_byte_from_lhs);
struct aws_byte_cursor old_rhs = rhs;
struct store_byte_from_buffer old_byte_from_rhs;
save_byte_from_array(rhs.ptr, rhs.len, &old_byte_from_rhs);

/* operation under verification */
if (aws_byte_cursor_eq((nondet_bool() ? &lhs : NULL), (nondet_bool() ? &rhs : NULL))) {
assert(lhs.len == rhs.len);
if (lhs.len > 0) {
assert_bytes_match(lhs.ptr, rhs.ptr, lhs.len);
}
}

/* assertions */
assert(aws_byte_cursor_is_valid(&lhs));
assert(aws_byte_cursor_is_valid(&rhs));
if (lhs.len != 0) {
assert_byte_from_buffer_matches(lhs.ptr, &old_byte_from_lhs);
}
if (rhs.len != 0) {
assert_byte_from_buffer_matches(rhs.ptr, &old_byte_from_rhs);
}
}
4 changes: 4 additions & 0 deletions .cbmc-batch/jobs/aws_byte_cursor_eq/cbmc-batch.yaml
Original file line number Diff line number Diff line change
@@ -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;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;memcmp.0:11;--object-bits;8"
goto: aws_byte_cursor_eq_harness.goto
expected: "SUCCESSFUL"
33 changes: 33 additions & 0 deletions .cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
# 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 ../Makefile.aws_byte_buf

UNWINDSET += memcmp.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
UNWINDSET += aws_array_eq_ignore_case.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 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 += $(HELPERDIR)/stubs/memcmp_override.c
DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
DEPENDENCIES += $(SRCDIR)/source/common.c

ENTRY = aws_byte_cursor_eq_ignore_case_harness
###########

include ../Makefile.common
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
/*
* 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/byte_buf.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>

void aws_byte_cursor_eq_ignore_case_harness() {
/* parameters */
struct aws_byte_cursor lhs;
struct aws_byte_cursor rhs;

/* assumptions */
__CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE));
ensure_byte_cursor_has_allocated_buffer_member(&lhs);
__CPROVER_assume(aws_byte_cursor_is_valid(&lhs));
if (nondet_bool()) {
rhs = lhs;
} else {
__CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE));
ensure_byte_cursor_has_allocated_buffer_member(&rhs);
__CPROVER_assume(aws_byte_cursor_is_valid(&rhs));
}

/* save current state of the data structure */
struct aws_byte_cursor old_lhs = lhs;
struct store_byte_from_buffer old_byte_from_lhs;
save_byte_from_array(lhs.ptr, lhs.len, &old_byte_from_lhs);
struct aws_byte_cursor old_rhs = rhs;
struct store_byte_from_buffer old_byte_from_rhs;
save_byte_from_array(rhs.ptr, rhs.len, &old_byte_from_rhs);

/* operation under verification */
if (aws_byte_cursor_eq_ignore_case((nondet_bool() ? &lhs : NULL), (nondet_bool() ? &rhs : NULL))) {
assert(lhs.len == rhs.len);
}

/* assertions */
assert(aws_byte_cursor_is_valid(&lhs));
assert(aws_byte_cursor_is_valid(&rhs));
if (lhs.len != 0) {
assert_byte_from_buffer_matches(lhs.ptr, &old_byte_from_lhs);
}
if (rhs.len != 0) {
assert_byte_from_buffer_matches(rhs.ptr, &old_byte_from_rhs);
}
}
Original file line number Diff line number Diff line change
@@ -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;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;memcmp.0:11,aws_array_eq_ignore_case.0:11;--object-bits;8"
goto: aws_byte_cursor_eq_ignore_case_harness.goto
expected: "SUCCESSFUL"
12 changes: 8 additions & 4 deletions source/byte_buf.c
Original file line number Diff line number Diff line change
Expand Up @@ -272,13 +272,17 @@ int aws_byte_buf_cat(struct aws_byte_buf *dest, size_t number_of_args, ...) {
}

bool aws_byte_cursor_eq(const struct aws_byte_cursor *a, const struct aws_byte_cursor *b) {
AWS_ASSERT(a && b);
return aws_array_eq(a->ptr, a->len, b->ptr, b->len);
AWS_PRECONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
bool rv = aws_array_eq(a->ptr, a->len, b->ptr, b->len);
AWS_POSTCONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
return rv;
}

bool aws_byte_cursor_eq_ignore_case(const struct aws_byte_cursor *a, const struct aws_byte_cursor *b) {
AWS_ASSERT(a && b);
return aws_array_eq_ignore_case(a->ptr, a->len, b->ptr, b->len);
AWS_PRECONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
bool rv = aws_array_eq_ignore_case(a->ptr, a->len, b->ptr, b->len);
AWS_POSTCONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
return rv;
}

/* Every possible uint8_t value, lowercased */
Expand Down