From 30522e7e3892e0373beb807643311d7f9d7ac4d9 Mon Sep 17 00:00:00 2001 From: Ubuntu Date: Fri, 5 Dec 2025 19:35:37 +0000 Subject: [PATCH 1/2] Add cbmc proof harness for aws_string_new_from_buf --- .../proofs/aws_string_new_from_buf/Makefile | 23 +++++++++++++ .../aws_string_new_from_buf_harness.c | 32 +++++++++++++++++++ .../aws_string_new_from_buf/cbmc-proof.txt | 1 + 3 files changed, 56 insertions(+) create mode 100644 verification/cbmc/proofs/aws_string_new_from_buf/Makefile create mode 100644 verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c create mode 100644 verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt diff --git a/verification/cbmc/proofs/aws_string_new_from_buf/Makefile b/verification/cbmc/proofs/aws_string_new_from_buf/Makefile new file mode 100644 index 000000000..21b0b26fc --- /dev/null +++ b/verification/cbmc/proofs/aws_string_new_from_buf/Makefile @@ -0,0 +1,23 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0. + +include ../Makefile.aws_string +include ../Makefile.aws_byte_buf + +CBMCFLAGS += + +PROOF_UID = aws_string_new_from_buf +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(PROOFDIR)/$(HARNESS_ENTRY).c + +PROOF_SOURCES += $(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c +PROJECT_SOURCES += $(SRCDIR)/source/allocator.c +PROOF_SOURCES += $(PROOF_SOURCE)/utils.c +PROOF_SOURCES += $(PROOF_STUB)/error.c + +PROJECT_SOURCES += $(SRCDIR)/source/byte_buf.c +PROJECT_SOURCES += $(SRCDIR)/source/common.c +PROJECT_SOURCES += $(SRCDIR)/source/string.c + +include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c b/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c new file mode 100644 index 000000000..77b683bbf --- /dev/null +++ b/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c @@ -0,0 +1,32 @@ +/** + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0. + */ + +#include +#include +#include +#include + +void aws_string_new_from_buf_harness() { + /* parameters */ + struct aws_allocator *allocator; + struct aws_byte_buf buf; + + /* precondition */ + ASSUME_DEFAULT_ALLOCATOR(allocator); + __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)); + + /* operation under verification */ + struct aws_string *str = aws_string_new_from_buf(allocator, &buf); + + /* assertions */ + if (str) { + assert(str->len == buf.len); // length matches + assert(str->bytes[str->len] == 0); // Null terminated + assert_bytes_match(str->bytes, buf.buffer, str->len); // bytes match + assert(aws_string_is_valid(str)); // valid string + } +} diff --git a/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt b/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt new file mode 100644 index 000000000..9e15304c6 --- /dev/null +++ b/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt @@ -0,0 +1 @@ +This file marks the directory as containing a CBMC proof From 831d12ccb80f7890302905488ee34a662fdef0f5 Mon Sep 17 00:00:00 2001 From: GeorgiaGriffin Date: Fri, 12 Dec 2025 16:17:46 +0000 Subject: [PATCH 2/2] Fix formatting. --- .../cbmc/proofs/aws_string_new_from_buf/Makefile | 1 + .../aws_string_new_from_buf_harness.c | 9 +++++---- .../cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt | 1 + 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/verification/cbmc/proofs/aws_string_new_from_buf/Makefile b/verification/cbmc/proofs/aws_string_new_from_buf/Makefile index 21b0b26fc..cb6e6a4e0 100644 --- a/verification/cbmc/proofs/aws_string_new_from_buf/Makefile +++ b/verification/cbmc/proofs/aws_string_new_from_buf/Makefile @@ -21,3 +21,4 @@ PROJECT_SOURCES += $(SRCDIR)/source/common.c PROJECT_SOURCES += $(SRCDIR)/source/string.c include ../Makefile.common + diff --git a/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c b/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c index 77b683bbf..99913ad07 100644 --- a/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c +++ b/verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c @@ -24,9 +24,10 @@ void aws_string_new_from_buf_harness() { /* assertions */ if (str) { - assert(str->len == buf.len); // length matches - assert(str->bytes[str->len] == 0); // Null terminated - assert_bytes_match(str->bytes, buf.buffer, str->len); // bytes match - assert(aws_string_is_valid(str)); // valid string + assert(str->len == buf.len); + assert(str->bytes[str->len] == 0); + assert_bytes_match(str->bytes, buf.buffer, str->len); + assert(aws_string_is_valid(str)); } } + diff --git a/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt b/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt index 9e15304c6..6186d166e 100644 --- a/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt +++ b/verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt @@ -1 +1,2 @@ This file marks the directory as containing a CBMC proof +