Skip to content

goto_symex: rename type symbols only when needed [blocks: #3652] #3633

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

Merged
merged 5 commits into from
Jan 24, 2019
Merged

goto_symex: rename type symbols only when needed [blocks: #3652] #3633

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
abdbbbc
has_subtype: handle struct/union tag types
tautschnig Jan 23, 2019
3d9af8e
Make tests oblivious to tag type expansion
tautschnig Jan 23, 2019
fe03ab9
Accept base type equality
tautschnig Jan 23, 2019
7e74b97
String refinement: handle both struct and struct tag types
tautschnig Jan 23, 2019
74d1548
goto_symex: rename type symbols only when needed
Dec 27, 2018
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
51 changes: 51 additions & 0 deletions src/goto-symex/goto_symex_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I don't think type.id() == ID_class should ever evaluate to true. A class is represented as ID_struct with ID_C_class set to true. If I'm wrong in saying this then we've got a lot more work to do elsewhere.

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, these should be cleaned out.

Copy link
Member Author

Choose a reason for hiding this comment

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

#3635

{
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);
Copy link
Contributor

Choose a reason for hiding this comment

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

This only looks at the first non-pointer component of the struct, which is strange, but I cannot say whether this is correct because the function is not documented, so please document.

Copy link
Contributor

Choose a reason for hiding this comment

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

Oooh, I missed that, @kroening pretty sure this is a real bug

Copy link
Contributor

Choose a reason for hiding this comment

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

(suggests a new test -- AFAIK GCC allows such variable-size structs?)

Copy link
Collaborator

@tautschnig tautschnig Jan 24, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

I think I've found a way to construct a failing test, I'll post a follow-up PR to include a test, a fix, and the suggested documentation.

Copy link
Collaborator

Choose a reason for hiding this comment

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

The failure I thought I had found was one caused by integer overflow - I haven't actually managed to produce a proper failure. See #3918 for my attempt and the cleanup.

}

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

Expand Down