Adds --expand-pointer-predicates to goto-instrument [depends-on: #3769, blocks #2706]

[qaphla]

This builds on #2635.
The only new commit since then is 9be31ff.

This adds a new built-in predicate, __CPROVER_points_to_valid_memory, and provides the --expand-pointer-predicates pass to goto-instrument to handle the side effects that it has in assumptions. More detail can be found in the commit message.

This differs from #2602 in that unlike __CPROVER_r_ok and __CPROVER_w_ok, __CPROVER_points_to_valid_memory(ptr, size) will, when used in an assumption, ensure that there is a suitable memory object at ptr by creating one if necessary. It is, however, likely that __CPROVER_points_to_valid_memory can be made to take advantage of __CPROVER_r/w_ok in its implementation once those make it into develop.

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: dd6c63c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80542769
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

[smowton]

Made a few inline comments on the new commit. Broader points:

(1) what relation if any does this have to the existing memory validity checks introduced by goto_check? Should this be using parts of goto-check instead of implementing a new way of introducing checks?

(2) It seems odd that the meaning of the predicate is remarkably different in assume context from assert context (and not implemented at all in expression or GOTO-guard context). Should these be different operations?

[qaphla]

(1) As used in assertions, __CPROVER_points_to_valid_memory(ptr, size) corresponds exactly to the validity checks introduced by goto_check given an access to the 0th byte and the size - 1th byte of ptr. I think it is still useful to have a syntax for generating these checks more concisely than writing down those two dereferences and letting --pointer-check generate them. That said, the assertion portion of this could easily be put into goto-check (as it should be, when cleaned up, identical to #2602, which is built inside goto-check).

The assumption portion is the main feature that prompted me to develop this, and probably could be put into goto_check if desired, but that seems a bit strange to me, as goto_check seems to deal entirely (almost entirely? I'm not sure what enable_assert_to_assume is doing) with assertions and inserting checks for properties.

(2) I am admittedly biased, but it doesn't seem strange at all to me that the implementation of the predicate is different in assume and assert contexts. The expression resulting from expanding the predicate is the same in both cases, and the only difference is that in assume context, we add an additional set of instructions to create a new memory object for ptr to refer to if none exists. It appears that if no sch object exists, then assumptions about POINTER_OBJECT(ptr) or POINTER_OFFSET(ptr) do not accomplish anything, and so to get anything useful out of the assumptions, we need to ensure than such an object exists. In most cases, I agree, #2602's method is sufficient. This feature arose from work on contracts and the desire to analyze pieces of code in isolation, where it is useful to be able to make such assumptions and not have to worry about setting up a harness that creates objects for each pointer. This use case also provides the reason that I would like to have a single predicate that works like this in both assume and assert contexts, as I would like to be able to write down one contract which can be either assumed or asserted in the correct locations (e.g. a precondition should be asserted before the function call, and assumed at the beginning of the code that checks the function), which having two separate predicates would prevent. This is also why I have only addressed assume and assert contexts, though thinking further about it, it seems that the only real distinction that needs to be made is between assume contexts and everything else. This is an easy enough change to make, but should probably wait until it's clearer whether this belongs in goto_check or not. (I think it likely that it does, but need to figure out how to handle adding assumptions in goto_check).

[smowton]

Hmm. My instinct is the harness should do the right thing (e.g. when verifying Java we should usually offer a nondet choice between NULL and a fresh object), and the meaning of the predicate should be the same in all contexts, but more senior people (@peterschrammel @tautschnig @kroening) may differ.

[martin-cs]

I see and agree with @smowton 's concerns about the asymmetry of the semantics of this. I also, very much, see your use case and wanting to be able to generate sane harnesses with a minimal amount of hassle. However I'm not sure this is the right way of going about things. Assuming that something points to a valid location is not the same as assuming that there is a new, unique location that it points to. I think this approach may run into a lot of complexity around aliasing.

To my mind the right way of approaching this problem is to have a dual to generate-function-bodies that generates a calling harness (either 1 shot or dynamically builds one up using verification failures) for an arbitrary piece of code. Assumptions about writeability could be used in that to build a sensible context.

[TGWDB]

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.