Skip to content

Base-type-eq: check pointer types really match [blocks: #4023] #4020

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 3 commits into from
Closed

Base-type-eq: check pointer types really match [blocks: #4023] #4020

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
978d0b4
Base-type-eq: check pointer types really match
smowton Jan 10, 2019
76328dc
Java frontend: get qualified generic types of static fields
smowton Feb 1, 2019
364aa68
Symex-dereference: compare subtypes rather than making a pointer type…
smowton Feb 1, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 6 additions & 10 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
}
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/symex_dereference.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
28 changes: 28 additions & 0 deletions src/util/base_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please use two iterators over the two collections, just like irept::operator== does. Using find is expensive and unnecessary as you can do this with a linear algorithm.

{
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());
}
Expand Down