Faster CBMC stubs for memset and memcpy (#300)

* new memset and memcpy functions that are often faster for CBMC to analyze

* PR comments addressed

Author: danielsn

.cbmc-batch/jobs/memcpy_using_uint64/Makefile

@@ -0,0 +1,33 @@
+# 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.
+
+###########
+# Max needs to be big enough to have multiple loop unrollings to have full coverage
+# 160 is well larger than that, and still completes quite fast: ~ 40s
+MAX = 160
+DEFINES += -DMAX=$(MAX)
+
+UNWINDSET += memcpy_impl.0:$(shell echo $$(($(MAX) + 1)))
+UNWINDSET += memcpy_using_uint64_impl.0:$(shell echo $$(( $$(( $(MAX) / 8 )) + 1)))
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_using_uint64.c
+
+ENTRY = memcpy_using_uint64_harness
+
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/memcpy_using_uint64/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:161,memcpy_using_uint64_impl.0:21"
+goto: memcpy_using_uint64_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c

@@ -0,0 +1,36 @@
+/*
+ * 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 <proof_helpers/utils.h>
+#include <stddef.h>
+
+void *memcpy_impl(void *dst, const void *src, size_t n);
+void *memcpy_using_uint64_impl(void *dst, const void *src, size_t n);
+
+/*
+ * Check that the optimized version of memcpy is memory safe
+ * And that it matches the naive version
+ */
+void memcpy_using_uint64_harness() {
+    char s[MAX];
+    char d1[MAX];
+    char d2[MAX];
+
+    unsigned size;
+    __CPROVER_assume(size < MAX);
+    memcpy_impl(d1, s, size);
+    memcpy_using_uint64_impl(d2, s, size);
+    assert_bytes_match(d1, d2, size);
+}

.cbmc-batch/jobs/memset_override_0/Makefile

@@ -0,0 +1,33 @@
+# 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.
+
+###########
+# Max needs to be big enough to have multiple loop unrollings to have full coverage
+# 160 is well larger than that, and still completes quite fast: ~ 40s
+MAX = 160
+DEFINES += -DMAX=$(MAX)
+
+UNWINDSET += memset_impl.0:$(shell echo $$(($(MAX) + 1)))
+UNWINDSET += memset_override_0_impl.0:$(shell echo $$(( $$(( $(MAX) / 8 )) + 1)))
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memset_override.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memset_override_0.c
+
+ENTRY = memset_override_0_harness
+
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/memset_override_0/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;memset_impl.0:161,memset_override_0_impl.0:21"
+goto: memset_override_0_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c

@@ -0,0 +1,40 @@
+/*
+ * 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 <proof_helpers/utils.h>
+#include <stddef.h>
+
+void *memset_impl(void *dst, int c, size_t n);
+void *memset_override_0_impl(void *dst, int c, size_t n);
+
+/*
+ * Check that the optimized version of memset is memory safe
+ * And that it matches the naive version
+ */
+void memset_override_0_harness() {
+
+    short d1[MAX];
+    short d2[MAX];
+    int c;
+    __CPROVER_assume(c == 0); // asserted in the implementation
+
+    unsigned size;
+    __CPROVER_assume((size & 0x7) == 0); // asserted in the implementation
+    __CPROVER_assume(size < MAX);
+    memset_impl(d1, c, size);
+    memset_override_0_impl(d2, c, size);
+    assert_bytes_match(d1, d2, size);
+    assert_all_bytes_are(d2, c, size);
+}

.cbmc-batch/jobs/memset_using_uint64/Makefile

@@ -0,0 +1,32 @@
+# 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.
+
+###########
+# Max needs to be big enough to have multiple loop unrollings to have full coverage
+# 160 is well larger than that, and still completes quite fast: ~ 40s
+MAX = 160
+DEFINES += -DMAX=$(MAX)
+UNWINDSET += memset_impl.0:$(shell echo $$(($(MAX) + 1)))
+UNWINDSET += memset_using_uint64_impl.0:$(shell echo $$(( $$(( $(MAX) / 8 )) + 1)))
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memset_override.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memset_using_uint64.c
+
+ENTRY = memset_using_uint64_harness
+
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/memset_using_uint64/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;memset_impl.0:161,memset_using_uint64_impl.0:21"
+goto: memset_using_uint64_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c

@@ -0,0 +1,37 @@
+/*
+ * 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 <proof_helpers/utils.h>
+#include <stddef.h>
+
+void *memset_impl(void *dst, int c, size_t n);
+void *memset_using_uint64_impl(void *dst, int c, size_t n);
+
+/*
+ * Check that the optimized version of memset is memory safe
+ * And that it matches the naive version
+ */
+void memset_using_uint64_harness() {
+
+    short d1[MAX];
+    short d2[MAX];
+    int c;
+    unsigned size;
+    __CPROVER_assume(size < MAX);
+    memset_impl(d1, c, size);
+    memset_using_uint64_impl(d2, c, size);
+    assert_bytes_match(d1, d2, size);
+    assert_all_bytes_are(d2, c, size);
+}

.cbmc-batch/stubs/memcpy_using_uint64.c

@@ -0,0 +1,81 @@
+/*
+ * 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.
+ */
+
+/**
+ * FUNCTION: memcpy
+ *
+ * This function overrides the original implementation of the memcpy function
+ * from string.h. It copies the values of n bytes from the *src to the *dst.
+ * It also checks if the size of the arrays pointed to by both the *dst and
+ * *src parameters are at least n bytes and if they overlap.
+ *
+ * This takes advantage of the fact that 64bit operations require fewer array updates,
+ * which can make this version faster than the naive unrolling when used in CBMC.
+ * Benchmark your particular proof to know for sure.
+ */
+
+#include <stddef.h>
+#include <stdint.h>
+
+void *memcpy_using_uint64_impl(void *dst, const void *src, size_t n) {
+    __CPROVER_precondition(
+        __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+            ((const char *)src >= (const char *)dst + n) || ((const char *)dst >= (const char *)src + n),
+        "memcpy src/dst overlap");
+    __CPROVER_precondition(__CPROVER_r_ok(src, n), "memcpy source region readable");
+    __CPROVER_precondition(__CPROVER_w_ok(dst, n), "memcpy destination region writeable");
+
+    size_t num_uint64s = n >> 3;
+    size_t rem = n & 0x7;
+
+    uint8_t *d = (uint8_t *)dst;
+    const uint8_t *s = (const uint8_t *)src;
+
+    // Use fallthrough to unroll the remainder loop
+    switch (rem) {
+        case 7:
+            d[6] = s[6];
+        case 6:
+            d[5] = s[5];
+        case 5:
+            d[4] = s[4];
+        case 4:
+            d[3] = s[3];
+        case 3:
+            d[2] = s[2];
+        case 2:
+            d[1] = s[1];
+        case 1:
+            d[0] = s[0];
+    }
+
+    d += rem;
+    s += rem;
+
+    for (size_t i = 0; i < num_uint64s; ++i) {
+        ((uint64_t *)d)[i] = ((const uint64_t *)s)[i];
+    }
+
+    return dst;
+}
+
+void *memcpy(void *dst, const void *src, size_t n) {
+    return memcpy_using_uint64_impl(dst, src, n);
+}
+
+void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size) {
+    (void)size;
+    return memcpy_using_uint64_impl(dst, src, n);
+}