enable nondeterministic pointers #6326

kroening · 2021-09-01T12:49:09Z

This commit enables the use of nondeterministic pointers, to allow
declarative modeling of states that include pointers.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

danielsn · 2021-09-02T14:23:36Z

What would be the semantics for this case (slight modification of the previous test case)

int *nondet_pointer();

int main()
{
  int *q = nondet_pointer(); // Reordered to be 1st
  int x = 123;
  int *p = &x;

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

  return 0;
}

danielsn · 2021-09-02T14:25:36Z

Also

int *nondet_pointer();

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

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

  return 0;
}

jimgrundy · 2021-09-02T22:55:59Z

What would be the semantics for this case (slight modification of the previous test case)

int *nondet_pointer();

int main()
{
  int *q = nondet_pointer(); // Reordered to be 1st
  int x = 123;
  int *p = &x;

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

  return 0;
}

My expectation would be that q must be NULL because there are no other pointers to choose from when q is assigned, therefore the then clause of the conditional is unreachable and the assertion vacuously true.

jimgrundy · 2021-09-02T23:03:44Z

regression/cbmc/nondet-pointer/nondet-pointer2.c

+  int *py = &y;
+  int *q = nondet_pointer();
+
+  if(q == px || q == py)


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?

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

jimgrundy · 2021-09-02T23:09:16Z

Also

int *nondet_pointer();

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

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

  return 0;
}

Here I am expecting q must be either NULL or a pointer derived from p since that is the only pointer around. The assumption makes q equal to p and since it must have been derived from p it is safe to dereference and so I expect *q to be 123 and the assertion to pass.

remi-delmas-3000 · 2021-09-03T16:35:38Z

Would that last assertion pass or fail ?

int *nondet_pointer();

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

  if(p == q) {
      __CPROVER_assume(*q == 123);
      __CPROVER_assert(x == 123, "would that pass or fail ?");
  }
  return 0;
}

jimgrundy · 2021-09-07T00:04:57Z

We will have to put this one on hold for a bit. We discovered an unsoundness Friday when this is combined with the loop contracts feature. We will have to add some more checks to loop contracts to ensure we don't break soundness when this is added. I'll follow up with an explanation.

jimgrundy · 2021-09-07T13:30:27Z

We will have to put this one on hold for a bit. We discovered an unsoundness Friday when this is combined with the loop contracts feature. We will have to add some more checks to loop contracts to ensure we don't break soundness when this is added. I'll follow up with an explanation.

Maybe no issue. Will investigate further within a couple of days.

jimgrundy · 2021-09-09T19:06:16Z

Looks like there is not an issue with nondet_pointer ... only perhaps with when we should use it. Let's proceed with documenting this so we can merge it.

SaswatPadhi · 2021-09-10T12:08:38Z

Looks like there is not an issue with nondet_pointer ... only perhaps with when we should use it. Let's proceed with documenting this so we can merge it.

According to our offline discussions, the invalid pointers introduced by nondet_pointer don't work with existing IS_INVALID check. It would be nice if we could update that check as part of this PR to keep things consistent.

jimgrundy · 2021-09-10T23:52:14Z

@kroening Can you also make the necessary updates to the is_invalid check for consistency with this new feature?

jimgrundy · 2021-10-14T22:21:04Z

Did I see the IS_INVALID which we need to pair with this make it in via another PR?

SaswatPadhi · 2021-10-14T22:24:03Z

Did I see the IS_INVALID which we need to pair with this make it in via another PR?

Perhaps #6366

qinheping · 2021-10-20T23:14:59Z

regression/cbmc/nondet-pointer/nondet-pointer5.c

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


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.

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

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.

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.

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.

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

tautschnig · 2021-11-01T13:34:03Z

Shouldn't we also

include the invalid object in the list of candidate objects (just like NULL is included) and
amend https://github.com/diffblue/cbmc/blob/ce2680b724d650c404468eb0070c8b402735ec66/src/goto-symex/goto_symex_state.cpp#L823..L836 to use a nondet symbol (or perhaps provide a way to directly update the points-to set)?

This commit enables the use of nondeterministic pointers, to allow declarative modeling of states that include pointers.

codecov · 2021-11-29T13:29:15Z

Codecov Report

Merging #6326 (3789670) into develop (f5789d0) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #6326   +/-   ##
========================================
  Coverage    76.04%   76.04%           
========================================
  Files         1546     1546           
  Lines       165485   165494    +9     
========================================
+ Hits        125836   125858   +22     
+ Misses       39649    39636   -13

