Skip to content

Simplify and avoid redundant typecasts in build_object_descriptor #4183

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 4 commits into from
Feb 14, 2019
Merged

Simplify and avoid redundant typecasts in build_object_descriptor #4183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2d72002
build_object_descriptor: avoid redundant typecasts
smowton Feb 13, 2019
992a3c3
Simplify object descriptor offset after construction
smowton Feb 13, 2019
8c231e9
Generics unit test: set integer widths
smowton Feb 14, 2019
7d0ce45
Remove now-unnecessary simplify after object_descriptor_exprt::build
smowton Feb 14, 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
2 changes: 2 additions & 0 deletions jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ SCENARIO(
"Instantiate generic parameters of superclasses",
"[core][goto_program_generics][generic_bases_test]")
{
config.ansi_c.set_LP64();

GIVEN(
"A class extending a generic class instantiated with a standard library "
"class")
Expand Down
2 changes: 0 additions & 2 deletions src/goto-symex/symex_clean_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,6 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
{
object_descriptor_exprt ode;
ode.build(expr, ns);
if(do_simplify)
simplify(ode.offset(), ns);

expr = ode.root_object();

Expand Down
24 changes: 13 additions & 11 deletions src/util/std_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
#include "expr_util.h"
#include "mathematical_types.h"
#include "pointer_offset_size.h"
#include "simplify_expr.h"

bool constant_exprt::value_is_zero_string() const
{
Expand Down Expand Up @@ -72,10 +73,11 @@ static void build_object_descriptor_rec(
exprt sub_size=size_of_expr(expr.type(), ns);
CHECK_RETURN(sub_size.is_not_nil());

dest.offset()=
plus_exprt(dest.offset(),
mult_exprt(typecast_exprt(index.index(), index_type()),
typecast_exprt(sub_size, index_type())));
dest.offset() = plus_exprt(
dest.offset(),
mult_exprt(
typecast_exprt::conditional_cast(index.index(), index_type()),
typecast_exprt::conditional_cast(sub_size, index_type())));
}
else if(expr.id()==ID_member)
{
Expand All @@ -87,9 +89,8 @@ static void build_object_descriptor_rec(
exprt offset=member_offset_expr(member, ns);
CHECK_RETURN(offset.is_not_nil());

dest.offset()=
plus_exprt(dest.offset(),
typecast_exprt(offset, index_type()));
dest.offset() = plus_exprt(
dest.offset(), typecast_exprt::conditional_cast(offset, index_type()));
}
else if(expr.id()==ID_byte_extract_little_endian ||
expr.id()==ID_byte_extract_big_endian)
Expand All @@ -100,10 +101,10 @@ static void build_object_descriptor_rec(

build_object_descriptor_rec(ns, be.op(), dest);

dest.offset()=
plus_exprt(dest.offset(),
typecast_exprt(to_byte_extract_expr(expr).offset(),
index_type()));
dest.offset() = plus_exprt(
dest.offset(),
typecast_exprt::conditional_cast(
to_byte_extract_expr(expr).offset(), index_type()));
}
else if(expr.id()==ID_typecast)
{
Expand Down Expand Up @@ -145,6 +146,7 @@ void object_descriptor_exprt::build(
offset()=from_integer(0, index_type());

build_object_descriptor_rec(ns, expr, *this);
simplify(offset(), ns);
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm a bit worried about the cost, can you check that callees don't currently run this after invoking build? (And if they do, remove it from those places.)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Checked, there was one redundant simplify (presumably working around the same issue). A couple of others use the offset to build a composite expression then simplify that, and so would have coincidentally dodged this problem. Some others uses ode.offset().is_zero(), which will probably have failed spuriously before when the offset was composite-but-constant.

}

shift_exprt::shift_exprt(
Expand Down