From 9ec02e631c5b38cfc904638b562ebe7fa0832eb3 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 29 May 2019 15:43:32 -0400 Subject: [PATCH 1/3] Adds pre and postconditions to aws_byte_cursor_eq and aws_byte_cursor_eq_ignore_case functions Signed-off-by: Felipe R. Monteiro --- source/byte_buf.c | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/source/byte_buf.c b/source/byte_buf.c index b8db90172..877bbe51c 100644 --- a/source/byte_buf.c +++ b/source/byte_buf.c @@ -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 */ From f9e57869326e0c13d90a723b3045222bd443111d Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 29 May 2019 15:44:00 -0400 Subject: [PATCH 2/3] Adds a proof harness for aws_byte_cursor_eq function Signed-off-by: Felipe R. Monteiro --- .cbmc-batch/jobs/aws_byte_cursor_eq/Makefile | 32 ++++++++++ .../aws_byte_cursor_eq_harness.c | 62 +++++++++++++++++++ .../jobs/aws_byte_cursor_eq/cbmc-batch.yaml | 4 ++ 3 files changed, 98 insertions(+) create mode 100644 .cbmc-batch/jobs/aws_byte_cursor_eq/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_cursor_eq/aws_byte_cursor_eq_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_cursor_eq/cbmc-batch.yaml diff --git a/.cbmc-batch/jobs/aws_byte_cursor_eq/Makefile b/.cbmc-batch/jobs/aws_byte_cursor_eq/Makefile new file mode 100644 index 000000000..702e847a7 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_cursor_eq/Makefile @@ -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 diff --git a/.cbmc-batch/jobs/aws_byte_cursor_eq/aws_byte_cursor_eq_harness.c b/.cbmc-batch/jobs/aws_byte_cursor_eq/aws_byte_cursor_eq_harness.c new file mode 100644 index 000000000..3eab0f71b --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_cursor_eq/aws_byte_cursor_eq_harness.c @@ -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 +#include +#include + +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); + } +} diff --git a/.cbmc-batch/jobs/aws_byte_cursor_eq/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_cursor_eq/cbmc-batch.yaml new file mode 100644 index 000000000..3ee768323 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_cursor_eq/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;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;memcmp.0:11;--object-bits;8" +goto: aws_byte_cursor_eq_harness.goto +expected: "SUCCESSFUL" From 001bda0d75889560f27a853b7ccb1965a9a2bd9a Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 29 May 2019 15:44:19 -0400 Subject: [PATCH 3/3] Adds a proof harness for aws_byte_cursor_eq_ignore_case function Signed-off-by: Felipe R. Monteiro --- .../aws_byte_cursor_eq_ignore_case/Makefile | 33 +++++++++++ .../aws_byte_cursor_eq_ignore_case_harness.c | 59 +++++++++++++++++++ .../cbmc-batch.yaml | 4 ++ 3 files changed, 96 insertions(+) create mode 100644 .cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/aws_byte_cursor_eq_ignore_case_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/cbmc-batch.yaml diff --git a/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/Makefile b/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/Makefile new file mode 100644 index 000000000..4be8d5911 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/Makefile @@ -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 diff --git a/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/aws_byte_cursor_eq_ignore_case_harness.c b/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/aws_byte_cursor_eq_ignore_case_harness.c new file mode 100644 index 000000000..cffd69900 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/aws_byte_cursor_eq_ignore_case_harness.c @@ -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 +#include +#include + +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); + } +} diff --git a/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/cbmc-batch.yaml new file mode 100644 index 000000000..d4f28887d --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/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;--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"