goto_symex: rename type symbols only when needed [blocks: #3652] #3633
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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::Intf)\)\[email protected]\.@class_identifier | ||
| -- | ||
| ^warning: ignoring | ||
| -- | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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); | ||
|
There was a problem hiding this comment. 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. There was a problem hiding this comment. Oooh, I missed that, @kroening pretty sure this is a real bug There was a problem hiding this comment. (suggests a new test -- AFAIK GCC allows such variable-size structs?) There was a problem hiding this comment. 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. There was a problem hiding this comment. 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 | ||
|
|
||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
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_classshould ever evaluate to true. Aclassis represented asID_structwithID_C_classset totrue. If I'm wrong in saying this then we've got a lot more work to do elsewhere.There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#3635