From 5a25a951ca3b9411aa1551f673b8225d89412b65 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Fri, 11 Jun 2021 19:14:05 +0100 Subject: [PATCH 1/5] Enable and use the automatic limit for array-as-uninterpreted-function This is a duplicate of PR #2108. This is here for alternative author management. Fixes #6130 --- src/solvers/flattening/boolbv.cpp | 8 +++----- src/solvers/flattening/boolbv.h | 2 +- src/solvers/flattening/boolbv_width.cpp | 12 +----------- 3 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 774218167dc..ed4a5084ee6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -539,14 +539,12 @@ bool boolbvt::is_unbounded_array(const typet &type) const if(unbounded_array==unbounded_arrayt::U_ALL) return true; - const exprt &size=to_array_type(type).size(); - - const auto s = numeric_cast(size); - if(!s.has_value()) + const std::size_t size = boolbv_width(type); + if(size == 0) return true; if(unbounded_array==unbounded_arrayt::U_AUTO) - if(*s > MAX_FLATTENED_ARRAY_SIZE) + if(size > MAX_FLATTENED_ARRAY_SIZE) return true; return false; diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 0104a04ba69..8bb00cb9cdd 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -47,7 +47,7 @@ class boolbvt:public arrayst message_handlert &message_handler, bool get_array_constraints = false) : arrayst(_ns, _prop, message_handler, get_array_constraints), - unbounded_array(unbounded_arrayt::U_NONE), + unbounded_array(unbounded_arrayt::U_AUTO), bv_width(_ns), bv_utils(_prop), functions(*this), diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 39e5439cf08..09d1c3d0946 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -136,13 +135,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const else { mp_integer total = *array_size * sub_width; - if(total>(1<<30)) // realistic limit - throw analysis_exceptiont("array too large for flattening"); - - if(total < 0) - entry.total_width = 0; - else - entry.total_width = numeric_cast_v(total); + entry.total_width = numeric_cast_v(total); } } else if(type_id==ID_vector) @@ -153,9 +146,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const const auto vector_size = numeric_cast_v(vector_type.size()); mp_integer total = vector_size * sub_width; - if(total > (1 << 30)) // realistic limit - throw analysis_exceptiont("vector too large for flattening"); - entry.total_width = numeric_cast_v(vector_size * sub_width); } else if(type_id==ID_complex) From e307538cb96ce5a7ad449378f22dbd8acc6dfa79 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Fri, 11 Jun 2021 19:14:05 +0100 Subject: [PATCH 2/5] Enable and use the automatic limit for array-as-uninterpreted-function This is a duplicate of PR #2108. This is here for alternative author management. Fixes #6130 --- src/solvers/flattening/boolbv.cpp | 8 +++----- src/solvers/flattening/boolbv.h | 2 +- src/solvers/flattening/boolbv_width.cpp | 12 +----------- 3 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index dce9c55f267..cb0c52ec8b4 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -539,14 +539,12 @@ bool boolbvt::is_unbounded_array(const typet &type) const if(unbounded_array==unbounded_arrayt::U_ALL) return true; - const exprt &size=to_array_type(type).size(); - - const auto s = numeric_cast(size); - if(!s.has_value()) + const std::size_t size = boolbv_width(type); + if(size == 0) return true; if(unbounded_array==unbounded_arrayt::U_AUTO) - if(*s > MAX_FLATTENED_ARRAY_SIZE) + if(size > MAX_FLATTENED_ARRAY_SIZE) return true; return false; diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index fc3b1484b96..3bda86f2cfa 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -47,7 +47,7 @@ class boolbvt:public arrayst message_handlert &message_handler, bool get_array_constraints = false) : arrayst(_ns, _prop, message_handler, get_array_constraints), - unbounded_array(unbounded_arrayt::U_NONE), + unbounded_array(unbounded_arrayt::U_AUTO), bv_width(_ns), bv_utils(_prop), functions(*this), diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 39e5439cf08..09d1c3d0946 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -136,13 +135,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const else { mp_integer total = *array_size * sub_width; - if(total>(1<<30)) // realistic limit - throw analysis_exceptiont("array too large for flattening"); - - if(total < 0) - entry.total_width = 0; - else - entry.total_width = numeric_cast_v(total); + entry.total_width = numeric_cast_v(total); } } else if(type_id==ID_vector) @@ -153,9 +146,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const const auto vector_size = numeric_cast_v(vector_type.size()); mp_integer total = vector_size * sub_width; - if(total > (1 << 30)) // realistic limit - throw analysis_exceptiont("vector too large for flattening"); - entry.total_width = numeric_cast_v(vector_size * sub_width); } else if(type_id==ID_complex) From 1ad790f40af93b7fb02f04194d8442353a8e8c50 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 22 Jun 2021 10:48:44 +0100 Subject: [PATCH 3/5] Error handling for very large size arrays and vectors This reinstates and improves the error handling for very large arrays and vectors with the limit of 1 << 30 (from old code). This prevents exceptions in the cast which can occur for extremely large values. --- src/solvers/flattening/boolbv_width.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 09d1c3d0946..90b9eda01b2 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -135,7 +135,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const else { mp_integer total = *array_size * sub_width; - entry.total_width = numeric_cast_v(total); + if(total>(1<<30)) // realistic limit + throw analysis_exceptiont("array too large for flattening"); + if(total < 0) + entry.total_width = 0; + else + entry.total_width = numeric_cast_v(total); } } else if(type_id==ID_vector) @@ -146,7 +151,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const const auto vector_size = numeric_cast_v(vector_type.size()); mp_integer total = vector_size * sub_width; - entry.total_width = numeric_cast_v(vector_size * sub_width); + if(total > (1 << 30)) // realistic limit + throw analysis_exceptiont("vector too large for flattening"); + if(total < 0) + entry.total_width = 0; + else + entry.total_width = numeric_cast_v(vector_size * sub_width); } else if(type_id==ID_complex) { From bc0256555c53082705fb6e9b111d47471cb194ee Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 22 Jun 2021 11:36:54 +0100 Subject: [PATCH 4/5] Add regression test for size limit check This adds a regression test to check that the size limit for arrays is caught and cleanly handled (with appropriate error). --- regression/cbmc/array_too_big/test.c | 13 +++++++++++++ regression/cbmc/array_too_big/test.desc | 11 +++++++++++ 2 files changed, 24 insertions(+) create mode 100644 regression/cbmc/array_too_big/test.c create mode 100644 regression/cbmc/array_too_big/test.desc diff --git a/regression/cbmc/array_too_big/test.c b/regression/cbmc/array_too_big/test.c new file mode 100644 index 00000000000..6bf1f0d54cb --- /dev/null +++ b/regression/cbmc/array_too_big/test.c @@ -0,0 +1,13 @@ +#include +#include +#include + +int main() +{ + size_t size; + size = 1<<31; // Chosen to be beyond the coded limit in cbmc source + uint8_t *ptr = malloc(size); + __CPROVER_assume(ptr != NULL); + uint8_t *ptr_end = ptr + size; + assert(ptr <= ptr_end); +} diff --git a/regression/cbmc/array_too_big/test.desc b/regression/cbmc/array_too_big/test.desc new file mode 100644 index 00000000000..14f6979ca06 --- /dev/null +++ b/regression/cbmc/array_too_big/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--pointer-overflow-check --pointer-check +^EXIT=6$ +^SIGNAL=0$ +^array too large for flattening$ +-- +VERIFICATION +-- +This test is to check that arrays that are too large are correctly +error handled to prevent exceptions in other parts of the code. From 8659dac170b711b754b5575ff140e95f4c1bea78 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Fri, 9 Jul 2021 10:18:25 +0100 Subject: [PATCH 5/5] Revert "Add regression test for size limit check" This reverts commit bc0256555c53082705fb6e9b111d47471cb194ee. --- regression/cbmc/array_too_big/test.c | 13 ------------- regression/cbmc/array_too_big/test.desc | 11 ----------- 2 files changed, 24 deletions(-) delete mode 100644 regression/cbmc/array_too_big/test.c delete mode 100644 regression/cbmc/array_too_big/test.desc diff --git a/regression/cbmc/array_too_big/test.c b/regression/cbmc/array_too_big/test.c deleted file mode 100644 index 6bf1f0d54cb..00000000000 --- a/regression/cbmc/array_too_big/test.c +++ /dev/null @@ -1,13 +0,0 @@ -#include -#include -#include - -int main() -{ - size_t size; - size = 1<<31; // Chosen to be beyond the coded limit in cbmc source - uint8_t *ptr = malloc(size); - __CPROVER_assume(ptr != NULL); - uint8_t *ptr_end = ptr + size; - assert(ptr <= ptr_end); -} diff --git a/regression/cbmc/array_too_big/test.desc b/regression/cbmc/array_too_big/test.desc deleted file mode 100644 index 14f6979ca06..00000000000 --- a/regression/cbmc/array_too_big/test.desc +++ /dev/null @@ -1,11 +0,0 @@ -CORE -test.c ---pointer-overflow-check --pointer-check -^EXIT=6$ -^SIGNAL=0$ -^array too large for flattening$ --- -VERIFICATION --- -This test is to check that arrays that are too large are correctly -error handled to prevent exceptions in other parts of the code.