From 0795ec28c21ef87f38ce3781017f6fc8f376ca0d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 3 Nov 2022 11:47:47 +0000 Subject: [PATCH 1/4] Enforce dereferencing bitvectors requiring a size that is multiple of 8. --- src/ansi-c/c_typecheck_expr.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 28e03bd5c21..7e32db9f181 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1805,6 +1805,17 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr) error() << "dereferencing void pointer" << eom; throw 0; } + + if(is_signed_or_unsigned_bitvector(expr.type())) + { + auto bv_type_width = to_bitvector_type(expr.type()).get_width(); + if(bv_type_width % 8 != 0) + { + throw invalid_source_file_exceptiont{ + "only bitvectors of size multiple of 8 can be dereferenced", + expr.source_location()}; + } + } } else { From 8c5eae2d941e429a3205c0246e491b04d17646d1 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 3 Nov 2022 11:56:46 +0000 Subject: [PATCH 2/4] Add original test case as a regression test in ansi-c/ folder. --- regression/ansi-c/Issue_7104_Bv_Size/deref.c | 18 ++++++++++++++++++ .../ansi-c/Issue_7104_Bv_Size/deref.desc | 13 +++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 regression/ansi-c/Issue_7104_Bv_Size/deref.c create mode 100644 regression/ansi-c/Issue_7104_Bv_Size/deref.desc diff --git a/regression/ansi-c/Issue_7104_Bv_Size/deref.c b/regression/ansi-c/Issue_7104_Bv_Size/deref.c new file mode 100644 index 00000000000..03ed31cc694 --- /dev/null +++ b/regression/ansi-c/Issue_7104_Bv_Size/deref.c @@ -0,0 +1,18 @@ +struct Foo1 +{ + __CPROVER_bitvector[1] m_array[2]; +}; +struct Foo8 +{ + __CPROVER_bitvector[8] m_array[2]; +}; + +int main(void) +{ + struct Foo1 f1; + struct Foo8 f8; + + __CPROVER_assert(f1.m_array[1] == *(f1.m_array + 1), ""); + __CPROVER_assert(f8.m_array[1] == *(f8.m_array + 1), ""); + return 0; +} diff --git a/regression/ansi-c/Issue_7104_Bv_Size/deref.desc b/regression/ansi-c/Issue_7104_Bv_Size/deref.desc new file mode 100644 index 00000000000..3ed380e4daf --- /dev/null +++ b/regression/ansi-c/Issue_7104_Bv_Size/deref.desc @@ -0,0 +1,13 @@ +CORE +deref.c + +^EXIT=1$ +^SIGNAL=0$ +only bitvectors of size multiple of 8 can be dereferenced +^CONVERSION ERROR$ +-- +-- +This is checking that dereferenced __CPROVER_bitvectors always have a size +that is a multiple of 8. + +For more information, please have a look at https://github.com/diffblue/cbmc/issues/7104 From 7777ccd8a0e0e8d1b94ff064a519e6cd6a0fb5ab Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 14 Nov 2022 17:26:54 +0000 Subject: [PATCH 3/4] Move check for bv size to flattening/ instead of ansi-c/ --- regression/ansi-c/Issue_7104_Bv_Size/deref.desc | 2 +- src/ansi-c/c_typecheck_expr.cpp | 11 ----------- src/solvers/flattening/boolbv_byte_extract.cpp | 6 ++++++ 3 files changed, 7 insertions(+), 12 deletions(-) diff --git a/regression/ansi-c/Issue_7104_Bv_Size/deref.desc b/regression/ansi-c/Issue_7104_Bv_Size/deref.desc index 3ed380e4daf..40063c609da 100644 --- a/regression/ansi-c/Issue_7104_Bv_Size/deref.desc +++ b/regression/ansi-c/Issue_7104_Bv_Size/deref.desc @@ -3,7 +3,7 @@ deref.c ^EXIT=1$ ^SIGNAL=0$ -only bitvectors of size multiple of 8 can be dereferenced +only bitvectors of size multiple of 8 bits can be dereferenced ^CONVERSION ERROR$ -- -- diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 7e32db9f181..28e03bd5c21 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1805,17 +1805,6 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr) error() << "dereferencing void pointer" << eom; throw 0; } - - if(is_signed_or_unsigned_bitvector(expr.type())) - { - auto bv_type_width = to_bitvector_type(expr.type()).get_width(); - if(bv_type_width % 8 != 0) - { - throw invalid_source_file_exceptiont{ - "only bitvectors of size multiple of 8 can be dereferenced", - expr.source_location()}; - } - } } else { diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 01cb688063f..b63ffbffad9 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -40,6 +40,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) } const std::size_t width = boolbv_width(expr.type()); + if(width % 8 != 0) + { + throw invalid_source_file_exceptiont{ + "only bitvectors of size multiple of 8 bits can be dereferenced", + expr.source_location()}; + } // special treatment for bit-fields and big-endian: // we need byte granularity From 81987b3178a53e830ffd57b5f86b0d25bcd89052 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 15 Nov 2022 10:24:14 +0000 Subject: [PATCH 4/4] Change invalid_source_file_exceptiont to a call to conversion_failed --- src/solvers/flattening/boolbv_byte_extract.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index b63ffbffad9..c21f8bbaa27 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -42,9 +42,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) const std::size_t width = boolbv_width(expr.type()); if(width % 8 != 0) { - throw invalid_source_file_exceptiont{ - "only bitvectors of size multiple of 8 bits can be dereferenced", - expr.source_location()}; + // throw invalid_source_file_exceptiont{ + // "only bitvectors of size multiple of 8 bits can be dereferenced", + // expr.source_location()}; + conversion_failed(expr); } // special treatment for bit-fields and big-endian: