__CPROVER_r/w_ok does not require null or a valid pointer #6416

kroening · 2021-10-26T19:02:13Z

The definition of __CPROVER_r/w_ok (in goto_check.cpp) does include the case
of an invalid pointer, and thus, there is no need to check that the pointer
given to these predicates is valid.

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.

tautschnig

Looks good to me, except I'd like to understand the rw_ok removal from documentation.

doc/architectural/memory-primitives.md

codecov · 2021-10-26T20:46:42Z

Codecov Report

Merging #6416 (f060b9c) into develop (f6fa03c) will increase coverage by 0.78%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6416      +/-   ##
===========================================
+ Coverage    75.98%   76.77%   +0.78%     
===========================================
  Files         1524     1546      +22     
  Lines       164299   171584    +7285     
===========================================
+ Hits        124843   131729    +6886     
- Misses       39456    39855     +399

Impacted Files	Coverage Δ
src/analyses/goto_check.cpp	`91.11% <100.00%> (+2.63%)`	⬆️
src/goto-instrument/loop_utils.cpp	`84.78% <0.00%> (-6.13%)`	⬇️
src/util/endianness_map.cpp	`73.33% <0.00%> (-3.34%)`	⬇️
src/goto-symex/symex_dead.cpp	`96.96% <0.00%> (-3.04%)`	⬇️
src/goto-symex/goto_symex.h	`90.00% <0.00%> (-2.31%)`	⬇️
src/goto-programs/read_bin_goto_object.cpp	`86.09% <0.00%> (-1.84%)`	⬇️
src/ansi-c/ansi_c_internal_additions.cpp	`89.71% <0.00%> (-0.65%)`	⬇️
src/goto-programs/goto_convert_class.h	`86.81% <0.00%> (-0.49%)`	⬇️
src/goto-symex/frame.h	`100.00% <0.00%> (ø)`
src/analyses/call_graph.h	`100.00% <0.00%> (ø)`
... and 100 more

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 07895ef...f060b9c. Read the comment docs.

feliperodri · 2021-10-26T20:58:31Z

doc/architectural/memory-primitives.md

+At present, all three primitives are equivalent as all memory in CBMC is considered
 both readable and writeable. If `p` is the null pointer, the primitives return
 false. If `p` is valid, the primitives return true if the memory segment


If size is zero, shouldn't this primitive return true even if the pointer is NULL or invalid? cc. @SaswatPadhi

+1. Intuitively, reading / writing "nothing" to any memory location could always (vacuously) succeed.

It's a design decision, however, and so we could choose to not do it this way and always for validity.
But currently there seems to be an issue with checking validity of a malloc(0) result. The standard says that it's not supposed to be deref'ed, so I am not exactly sure what "valid" would mean for the returned pointer.

char *p = malloc(0); assert(__CPROVER_r_ok(p, 0)); // fails with --pointer-primitive-check; passes otherwise

@feliperodri, correct me if I am wrong here, but this is what we observed, right?

I don't think we should attempt to give meaning to "zero width memory accesses".

I am perfectly happy for "__CPROVER_r_ok(p,0))" to fail if p is NULL or invalid.

But, I would want to dig a little into this example by looking at two cases (recall that an implementation of malloc is allowed to return a non-null value for malloc(0), though it may also return NULL):

char *p = malloc(0); if (p == NULL) { assert(__CPROVER_r_ok(p,0)); } else { assert(__CPROVER_r_ok(p,0)); }

Consider following cases:

First assert & pointer-primitive-checks enabled:

I'm OK with any outcome here: fail with pointer primitive check, fails because __CPROVER_r_ok returned false, or passes. I think Daniel would like this to fail with a pointer primitive check, and I can get on board with that.

First assert & pointer-primtive-checks disabled:

I'm OK with any outcome here: fails because __CPROVER_r_ok returned false, or passes

Second assert & pointer-primtive-checks enabled:

I'm of the opinion that this must pass

Second assert & pointer-primtive-checks disabled:

I'm of the opinion that this must pass

If cases 3 and 4 were to fail we're going to have to write a lot more special cases in our assertions than we need to handle degenerate cases where functions are called with size 0. Those special cases shouldn't be needed.

For case 1 - I think Daniel's desire to not give meaning to 0 size regions argues for keeping the expectation that this fails the pointer-primitive-check if that is enabled.

For case 2 - I'm not sure I care, but no matter whether you return true or false you are picking a meaning for a zero sized access to a NULL pointer.

I suppose I'm happy with undefined behavior when size is 0... because I can always defined my own version that is __jim_r_ok(p,size) = (size == 0) || __CPROVER_r_ok(p, size);
Mind you if I wanted something like __jim_r_ok that would fail if p was invalid even if size was 0 and pointer-checks were in abled I guess I would be out of luck. I can probably live with that too.

You can get the version that fails with size 0 simply like this:
(size == 0) ? 0 : __CPROVER_r_ok(p, size)

I meant when called with the -pointer-checks enabled would fail (not return false) with a pointer check error if called with __jim_r_ok(invalid-pointer,0).

