From e06926febbace08e311f666eb195ebe3a05a85b0 Mon Sep 17 00:00:00 2001 From: Akshay Utture Date: Thu, 28 Jul 2022 10:05:44 -0400 Subject: [PATCH 1/3] Added an FAQ about array theory in CBMC --- docs/src/SUMMARY.md | 3 ++- docs/src/faq/array-theory.md | 19 +++++++++++++++++++ 2 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 docs/src/faq/array-theory.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 3f50dec..0cfc957 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -27,6 +27,7 @@ * [How does malloc work?](faq/malloc.md) * [How do I write a good stub?]() * [What do I do when CBMC won't stop?](faq/termination.md) + * [Does CBMC have any support for using array-theory?](faq/array-theory.md) * [CBMC project management](management/README.md) * [Project planning](management/Plan-your-proof.md) @@ -37,4 +38,4 @@ * [CBMC projects](projects.md) -* [CBMC resources](resources.md) \ No newline at end of file +* [CBMC resources](resources.md) diff --git a/docs/src/faq/array-theory.md b/docs/src/faq/array-theory.md new file mode 100644 index 0000000..e110539 --- /dev/null +++ b/docs/src/faq/array-theory.md @@ -0,0 +1,19 @@ +# Does CBMC have any support for using array theory? + +CBMC provides support for reasoning about arrays using array theory. (Note that we are still working with a SAT back-end here, and this does not use an SMT solver) +A fixed length array uses CBMC's typical bit-vector representation of an array, but a variable length array uses CBMC's array theory. +To activate CBMC's array-theory for fixed length arrays, use the following workaround. + +``` +unsigned long size; // non deterministically pick the size +ArrayElement *a = malloc(size * sizeof(ArrayElement)); +__CPROVER_assume(size == MAX_SIZE); // fix the size to a constant after the allocation +``` +[See https://github.com/diffblue/cbmc/issues/7012 to read more about the workaround and track the fix] + +## Performance impact of using CBMC's array theory feature. + +CBMC’s array theory generates a number of constraints that is quadratic in the number of accesses to an array, and could be slower in cases with large number of accesses (worse for write accesses). However, unlike the bit-vector encoding, the number of constraints is not dependent on the size of the array itself. + +Hence, array theory is better when you have a small number of accesses with non-constant index into a very large array. An example of this is when you want to reason about a single insertion of an element at a non-constant index in a large array. + From fc7133fc287220e0bf4578adf04655bf010e20e0 Mon Sep 17 00:00:00 2001 From: Akshay Utture Date: Wed, 10 Aug 2022 17:34:50 -0400 Subject: [PATCH 2/3] Added an Advanced-Questions section and moved the array-theory page to that section --- docs/src/SUMMARY.md | 4 +++- docs/src/advanced-questions/README.md | 8 ++++++++ docs/src/{faq => advanced-questions}/array-theory.md | 0 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 docs/src/advanced-questions/README.md rename docs/src/{faq => advanced-questions}/array-theory.md (100%) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 0cfc957..271d6a0 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -27,7 +27,9 @@ * [How does malloc work?](faq/malloc.md) * [How do I write a good stub?]() * [What do I do when CBMC won't stop?](faq/termination.md) - * [Does CBMC have any support for using array-theory?](faq/array-theory.md) + +* [Advanced Questions](advanced-questions/README.md) + * [Does CBMC have any support for using array-theory?](advanced-questions/array-theory.md) * [CBMC project management](management/README.md) * [Project planning](management/Plan-your-proof.md) diff --git a/docs/src/advanced-questions/README.md b/docs/src/advanced-questions/README.md new file mode 100644 index 0000000..8f554cb --- /dev/null +++ b/docs/src/advanced-questions/README.md @@ -0,0 +1,8 @@ +# Advanced Questions (Infrequently asked questions) + +Here are answers to some questions asked by advanced CBMC users. +Please send us any questions you have by +[filing an issue with us](https://github.com/model-checking/cbmc-training/issues) +on GitHub. + +* [Does CBMC have any support for using array-theory?](array-theory.md) \ No newline at end of file diff --git a/docs/src/faq/array-theory.md b/docs/src/advanced-questions/array-theory.md similarity index 100% rename from docs/src/faq/array-theory.md rename to docs/src/advanced-questions/array-theory.md From 3a8d29c72dbfff5861ef8d5010bfeae17bac307c Mon Sep 17 00:00:00 2001 From: Akshay Utture Date: Wed, 10 Aug 2022 17:38:51 -0400 Subject: [PATCH 3/3] Added a date for the array-theory page --- docs/src/advanced-questions/array-theory.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/src/advanced-questions/array-theory.md b/docs/src/advanced-questions/array-theory.md index e110539..5033e3c 100644 --- a/docs/src/advanced-questions/array-theory.md +++ b/docs/src/advanced-questions/array-theory.md @@ -1,4 +1,5 @@ # Does CBMC have any support for using array theory? +[Article Date: Aug 10, 2022] CBMC provides support for reasoning about arrays using array theory. (Note that we are still working with a SAT back-end here, and this does not use an SMT solver) A fixed length array uses CBMC's typical bit-vector representation of an array, but a variable length array uses CBMC's array theory.