From cd6078285409c7b0cbcb15fa8ec9cb854f92797a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 28 Nov 2017 09:57:07 +0000 Subject: [PATCH 1/2] Fix for the constant arrays marked as nondet issue. --- regression/cbmc/no_nondet_static/main.c | 69 +++++++++++++++++++++ regression/cbmc/no_nondet_static/test.desc | 29 +++++++++ src/goto-instrument/nondet_static.cpp | 3 +- src/util/type.cpp | 71 ++++++++++++++++++++++ src/util/type.h | 6 ++ 5 files changed, 177 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc/no_nondet_static/main.c create mode 100644 regression/cbmc/no_nondet_static/test.desc diff --git a/regression/cbmc/no_nondet_static/main.c b/regression/cbmc/no_nondet_static/main.c new file mode 100644 index 00000000000..f3c0f361503 --- /dev/null +++ b/regression/cbmc/no_nondet_static/main.c @@ -0,0 +1,69 @@ +int x; +int y = 23; +const int z = 23; + +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 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; }; + +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} }; + +typedef int Int; +typedef const int Const_Int; + +const Int p = 23; +Const_Int q = 23; + + +#include + +int main (int argc, char **argv) +{ + /* 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); + + return 0; +} diff --git a/regression/cbmc/no_nondet_static/test.desc b/regression/cbmc/no_nondet_static/test.desc new file mode 100644 index 00000000000..0ca5fcc6d1a --- /dev/null +++ b/regression/cbmc/no_nondet_static/test.desc @@ -0,0 +1,29 @@ +CORE +main.c +--nondet-static +^VERIFICATION FAILED$ +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 +-- +-- diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 2d0cd7cd055..83ad08c4919 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -18,6 +18,7 @@ Date: November 2011 #include #include #include +#include #include #include @@ -51,7 +52,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); diff --git a/src/util/type.cpp b/src/util/type.cpp index 288666ac443..7d9aec69e5f 100644 --- a/src/util/type.cpp +++ b/src/util/type.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "type.h" +#include "std_types.h" +#include "namespace.h" void typet::copy_to_subtypes(const typet &type) { @@ -34,3 +36,72 @@ 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 = + [](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(component.type().id() == ID_pointer) + return component.type().get_bool(ID_C_constant); + if(component.type().get_bool(ID_C_constant)) + return true; + } + } + return false; + }; + + // There are 3 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; + + // 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); + } + + // In a case like this, were 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 false; +} diff --git a/src/util/type.h b/src/util/type.h index 7e9b3a47e87..b6bec32b9ed 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_TYPE_H #include +#include "namespace.h" #define SUBTYPE_IN_GETSUB #define SUBTYPES_IN_GETSUB @@ -203,4 +204,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 From b5faf52ff366d5a64260a84952f5f25ab5eb9406 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2017 17:13:34 +0000 Subject: [PATCH 2/2] Fix the handling of recursive data types. --- regression/cbmc/no_nondet_static/main.c | 33 ++++++++++++++- regression/cbmc/no_nondet_static/test.desc | 7 ++++ src/goto-instrument/nondet_static.cpp | 1 - src/util/type.cpp | 49 +++++++++++----------- src/util/type.h | 3 +- 5 files changed, 66 insertions(+), 27 deletions(-) diff --git a/regression/cbmc/no_nondet_static/main.c b/regression/cbmc/no_nondet_static/main.c index f3c0f361503..1c000444da0 100644 --- a/regression/cbmc/no_nondet_static/main.c +++ b/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 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; } diff --git a/regression/cbmc/no_nondet_static/test.desc b/regression/cbmc/no_nondet_static/test.desc index 0ca5fcc6d1a..4f2a282f623 100644 --- a/regression/cbmc/no_nondet_static/test.desc +++ b/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 -- -- diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 83ad08c4919..587b935f80a 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -18,7 +18,6 @@ Date: November 2011 #include #include #include -#include #include #include diff --git a/src/util/type.cpp b/src/util/type.cpp index 7d9aec69e5f..a83e5576717 100644 --- a/src/util/type.cpp +++ b/src/util/type.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #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,6 +74,14 @@ 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: @@ -84,11 +89,11 @@ bool is_constant_or_has_constant_components( // 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; }; @@ -96,11 +101,7 @@ bool is_constant_or_has_constant_components( 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; diff --git a/src/util/type.h b/src/util/type.h index b6bec32b9ed..8bf58296c61 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -11,11 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_TYPE_H #include -#include "namespace.h" #define SUBTYPE_IN_GETSUB #define SUBTYPES_IN_GETSUB +class namespacet; + /*! \brief The type of an expression */ class typet:public irept