Ah, apologies; I misunderstood.

feliperodri · 2021-10-26T21:04:05Z

cc. @jimgrundy @markrtuttle @remi-delmas-3000

kroening · 2021-10-27T08:58:20Z

Ok, let's do the following: __CPROVER_r/w_ok(p, s) is true when s is zero and p points either into the object, or at the byte that's just one beyond the object.

This implies that it's true when s is zero and p has offset zero and the object has size zero.

jimgrundy · 2021-10-27T13:15:42Z

I like very much where we ended up on this. Thanks Daniel.

This adds documentation for __CPROVER_rw_ok, in addition to r_ok and w_ok.

The definition of __CPROVER_r/w_ok (in goto_check.cpp) does include the case of an invalid pointer, and thus, there is no need to check that the pointer given to these predicates is valid.

Dead/deallocated objects still pose a problem.

tautschnig

The following example might serve to demonstrate why, in my opinion, this check should not be removed:

#include <stdlib.h>

int main()
{
  int *p = malloc(sizeof(int));
  free(p);
  __CPROVER_assume(__CPROVER_r_ok(p, sizeof(int)));
  __CPROVER_assert(0, "should be unreachable");
}

CBMC wrongly reports that this assertion is reachable (but --pointer-primitive-check calls out the problem in the assumption).

jimgrundy · 2021-12-01T18:17:46Z

Wouldn't I want __CPROVER_r_ok(p, sizeof(int)) in this case (p has just been free-ed) to return false rather than error out?

martin-cs · 2021-12-08T21:14:09Z

@tautschnig happy to review this when / if you are happy with the requested changes.

martin-cs · 2023-09-18T09:05:54Z

@tautschnig as #7395 is now merged, does this need to be revisited?

kroening force-pushed the cprover_r_ok_pointer_check branch from 7ec3a38 to a3f383b Compare October 26, 2021 19:25

kroening marked this pull request as ready for review October 26, 2021 20:01

kroening requested review from chrisr-diffblue, martin-cs, peterschrammel and tautschnig as code owners October 26, 2021 20:01

tautschnig reviewed Oct 26, 2021

View reviewed changes

doc/architectural/memory-primitives.md Show resolved Hide resolved

tautschnig assigned kroening Oct 26, 2021

feliperodri reviewed Oct 26, 2021

View reviewed changes

kroening force-pushed the cprover_r_ok_pointer_check branch 2 times, most recently from 878192a to 9663df6 Compare October 27, 2021 08:56

kroening force-pushed the cprover_r_ok_pointer_check branch 2 times, most recently from f10ef42 to 023e6e8 Compare October 27, 2021 09:46

feliperodri approved these changes Oct 27, 2021

View reviewed changes

feliperodri requested review from SaswatPadhi, tautschnig and jimgrundy October 27, 2021 17:49

feliperodri added the aws Bugs or features of importance to AWS CBMC users label Oct 27, 2021

kroening added 2 commits October 28, 2021 18:36

Document __CPROVER_rw_ok

3e8b6df

This adds documentation for __CPROVER_rw_ok, in addition to r_ok and w_ok.

__CPROVER_r/w_ok does not require null or a valid pointer

f060b9c

The definition of __CPROVER_r/w_ok (in goto_check.cpp) does include the case of an invalid pointer, and thus, there is no need to check that the pointer given to these predicates is valid.

kroening force-pushed the cprover_r_ok_pointer_check branch from 023e6e8 to f060b9c Compare October 28, 2021 17:37

tautschnig previously approved these changes Oct 28, 2021

View reviewed changes

tautschnig assigned peterschrammel and martin-cs and unassigned kroening Oct 28, 2021

jimgrundy linked an issue Nov 23, 2021 that may be closed by this pull request

Preconditions of cbmc library function memcpy are too strong #6472

Closed

tautschnig requested changes Dec 1, 2021

View reviewed changes

jimgrundy closed this Dec 1, 2021

jimgrundy reopened this Dec 1, 2021

kroening mentioned this pull request Dec 2, 2021

Split goto_check #6497

Merged

4 tasks

tautschnig mentioned this pull request Mar 15, 2022

Spurious pointer arithmetic errors #6705

Closed

SaswatPadhi removed request for SaswatPadhi and chrisr-diffblue September 17, 2022 23:56

__CPROVER_r/w_ok does not require null or a valid pointer #6416

Are you sure you want to change the base?

__CPROVER_r/w_ok does not require null or a valid pointer #6416

Uh oh!

Conversation

kroening commented Oct 26, 2021

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Oct 26, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

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!

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!

feliperodri commented Oct 26, 2021

Uh oh!

kroening commented Oct 27, 2021

Uh oh!

jimgrundy commented Oct 27, 2021

Uh oh!

tautschnig left a comment • 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!

jimgrundy commented Dec 1, 2021

Uh oh!

martin-cs commented Dec 8, 2021

Uh oh!

martin-cs commented Sep 18, 2023

Uh oh!

Uh oh!

codecov bot commented Oct 26, 2021 •

edited

Loading

tautschnig left a comment •

edited

Loading