Update file structure for proofs (#277)

awslabs · Mar 15, 2019 · a09c186 · a09c186
1 parent 56e3549
commit a09c186
Show file tree

Hide file tree

Showing 35 changed files with 287 additions and 1,054 deletions.
diff --git a/.cbmc-batch/config.h b/.cbmc-batch/config.h
diff --git a/.cbmc-batch/aws/common/config.h → .cbmc-batch/include/aws/common/config.h b/.cbmc-batch/aws/common/config.h → .cbmc-batch/include/aws/common/config.h
diff --git a/.cbmc-batch/include/proof_helpers/make_common_data_structures.h b/.cbmc-batch/include/proof_helpers/make_common_data_structures.h
@@ -0,0 +1,36 @@
+/*
+ * Copyright 2018 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.
+ */
+
+#pragma once
+
+#include <aws/common/array_list.h>
+#include <aws/common/common.h>
+
+#include "nondet.h"
+
+#include <stdlib.h>
+
+#define MAX_INITIAL_ITEM_ALLOCATION 2
+#define MAX_ITEM_SIZE 2
+#define MAX_STR_LEN 32
+#define MAX_BUF_LEN 32
+
+#define ASSUME_VALID_MEMORY(ptr) ptr = malloc(sizeof(*(ptr)))
+#define ASSUME_VALID_MEMORY_COUNT(ptr, count) ptr = malloc(sizeof(*(ptr)) * (count))
+#define ASSUME_DEFAULT_ALLOCATOR(allocator) allocator = aws_default_allocator()
+#define ASSUME_ARBITRARY_ARRAY_LIST(list, item_count, item_size)                                                       \
+    list = make_arbitrary_array_list((item_count), (item_size))
+
+struct aws_array_list *make_arbitrary_array_list(size_t item_count, size_t item_size);
diff --git a/.cbmc-batch/include/proof_helpers/nondet.h b/.cbmc-batch/include/proof_helpers/nondet.h
@@ -0,0 +1,29 @@
+/*
+ * Copyright 2018 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.
+ */
+
+#pragma once
+
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+
+/**
+ * Non-determinstic functions used in CBMC proofs
+ */
+size_t nondet_size_t();
+int nondet_int();
+uint8_t nondet_uint8_t();
+bool nondet_bool();
+void *nondet_voidp();
diff --git a/.cbmc-batch/jobs/Makefile.common b/.cbmc-batch/jobs/Makefile.common
@@ -37,7 +37,7 @@ GOTO_INSTRUMENT ?= goto-instrument
 HELPERDIR ?= $(SRCDIR)/.cbmc-batch
 
 INC += \
-	-I$(HELPERDIR)/. \
+	-I$(HELPERDIR)/include/ \
 	-I$(SRCDIR)/include/
 
 SIMPLIFY ?= 0

diff --git a/.cbmc-batch/jobs/aws_add_size_checked/Makefile b/.cbmc-batch/jobs/aws_add_size_checked/Makefile
@@ -17,8 +17,9 @@
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+DEPENDENCIES = $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_add_size_checked_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_add_size_checked/aws_add_size_checked_harness.c b/.cbmc-batch/jobs/aws_add_size_checked/aws_add_size_checked_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/math.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 /**
  * Adds a + b and returns the result in *r. If the result

diff --git a/.cbmc-batch/jobs/aws_add_size_saturating/Makefile b/.cbmc-batch/jobs/aws_add_size_saturating/Makefile
@@ -17,8 +17,9 @@
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_add_size_saturating_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_add_size_saturating/aws_add_size_saturating_harness.c b/.cbmc-batch/jobs/aws_add_size_saturating/aws_add_size_saturating_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/math.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 /**
  * Adds a + b.  If the result overflows returns 2^64 - 1.

diff --git a/.cbmc-batch/jobs/aws_array_list_init_dynamic/Makefile b/.cbmc-batch/jobs/aws_array_list_init_dynamic/Makefile
@@ -17,10 +17,10 @@
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
-	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(SRCDIR)/source/array_list.c \
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_array_list_init_dynamic_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_array_list_init_dynamic/aws_array_list_init_dynamic_harness.c b/.cbmc-batch/jobs/aws_array_list_init_dynamic/aws_array_list_init_dynamic_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/array_list.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_array_list_init_dynamic_harness() {
     struct aws_array_list *list;

diff --git a/.cbmc-batch/jobs/aws_array_list_init_static/Makefile b/.cbmc-batch/jobs/aws_array_list_init_static/Makefile
@@ -17,10 +17,10 @@
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
-	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(SRCDIR)/source/array_list.c \
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_array_list_init_static_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_array_list_init_static/aws_array_list_init_static_harness.c b/.cbmc-batch/jobs/aws_array_list_init_static/aws_array_list_init_static_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/array_list.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_array_list_init_static_harness() {
     struct aws_array_list *list;

diff --git a/.cbmc-batch/jobs/aws_array_list_push_back/Makefile b/.cbmc-batch/jobs/aws_array_list_push_back/Makefile
@@ -14,18 +14,18 @@
 ###########
 #NOTE: If we don't use the unwindset, leave it empty
 CBMC_UNWINDSET = --unwindset
-CBMC_UNWINDSET += __builtin___memcpy_chk.0:33,
+CBMC_UNWINDSET += __builtin___memcpy_chk.0:5,
 CBMC_UNWINDSET := $(CBMC_UNWINDSET)aws_mem_release:1,
-CBMC_UNWINDSET := $(CBMC_UNWINDSET)memcpy.0:33,
-CBMC_UNWINDSET := $(CBMC_UNWINDSET)strlen.0:33
+CBMC_UNWINDSET := $(CBMC_UNWINDSET)memcpy.0:5,
+CBMC_UNWINDSET := $(CBMC_UNWINDSET)strlen.0:5
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
-	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c \
-	       $(HELPERDIR)/patches/string.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(HELPERDIR)/stubs/memcpy_override.c \
+	       $(SRCDIR)/source/array_list.c \
+       	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_array_list_push_back_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_array_list_push_back/aws_array_list_push_back_harness.c b/.cbmc-batch/jobs/aws_array_list_push_back/aws_array_list_push_back_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/array_list.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_array_list_push_back_harness() {
     size_t item_count = nondet_size_t();

diff --git a/.cbmc-batch/jobs/aws_array_list_push_back/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_array_list_push_back/cbmc-batch.yaml
@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--pointer-check;--function;aws_array_list_push_back_harness;--unwindset;strlen.0:33,memcpy.0:33,__builtin___memcpy_chk.0:33,aws_mem_release:1;--unwinding-assertions"
+cbmcflags: "--bounds-check;--pointer-check;--function;aws_array_list_push_back_harness;--unwindset;strlen.0:5,memcpy.0:5,__builtin___memcpy_chk.0:5,aws_mem_release:1;--unwinding-assertions"
 goto: aws_array_list_push_back_harness.goto
 expected: "SUCCESSFUL"
diff --git a/.cbmc-batch/jobs/aws_array_list_set_at/Makefile b/.cbmc-batch/jobs/aws_array_list_set_at/Makefile
@@ -14,18 +14,18 @@
 ###########
 #NOTE: If we don't use the unwindset, leave it empty
 CBMC_UNWINDSET = --unwindset
-CBMC_UNWINDSET += __builtin___memcpy_chk.0:33,
+CBMC_UNWINDSET += __builtin___memcpy_chk.0:5,
 CBMC_UNWINDSET := $(CBMC_UNWINDSET)aws_mem_release:1,
-CBMC_UNWINDSET := $(CBMC_UNWINDSET)memcpy.0:33,
-CBMC_UNWINDSET := $(CBMC_UNWINDSET)strlen.0:33
+CBMC_UNWINDSET := $(CBMC_UNWINDSET)memcpy.0:5,
+CBMC_UNWINDSET := $(CBMC_UNWINDSET)strlen.0:5
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
-	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c \
-	       $(HELPERDIR)/patches/string.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(HELPERDIR)/stubs/memcpy_override.c \
+	       $(SRCDIR)/source/array_list.c \
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_array_list_set_at_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_array_list_set_at/aws_array_list_set_at_harness.c b/.cbmc-batch/jobs/aws_array_list_set_at/aws_array_list_set_at_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/array_list.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_array_list_set_at_harness() {
     size_t initial_item_allocation = nondet_size_t();

diff --git a/.cbmc-batch/jobs/aws_array_list_set_at/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_array_list_set_at/cbmc-batch.yaml
@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--pointer-check;--function;aws_array_list_set_at_harness;--unwindset;strlen.0:33,memcpy.0:33,__builtin___memcpy_chk.0:33,aws_mem_release:1;--unwinding-assertions"
+cbmcflags: "--bounds-check;--pointer-check;--function;aws_array_list_set_at_harness;--unwindset;strlen.0:5,memcpy.0:5,__builtin___memcpy_chk.0:5,aws_mem_release:1;--unwinding-assertions"
 goto: aws_array_list_set_at_harness.goto
 expected: "SUCCESSFUL"
diff --git a/.cbmc-batch/jobs/aws_byte_buf_append/Makefile b/.cbmc-batch/jobs/aws_byte_buf_append/Makefile
@@ -19,11 +19,11 @@ CBMC_UNWINDSET := $(CBMC_UNWINDSET)memcpy.0:33
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(HELPERDIR)/stubs/memcpy_override.c \
 	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c \
-	       $(HELPERDIR)/patches/string.c
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_byte_buf_append_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c b/.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/byte_buf.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_byte_buf_append_harness() {
     size_t len1 = nondet_size_t();

diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/Makefile b/.cbmc-batch/jobs/aws_byte_buf_from_c_str/Makefile
@@ -18,10 +18,10 @@ CBMC_UNWINDSET += strlen.0:33
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
 	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_byte_buf_from_c_str_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/aws_byte_buf_from_c_str_harness.c b/.cbmc-batch/jobs/aws_byte_buf_from_c_str/aws_byte_buf_from_c_str_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/byte_buf.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_byte_buf_from_c_str_harness() {
     size_t len = nondet_size_t();

diff --git a/.cbmc-batch/jobs/aws_byte_buf_init/Makefile b/.cbmc-batch/jobs/aws_byte_buf_init/Makefile
@@ -17,10 +17,10 @@
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/array_list.c \
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
 	       $(SRCDIR)/source/byte_buf.c \
-	       $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_byte_buf_init_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_byte_buf_init/aws_byte_buf_init_harness.c b/.cbmc-batch/jobs/aws_byte_buf_init/aws_byte_buf_init_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/byte_buf.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 void aws_byte_buf_init_harness() {
     struct aws_allocator *allocator;

diff --git a/.cbmc-batch/jobs/aws_mul_size_checked/Makefile b/.cbmc-batch/jobs/aws_mul_size_checked/Makefile
@@ -15,10 +15,11 @@
 #NOTE: If we don't use the unwindset, leave it empty
 #CBMC_UNWINDSET = --unwindset
 
-CBMCFLAGS += 
+CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+  	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_mul_size_checked_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_mul_size_checked/aws_mul_size_checked_harness.c b/.cbmc-batch/jobs/aws_mul_size_checked/aws_mul_size_checked_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/math.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 /**
  * Multiplies a * b and returns the result in *r. If the result

diff --git a/.cbmc-batch/jobs/aws_mul_size_saturating/Makefile b/.cbmc-batch/jobs/aws_mul_size_saturating/Makefile
@@ -17,8 +17,9 @@
 
 CBMCFLAGS +=
 
-DEPENDENCIES = $(SRCDIR)/source/common.c \
-	       $(SRCDIR)/source/error.c
+DEPENDENCIES =  $(HELPERDIR)/source/make_common_data_structures.c \
+		   $(HELPERDIR)/stubs/error.c \
+	       $(SRCDIR)/source/common.c
 
 ENTRY = aws_mul_size_saturating_harness
 ###########

diff --git a/.cbmc-batch/jobs/aws_mul_size_saturating/aws_mul_size_saturating_harness.c b/.cbmc-batch/jobs/aws_mul_size_saturating/aws_mul_size_saturating_harness.c
@@ -1,5 +1,5 @@
 #include <aws/common/math.h>
-#include <proof_helpers.h>
+#include <proof_helpers/make_common_data_structures.h>
 
 /**
  * Multiplies a * b. If the result overflows, returns 2^64 - 1.