Symex: resolve class-identifier comparisons

[smowton]

Ideally we would resolve comparisons like x.@class_identifier == "A" using our existing constant
propagation framework. However, it only classifies a structured object as a constant if all its fields
are constant -- there is no scope for a part-constant object, in the way that @class_identifier is
initialised once and then cannot change subsequently.

Therefore, instead we enforce the invariant that @class_identifier must match the actual type of the
object x.

This significantly improves symex processing virtual function dispatch, as it can determine when certain
callees are unreachable, and so potentially vastly simplify the resulting formula.

This needs tests writing, but adding early for comment. I don't expect this to get in exactly as written, but some avenue to provide this sort of information is needed.

[tautschnig]

A few remarks:

1. Explicit nondet initialisation #35 may solve the underlying problem without further work.
2. I've got old patches lying around that make goto-symex field-sensitive. For C, this sometimes introduces overhead (because not all accesses are type-consistent), but for Java it might be a major improvement. (It's tautschnig@694d646 and the five commit following it. They are almost 4 years old, so will require a bit of work to rebase.)
3. It would seem to be a generally desirable idea to add a == b conditions to the constant propagator.
4. The newly proposed code is on a (very) hot path and needs careful benchmarking.

[smowton]

1. I don't think Explicit nondet initialisation #35 does the trick -- even if you initialize an object with { .@class_identifier = "java::A", .intfield = NONDET(int) }, as Explicit nondet initialisation #35 would permit, propagation of the constant @class_identifier will fail as soon as we assigned intfield with something non-constant, due to lack of field-sensitivity in const prop.
2. That would do the trick alright; my only worry is it'll be a lot of work getting the corner cases right, but I'm happy to have a go at rebasing this.
3. Not sure what you mean?
4. Agreed it'll need benchmarking, but not sure that's a highly optimised path to begin with -- after all, we just ran the whole SSA-rename and simplify gizmos over the expression, and this test is likely to fail fast for 99% of GOTOs

Possible courses of action:

1. Are you opposed to a special case just for RTTI fields, which are even easier to propagate than other constants since we don't need the const-prop data structure at all?
2. If you are, how about annotating such fields as constant (meaning their first non-decl write is definitive), then recording them, field-sensitive, against the l1 identifier when they are written, since they can't be overwritten? Then on the read side we could make an extra check when the outermost op is an ID_member referring to a constant field.
3. If that worked out, then you could extend this to C++ const fields, then experiment with more general field sensitivity.

My preference is to start with RTTI fields then go from there, since they're so easy to solve and so profitable when symex can resolve them. What do you think?

[smowton]

This one is harder than #2121 and #2125 to make less specific without lots of extra work to implement part or all of field sensitivity, and deal with whatever complications that raises.

I suggest permit the name @class_identifier to be magic for now as a stop-gap (this will be useful to other languages too, since RTTI inspection like this is common), then if and when we have a mature field-sensitive symex we can retire it as redundant.

[smowton]

Moving this to a private branch for now, as @kroening took the view this was too specific and the field sensitivity patch set should be used instead. Over to you on that bit @tautschnig as we don't have the bandwidth to revive and properly test the patchset in a reasonable timeframe.