Merge pull request diffblue#2173 from svorenova/gs_tg1121

[TG-1121] Bugfix for multi-dimensional arrays with non-const size and non-const access

Author: Thomas Kiley

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]*)$

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]*)$

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]*)$

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$

src/pointer-analysis/value_set_dereference.cpp

@@ -201,8 +201,38 @@ 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;
+  }
+  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