From ff6685f94c49803542a0f5cb8d6b643ca85edf65 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 1 Mar 2021 12:20:54 +0000 Subject: [PATCH] Value set dereferencing: do not treat struct prefixes as equal Two distinct struct types cannot be cast between, even when one is a prefix of the other. Value set dereferencing taking this approach just resulted in propositional encoding producing a warning about invalid type casts. --- .../test_no_simplify_vccs.desc | 11 ------- regression/cbmc/struct2/main.c | 24 ++++++++++++++ regression/cbmc/struct2/test.desc | 11 +++++++ regression/cbmc/struct5/main.c | 28 +++++++++++++++++ regression/cbmc/struct5/test.desc | 8 +++++ src/cprover/may_alias.cpp | 31 ++++++++++++++++++- .../value_set_dereference.cpp | 16 ---------- src/util/std_types.cpp | 29 ----------------- src/util/std_types.h | 2 -- 9 files changed, 101 insertions(+), 59 deletions(-) delete mode 100644 jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc create mode 100644 regression/cbmc/struct2/main.c create mode 100644 regression/cbmc/struct2/test.desc create mode 100644 regression/cbmc/struct5/main.c create mode 100644 regression/cbmc/struct5/test.desc diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc deleted file mode 100644 index 74fb1af9613..00000000000 --- a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc +++ /dev/null @@ -1,11 +0,0 @@ -CORE -Test ---function Test.main --no-simplify --unwind 10 --show-vcc -^EXIT=0$ -^SIGNAL=0$ -"java::Impl1" = cast\(\{ \{ "java::Impl1" \}, 0 \}, struct (\{ struct \{ string @class_identifier \} @java.lang.Object \}|java::Intf)\)\.@java.lang.Object\.@class_identifier --- -^warning: ignoring --- -This checks that the test generates the VCC testing the class-id that we're -intending to simplify away in the main test. diff --git a/regression/cbmc/struct2/main.c b/regression/cbmc/struct2/main.c new file mode 100644 index 00000000000..0f2c3867032 --- /dev/null +++ b/regression/cbmc/struct2/main.c @@ -0,0 +1,24 @@ +struct T +{ + // intentionally empty to trigger is_prefix_of code (empty structs, however, + // are a GCC-only feature) +}; + +struct S +{ + struct T t; + int other; +}; + +void foo(struct S s2) +{ + struct T *p = &s2.t; + struct T t2 = *p; + __CPROVER_assert(0, ""); +} + +int main() +{ + struct S s; + foo(s); +} diff --git a/regression/cbmc/struct2/test.desc b/regression/cbmc/struct2/test.desc new file mode 100644 index 00000000000..8c6408a3ba0 --- /dev/null +++ b/regression/cbmc/struct2/test.desc @@ -0,0 +1,11 @@ +CORE gcc-only no-new-smt +main.c + +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test must not generate a warning about typecasts (between different struct +types) being ignored. diff --git a/regression/cbmc/struct5/main.c b/regression/cbmc/struct5/main.c new file mode 100644 index 00000000000..ca759d39b54 --- /dev/null +++ b/regression/cbmc/struct5/main.c @@ -0,0 +1,28 @@ +#include + +struct a +{ + int x; +}; +struct b +{ + struct a p; + int y; +}; + +int f00(struct a *ptr) +{ + return ptr->x; +} + +int main() +{ + struct b z = {{1}, 2}; + + assert(&z == &(z.p)); + assert(&z == &(z.p.x)); + + assert(f00(&z) == z.p.x); + + return 0; +} diff --git a/regression/cbmc/struct5/test.desc b/regression/cbmc/struct5/test.desc new file mode 100644 index 00000000000..278f468e130 --- /dev/null +++ b/regression/cbmc/struct5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp index 046fbbcd84c..971fdbc4249 100644 --- a/src/cprover/may_alias.cpp +++ b/src/cprover/may_alias.cpp @@ -71,6 +71,34 @@ bool is_object_field_element(const exprt &expr) return false; } +/// Returns true if struct \p a is a prefix of \p b, i.e., if this struct has +/// n components then the component types and names of this struct must match +/// the first n components of \p b. +/// \param a: Struct type that may be a prefix. +/// \param b: Struct type to compare with. +static bool struct_is_prefix_of(const struct_typet &a, const struct_typet &b) +{ + const struct_typet::componentst &ot_components = b.components(); + const struct_typet::componentst &tt_components = a.components(); + + if(ot_components.size() < tt_components.size()) + return false; + + struct_typet::componentst::const_iterator ot_it = ot_components.begin(); + + for(const auto &tt_c : tt_components) + { + if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name()) + { + return false; // they just don't match + } + + ot_it++; + } + + return true; // ok, a is a prefix of b +} + bool prefix_of(const typet &a, const typet &b, const namespacet &ns) { if(a == b) @@ -88,7 +116,8 @@ bool prefix_of(const typet &a, const typet &b, const namespacet &ns) const auto &a_struct = to_struct_type(a); const auto &b_struct = to_struct_type(b); - return a_struct.is_prefix_of(b_struct) || b_struct.is_prefix_of(a_struct); + return struct_is_prefix_of(a_struct, b_struct) || + struct_is_prefix_of(b_struct, a_struct); } static std::optional find_object(const exprt &expr) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index dd17eced5e6..6d16b3f04f8 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -372,22 +372,6 @@ bool value_set_dereferencet::dereference_type_compare( if(object_type == dereference_type) return true; // ok, they just match - // check for struct prefixes - const typet &ot_base = object_type.id() == ID_struct_tag - ? ns.follow_tag(to_struct_tag_type(object_type)) - : object_type; - const typet &dt_base = dereference_type.id() == ID_struct_tag - ? ns.follow_tag(to_struct_tag_type(dereference_type)) - : dereference_type; - - if(ot_base.id()==ID_struct && - dt_base.id()==ID_struct) - { - if(to_struct_type(dt_base).is_prefix_of( - to_struct_type(ot_base))) - return true; // ok, dt is a prefix of ot - } - // we are generous about code pointers if(dereference_type.id()==ID_code && object_type.id()==ID_code) diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 6052b1d6e21..cca396355bc 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -112,35 +112,6 @@ struct_typet::get_base(const irep_idt &id) const return {}; } -/// Returns true if the struct is a prefix of \a other, i.e., if this struct -/// has n components then the component types and names of this struct must -/// match the first n components of \a other struct. -/// \param other: Struct type to compare with. -bool struct_typet::is_prefix_of(const struct_typet &other) const -{ - const componentst &ot_components=other.components(); - const componentst &tt_components=components(); - - if(ot_components.size()< - tt_components.size()) - return false; - - componentst::const_iterator - ot_it=ot_components.begin(); - - for(const auto &tt_c : tt_components) - { - if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name()) - { - return false; // they just don't match - } - - ot_it++; - } - - return true; // ok, *this is a prefix of ot -} - /// Returns true if the type is a reference. bool is_reference(const typet &type) { diff --git a/src/util/std_types.h b/src/util/std_types.h index b875c5b0023..336453f49bb 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -239,8 +239,6 @@ class struct_typet:public struct_union_typet { } - bool is_prefix_of(const struct_typet &other) const; - /// A struct may be a class, where members may have access restrictions. bool is_class() const {