Fix the handling of recursive data types.

Author: NlightNFotis

regression/cbmc/no_nondet_static/main.c

@@ -1,6 +1,9 @@
+#define NULL 0
+
 int x;
 int y = 23;
 const int z = 23;
+const int array[] = { 5, 6, 7, 8};
 
 struct s { int x; };
 struct s s1;
@@ -17,15 +20,36 @@ struct u u1;
 struct u u2 = { 23 };
 const struct u u3 = { 23 };
 
+struct list { const int datum; struct list * next; };
+
+// The point of this is that cbmc needs to correctly handle
+// the embedded datum int the nested struct which is const,
+// while not falling into infinite recursion from the 
+// recursive field.
+struct another_list {
+    struct a_list { 
+        struct a_list * next; 
+        const int datum; 
+    } embedded;
+    int a;
+};
+
 struct contains_pointer {  int x; int *p; };
 // const int *p : declare p as pointer to const int
 struct contains_pointer_to_const {  int x; const int *p; };
 // int * const p : declare p as const pointer to int
 struct contains_constant_pointer {  int x; int * const p; };
+// this should cause a bug
+struct contains_pointer_to_const_point {  int x; int * y; int * const p; };
 
 struct contains_pointer a[3] = { {23, &x}, {23, &x}, {23, &x} };
 struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
 struct contains_pointer_to_const c[3] = { {23, &z}, {23, &z}, {23, &z} };
+struct contains_pointer_to_const_point d[3]= { {23, &y, &z}, {23, &y, &z}, {23, &y, &z} };
+
+struct list node = {10, NULL};
+
+struct another_list one_list = {{10, NULL}, 5};
 
 typedef int Int;
 typedef const int Const_Int;
@@ -37,7 +61,9 @@ Const_Int q = 23;
 #include <assert.h>
 
 int main (int argc, char **argv) 
-{  
+{
+  struct list linked_list = {5, &node};
+
   /* Pass normally but fail with nondet-static */
   assert(x == 0);
   assert(y == 23);
@@ -64,6 +90,11 @@ int main (int argc, char **argv)
   assert(t2.x == 23);
   assert(b[1].x == 23);
   assert(b[1].p == &y);
+  assert(d[1].y == &y);
+  assert(linked_list.datum == 5);
+  assert(linked_list.next->datum == 10);
+  assert(one_list.a == 5);
+  assert(array[1] == 6);
 
   return 0;
 }

regression/cbmc/no_nondet_static/test.desc

@@ -2,6 +2,8 @@ CORE
 main.c
 --nondet-static
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 assertion x == 0: FAILURE
 assertion y == 23: FAILURE
 assertion s1.x == 0: FAILURE
@@ -25,5 +27,10 @@ assertion t1.x == 0: SUCCESS
 assertion t2.x == 23: SUCCESS
 assertion b\[1\].x == 23: SUCCESS
 assertion b\[1\].p == &y: SUCCESS
+assertion d\[1\].y == &y: SUCCESS
+assertion linked_list.datum == 5: SUCCESS
+assertion linked_list.next->datum == 10: SUCCESS
+assertion one_list.a == 5: SUCCESS
+assertion array\[1\] == 6: SUCCESS
 --
 --

src/goto-instrument/nondet_static.cpp

@@ -18,7 +18,6 @@ Date: November 2011
 #include <util/std_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
-#include <util/type.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/goto_functions.h>

src/util/type.cpp

@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "type.h"
 #include "std_types.h"
 #include "namespace.h"
@@ -48,26 +47,24 @@ bool is_number(const typet &type)
 bool is_constant_or_has_constant_components(
   const typet &type, const namespacet &ns)
 {
-  // Helper function to avoid the code duplication
-  // in the branches below.
+  // Helper function to avoid the code duplication in the branches
+  // below.
   const auto has_constant_components =
-  [](const typet &subtype) -> bool
-  {
-    if(subtype.id() == ID_struct || subtype.id() == ID_union)
+    [&ns](const typet &subtype) -> bool
     {
-      const auto &struct_union_type = to_struct_union_type(subtype);
-      for(const auto &component : struct_union_type.components())
+      if(subtype.id() == ID_struct || subtype.id() == ID_union)
       {
-        if(component.type().id() == ID_pointer)
-          return component.type().get_bool(ID_C_constant);
-        if(component.type().get_bool(ID_C_constant))
-          return true;
+        const auto &struct_union_type = to_struct_union_type(subtype);
+        for(const auto &component : struct_union_type.components())
+        {
+          if(is_constant_or_has_constant_components(component.type(), ns))
+            return true;
+        }
       }
-    }
-    return false;
-  };
+      return false;
+    };
 
-  // There are 3 possibilities the code below is handling.
+  // There are 4 possibilities the code below is handling.
   // The possibilities are enumerated as comments, to show
   // what each code is supposed to be handling. For more
   // comprehensive test case for this, take a look at
@@ -77,30 +74,34 @@ bool is_constant_or_has_constant_components(
   if(type.get_bool(ID_C_constant))
     return true;
 
+  // This is a termination condition to break the recursion
+  // for recursive types such as the following:
+  // struct list { const int datum; struct list * next; };
+  // NOTE: the difference between this condition and the previous
+  // one is that this one always returns.
+  if(type.id()==ID_pointer)
+    return type.get_bool(ID_C_constant);
+
   // When we have a case like the following, we don't immediately
   // see the struct t. Instead, we only get to see symbol t1, which
   // we have to use the namespace to resolve to its definition:
   // struct t { const int a; };
   // struct t t1;
   if(type.id() == ID_symbol)
   {
-    const auto &subtype = ns.follow(type);
-    return has_constant_components(subtype);
+    const auto &resolved_type = ns.follow(type);
+    return has_constant_components(resolved_type);
   }
 
-  // In a case like this, were we see an array (b[3] here), we know that
+  // In a case like this, where we see an array (b[3] here), we know that
   // the array contains subtypes. We get the first one, and
   // then resolve it to its  definition through the usage of the namespace.
   // struct contains_constant_pointer { int x; int * const p; };
   // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
   if(type.has_subtype())
   {
     const auto &subtype = type.subtype();
-    if(subtype.id() == ID_symbol)
-    {
-      const auto &new_subtype = ns.follow(to_symbol_type(subtype));
-      return has_constant_components(new_subtype);
-    }
+    return is_constant_or_has_constant_components(subtype, ns);
   }
 
   return false;

src/util/type.h

@@ -11,11 +11,12 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_TYPE_H
 
 #include <util/source_location.h>
-#include "namespace.h"
 
 #define SUBTYPE_IN_GETSUB
 #define SUBTYPES_IN_GETSUB
 
+class namespacet;
+
 /*! \brief The type of an expression
 */
 class typet:public irept