Temporarily disable the __CPROVER_{r,w}_ok macros (#600)

karkhaz · danielsn · web-flow · commit a4703488280a · 2020-03-11T10:31:41.000-07:00
* Temporarily disable the __CPROVER_{r,w}_ok macros This is while we work to resolve an issue with CBMC, described at diffblue/cbmc#5194 * fix aws_array_list_back * fix aws_array_list_front * fix aws_array_list_get_at * fix aws_byte_cursor_read_u8 proof * fix CBMC proof for aws_array_list_set_at * fix aws_byte_buf_write_from_whole_cursor CBMC proof, and minor issue in aws_byte_buf_write * fix CBMC proof for aws_array_list_push_back * fix byte_cursor read proofs Co-authored-by: Daniel Schwartz-Narbonne <dsn@amazon.com>
diff --git a/.cbmc-batch/include/proof_helpers/aws_byte_cursor_read_common.h b/.cbmc-batch/include/proof_helpers/aws_byte_cursor_read_common.h
@@ -20,14 +20,14 @@
 void aws_byte_cursor_read_common_harness() {
     /* parameters */
     struct aws_byte_cursor cur;
-    size_t length;
-    DEST_TYPE *dest = can_fail_malloc(length);
+    DEST_TYPE *dest = can_fail_malloc(sizeof(*dest));
 
     /* assumptions */
     ensure_byte_cursor_has_allocated_buffer_member(&cur);
     __CPROVER_assume(aws_byte_cursor_is_valid(&cur));
+    __CPROVER_assume(cur.len >= BYTE_WIDTH);
     __CPROVER_assume(AWS_MEM_IS_READABLE(cur.ptr, BYTE_WIDTH));
-    __CPROVER_assume(AWS_OBJECT_PTR_IS_WRITABLE(dest));
+    __CPROVER_assume(dest != NULL);
 
     /* save current state of the data structure */
     struct aws_byte_cursor old_cur = cur;
diff --git a/.cbmc-batch/jobs/aws_array_list_back/Makefile b/.cbmc-batch/jobs/aws_array_list_back/Makefile
@@ -23,7 +23,6 @@ DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
-DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
 DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 
diff --git a/.cbmc-batch/jobs/aws_array_list_back/aws_array_list_back_harness.c b/.cbmc-batch/jobs/aws_array_list_back/aws_array_list_back_harness.c
@@ -23,14 +23,12 @@ void aws_array_list_back_harness() {
 
     /* data structure */
     struct aws_array_list list;
+    void *val = can_fail_malloc(list.item_size);
 
     /* assumptions */
     __CPROVER_assume(aws_array_list_is_bounded(&list, MAX_INITIAL_ITEM_ALLOCATION, MAX_ITEM_SIZE));
     ensure_array_list_has_allocated_data_member(&list);
     __CPROVER_assume(aws_array_list_is_valid(&list));
-    size_t malloc_size;
-    __CPROVER_assume(malloc_size <= list.item_size);
-    void *val = can_fail_malloc(malloc_size);
 
     /* save current state of the data structure */
     struct aws_array_list old = list;
diff --git a/.cbmc-batch/jobs/aws_array_list_back/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_array_list_back/cbmc-batch.yaml
@@ -1,4 +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:3;--object-bits;8"
-goto: aws_array_list_back_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_array_list_back_harness.goto
+jobos: ubuntu16
diff --git a/.cbmc-batch/jobs/aws_array_list_front/Makefile b/.cbmc-batch/jobs/aws_array_list_front/Makefile
@@ -26,7 +26,6 @@ DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
-DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
 DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 
diff --git a/.cbmc-batch/jobs/aws_array_list_front/aws_array_list_front_harness.c b/.cbmc-batch/jobs/aws_array_list_front/aws_array_list_front_harness.c
@@ -27,9 +27,7 @@ void aws_array_list_front_harness() {
     __CPROVER_assume(aws_array_list_is_bounded(&list, MAX_INITIAL_ITEM_ALLOCATION, MAX_ITEM_SIZE));
     ensure_array_list_has_allocated_data_member(&list);
     __CPROVER_assume(aws_array_list_is_valid(&list));
-    size_t malloc_size;
-    __CPROVER_assume(malloc_size <= list.item_size);
-    void *val = can_fail_malloc(malloc_size);
+    void *val = can_fail_malloc(list.item_size);
 
     /* save current state of the data structure */
     struct aws_array_list old = list;
diff --git a/.cbmc-batch/jobs/aws_array_list_front/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_array_list_front/cbmc-batch.yaml
@@ -1,4 +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:3;--object-bits;8"
-goto: aws_array_list_front_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_array_list_front_harness.goto
+jobos: ubuntu16
diff --git a/.cbmc-batch/jobs/aws_array_list_get_at/Makefile b/.cbmc-batch/jobs/aws_array_list_get_at/Makefile
@@ -23,7 +23,6 @@ DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
-DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
 DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 
diff --git a/.cbmc-batch/jobs/aws_array_list_get_at/aws_array_list_get_at_harness.c b/.cbmc-batch/jobs/aws_array_list_get_at/aws_array_list_get_at_harness.c
@@ -27,9 +27,7 @@ void aws_array_list_get_at_harness() {
     __CPROVER_assume(aws_array_list_is_bounded(&list, MAX_INITIAL_ITEM_ALLOCATION, MAX_ITEM_SIZE));
     ensure_array_list_has_allocated_data_member(&list);
     __CPROVER_assume(aws_array_list_is_valid(&list));
-    size_t malloc_size;
-    __CPROVER_assume(malloc_size <= list.item_size);
-    void *val = can_fail_malloc(malloc_size);
+    void *val = can_fail_malloc(list.item_size);
     size_t index;
 
     /* save current state of the data structure */
diff --git a/.cbmc-batch/jobs/aws_array_list_get_at/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_array_list_get_at/cbmc-batch.yaml
@@ -1,4 +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:3;--object-bits;8"
-goto: aws_array_list_get_at_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_array_list_get_at_harness.goto
+jobos: ubuntu16
diff --git a/.cbmc-batch/jobs/aws_array_list_push_back/Makefile b/.cbmc-batch/jobs/aws_array_list_push_back/Makefile
@@ -22,7 +22,6 @@ DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
-DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
 DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 
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
@@ -17,7 +17,7 @@
 #include <proof_helpers/make_common_data_structures.h>
 
 /**
- * Runtime: 18s
+ * Runtime: 4 min
  */
 void aws_array_list_push_back_harness() {
     /* data structure */
@@ -28,9 +28,7 @@ void aws_array_list_push_back_harness() {
     ensure_array_list_has_allocated_data_member(&list);
     __CPROVER_assume(aws_array_list_is_valid(&list));
     __CPROVER_assume(list.data != NULL);
-    size_t malloc_size;
-    __CPROVER_assume(malloc_size <= list.item_size);
-    void *val = can_fail_malloc(malloc_size);
+    void *val = can_fail_malloc(list.item_size);
 
     /* save current state of the data structure */
     struct aws_array_list old = list;
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;--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;--object-bits;8"
-goto: aws_array_list_push_back_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_array_list_push_back_harness.goto
+jobos: ubuntu16
diff --git a/.cbmc-batch/jobs/aws_array_list_set_at/Makefile b/.cbmc-batch/jobs/aws_array_list_set_at/Makefile
@@ -22,7 +22,6 @@ DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
-DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
 DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 
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
@@ -17,7 +17,7 @@
 #include <proof_helpers/make_common_data_structures.h>
 
 /**
- * Runtime: 20s
+ * Runtime: 3m 42s
  */
 void aws_array_list_set_at_harness() {
     /* data structure */
@@ -29,8 +29,7 @@ void aws_array_list_set_at_harness() {
     __CPROVER_assume(aws_array_list_is_valid(&list));
     __CPROVER_assume(list.data != NULL);
     size_t malloc_size;
-    __CPROVER_assume(malloc_size <= list.item_size);
-    void *val = can_fail_malloc(malloc_size);
+    void *val = can_fail_malloc(list.item_size);
     size_t index;
 
     /* save current state of the data structure */
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;--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;--object-bits;8"
-goto: aws_array_list_set_at_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_array_list_set_at_harness.goto
+jobos: ubuntu16
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
@@ -22,7 +22,6 @@ 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
 
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
@@ -28,7 +28,6 @@ void aws_byte_buf_write_from_whole_cursor_harness() {
     __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));
-    __CPROVER_assume(AWS_MEM_IS_WRITABLE(src.ptr, src.len));
 
     /* save current state of the parameters */
     struct aws_byte_buf buf_old = buf;
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
@@ -1,4 +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"
+goto: aws_byte_buf_write_from_whole_cursor_harness.goto
+jobos: ubuntu16
diff --git a/.cbmc-batch/jobs/aws_byte_cursor_read_be16/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_cursor_read_be16/cbmc-batch.yaml
@@ -1,4 +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;--object-bits;8"
-goto: aws_byte_cursor_read_be16_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_byte_cursor_read_be16_harness.goto
+jobos: ubuntu16
diff --git a/.cbmc-batch/jobs/aws_byte_cursor_read_u8/aws_byte_cursor_read_u8_harness.c b/.cbmc-batch/jobs/aws_byte_cursor_read_u8/aws_byte_cursor_read_u8_harness.c
@@ -21,6 +21,7 @@ void aws_byte_cursor_read_u8_harness() {
     /* parameters */
     struct aws_byte_cursor cur;
     size_t length;
+    __CPROVER_assume(length >=1);
     uint8_t *dest = bounded_malloc(length);
 
     /* assumptions */
diff --git a/.cbmc-batch/jobs/aws_byte_cursor_read_u8/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_cursor_read_u8/cbmc-batch.yaml
@@ -1,4 +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;--object-bits;8"
-goto: aws_byte_cursor_read_u8_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_byte_cursor_read_u8_harness.goto
+jobos: ubuntu16
diff --git a/include/aws/common/assert.h b/include/aws/common/assert.h
@@ -96,8 +96,6 @@ AWS_EXTERN_C_END
 #    define AWS_POSTCONDITION1(cond) __CPROVER_assert((cond), #    cond " check failed")
 #    define AWS_FATAL_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation))
 #    define AWS_FATAL_POSTCONDITION1(cond) __CPROVER_assert((cond), #    cond " check failed")
-#    define AWS_MEM_IS_READABLE(base, len) __CPROVER_r_ok((base), (len))
-#    define AWS_MEM_IS_WRITABLE(base, len) __CPROVER_w_ok((base), (len))
 #else
 #    define AWS_PRECONDITION2(cond, expl) AWS_ASSERT(cond)
 #    define AWS_PRECONDITION1(cond) AWS_ASSERT(cond)
@@ -107,12 +105,17 @@ AWS_EXTERN_C_END
 #    define AWS_POSTCONDITION1(cond) AWS_ASSERT(cond)
 #    define AWS_FATAL_POSTCONDITION2(cond, expl) AWS_FATAL_ASSERT(cond)
 #    define AWS_FATAL_POSTCONDITION1(cond) AWS_FATAL_ASSERT(cond)
+#endif /* CBMC */
 
 /* the C runtime does not give a way to check these properties,
- * but we can at least check that the pointer is valid */
-#    define AWS_MEM_IS_READABLE(base, len) (((len) == 0) || (base))
-#    define AWS_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base))
-#endif /* CBMC */
+ * but we can at least check that the pointer is valid.
+ * these macros are intended to be used with CBMC proofs, but will not use CBMC
+ * intrinsics until https://github.com/diffblue/cbmc/issues/5194 is fixed.*/
+#define AWS_MEM_IS_READABLE(base, len) (((len) == 0) || (base))
+#define AWS_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base))
+
+#define __CPROVER_r_ok(base, len) (AWS_MEM_IS_READABLE(base, len))
+#define __CPROVER_w_ok(base, len) (AWS_MEM_IS_WRITEABLE(base, len))
 
 #define AWS_RETURN_ERROR_IF_IMPL(type, cond, err, explanation)                                                         \
     do {                                                                                                               \
diff --git a/source/byte_buf.c b/source/byte_buf.c
@@ -1080,6 +1080,7 @@ bool aws_byte_cursor_read_and_fill_buffer(
  */
 bool aws_byte_cursor_read_u8(struct aws_byte_cursor *AWS_RESTRICT cur, uint8_t *AWS_RESTRICT var) {
     AWS_PRECONDITION(aws_byte_cursor_is_valid(cur));
+    AWS_PRECONDITION(AWS_MEM_IS_WRITABLE(var, 1));
     bool rv = aws_byte_cursor_read(cur, var, 1);
     AWS_POSTCONDITION(aws_byte_cursor_is_valid(cur));
     return rv;
@@ -1262,6 +1263,11 @@ bool aws_byte_buf_write(struct aws_byte_buf *AWS_RESTRICT buf, const uint8_t *AW
     AWS_PRECONDITION(aws_byte_buf_is_valid(buf));
     AWS_PRECONDITION(AWS_MEM_IS_READABLE(src, len), "Input array [src] must be readable up to [len] bytes.");
 
+    if (len == 0) {
+	AWS_POSTCONDITION(aws_byte_buf_is_valid(buf));
+	return true;
+    }
+
     if (buf->len > (SIZE_MAX >> 1) || len > (SIZE_MAX >> 1) || buf->len + len > buf->capacity) {
         AWS_POSTCONDITION(aws_byte_buf_is_valid(buf));
         return false;
