From 7b9a20a75e42ef2b557a9e47524bc849f2127012 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 9 May 2018 14:14:53 +0100 Subject: [PATCH 1/4] Allow pointers to be dereferenced to void types --- .../value_set_dereference.cpp | 22 +++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 8b2ed99baab..dfbc7cc76db 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -201,8 +201,26 @@ bool value_set_dereferencet::dereference_type_compare( const typet &object_type, const typet &dereference_type) const { - if(dereference_type.id()==ID_empty) - return true; // always ok + // check if the two types have matching number of ID_pointer levels, with + // the dereference type eventually pointing to void; then this is ok + // for example: + // - dereference_type=void is ok (no matter what object_type is); + // - object_type=(int *), dereference_type=(void *) is ok; + // - object_type=(int **), dereference_type=(void **) is ok; + // - object_type=(int **), dereference_type=(void *) is ok; + // - object_type=(int *), dereference_type=(void **) is not ok; + const typet *object_unwrapped = &object_type; + const typet *dereference_unwrapped = &dereference_type; + while(object_unwrapped->id() == ID_pointer && + dereference_unwrapped->id() == ID_pointer) + { + object_unwrapped = &object_unwrapped->subtype(); + dereference_unwrapped = &dereference_unwrapped->subtype(); + } + if(dereference_unwrapped->id() == ID_empty) + { + return true; + } if(base_type_eq(object_type, dereference_type, ns)) return true; // ok, they just match From 146bb2900db2aad6caeeef0209a4b5211079bf12 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 14 May 2018 10:40:49 +0100 Subject: [PATCH 2/4] Adding debug information to dereference type comparison --- src/pointer-analysis/value_set_dereference.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index dfbc7cc76db..89932081e17 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -221,6 +221,18 @@ bool value_set_dereferencet::dereference_type_compare( { return true; } + else if(dereference_unwrapped->id() == ID_pointer && + object_unwrapped->id() != ID_pointer) + { +#ifdef DEBUG + std::cout << "value_set_dereference: the dereference type has " + "too many ID_pointer levels" + << std::endl; + std::cout << " object_type: " << object_type.pretty() << std::endl; + std::cout << " dereference_type: " << dereference_type.pretty() + << std::endl; +#endif + } if(base_type_eq(object_type, dereference_type, ns)) return true; // ok, they just match From bc173282c55950d47bf2d8cabcc55b921e301aba Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 9 May 2018 14:40:25 +0100 Subject: [PATCH 3/4] Enable previously failing regression tests --- .../test_float_multidim_1.desc | 11 ++++------- .../test_ref_multidim_1.desc | 11 ++++------- .../test_ref_multidim_2.desc | 11 ++++------- 3 files changed, 12 insertions(+), 21 deletions(-) diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc index 54c7ed67f46..98169774c6f 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc @@ -1,12 +1,9 @@ -KNOWNBUG +CORE FloatMultidim1.class --function FloatMultidim1.f --cover location --unwind 3 \d+ of \d+ covered ^EXIT=0$ ^SIGNAL=0$ --- --- -This crashes during symex, with error 'cannot unpack array of nonconst size' -when trying to access the element of the array. Symex uses byte_extract_little -_endian to access the element which does not get simplified (it seems the -problem is that the types in the instruction do not match). TG-1121 +y=1$ +y=[2-4]$ +y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc index f96f028e32f..c4a07a7c56b 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc @@ -1,12 +1,9 @@ -KNOWNBUG +CORE RefMultidim1.class --function RefMultidim1.f --cover location --unwind 3 \d+ of \d+ covered ^EXIT=0$ ^SIGNAL=0$ --- --- -This crashes during symex, with error 'cannot unpack array of nonconst size' -when trying to access the element of the array. Symex uses byte_extract_little -_endian to access the element which does not get simplified (it seems the -problem is that the types in the instruction do not match). TG-1121 +y=1$ +y=[2-4]$ +y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc index 190b154c371..1f46e69a206 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc @@ -1,12 +1,9 @@ -KNOWNBUG +CORE RefMultidim2.class --function RefMultidim2.f --cover location --unwind 3 \d+ of \d+ covered ^EXIT=0$ ^SIGNAL=0$ --- --- -This crashes during symex, with error 'cannot unpack array of nonconst size' -when trying to access the element of the array. Symex uses byte_extract_little -_endian to access the element which does not get simplified (it seems the -problem is that the types in the instruction do not match). TG-1121 +y=1$ +y=[2-4]$ +y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ From 6af22701e96b3b9a923a867d8325f94a07d20518 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 9 May 2018 14:41:00 +0100 Subject: [PATCH 4/4] Update regression test that no longer throws an exception --- .../jbmc/dynamic-multi-dimensional-array/test.desc | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc index c9600f50852..a4220527596 100644 --- a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc +++ b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc @@ -1,10 +1,5 @@ CORE TestClass.class --function TestClass.f --cover location --unwind 2 -Source GOTO statement: .* -(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows) -^EXIT=6$ --- --- -The exception thrown in this test is the symptom of a bug; the purpose of this -test is the validate the output of that exception +^EXIT=0$ +^SIGNAL=0$