Impacted Files	Coverage Δ
src/pointer-analysis/value_set.cpp	`82.94% <100.00%> (+1.75%)`	⬆️
src/pointer-analysis/value_set_dereference.cpp	`95.03% <0.00%> (+0.33%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 0d62ff5...3789670. Read the comment docs.

martin-cs

Yes. I wonder if it should include an / the invalid object or some other kind of "this pointer points to something that is not accessible via other means" / "writes to this are effectively ignored" partially because that would be useful but also because hooks on this could be used to drive a refinement loop of "what input data structure is assumed".

martin-cs · 2021-11-30T17:42:51Z

src/pointer-analysis/value_set.cpp

+  {
+    if(expr.type().id() == ID_pointer)
+    {
+      // we'll take the union of all objects we see, with unspecified offsets


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.

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

kroening · 2021-12-01T11:45:15Z

@tautschnig will progress #6442, but we'll merge this for now.

kroening added the aws Bugs or features of importance to AWS CBMC users label Sep 1, 2021

jimgrundy reviewed Sep 2, 2021

View reviewed changes

kroening force-pushed the any_object branch 2 times, most recently from 5bc017d to b8b6272 Compare September 28, 2021 12:44

jimgrundy added the aws-high label Oct 14, 2021

qinheping reviewed Oct 20, 2021

View reviewed changes

tautschnig self-assigned this Nov 19, 2021

SaswatPadhi mentioned this pull request Nov 20, 2021

Add support for assigns clauses on loops #6249

Merged

5 tasks

enable nondeterministic pointers

3789670

This commit enables the use of nondeterministic pointers, to allow declarative modeling of states that include pointers.

tautschnig force-pushed the any_object branch from b8b6272 to 3789670 Compare November 29, 2021 11:57

tautschnig marked this pull request as ready for review November 30, 2021 14:00

tautschnig requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners November 30, 2021 14:00

tautschnig assigned peterschrammel and unassigned tautschnig Nov 30, 2021

tautschnig assigned martin-cs Nov 30, 2021

martin-cs approved these changes Nov 30, 2021

View reviewed changes

kroening merged commit d460e1c into develop Dec 1, 2021

kroening deleted the any_object branch December 1, 2021 11:45

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Aug 6, 2022

Temporarily revert diffblue#6326

d3f6368

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Aug 6, 2022

Temporarily revert diffblue#6326

6547191

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Aug 12, 2022

Temporarily revert diffblue#6326

517be07

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Aug 17, 2022

Temporarily revert diffblue#6326

f9592c0

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Aug 17, 2022

Temporarily revert diffblue#6326

fbb3379

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Sep 7, 2022

Temporarily revert diffblue#6326

2cc2a8d

tautschnig mentioned this pull request Oct 8, 2022

Incorrect encoding of function pointer operations in CBMC #7213

Open

qinheping mentioned this pull request Oct 18, 2022

Loop invariants cause va_list to fail #7199

Closed

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Nov 19, 2022

Temporarily revert diffblue#6326

b182458

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Nov 19, 2022

Temporarily revert diffblue#6326

182ac5c

peterschrammel added a commit to peterschrammel/cbmc that referenced this pull request Dec 4, 2022

Temporarily revert diffblue#6326

ad530bf

tautschnig mentioned this pull request May 19, 2023

Performance problem with --pointer-checks, --pointer-primitive-checks #7378

Closed

enable nondeterministic pointers #6326

enable nondeterministic pointers #6326

Uh oh!

Conversation

kroening commented Sep 1, 2021

Uh oh!

danielsn commented Sep 2, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

danielsn commented Sep 2, 2021

Uh oh!

jimgrundy commented Sep 2, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jimgrundy commented Sep 2, 2021

Uh oh!

remi-delmas-3000 commented Sep 3, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jimgrundy commented Sep 7, 2021

Uh oh!

jimgrundy commented Sep 7, 2021

Uh oh!

jimgrundy commented Sep 9, 2021

Uh oh!

SaswatPadhi commented Sep 10, 2021

Uh oh!

jimgrundy commented Sep 10, 2021

Uh oh!

jimgrundy commented Oct 14, 2021

Uh oh!

SaswatPadhi commented Oct 14, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jimgrundy Oct 28, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Nov 1, 2021

Uh oh!

codecov bot commented Nov 29, 2021

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Dec 1, 2021

Uh oh!

Uh oh!

danielsn commented Sep 2, 2021 •

edited

Loading

remi-delmas-3000 commented Sep 3, 2021 •

edited

Loading

jimgrundy Oct 28, 2021 •

edited

Loading