Killing `#return_value` behaves inconsistently

[smowton]

Suppose we have f like:

f { if(nondet) return new A(); else throw new B(); }

On the first call to f, the two arms of the if produce value sets { f#return_value -> { dynamic_object1 }, @inflight_exception -> { null } } and { @inflight_exception -> { dynamic_object2 } } respectively. These merge "cleanly" to give { f#return_value -> { dynamic_object1 }, @inflight_exception -> { null, dynamic_object2 } } allowing the caller to proceed as if the return value is certainly a pointer to DO1. However, the caller then runs

DEAD f#return_value

This leads to a value-set f#return_value -> { f#return_value$object }, which is different to the value-set we had when the program started before it was referenced at all.

Then when we call f again, our two value sets are:
{ f#return_value -> { dynamic_object1 }, @inflight_exception -> { null } } and { f#return_value -> { f#return_value$object }, @inflight_exception -> { dynamic_object2 } }

These merge to produce { f#return_value -> { dynamic_object1, f#return_value$object }, @inflight_exception -> { null, dynamic_object2 } }, and the caller's certainty that f#return_value has a single determined referee is suddenly gone.

One of these behaviours is wrong (the two calls should behave the same): either f#return_value should have been initialised with f#return_value$object, or the DEAD should delete it from the value-set completely. But which?

[tautschnig]

I believe the problem is that we do DEAD f#return_value even though we never have a declaration for f#return_value. The latter actually seems right, because it has static lifetime. Killing f#return_value seems wrong.

[smowton]

Note if you just skip the DEAD instruction then you'll get the same inaccuracy except we'll believe it may have it's old value, rather than the special dead value. The inconsistency between first and second call will remain

[smowton]

Further thoughts:

1. In some dialects of C it's possible to compile functions that don't return on some or all paths, even if their type indicates they should. Presumably we want to detect that in the same way that we detect use of an uninitialised local or field of a dynamic object. This suggests we ought to initialise the #return_value variable, or treat absence from the value-set the same as having the $object reference there. Alternatively if you're happy to disregard this source of undefined behaviour (as currently happens on the first call) then we should ignore it the same way each time.
2. In Java we have a source-language guarantee that there are no paths where the return value is undefined, except for those which throw. I have a plan to solve that by threading control-flow from the END_FUNCTION to the immediate-successor exception check, but this might be overkill if we can solve the problem by appropriate value-set management rules.
3. Whether we decide that DEAD means clearing the value-set or storing a special undefined value, we could achieve consistency by executing it before rather than after the call. Such a DEAD would better be called "FRESH", or indeed "DECL" except in that that would be pretty confusing considering it's a global.
4. We should clarify what value_sett is designed to achieve here. At present I would say it under-approximates the true alias set, since two undefined variables x and y are assumed not to alias (they point to x$object and y$object respectively), and value-set union where some values are not defined at all on the other branch ignores the missing values rather than introducing an unknown value. If that is intended I would say it's consistent to either (a) remove an entry from the value-set completely on a DEAD instruction, or equivalently (b) on a merge with a $object or other pessimistic value, discard the pessimistic value.

[smowton]

Partial solution: #4343