Fixes to pointer handling in goto_rw [depends-on: #2646]

[tautschnig]

1. This reverts commit 55d1297. Pointers require dereferencing, and taking an address of an object does not induce any reads on the object.
2. goto_rw tries to be over-approximating in its set of read/written objects, but had previously failed to do so in case of pointers. With the new fallback to __CPROVER_memory this ought to be resolved (albeit in a very coarse manner).

[tautschnig]

@lucasccordeiro This will affect the slicer - hopefully in a positive way.

[tautschnig]

While the changes would seem to be the right thing to do(TM) they break 3 slicing tests. I will investigate.

[lucasccordeiro]

@tautschnig: Thanks for letting me know. If you have doubts about the slicing tests, I'll be happy to clarify.

[martin-cs]

I'm fine with this although I note that @lucasccordeiro (i|wa)s the keeper of the slicer.

[tautschnig]

While I'm of course very much convinced that my changes are the right-thing-to-do(TM), it would be great to have input from @smowton and @lucasccordeiro.

[thk123]

I don't really know enough about what is going on here to provide meaningful comment, though it is surprising to be reverting such an old commit. Unfortunately, the original PR did not include any tests so hard to know whether what this was originally trying to fix remains fixed...

[tautschnig]

I don't really know enough about what is going on here to provide meaningful comment, though it is surprising to be reverting such an old commit.

I think the first time I committed this revert to some local branch was the day that I noticed its existence :-)

Unfortunately, the original PR did not include any tests so hard to know whether what this was originally trying to fix remains fixed...

Would @AnnaTrost be available (I heard rumors this might be the case) and be able to contribute some tests?

[smowton]

We may follow this up with upstreaming a patch from the security product, which identifies dynamic objects per allocation site (i.e. the same granularity as value_sett's dynamic_object* identifiers). However this is clearly a step in the right direction which we should take for now.

One concern: does goto-rw have any concept of a strong write (for example, x = 0; x = 1; return x; reading the second but not the first write to x)? If so, is there any danger it will think *heap_ptr1 = 0; *heap_ptr2 = 1; return *dynamic_ptr1; isn't using the first write, since both the derefs will resolve to __CPROVER_memory?

[TGWDB]

@tautschnig This PR seems to be in limbo, do you think you may update this and try to merge it, or should we close it due to age?

[TGWDB]

Closing this PR due to age and lack of clear direction. Please reopen if you believe this closure is erroneous and this will be updated/fixed.