Merge pull request #1654 from NlightNFotis/fotis/pb10_develop

Fix for the handling of constant arrays and members of structs being marked nondet.

Author: tautschnig

regression/cbmc/no_nondet_static/main.c

@@ -0,0 +1,100 @@
+#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;
+struct s s2 = { 23 };
+const struct s s3 = { 23 };
+
+struct t { int x; const int y; };
+struct t t1;
+struct t t2 = { 23, 23 };
+const struct t t3 = { 23, 23 };
+
+struct u { const int x; };
+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;
+
+const Int p = 23;
+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);
+  assert(s1.x == 0);
+  assert(s2.x == 23);
+  assert(a[0].x == 23);
+  assert(a[0].p == &x);
+  assert(c[2].x == 23);
+  assert(c[2].p == &z);
+  
+  /* Should still pass */
+  assert(z == 23);
+  assert(s3.x == 23);
+  assert(t1.y == 0);
+  assert(t2.y == 23);
+  assert(t3.x == 23);
+  assert(t3.y == 23);
+  assert(u1.x == 0);
+  assert(u2.x == 23);
+  assert(u3.x == 23);
+  assert(p == 23);
+  assert(q == 23);
+  assert(t1.x == 0);
+  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

@@ -0,0 +1,36 @@
+CORE
+main.c
+--nondet-static
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+assertion x == 0: FAILURE
+assertion y == 23: FAILURE
+assertion s1.x == 0: FAILURE
+assertion s2.x == 23: FAILURE
+assertion a\[0\].x == 23: FAILURE
+assertion a\[0\].p == &x: FAILURE
+assertion c\[2\].x == 23: FAILURE
+assertion c\[2\].p == &z: FAILURE
+assertion z == 23: SUCCESS
+assertion s3.x == 23: SUCCESS
+assertion t1.y == 0: SUCCESS
+assertion t2.y == 23: SUCCESS
+assertion t3.x == 23: SUCCESS
+assertion t3.y == 23: SUCCESS
+assertion u1.x == 0: SUCCESS
+assertion u2.x == 23: SUCCESS
+assertion u3.x == 23: SUCCESS
+assertion p == 23: SUCCESS
+assertion q == 23: SUCCESS
+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

@@ -51,7 +51,7 @@ void nondet_static(
         continue;
 
       // constant?
-      if(sym.type().get_bool(ID_C_constant))
+      if(is_constant_or_has_constant_components(sym.type(), ns))
         continue;
 
       i_it=init.insert_before(++i_it);

src/util/type.cpp

@@ -6,8 +6,9 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "type.h"
+#include "std_types.h"
+#include "namespace.h"
 
 void typet::copy_to_subtypes(const typet &type)
 {
@@ -34,3 +35,74 @@ bool is_number(const typet &type)
          id==ID_floatbv ||
          id==ID_fixedbv;
 }
+
+/// Identify if a given type is constant itself or
+/// contains constant components. Examples include:
+///  - const int a;
+///  - struct contains_constant_pointer {  int x; int * const p; };
+///  - const int b[3];
+/// \param type The type we want to query constness of.
+/// \param ns The namespace, needed for resolution of symbols.
+/// \return Whether passed in type is const or not.
+bool is_constant_or_has_constant_components(
+  const typet &type, const namespacet &ns)
+{
+  // Helper function to avoid the code duplication in the branches
+  // below.
+  const auto has_constant_components =
+    [&ns](const typet &subtype) -> bool
+    {
+      if(subtype.id() == ID_struct || subtype.id() == ID_union)
+      {
+        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;
+    };
+
+  // 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
+  // regression/cbmc/no_nondet_static/main.c
+
+  // const int a;
+  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 &resolved_type = ns.follow(type);
+    return has_constant_components(resolved_type);
+  }
+
+  // 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();
+    return is_constant_or_has_constant_components(subtype, ns);
+  }
+
+  return false;
+}

src/util/type.h

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #define SUBTYPE_IN_GETSUB
 #define SUBTYPES_IN_GETSUB
 
+class namespacet;
+
 /*! \brief The type of an expression
 */
 class typet:public irept
@@ -203,4 +205,9 @@ pre-defined types:
 bool is_number(const typet &type);
 // rational, real, integer, complex, unsignedbv, signedbv, floatbv
 
+// Is the passed in type const qualified?
+bool is_constant_or_has_constant_components(
+    const typet &type,
+    const namespacet &ns);
+
 #endif // CPROVER_UTIL_TYPE_H