From 978d0b4af20325fba17b8e2b8719bebbf9edb82a Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 15:09:59 +0000 Subject: [PATCH 1/3] Base-type-eq: check pointer types really match Generally base-type-eq's task is to ensure that types match up to substitution of a type's body for a symbol referring to that type. However now that derivatives of pointers exist with named subexpressions (e.g. java_generic_parametert), it is now possible for types not involving symbols to be `base_type_eq` but not `==`. This resolves that particular case by checking that the names subexpressions match exactly. --- src/util/base_type.cpp | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index d98af3c5f9d..556f9017f46 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -253,6 +253,34 @@ bool base_type_eqt::base_type_eq_rec( } else if(type1.id()==ID_pointer) { + // Types dervied from pointer, such as java_generic_parametert, may have + // qualifiers given as named subexpressions: + const auto &named_subs1 = type1.get_named_sub(); + const auto &named_subs2 = type2.get_named_sub(); + + for(const auto &name_and_sub : named_subs1) + { + if(irept::is_comment(name_and_sub.first)) + continue; + auto other_sub = named_subs2.find(name_and_sub.first); + if( + other_sub == named_subs2.end() || + name_and_sub.second != other_sub->second) + { + return false; + } + } + + for(const auto &name_and_sub : named_subs2) + { + if(irept::is_comment(name_and_sub.first)) + continue; + auto other_sub = named_subs1.find(name_and_sub.first); + // Equality already checked above + if(other_sub == named_subs1.end()) + return false; + } + return base_type_eq_rec( to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype()); } From 76328dc44412679f7a127b121e02f292dd729822 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 1 Feb 2019 17:31:29 +0000 Subject: [PATCH 2/3] Java frontend: get qualified generic types of static fields Before it would unintentionally erase SomeClass.field from A to just the unqualified A type. --- .../java_bytecode_convert_method.cpp | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 320ef2c90aa..e3e9091a567 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1554,12 +1554,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( const bool is_assertions_disabled_field= field_name.find("$assertionsDisabled")!=std::string::npos; + const irep_idt field_id( + get_static_field(arg0.get_string(ID_class), field_name)); const symbol_exprt symbol_expr( - get_static_field(arg0.get_string(ID_class), field_name), arg0.type()); - - INVARIANT( - symbol_table.has_symbol(symbol_expr.get_identifier()), - "getstatic symbol should have been created before method conversion"); + symbol_table.lookup_ref(field_id).symbol_expr()); convert_getstatic( arg0, symbol_expr, is_assertions_disabled_field, c, results); @@ -1574,12 +1572,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( PRECONDITION(op.size() == 1 && results.empty()); const auto &field_name=arg0.get_string(ID_component_name); + const irep_idt field_id( + get_static_field(arg0.get_string(ID_class), field_name)); const symbol_exprt symbol_expr( - get_static_field(arg0.get_string(ID_class), field_name), arg0.type()); - - INVARIANT( - symbol_table.has_symbol(symbol_expr.get_identifier()), - "putstatic symbol should have been created before method conversion"); + symbol_table.lookup_ref(field_id).symbol_expr()); c = convert_putstatic(i_it->source_location, arg0, op, symbol_expr); } From 364aa68dfd8c0011a9d0cdefa07c7b01337b95f3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 1 Feb 2019 17:32:08 +0000 Subject: [PATCH 3/3] Symex-dereference: compare subtypes rather than making a pointer type just to compare This makes the invariant pass, but this surely warrants more attention -- type consistency is difficult to achieve when pointers are qualified and dereferencing and then taking the address again doesn't retain that information (but I don't know the logic behind the design decision in enough detail to change it) --- src/goto-symex/symex_dereference.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index f0395e45418..b50de7c98fd 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -238,7 +238,7 @@ exprt goto_symext::address_arithmetic( const typet &expr_type = expr.type(); INVARIANT((expr_type.id()==ID_array && !keep_array) || - base_type_eq(pointer_type(expr_type), result.type(), ns), + base_type_eq(expr_type, result.type().subtype(), ns), "either non-persistent array or pointer to result"); return result;