Skip to content

Fix value-set make_member function #3570

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 3 commits into from
Dec 17, 2018
Merged

Fix value-set make_member function #3570

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
71fc87d
get_subexpression_at_offset: use typecast_exprt for pointer-to-pointe…
smowton Dec 14, 2018
c1314ae
Value-set: replace unsound typecast simplification with simplify_expr
smowton Dec 14, 2018
8d88c97
Enable previously-failing test Linking7/member-name-mismatch
smowton Dec 14, 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
6 changes: 3 additions & 3 deletions regression/cbmc/Linking7/member-name-mismatch.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
KNOWNBUG
CORE
main.c
module2.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
line 21 assertion \*g\.a == 42: SUCCESS
line 22 assertion \*g\.c == 41: FAILURE
^\*\* 1 of 2 failed
--
^warning: ignoring
--
This is either a bug in goto-symex or value_sett (where the invariant fails).
2 changes: 2 additions & 0 deletions regression/cbmc/Linking7/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,5 +5,7 @@ module.c
^SIGNAL=0$
^VERIFICATION FAILED$
^\*\* 1 of 2 failed
line 21 assertion \*g\.a == 42: SUCCESS
line 22 assertion \*g\.b == 41: FAILURE
--
^warning: ignoring
1 change: 1 addition & 0 deletions scripts/delete_failing_smt2_solver_tests
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ rm Float6/test.desc
rm Float8/test.desc
rm Linking4/test.desc
rm Linking7/test.desc
rm Linking7/member-name-mismatch.desc
rm Malloc19/test.desc
rm Malloc23/test.desc
rm Malloc24/test.desc
Expand Down
35 changes: 4 additions & 31 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1630,37 +1630,10 @@ exprt value_sett::make_member(
const struct_union_typet &struct_union_type=
to_struct_union_type(ns.follow(src.type()));

if(src.id()==ID_struct ||
src.id()==ID_constant)
{
std::size_t no=struct_union_type.component_number(component_name);
assert(no<src.operands().size());
return src.operands()[no];
}
else if(src.id()==ID_with)
{
assert(src.operands().size()==3);

// see if op1 is the member we want
const exprt &member_operand=src.op1();

if(component_name==member_operand.get(ID_component_name))
// yes! just take op2
return src.op2();
else
// no! do this recursively
return make_member(src.op0(), component_name, ns);
}
else if(src.id()==ID_typecast)
{
// push through typecast
assert(src.operands().size()==1);
return make_member(src.op0(), component_name, ns);
}

// give up
const typet &subtype = struct_union_type.component_type(component_name);
member_exprt member_expr(src, component_name, subtype);
exprt member_expr = member_exprt(src, component_name, subtype);

simplify(member_expr, ns);

return std::move(member_expr);
return member_expr;
Copy link
Collaborator

Choose a reason for hiding this comment

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

I believe this should stay as return std::move(member_expr);

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Not so! It's type now matches the return type, so I leave it out and enable RVO. I hope a forthcoming version of C++ renders this distinction unnecessary...

Copy link
Collaborator

Choose a reason for hiding this comment

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

Oops, sorry, I ignored that you had used exprt member_expr ....

}
7 changes: 7 additions & 0 deletions src/util/pointer_offset_size.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -655,6 +655,13 @@ exprt get_subexpression_at_offset(
return result;
}

if(
offset_bytes == 0 && expr.type().id() == ID_pointer &&
target_type_raw.id() == ID_pointer)
{
return typecast_exprt(expr, target_type_raw);
}

const typet &source_type = ns.follow(expr.type());
const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
if(!target_size_bits.has_value())
Expand Down