Improve handling of invalid pointers in assigns clause

[ArenBabikian]

CBMC version: 5.29.0
Operating system: Ubuntu20
Exact command line resulting in the issue: See below
What behaviour did you expect: n/a
What happened instead: n/a

---

The current implementation of the assigns clause considers the cross product of the writeable set (all the variable to which the program may write to) and the assigns clause set (all the variables included in the assigns clause). For example, let us consider the case where the writeable set contains A, B and the assigns clause set contains A', B'. When using the --enforce-contract flag with goto-instrument, every time a variable is defined, the generated goto program will assert the following: ( A == A' || A == B' ) && ( B == A' || B == B' ), while validating all elements in either set.

This is implemented here, where and element in the writeable set is represented by the called_target variable, while an element in the assigns clause set is represented by target.

The problem occurs when an invalid pointer is contained in the writeable set (which happens when an invalid pointer is passed as a parameter during a function call). In such a case, CBMC will try to validate the invalid pointer, which will cause an error.

A simple solution to this issue is proposed in #6077, however a better solution would involve checking the validity of writeable set elements during the creation of the goto program and handling invalid pointers as a special case regarding the generated assertion.

[SaswatPadhi]

A simple solution to this issue is proposed in #6077, however a better solution would involve checking the validity of writeable set elements during the creation of the goto program and handling invalid pointers as a special case regarding the generated assertion.

Just a bit of clarification:

Validity of the writeable set cannot always be established simply during the creation of goto program. It would require symbolic execution of the function.

But the optimisation that we can perform during goto program creation is to propagate constants as much as possible and detect some cases of invalid pointers (NULL is an obvious one, if it results out of constant prop). So the general check that you have introduced in #6077 is going to remain, but we could optimize it out (not generate it at all) in some cases.

[SaswatPadhi]

This issue has been fixed in #6365.