From c27fcc8da20835d57628997d3b653f83269ac569 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 3 Jun 2019 16:22:20 -0400 Subject: [PATCH] Adds proof harnesses for aws_byte_buf_write* functions (#361) * Adds proof harness for aws_byte_buf_write function --- .cbmc-batch/include/proof_helpers/utils.h | 12 +++- .../jobs/aws_byte_buf_write_be16/Makefile | 32 +++++++++++ .../aws_byte_buf_write_be16_harness.c | 44 +++++++++++++++ .../aws_byte_buf_write_be16/cbmc-batch.yaml | 4 ++ .../jobs/aws_byte_buf_write_be32/Makefile | 32 +++++++++++ .../aws_byte_buf_write_be32_harness.c | 44 +++++++++++++++ .../aws_byte_buf_write_be32/cbmc-batch.yaml | 4 ++ .../jobs/aws_byte_buf_write_be64/Makefile | 32 +++++++++++ .../aws_byte_buf_write_be64_harness.c | 44 +++++++++++++++ .../aws_byte_buf_write_be64/cbmc-batch.yaml | 4 ++ .../Makefile | 32 +++++++++++ ...byte_buf_write_from_whole_buffer_harness.c | 55 +++++++++++++++++++ .../cbmc-batch.yaml | 4 ++ .../Makefile | 32 +++++++++++ ...byte_buf_write_from_whole_cursor_harness.c | 55 +++++++++++++++++++ .../cbmc-batch.yaml | 4 ++ .../jobs/aws_byte_buf_write_u8/Makefile | 32 +++++++++++ .../aws_byte_buf_write_u8_harness.c | 44 +++++++++++++++ .../aws_byte_buf_write_u8/cbmc-batch.yaml | 4 ++ .cbmc-batch/source/utils.c | 13 +++++ include/aws/common/byte_buf.h | 6 ++ tests/cursor_test.c | 2 +- 22 files changed, 533 insertions(+), 2 deletions(-) create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be16/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be16/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be32/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be32/aws_byte_buf_write_be32_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be32/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be64/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be64/aws_byte_buf_write_be64_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_be64/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/aws_byte_buf_write_from_whole_buffer_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/aws_byte_buf_write_from_whole_cursor_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_u8/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_u8/aws_byte_buf_write_u8_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_write_u8/cbmc-batch.yaml diff --git a/.cbmc-batch/include/proof_helpers/utils.h b/.cbmc-batch/include/proof_helpers/utils.h index 787163800..d3b0d2e4d 100644 --- a/.cbmc-batch/include/proof_helpers/utils.h +++ b/.cbmc-batch/include/proof_helpers/utils.h @@ -73,11 +73,21 @@ void assert_array_list_equivalence( * it is necessary to select a non-deterministic byte from the rhs aws_byte_buf structure * (use save_byte_from_array function), so it can properly assert all bytes match. */ -void assert_byte_buf_equivalence( +void assert_byte_cursor_equivalence( const struct aws_byte_buf *const lhs, const struct aws_byte_buf *const rhs, const struct store_byte_from_buffer *const rhs_byte); +/** + * Asserts two aws_byte_cursor structures are equivalent. Prior to using this function, + * it is necessary to select a non-deterministic byte from the rhs aws_byte_cursor structure + * (use save_byte_from_array function), so it can properly assert all bytes match. + */ +void assert_byte_buf_equivalence( + const struct aws_byte_cursor *const lhs, + const struct aws_byte_cursor *const rhs, + const struct store_byte_from_buffer *const rhs_byte); + /** * Nondeterministically selects a byte from a hash_table implementation and stores it into a * store_array_list_byte structure. diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be16/Makefile b/.cbmc-batch/jobs/aws_byte_buf_write_be16/Makefile new file mode 100644 index 000000000..572fc5855 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be16/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 += memcpy_impl.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/memcpy_override.c +DEPENDENCIES += $(SRCDIR)/source/byte_buf.c +DEPENDENCIES += $(SRCDIR)/source/common.c + +ENTRY = aws_byte_buf_write_be16_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c b/.cbmc-batch/jobs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c new file mode 100644 index 000000000..0435260a4 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c @@ -0,0 +1,44 @@ +/* + * 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 + +void aws_byte_buf_write_be16_harness() { + /* parameters */ + struct aws_byte_buf buf; + uint16_t x; + + /* assumptions */ + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); + + /* save current state of the parameters */ + struct aws_byte_buf old = buf; + struct store_byte_from_buffer old_byte_from_buf; + save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf); + + /* operation under verification */ + if (aws_byte_buf_write_be16(&buf, x)) { + assert(buf.len == old.len + 2); + assert(old.capacity == buf.capacity); + assert(old.allocator == buf.allocator); + } else { + assert_byte_buf_equivalence(&buf, &old, &old_byte_from_buf); + } + + assert(aws_byte_buf_is_valid(&buf)); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be16/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_write_be16/cbmc-batch.yaml new file mode 100644 index 000000000..621e9d565 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be16/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;memcpy_impl.0:11;--object-bits;8" +goto: aws_byte_buf_write_be16_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be32/Makefile b/.cbmc-batch/jobs/aws_byte_buf_write_be32/Makefile new file mode 100644 index 000000000..30898ffbf --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be32/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 += memcpy_impl.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/memcpy_override.c +DEPENDENCIES += $(SRCDIR)/source/byte_buf.c +DEPENDENCIES += $(SRCDIR)/source/common.c + +ENTRY = aws_byte_buf_write_be32_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be32/aws_byte_buf_write_be32_harness.c b/.cbmc-batch/jobs/aws_byte_buf_write_be32/aws_byte_buf_write_be32_harness.c new file mode 100644 index 000000000..83c4f684d --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be32/aws_byte_buf_write_be32_harness.c @@ -0,0 +1,44 @@ +/* + * 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 + +void aws_byte_buf_write_be32_harness() { + /* parameters */ + struct aws_byte_buf buf; + uint32_t x; + + /* assumptions */ + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); + + /* save current state of the parameters */ + struct aws_byte_buf old = buf; + struct store_byte_from_buffer old_byte_from_buf; + save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf); + + /* operation under verification */ + if (aws_byte_buf_write_be32(&buf, x)) { + assert(buf.len == old.len + 4); + assert(old.capacity == buf.capacity); + assert(old.allocator == buf.allocator); + } else { + assert_byte_buf_equivalence(&buf, &old, &old_byte_from_buf); + } + + assert(aws_byte_buf_is_valid(&buf)); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be32/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_write_be32/cbmc-batch.yaml new file mode 100644 index 000000000..4d71c0355 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be32/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;memcpy_impl.0:11;--object-bits;8" +goto: aws_byte_buf_write_be32_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be64/Makefile b/.cbmc-batch/jobs/aws_byte_buf_write_be64/Makefile new file mode 100644 index 000000000..8671c4d13 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be64/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 += memcpy_impl.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/memcpy_override.c +DEPENDENCIES += $(SRCDIR)/source/byte_buf.c +DEPENDENCIES += $(SRCDIR)/source/common.c + +ENTRY = aws_byte_buf_write_be64_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be64/aws_byte_buf_write_be64_harness.c b/.cbmc-batch/jobs/aws_byte_buf_write_be64/aws_byte_buf_write_be64_harness.c new file mode 100644 index 000000000..8f76fa493 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be64/aws_byte_buf_write_be64_harness.c @@ -0,0 +1,44 @@ +/* + * 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 + +void aws_byte_buf_write_be64_harness() { + /* parameters */ + struct aws_byte_buf buf; + uint64_t x; + + /* assumptions */ + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); + + /* save current state of the parameters */ + struct aws_byte_buf old = buf; + struct store_byte_from_buffer old_byte_from_buf; + save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf); + + /* operation under verification */ + if (aws_byte_buf_write_be64(&buf, x)) { + assert(buf.len == old.len + 8); + assert(old.capacity == buf.capacity); + assert(old.allocator == buf.allocator); + } else { + assert_byte_buf_equivalence(&buf, &old, &old_byte_from_buf); + } + + assert(aws_byte_buf_is_valid(&buf)); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_be64/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_write_be64/cbmc-batch.yaml new file mode 100644 index 000000000..b31499c26 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_be64/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;memcpy_impl.0:11;--object-bits;8" +goto: aws_byte_buf_write_be64_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/Makefile b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/Makefile new file mode 100644 index 000000000..ce4207ce6 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/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 += memcpy_impl.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/memcpy_override.c +DEPENDENCIES += $(SRCDIR)/source/byte_buf.c +DEPENDENCIES += $(SRCDIR)/source/common.c + +ENTRY = aws_byte_buf_write_from_whole_buffer_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/aws_byte_buf_write_from_whole_buffer_harness.c b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/aws_byte_buf_write_from_whole_buffer_harness.c new file mode 100644 index 000000000..7ef39b05d --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/aws_byte_buf_write_from_whole_buffer_harness.c @@ -0,0 +1,55 @@ +/* + * 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 + +void aws_byte_buf_write_from_whole_buffer_harness() { + /* parameters */ + struct aws_byte_buf buf; + struct aws_byte_buf src; + + /* assumptions */ + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); + __CPROVER_assume(aws_byte_buf_is_bounded(&src, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&src); + __CPROVER_assume(aws_byte_buf_is_valid(&src)); + + /* save current state of the parameters */ + struct aws_byte_buf buf_old = buf; + struct store_byte_from_buffer old_byte_from_buf; + save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf); + struct aws_byte_buf src_old = src; + struct store_byte_from_buffer old_byte_from_src; + save_byte_from_array(src.buffer, src.len, &old_byte_from_src); + + /* operation under verification */ + if (aws_byte_buf_write_from_whole_buffer(&buf, src)) { + assert(buf.len == buf_old.len + src.len); + assert(buf_old.capacity == buf.capacity); + assert(buf_old.allocator == buf.allocator); + if (src.len > 0 && buf.len > 0) { + assert_bytes_match(buf.buffer + buf_old.len, src.buffer, src.len); + } + } else { + assert_byte_buf_equivalence(&buf, &buf_old, &old_byte_from_buf); + } + + assert(aws_byte_buf_is_valid(&buf)); + assert(aws_byte_buf_is_valid(&src)); + assert_byte_buf_equivalence(&src, &src_old, &old_byte_from_src); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/cbmc-batch.yaml new file mode 100644 index 000000000..a192aed51 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/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;memcpy_impl.0:11;--object-bits;8" +goto: aws_byte_buf_write_from_whole_buffer_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/Makefile b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/Makefile new file mode 100644 index 000000000..63c9d8ee0 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/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 += memcpy_impl.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/memcpy_override.c +DEPENDENCIES += $(SRCDIR)/source/byte_buf.c +DEPENDENCIES += $(SRCDIR)/source/common.c + +ENTRY = aws_byte_buf_write_from_whole_cursor_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/aws_byte_buf_write_from_whole_cursor_harness.c b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/aws_byte_buf_write_from_whole_cursor_harness.c new file mode 100644 index 000000000..6aab1a7da --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/aws_byte_buf_write_from_whole_cursor_harness.c @@ -0,0 +1,55 @@ +/* + * 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 + +void aws_byte_buf_write_from_whole_cursor_harness() { + /* parameters */ + struct aws_byte_buf buf; + struct aws_byte_cursor src; + + /* assumptions */ + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); + __CPROVER_assume(aws_byte_cursor_is_bounded(&src, MAX_BUFFER_SIZE)); + ensure_byte_cursor_has_allocated_buffer_member(&src); + __CPROVER_assume(aws_byte_cursor_is_valid(&src)); + + /* save current state of the parameters */ + struct aws_byte_buf buf_old = buf; + struct store_byte_from_buffer old_byte_from_buf; + save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf); + struct aws_byte_cursor src_old = src; + struct store_byte_from_buffer old_byte_from_src; + save_byte_from_array(src.ptr, src.len, &old_byte_from_src); + + /* operation under verification */ + if (aws_byte_buf_write_from_whole_cursor(&buf, src)) { + assert(buf.len == buf_old.len + src.len); + assert(buf_old.capacity == buf.capacity); + assert(buf_old.allocator == buf.allocator); + if (src.len > 0 && buf.len > 0) { + assert_bytes_match(buf.buffer + buf_old.len, src.ptr, src.len); + } + } else { + assert_byte_buf_equivalence(&buf, &buf_old, &old_byte_from_buf); + } + + assert(aws_byte_buf_is_valid(&buf)); + assert(aws_byte_cursor_is_valid(&src)); + assert_byte_cursor_equivalence(&src, &src_old, &old_byte_from_src); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/cbmc-batch.yaml new file mode 100644 index 000000000..2e9ddc089 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/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;memcpy_impl.0:11;--object-bits;8" +goto: aws_byte_buf_write_from_whole_cursor_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_u8/Makefile b/.cbmc-batch/jobs/aws_byte_buf_write_u8/Makefile new file mode 100644 index 000000000..dffb2743d --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_u8/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 += memcpy_impl.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/memcpy_override.c +DEPENDENCIES += $(SRCDIR)/source/byte_buf.c +DEPENDENCIES += $(SRCDIR)/source/common.c + +ENTRY = aws_byte_buf_write_u8_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_u8/aws_byte_buf_write_u8_harness.c b/.cbmc-batch/jobs/aws_byte_buf_write_u8/aws_byte_buf_write_u8_harness.c new file mode 100644 index 000000000..b42a97c4f --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_u8/aws_byte_buf_write_u8_harness.c @@ -0,0 +1,44 @@ +/* + * 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 + +void aws_byte_buf_write_u8_harness() { + /* parameters */ + struct aws_byte_buf buf; + uint8_t x; + + /* assumptions */ + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); + + /* save current state of the parameters */ + struct aws_byte_buf old = buf; + struct store_byte_from_buffer old_byte_from_buf; + save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf); + + /* operation under verification */ + if (aws_byte_buf_write_u8(&buf, x)) { + assert(buf.len == old.len + 1); + assert(old.capacity == buf.capacity); + assert(old.allocator == buf.allocator); + } else { + assert_byte_buf_equivalence(&buf, &old, &old_byte_from_buf); + } + + assert(aws_byte_buf_is_valid(&buf)); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_write_u8/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_write_u8/cbmc-batch.yaml new file mode 100644 index 000000000..6b1f4f4ec --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_write_u8/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;memcpy_impl.0:11;--object-bits;8" +goto: aws_byte_buf_write_u8_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/source/utils.c b/.cbmc-batch/source/utils.c index e949bbe9d..be4777188 100644 --- a/.cbmc-batch/source/utils.c +++ b/.cbmc-batch/source/utils.c @@ -88,6 +88,19 @@ void assert_byte_buf_equivalence( } } +void assert_byte_cursor_equivalence( + const struct aws_byte_cursor *const lhs, + const struct aws_byte_cursor *const rhs, + const struct store_byte_from_buffer *const rhs_byte) { + assert(!lhs == !rhs); + if (lhs && rhs) { + assert(lhs->len == rhs->len); + if (lhs->len > 0) { + assert_byte_from_buffer_matches(lhs->ptr, rhs_byte); + } + } +} + void save_byte_from_hash_table(const struct aws_hash_table *map, struct store_byte_from_buffer *storage) { struct hash_table_state *state = map->p_impl; size_t size_in_bytes; diff --git a/include/aws/common/byte_buf.h b/include/aws/common/byte_buf.h index 23060a11b..0804d9a07 100644 --- a/include/aws/common/byte_buf.h +++ b/include/aws/common/byte_buf.h @@ -826,6 +826,7 @@ AWS_STATIC_IMPL bool aws_byte_buf_write( AWS_STATIC_IMPL bool aws_byte_buf_write_from_whole_buffer( struct aws_byte_buf *AWS_RESTRICT buf, struct aws_byte_buf src) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf) && aws_byte_buf_is_valid(&src)); return aws_byte_buf_write(buf, src.buffer, src.len); } @@ -839,6 +840,7 @@ AWS_STATIC_IMPL bool aws_byte_buf_write_from_whole_buffer( AWS_STATIC_IMPL bool aws_byte_buf_write_from_whole_cursor( struct aws_byte_buf *AWS_RESTRICT buf, struct aws_byte_cursor src) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf) && aws_byte_cursor_is_valid(&src)); return aws_byte_buf_write(buf, src.ptr, src.len); } @@ -852,6 +854,7 @@ AWS_STATIC_IMPL bool aws_byte_buf_write_from_whole_cursor( cursor unchanged. */ AWS_STATIC_IMPL bool aws_byte_buf_write_u8(struct aws_byte_buf *AWS_RESTRICT buf, uint8_t c) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); return aws_byte_buf_write(buf, &c, 1); } @@ -863,6 +866,7 @@ AWS_STATIC_IMPL bool aws_byte_buf_write_u8(struct aws_byte_buf *AWS_RESTRICT buf * cursor unchanged. */ AWS_STATIC_IMPL bool aws_byte_buf_write_be16(struct aws_byte_buf *buf, uint16_t x) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); x = aws_hton16(x); return aws_byte_buf_write(buf, (uint8_t *)&x, 2); } @@ -875,6 +879,7 @@ AWS_STATIC_IMPL bool aws_byte_buf_write_be16(struct aws_byte_buf *buf, uint16_t * cursor unchanged. */ AWS_STATIC_IMPL bool aws_byte_buf_write_be32(struct aws_byte_buf *buf, uint32_t x) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); x = aws_hton32(x); return aws_byte_buf_write(buf, (uint8_t *)&x, 4); } @@ -887,6 +892,7 @@ AWS_STATIC_IMPL bool aws_byte_buf_write_be32(struct aws_byte_buf *buf, uint32_t * cursor unchanged. */ AWS_STATIC_IMPL bool aws_byte_buf_write_be64(struct aws_byte_buf *buf, uint64_t x) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); x = aws_hton64(x); return aws_byte_buf_write(buf, (uint8_t *)&x, 8); } diff --git a/tests/cursor_test.c b/tests/cursor_test.c index da32163ef..c54520057 100644 --- a/tests/cursor_test.c +++ b/tests/cursor_test.c @@ -231,7 +231,7 @@ static int s_byte_cursor_limit_tests_fn(struct aws_allocator *allocator, void *c ASSERT_TRUE(aws_byte_cursor_read(&cur, arr, 0)); ASSERT_TRUE(aws_byte_buf_write(&buffer, arr, 0)); - arrbuf.capacity = 0; + aws_byte_buf_clean_up(&arrbuf); ASSERT_TRUE(aws_byte_cursor_read_and_fill_buffer(&cur, &arrbuf)); ASSERT_TRUE(aws_byte_buf_write_from_whole_buffer(&buffer, arrbuf)); ASSERT_UINT_EQUALS(0, arr[0]);