Support joins during runtime check collection across branches

[hgouni]

Silicon supports joining branches with pure bodies during program execution, as an optimization over separately symbolically executing each branch. The collection of runtime checks requires, for each generated check, precise information about the path taken through the program for that check. Joining branches would require branching information to be separately tracked by (or alongside) the runtime check synthesizer. We should figure out a way to track branching information while both collecting runtime checks and supporting joins.

[jennalwise]

The rule for "unfolding in" expressions in Viper also relies on joins, so this may be important for this as well. Reducing the number of branches with join will improve Gradual Viper performance and if run-time checks could match, then likely performance in the C0 frontend could also be improved.

[jennalwise]

Consume originally consumed pure conditionals (conditionals that do not refer to heap locations) in eval using evalAndAssert. However, the case for pure conditionals in eval was removed, because the only thing it did differently for consume was to use joins, which we do not support. The case for impure conditionals in consume now applies to all conditionals no matter what. It seems the only downside is the performance losses from joins for the pure case.