From 503516ea02808a7c61468092cbcdfa63d4474246 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Fri, 5 Apr 2019 13:21:19 -0400 Subject: [PATCH 1/2] new memset and memcpy functions that are often faster for CBMC to analyze --- .cbmc-batch/jobs/memcpy_using_uint64/Makefile | 29 +++++++ .../jobs/memcpy_using_uint64/cbmc-batch.yaml | 4 + .../memcpy_using_uint64_harness.c | 40 +++++++++ .cbmc-batch/jobs/memset_override_0/Makefile | 29 +++++++ .../jobs/memset_override_0/cbmc-batch.yaml | 4 + .../memset_override_0_harness.c | 47 +++++++++++ .cbmc-batch/jobs/memset_using_uint64/Makefile | 29 +++++++ .../jobs/memset_using_uint64/cbmc-batch.yaml | 4 + .../memset_using_uint64_harness.c | 44 ++++++++++ .cbmc-batch/stubs/memcpy_using_uint64.c | 81 ++++++++++++++++++ .cbmc-batch/stubs/memset_override_0.c | 52 ++++++++++++ .cbmc-batch/stubs/memset_using_uint64.c | 83 +++++++++++++++++++ 12 files changed, 446 insertions(+) create mode 100644 .cbmc-batch/jobs/memcpy_using_uint64/Makefile create mode 100644 .cbmc-batch/jobs/memcpy_using_uint64/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c create mode 100644 .cbmc-batch/jobs/memset_override_0/Makefile create mode 100644 .cbmc-batch/jobs/memset_override_0/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c create mode 100644 .cbmc-batch/jobs/memset_using_uint64/Makefile create mode 100644 .cbmc-batch/jobs/memset_using_uint64/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c create mode 100644 .cbmc-batch/stubs/memcpy_using_uint64.c create mode 100644 .cbmc-batch/stubs/memset_override_0.c create mode 100644 .cbmc-batch/stubs/memset_using_uint64.c diff --git a/.cbmc-batch/jobs/memcpy_using_uint64/Makefile b/.cbmc-batch/jobs/memcpy_using_uint64/Makefile new file mode 100644 index 000000000..e32491578 --- /dev/null +++ b/.cbmc-batch/jobs/memcpy_using_uint64/Makefile @@ -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. + +########### +#NOTE: If we don't use the unwindset, leave it empty +UNWINDSET += memcpy_impl.0:161 +UNWINDSET += memcpy_using_uint64_impl.0:21 + +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 diff --git a/.cbmc-batch/jobs/memcpy_using_uint64/cbmc-batch.yaml b/.cbmc-batch/jobs/memcpy_using_uint64/cbmc-batch.yaml new file mode 100644 index 000000000..2eda0a802 --- /dev/null +++ b/.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" diff --git a/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c b/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c new file mode 100644 index 000000000..65605a11c --- /dev/null +++ b/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_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 +#include + +void *memcpy_impl(void *dst, const void *src, size_t n); +void *memcpy_using_uint64_impl(void *dst, const void *src, size_t n); + +const int MAX = 160; +/* + * Check that the optimized version of memcpy is memory safe + * And that it matches the naive version + * Coverage 100% + * Runtime: 40 seconds + */ + +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); +} diff --git a/.cbmc-batch/jobs/memset_override_0/Makefile b/.cbmc-batch/jobs/memset_override_0/Makefile new file mode 100644 index 000000000..74b969322 --- /dev/null +++ b/.cbmc-batch/jobs/memset_override_0/Makefile @@ -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. + +########### +#NOTE: If we don't use the unwindset, leave it empty +UNWINDSET += memset_impl.0:161 +UNWINDSET += memset_override_0_impl.0:21 + +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 diff --git a/.cbmc-batch/jobs/memset_override_0/cbmc-batch.yaml b/.cbmc-batch/jobs/memset_override_0/cbmc-batch.yaml new file mode 100644 index 000000000..6c9068ad5 --- /dev/null +++ b/.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" diff --git a/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c b/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c new file mode 100644 index 000000000..4b0aa496e --- /dev/null +++ b/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c @@ -0,0 +1,47 @@ +/* + * 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 + +/** + * Coverage: 100% + * Runtime: 50 Seconds + */ + +void *memset_impl(void *dst, int c, size_t n); +void *memset_override_0_impl(void *dst, int c, size_t n); + +const int MAX = 160; + +/* + * 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); +} diff --git a/.cbmc-batch/jobs/memset_using_uint64/Makefile b/.cbmc-batch/jobs/memset_using_uint64/Makefile new file mode 100644 index 000000000..a9dbecc3f --- /dev/null +++ b/.cbmc-batch/jobs/memset_using_uint64/Makefile @@ -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. + +########### +#NOTE: If we don't use the unwindset, leave it empty +UNWINDSET += memset_impl.0:161 +UNWINDSET += memset_using_uint64_impl.0:21 + +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 diff --git a/.cbmc-batch/jobs/memset_using_uint64/cbmc-batch.yaml b/.cbmc-batch/jobs/memset_using_uint64/cbmc-batch.yaml new file mode 100644 index 000000000..01fec1bfb --- /dev/null +++ b/.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" diff --git a/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c b/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c new file mode 100644 index 000000000..1e07c3b77 --- /dev/null +++ b/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_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 + +/** + * Coverage: 100% + * Runtime: 50 seconds + */ + +void *memset_impl(void *dst, int c, size_t n); +void *memset_using_uint64_impl(void *dst, int c, size_t n); + +const int MAX = 160; + +/* + * 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); +} diff --git a/.cbmc-batch/stubs/memcpy_using_uint64.c b/.cbmc-batch/stubs/memcpy_using_uint64.c new file mode 100644 index 000000000..afbce0ca7 --- /dev/null +++ b/.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 +#include + +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); +} diff --git a/.cbmc-batch/stubs/memset_override_0.c b/.cbmc-batch/stubs/memset_override_0.c new file mode 100644 index 000000000..40f880eca --- /dev/null +++ b/.cbmc-batch/stubs/memset_override_0.c @@ -0,0 +1,52 @@ +/* + * 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: memset + * + * Override the version of memset used by CBMC. + * 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 +#include + +void *memset_override_0_impl(void *dst, int c, size_t n) { + __CPROVER_precondition(__CPROVER_w_ok(dst, n), "memset destination region writeable"); + + assert(c == 0); + size_t num_uint64s = n >> 3; + size_t rem = n & 0x7; + assert(rem == 0); + + uint64_t *d = (uint64_t *)dst; + + for (size_t i = 0; i < num_uint64s; ++i) { + d[i] = 0; + } + + return dst; +} + +void *memset(void *s, int c, size_t n) { + return memset_override_0_impl(s, c, n); +} + +void *__builtin___memset_chk(void *s, int c, size_t n, size_t os) { + (void)os; + return memset_override_0_impl(s, c, n); +} diff --git a/.cbmc-batch/stubs/memset_using_uint64.c b/.cbmc-batch/stubs/memset_using_uint64.c new file mode 100644 index 000000000..2a888f9c7 --- /dev/null +++ b/.cbmc-batch/stubs/memset_using_uint64.c @@ -0,0 +1,83 @@ +/* + * 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: memset + * + * Override the version of memset used by CBMC. + * 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 +#include + +void *memset_using_uint64_impl(void *dst, int c, size_t n) { + __CPROVER_precondition(__CPROVER_w_ok(dst, n), "memset destination region writeable"); + + size_t num_uint64s = n >> 3; + size_t rem = n & 0x7; + + uint8_t *d = (uint8_t *)dst; + + // Use fallthrough to unroll the remainder loop + switch (rem) { + case 7: + d[6] = c; + case 6: + d[5] = c; + case 5: + d[4] = c; + case 4: + d[3] = c; + case 3: + d[2] = c; + case 2: + d[1] = c; + case 1: + d[0] = c; + } + + d += rem; + + uint64_t compounded = 0; + if (num_uint64s > 0 && c != 0) { + uint8_t *chars = (uint8_t *)&compounded; + chars[0] = c; + chars[1] = c; + chars[2] = c; + chars[3] = c; + chars[4] = c; + chars[5] = c; + chars[6] = c; + chars[7] = c; + } + + for (size_t i = 0; i < num_uint64s; ++i) { + ((uint64_t *)d)[i] = compounded; + } + + return dst; +} + +void *memset(void *s, int c, size_t n) { + return memset_using_uint64_impl(s, c, n); +} + +void *__builtin___memset_chk(void *s, int c, size_t n, size_t os) { + (void)os; + return memset_using_uint64_impl(s, c, n); +} From 76038900e41f384b414739b9a15a1c87e1c2fb00 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Tue, 9 Apr 2019 15:40:25 -0400 Subject: [PATCH 2/2] PR comments addressed --- .cbmc-batch/jobs/memcpy_using_uint64/Makefile | 10 +++++++--- .../memcpy_using_uint64/memcpy_using_uint64_harness.c | 4 ---- .cbmc-batch/jobs/memset_override_0/Makefile | 10 +++++++--- .../jobs/memset_override_0/memset_override_0_harness.c | 7 ------- .cbmc-batch/jobs/memset_using_uint64/Makefile | 9 ++++++--- .../memset_using_uint64/memset_using_uint64_harness.c | 7 ------- .cbmc-batch/stubs/memcpy_using_uint64.c | 2 +- 7 files changed, 21 insertions(+), 28 deletions(-) diff --git a/.cbmc-batch/jobs/memcpy_using_uint64/Makefile b/.cbmc-batch/jobs/memcpy_using_uint64/Makefile index e32491578..dc8f6caba 100644 --- a/.cbmc-batch/jobs/memcpy_using_uint64/Makefile +++ b/.cbmc-batch/jobs/memcpy_using_uint64/Makefile @@ -12,9 +12,13 @@ # limitations under the License. ########### -#NOTE: If we don't use the unwindset, leave it empty -UNWINDSET += memcpy_impl.0:161 -UNWINDSET += memcpy_using_uint64_impl.0:21 +# 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 += diff --git a/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c b/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c index 65605a11c..ead3ba243 100644 --- a/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c +++ b/.cbmc-batch/jobs/memcpy_using_uint64/memcpy_using_uint64_harness.c @@ -19,14 +19,10 @@ void *memcpy_impl(void *dst, const void *src, size_t n); void *memcpy_using_uint64_impl(void *dst, const void *src, size_t n); -const int MAX = 160; /* * Check that the optimized version of memcpy is memory safe * And that it matches the naive version - * Coverage 100% - * Runtime: 40 seconds */ - void memcpy_using_uint64_harness() { char s[MAX]; char d1[MAX]; diff --git a/.cbmc-batch/jobs/memset_override_0/Makefile b/.cbmc-batch/jobs/memset_override_0/Makefile index 74b969322..83dfd166d 100644 --- a/.cbmc-batch/jobs/memset_override_0/Makefile +++ b/.cbmc-batch/jobs/memset_override_0/Makefile @@ -12,9 +12,13 @@ # limitations under the License. ########### -#NOTE: If we don't use the unwindset, leave it empty -UNWINDSET += memset_impl.0:161 -UNWINDSET += memset_override_0_impl.0:21 +# 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 += diff --git a/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c b/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c index 4b0aa496e..adebc2ab9 100644 --- a/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c +++ b/.cbmc-batch/jobs/memset_override_0/memset_override_0_harness.c @@ -16,16 +16,9 @@ #include #include -/** - * Coverage: 100% - * Runtime: 50 Seconds - */ - void *memset_impl(void *dst, int c, size_t n); void *memset_override_0_impl(void *dst, int c, size_t n); -const int MAX = 160; - /* * Check that the optimized version of memset is memory safe * And that it matches the naive version diff --git a/.cbmc-batch/jobs/memset_using_uint64/Makefile b/.cbmc-batch/jobs/memset_using_uint64/Makefile index a9dbecc3f..b1f1cbde6 100644 --- a/.cbmc-batch/jobs/memset_using_uint64/Makefile +++ b/.cbmc-batch/jobs/memset_using_uint64/Makefile @@ -12,9 +12,12 @@ # limitations under the License. ########### -#NOTE: If we don't use the unwindset, leave it empty -UNWINDSET += memset_impl.0:161 -UNWINDSET += memset_using_uint64_impl.0:21 +# 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 += diff --git a/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c b/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c index 1e07c3b77..1d2a1d636 100644 --- a/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c +++ b/.cbmc-batch/jobs/memset_using_uint64/memset_using_uint64_harness.c @@ -16,16 +16,9 @@ #include #include -/** - * Coverage: 100% - * Runtime: 50 seconds - */ - void *memset_impl(void *dst, int c, size_t n); void *memset_using_uint64_impl(void *dst, int c, size_t n); -const int MAX = 160; - /* * Check that the optimized version of memset is memory safe * And that it matches the naive version diff --git a/.cbmc-batch/stubs/memcpy_using_uint64.c b/.cbmc-batch/stubs/memcpy_using_uint64.c index afbce0ca7..63a7ece6d 100644 --- a/.cbmc-batch/stubs/memcpy_using_uint64.c +++ b/.cbmc-batch/stubs/memcpy_using_uint64.c @@ -19,7 +19,7 @@ * 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.] + * *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.