Better abstraction for state merging for the OH

[jennalwise]

Gradual Viper calls shortCircuitEval on expressions like the one in this if statement:

if (x == null || x.f == 3)

shortCircuitEval branches on Ands and Ors due to the nature of short circuiting. x == null executes and x.f == 3 executes with x != null on the path condition. However, at the end of evaluation the symbolic states along each execution path are merged. During evaluation optimistic framing is possible and is added to the OH. For example, for x.f == 3, x.f may be optimistically framed and so a run-time check for if (x != null) then acc(x.f) is generated. Note how the current path condition is used in the run-time check, which includes x != null from the short circuit Or.

Thus, acc(x.f) cannot be added in the merged states without corresponding path information, otherwise Gradual Viper would be unsound. So, a simple union for merging does not work. If heap chunks collected during each path are unioned, then the heap chunk for x.f would be used to justify a following heap access of x.f (such as in y := x.f) statically whether x == null or not. But, access to x.f has only been dynamically checked when x != null.

The current solution is to not add anything to the OH beyond the first conjunctive term (x == null in the current example). This is not satisfactory, because Gradual Viper is not able to leverage all the possible information it has to reduce run-time checks. Is there a better abstraction to define the OH that helps with this? Could be related to issue #14 . Maybe using a variation on intersection for merging can work? The new solution should of course be sound and adhere to the gradual guarantee.