Skip to content

fix flattening of ID_invalid_pointer #2630

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 2 commits into from
Jul 30, 2018
Merged

fix flattening of ID_invalid_pointer #2630

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9b5847e
fix flattening of ID_invalid_pointer
Jul 30, 2018
060b59c
separate pointer check for integer addresses
Jul 30, 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
2 changes: 1 addition & 1 deletion regression/cbmc/Malloc23/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE
pointer outside dynamic object bounds in \*p: FAILURE
pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
\*\* 4 of 36 failed
\*\* 4 of [0-9]+ failed
--
^warning: ignoring
2 changes: 1 addition & 1 deletion regression/cbmc/bounds_check1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ main.c
\[\(.*\)i2\]: FAILURE
dest\[\(.*\)j2\]: FAILURE
payload\[\(.*\)[kl]2\]: FAILURE
\*\* 10 of 72 failed
\*\* 10 of [0-9]+ failed
--
^warning: ignoring
\[\(.*\)i\]: FAILURE
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc/memcpy1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.16\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed (long (long )?)?int\)n\) - (\(signed long (long )?int\))?1\): FAILURE$
\*\* 1 of 17 failed
\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.[0-9]+\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed (long (long )?)?int\)n\) - (\(signed long (long )?int\))?1\): FAILURE$
\*\* 1 of [0-9]+ failed
--
^warning: ignoring
8 changes: 4 additions & 4 deletions regression/cbmc/memory_allocation1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ main.c
--pointer-check
^EXIT=10$
^SIGNAL=0$
\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*p: SUCCESS
\[main.assertion.1\] assertion \*p==42: SUCCESS
\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
\[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
^\[main\.pointer_dereference\.2\] dereference failure: invalid integer address in \*p: SUCCESS$
Copy link
Collaborator

Choose a reason for hiding this comment

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

Huh? I'm finding it hard to reconcile this with the commit message.

^\[main\.assertion\.1\] assertion \*p==42: SUCCESS$
^\[main\.pointer_dereference\.[0-9]+\] dereference failure: invalid integer address in p\[.*1\]: FAILURE$
^\[main\.assertion\.2\] assertion \*\(p\+1\)==42: SUCCESS$
^VERIFICATION FAILED$
--
^warning: ignoring
27 changes: 17 additions & 10 deletions src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1003,8 +1003,7 @@ void goto_checkt::pointer_validity_check(
guard);
}

if(flags.is_unknown() ||
flags.is_integer_address())
if(flags.is_unknown())
add_guarded_claim(
or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
"dereference failure: pointer invalid",
Expand All @@ -1023,8 +1022,7 @@ void goto_checkt::pointer_validity_check(
guard);

if(flags.is_unknown() ||
flags.is_dynamic_heap() ||
flags.is_integer_address())
flags.is_dynamic_heap())
add_guarded_claim(
or_exprt(allocs, not_exprt(deallocated(pointer, ns))),
"dereference failure: deallocated dynamic object",
Expand All @@ -1034,8 +1032,7 @@ void goto_checkt::pointer_validity_check(
guard);

if(flags.is_unknown() ||
flags.is_dynamic_local() ||
flags.is_integer_address())
flags.is_dynamic_local())
add_guarded_claim(
or_exprt(allocs, not_exprt(dead_object(pointer, ns))),
"dereference failure: dead object",
Expand All @@ -1045,8 +1042,7 @@ void goto_checkt::pointer_validity_check(
guard);

if(flags.is_unknown() ||
flags.is_dynamic_heap() ||
flags.is_integer_address())
flags.is_dynamic_heap())
{
const or_exprt dynamic_bounds(
dynamic_object_lower_bound(pointer, ns, access_lb),
Expand All @@ -1067,8 +1063,7 @@ void goto_checkt::pointer_validity_check(

if(flags.is_unknown() ||
flags.is_dynamic_local() ||
flags.is_static_lifetime() ||
flags.is_integer_address())
flags.is_static_lifetime())
{
const or_exprt object_bounds(
object_lower_bound(pointer, ns, access_lb),
Expand All @@ -1082,6 +1077,18 @@ void goto_checkt::pointer_validity_check(
expr,
guard);
}

if(flags.is_unknown() ||
flags.is_integer_address())
{
add_guarded_claim(
implies_exprt(integer_address(pointer), allocs),
"dereference failure: invalid integer address",
"pointer dereference",
expr.find_source_location(),
expr,
guard);
}
Copy link
Collaborator

Choose a reason for hiding this comment

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

I suppose this change and what I mourned above just need to be moved into a separate commit.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

}
}

Expand Down
13 changes: 3 additions & 10 deletions src/solvers/flattening/bv_pointers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,26 +29,19 @@ literalt bv_pointerst::convert_rest(const exprt &expr)

if(!bv.empty())
{
bvt invalid_bv, null_bv;
bvt invalid_bv;
encode(pointer_logic.get_invalid_object(), invalid_bv);
encode(pointer_logic.get_null_object(), null_bv);

bvt equal_invalid_bv, equal_null_bv;
bvt equal_invalid_bv;
equal_invalid_bv.resize(object_bits);
equal_null_bv.resize(object_bits);

for(std::size_t i=0; i<object_bits; i++)
{
equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
invalid_bv[offset_bits+i]);
equal_null_bv[i] =prop.lequal(bv[offset_bits+i],
null_bv[offset_bits+i]);
}

literalt equal_invalid=prop.land(equal_invalid_bv);
literalt equal_null=prop.land(equal_null_bv);

return prop.lor(equal_invalid, equal_null);
return prop.land(equal_invalid_bv);
}
}
}
Expand Down