From abdbbbcf2ce2ba2ed10ee0b956750ab3aca630e9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Jan 2019 16:02:55 +0000 Subject: [PATCH 1/5] has_subtype: handle struct/union tag types Just like symbol or enum tags, we need to look into the expanded tags. --- src/util/expr_util.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 72d0a6d899f..6b066fd1182 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -174,6 +174,10 @@ bool has_subtype( push_if_not_visited(ns.follow(top)); else if(top.id() == ID_c_enum_tag) push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top))); + else if(top.id() == ID_struct_tag) + push_if_not_visited(ns.follow_tag(to_struct_tag_type(top))); + else if(top.id() == ID_union_tag) + push_if_not_visited(ns.follow_tag(to_union_tag_type(top))); else if(top.id() == ID_struct || top.id() == ID_union) { for(const auto &comp : to_struct_union_type(top).components()) From 3d9af8e93e8155f5c200263f11b10d79a04f4658 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Jan 2019 15:58:30 +0000 Subject: [PATCH 2/5] Make tests oblivious to tag type expansion The regular expressions now accept both the tag names as well as the expanded types/class names. --- .../simplify-classid-of-interface/test_no_simplify_vccs.desc | 2 +- jbmc/regression/jbmc/trace_class_identifier/test.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 index c79401ad1fe..4f9651fe82f 100644 --- 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 @@ -3,7 +3,7 @@ Test.class --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.lang.Object\.@class_identifier +"java::Impl1" = cast\(\{ \{ "java::Impl1" \}, 0 \}, struct (\{ struct \{ string @class_identifier \} @java.lang.Object \}|java::Intf)\)\.@java.lang.Object\.@class_identifier -- ^warning: ignoring -- diff --git a/jbmc/regression/jbmc/trace_class_identifier/test.desc b/jbmc/regression/jbmc/trace_class_identifier/test.desc index 6b9e42530fa..1407c762c3a 100644 --- a/jbmc/regression/jbmc/trace_class_identifier/test.desc +++ b/jbmc/regression/jbmc/trace_class_identifier/test.desc @@ -1,7 +1,7 @@ CORE TestGenTest.class --function TestGenTest.f --trace --json-ui -"data": "java::TestGenTest",$ +"data": "(java::TestGenTest|TestGenTest@class_model)",$ ^EXIT=10$ ^SIGNAL=0$ -- From fe03ab9b7583a6512368b10d28fccd45014853ab Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Jan 2019 16:00:31 +0000 Subject: [PATCH 3/5] Accept base type equality Until we have resolved partial tag expansion everywhere we need to use base_type_eq for cases where both tags and expanded types may occur. --- src/solvers/strings/string_refinement.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 23b84598de7..944b775538a 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -329,7 +329,7 @@ static void add_equations_for_symbol_resolution( continue; } - if(lhs.type() != rhs.type()) + if(!base_type_eq(lhs.type(), rhs.type(), ns)) { stream << log_message << "non equal types lhs: " << format(lhs) << "\n####################### rhs: " << format(rhs) << eom; From 7e74b9713bf34c7affc22f6f1ad44b868439da7b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Jan 2019 16:03:30 +0000 Subject: [PATCH 4/5] String refinement: handle both struct and struct tag types struct tags need to be expanded. --- src/solvers/strings/string_refinement.cpp | 33 ++++++++++++++--------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 944b775538a..f1b158f7d6f 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -348,9 +348,9 @@ static void add_equations_for_symbol_resolution( else if( lhs.type().id() != ID_pointer && has_char_pointer_subtype(lhs.type(), ns)) { - if(rhs.type().id() == ID_struct) + if(rhs.type().id() == ID_struct || rhs.type().id() == ID_struct_tag) { - const struct_typet &struct_type = to_struct_type(rhs.type()); + const struct_typet &struct_type = to_struct_type(ns.follow(rhs.type())); for(const auto &comp : struct_type.components()) { if(is_char_pointer_type(comp.type())) @@ -374,20 +374,22 @@ static void add_equations_for_symbol_resolution( /// This is meant to be used on the lhs of an equation with string subtype. /// \param lhs: expression which is either of string type, or a symbol /// representing a struct with some string members +/// \param ns: namespace to resolve type tags /// \return if lhs is a string return this string, if it is a struct return the /// members of the expression that have string type. -static std::vector extract_strings_from_lhs(const exprt &lhs) +static std::vector +extract_strings_from_lhs(const exprt &lhs, const namespacet &ns) { std::vector result; if(lhs.type() == string_typet()) result.push_back(lhs); - else if(lhs.type().id() == ID_struct) + else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag) { - const struct_typet &struct_type = to_struct_type(lhs.type()); + const struct_typet &struct_type = to_struct_type(ns.follow(lhs.type())); for(const auto &comp : struct_type.components()) { const std::vector strings_in_comp = extract_strings_from_lhs( - member_exprt(lhs, comp.get_name(), comp.type())); + member_exprt(lhs, comp.get_name(), comp.type()), ns); result.insert( result.end(), strings_in_comp.begin(), strings_in_comp.end()); } @@ -396,10 +398,12 @@ static std::vector extract_strings_from_lhs(const exprt &lhs) } /// \param expr: an expression +/// \param ns: namespace to resolve type tags /// \return all subexpressions of type string which are not if_exprt expressions /// this includes expressions of the form `e.x` if e is a symbol subexpression /// with a field `x` of type string -static std::vector extract_strings(const exprt &expr) +static std::vector +extract_strings(const exprt &expr, const namespacet &ns) { std::vector result; for(auto it = expr.depth_begin(); it != expr.depth_end();) @@ -411,7 +415,7 @@ static std::vector extract_strings(const exprt &expr) } else if(it->id() == ID_symbol) { - for(const exprt &e : extract_strings_from_lhs(*it)) + for(const exprt &e : extract_strings_from_lhs(*it, ns)) result.push_back(e); it.next_sibling_or_parent(); } @@ -438,9 +442,12 @@ static void add_string_equation_to_symbol_resolution( } else if(has_subtype(eq.lhs().type(), ID_string, ns)) { - if(eq.rhs().type().id() == ID_struct) + if( + eq.rhs().type().id() == ID_struct || + eq.rhs().type().id() == ID_struct_tag) { - const struct_typet &struct_type = to_struct_type(eq.rhs().type()); + const struct_typet &struct_type = + to_struct_type(ns.follow(eq.rhs().type())); for(const auto &comp : struct_type.components()) { const member_exprt lhs_data(eq.lhs(), comp.get_name(), comp.type()); @@ -484,7 +491,7 @@ union_find_replacet string_identifiers_resolution_from_equations( if(required_equations.insert(i).second) equations_to_treat.push(i); - std::vector rhs_strings = extract_strings(eq.rhs()); + std::vector rhs_strings = extract_strings(eq.rhs(), ns); for(const auto &expr : rhs_strings) equation_map.add(i, expr); } @@ -492,7 +499,7 @@ union_find_replacet string_identifiers_resolution_from_equations( eq.lhs().type().id() != ID_pointer && has_subtype(eq.lhs().type(), ID_string, ns)) { - std::vector lhs_strings = extract_strings_from_lhs(eq.lhs()); + std::vector lhs_strings = extract_strings_from_lhs(eq.lhs(), ns); for(const auto &expr : lhs_strings) equation_map.add(i, expr); @@ -504,7 +511,7 @@ union_find_replacet string_identifiers_resolution_from_equations( << format(eq.lhs().type()) << eom; } - for(const exprt &expr : extract_strings(eq.rhs())) + for(const exprt &expr : extract_strings(eq.rhs(), ns)) equation_map.add(i, expr); } } From 74d15488dee69ec0f449a4fcd2c2ff4cdca19dde Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 27 Dec 2018 16:15:47 +0000 Subject: [PATCH 5/5] goto_symex: rename type symbols only when needed Renaming a type is rarely needed: this is necessary only if the type contains a struct that contains a variable-sized member, which is a gcc extension. The key benefit of not renaming in all other cases is that struct and union tag types no longer get expanded. --- src/goto-symex/goto_symex_state.cpp | 51 +++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 75910181510..e17c9ac23da 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -618,12 +618,63 @@ void goto_symex_statet::rename_address( } } +static bool requires_renaming(const typet &type, const namespacet &ns) +{ + if(type.id() == ID_array) + { + const auto &array_type = to_array_type(type); + return requires_renaming(array_type.subtype(), ns) || + !array_type.size().is_constant(); + } + else if( + type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class) + { + const struct_union_typet &s_u_type = to_struct_union_type(type); + const struct_union_typet::componentst &components = s_u_type.components(); + + for(auto &component : components) + { + // be careful, or it might get cyclic + if(component.type().id() != ID_pointer) + return requires_renaming(component.type(), ns); + } + + return false; + } + else if(type.id() == ID_pointer) + { + return requires_renaming(to_pointer_type(type).subtype(), ns); + } + else if(type.id() == ID_symbol_type) + { + const symbolt &symbol = ns.lookup(to_symbol_type(type)); + return requires_renaming(symbol.type, ns); + } + else if(type.id() == ID_union_tag) + { + const symbolt &symbol = ns.lookup(to_union_tag_type(type)); + return requires_renaming(symbol.type, ns); + } + else if(type.id() == ID_struct_tag) + { + const symbolt &symbol = ns.lookup(to_struct_tag_type(type)); + return requires_renaming(symbol.type, ns); + } + + return false; +} + void goto_symex_statet::rename( typet &type, const irep_idt &l1_identifier, const namespacet &ns, levelt level) { + // check whether there are symbol expressions in the type; if not, there + // is no need to expand the struct/union tags in the type + if(!requires_renaming(type, ns)) + return; // no action + // rename all the symbols with their last known value // to the given level