Skip to content

enable nondeterministic pointers #6326

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 1 commit into from
Dec 1, 2021
Merged

enable nondeterministic pointers #6326

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 1 addition & 3 deletions regression/cbmc/Pointer14/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
typedef unsigned int size_t;

void *malloc(size_t size);
void *malloc(__CPROVER_size_t);

enum blockstate
{
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/String_Abstraction14/pass-in-implicit.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
void *malloc(unsigned);
void *malloc(__CPROVER_size_t);

void use_str(char *s)
{
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/String_Abstraction20/structs2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
void *malloc(unsigned);
void *malloc(__CPROVER_size_t);

typedef struct str_struct
{
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ CORE
double_deref_with_pointer_arithmetic.c
--show-vcc
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1
^EXIT=0$
^SIGNAL=0$
--
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
double_deref_with_pointer_arithmetic_single_alias.c
--show-vcc
\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
\{1\} main::argc!0@1#1 = 1
^EXIT=0$
^SIGNAL=0$
--
Expand Down
13 changes: 13 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
int *nondet_pointer();

int main()
{
int x = 123;
int *p = &x;
int *q = nondet_pointer();

if(p == q)
__CPROVER_assert(*q == 123, "value of *q");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
nondet-pointer1.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
14 changes: 14 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
int *nondet_pointer();

int main()
{
int x = 123, y = 456;
int *px = &x;
int *py = &y;
int *q = nondet_pointer();

if(q == px || q == py)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why is it sufficient to test if q == px or q == py? Should we not also have to test same_object?
Why do I say that? Daniel has pointed out to me that we can construct two pointers that are equal but have different provenance and accessing one may cause an error.
Suppose y comes after x in memory. Suppose we choose q to be derived from px (&x) but with an offset large enough to point it at y. Now q == py ... but is it legal to dereference it and get 456, or should I expect failure?

Copy link
Member Author

Choose a reason for hiding this comment

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

Nondeterministic pointers are outside of the semantics of C; we can make that go either way.

__CPROVER_assert(*q == 123 || *q == 456, "value of *q");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
nondet-pointer1.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
18 changes: 18 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer3.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
int *nondet_pointer();

int main()
{
int some_array[10];
int *p = some_array;
int *q = nondet_pointer();
int index;

__CPROVER_assume(index >= 0 && index < 10);
__CPROVER_assume(q == p);

q[index] = 123;

__CPROVER_assert(some_array[index] == 123, "value of array[index]");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
nondet-pointer1.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
18 changes: 18 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer4.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
int *nondet_pointer();

int main()
{
int some_array[10];
int *p = some_array;
int *q = nondet_pointer();
int index;

__CPROVER_assume(index >= 0 && index < 10);
__CPROVER_assume(q == p + index);

*q = 123;

__CPROVER_assert(some_array[index] == 123, "value of array[index]");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
nondet-pointer1.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
19 changes: 19 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer5.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
int *nondet_pointer();

int main()
{
int some_array[10];
int *p = some_array;
int *q = nondet_pointer();
int index;

__CPROVER_assume(index >= 0 && index < 10);
__CPROVER_assume(__CPROVER_same_object(p, q));
Copy link
Collaborator

Choose a reason for hiding this comment

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

When I run cbmc --pointer-primitive-check nondet-pointer5.c, I got the following result

** Results:
nondet-pointer5.c function main
[main.pointer_primitives.1] line 11 dead object in POINTER_OBJECT((const void *)p): SUCCESS
[main.pointer_primitives.2] line 11 pointer outside object bounds in POINTER_OBJECT((const void *)p): SUCCESS
[main.pointer_primitives.3] line 11 pointer invalid in POINTER_OBJECT((const void *)q): FAILURE
[main.pointer_primitives.4] line 11 deallocated dynamic object in POINTER_OBJECT((const void *)q): SUCCESS
[main.pointer_primitives.5] line 11 dead object in POINTER_OBJECT((const void *)q): SUCCESS
[main.pointer_primitives.6] line 11 pointer outside object bounds in POINTER_OBJECT((const void *)q): FAILURE
[main.pointer_primitives.7] line 12 pointer invalid in POINTER_OFFSET((const void *)q): SUCCESS
[main.pointer_primitives.8] line 12 deallocated dynamic object in POINTER_OFFSET((const void *)q): SUCCESS
[main.pointer_primitives.9] line 12 dead object in POINTER_OFFSET((const void *)q): SUCCESS
[main.pointer_primitives.10] line 12 pointer outside object bounds in POINTER_OFFSET((const void *)q): FAILURE
[main.assertion.1] line 16 value of array[index]: SUCCESS

** 3 of 11 failed (3 iterations)

The trace showed that the offset of the pointer q exceeds the object size, which violates the pointer-primitive check
POINTER_OBJECT(NULL) == POINTER_OBJECT(q) || POINTER_OFFSET(q) >= 0l && OBJECT_SIZE(q) >= (unsigned long int)POINTER_OFFSET(q) + 1ul.

Copy link
Contributor

Choose a reason for hiding this comment

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

Yeah --pointer-primitive-check shouldn't look into offsets when we are just comparing same_object

Copy link
Collaborator

@jimgrundy jimgrundy Oct 28, 2021 •
edited
Loading

Choose a reason for hiding this comment

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

Hey Daniel (@kroening). We were wondering about this regression that fails with this PR. We don't really need the offsets to be in range for the pointers for same_object to have a well defined meaning do we? Is there another assumption we could/should add to make this go away? Should same_object be relaxed to not worry about the legality of the indexes? Other thoughts? Thanks.

Copy link
Member Author

Choose a reason for hiding this comment

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

Not an easy question. You realise that this could result in a situation whereby you've just asserted same_object, and then you see a concrete trace of the program where that very pointer points at the beginning of some other object.

I can live with that, given that the C standard has a notion of a pointer that points just beyond the end of a sequence, but this is a prime candidate for confusing users.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Yes, we do realize that. We're needing to constrain a pointer in a loop invariant such that as the pointer is iterated through the array it remains pointing to the same object. We'll then further constrain it to be inbounds for the array (or one beyond). To do this without warnings we need to shut off the assertion about the index being out of range in the same_object check. We'd like to keep the other sanity checks though. We could define our own version were we shut off all the pointer-primitive checks, but just locally for that one assertion ... if we had the ability to do that with a pragma, which is a request on another thread. If we had that we could more easily make progress ourselves. Or, we could implement a version with no primitives checks as a new primitive - but that seems heavyweight.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I have put up #6491 to adjust the behaviour of pointer-primitive-check.

__CPROVER_assume(__CPROVER_POINTER_OFFSET(q) == sizeof(int) * index);

*q = 123;

__CPROVER_assert(some_array[index] == 123, "value of array[index]");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/nondet-pointer/nondet-pointer5.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
nondet-pointer1.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
18 changes: 17 additions & 1 deletion src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,6 +505,23 @@ void value_sett::get_value_set_rec(
else
insert(dest, exprt(ID_unknown, original_type));
}
else if(expr.id() == ID_nondet_symbol)
{
if(expr.type().id() == ID_pointer)
{
// we'll take the union of all objects we see, with unspecified offsets
Copy link
Collaborator

Choose a reason for hiding this comment

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

I worry a little that the semantics of "nondet but only on objects that exist at the point it was nondet'd" might introduce some unexpected effects BUT I am not sure I have a better idea of a clearer semantics.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think @tautschnig has a 2nd PR in the works that addresses this concern, but it builds on this PR.

values.iterate([this, &dest](const irep_idt &key, const entryt &value) {
for(const auto &object : value.object_map.read())
insert(dest, object.first, offsett());
});

// we'll add null, in case it's not there yet
insert(
dest,
exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
offsett());
}
}
else if(expr.id()==ID_if)
{
get_value_set_rec(
Expand Down Expand Up @@ -984,7 +1001,6 @@ void value_sett::get_value_set_rec(
}
else
{
// for example: expr.id() == ID_nondet_symbol
insert(dest, exprt(ID_unknown, original_type));
}

Expand Down