Unassume witness invariants during solving

[sim642]

This PR adds an unassume analysis, which loads a YAML witness before solving and emits Unassume events during the analysis at nodes which have invariants. Both base, apron and var_eq analysis handle these events to make their local states less precise to immediately account for all states matching the invariant. Since the parsed invariants should be from a completed analysis, they correspond to the fixpoint. Thus unassuming the invariants allows the analysis to directly jump to that fixpoint. The benefits of this are two-fold:

1. It avoids widening-narrowing iterations to reach the same fixpoint, speeding up the analysis (hopefully).
2. It avoids widening jumping over fixpoints (especially with apron that cannot narrow), making the analysis more precise.

Changes

Besides the unassuming, many surrounding bigger and smaller changes are included:

1. Extract base analysis branch invariant out to a separate BaseInvariant module. This is a fairly large part of base analysis code, but sufficiently self-contained that it can be decoupled. The real reason for doing this was to use a slightly modified version of invariant for unassuming without a complete copy of invariant.
2. Add widening tokens, a dynamic way to delay widenings: http://www2.in.tum.de/bib/files/mihaila13widening.pdf. This turned out to be necessary, otherwise unassume itself causes a widening and becomes even less precise than intended.
3. Add witness.invariant.exact, which allows disabling the generation of exact equality invariants that are useless for unassuming.
4. Add witness.invariant.exclude-vars, which is a list of regexes for variable names that invariants should not be generated for. This can be tuned for sv-benchmarks which have already been CIL-led and contain awful amounts of temporaries.
5. Improve base branch refinement for address sets, interval bound non-equality and disjunctions of address/int equalities.

TODO

• [x] Emit Unassume events after all transfer functions, not just assign.
• [x] Support unassuming preconditioned invariants.
• [x] Support unassuming multithreaded invariants about globals (at locations)? This kind of requires us to first generate such invariants properly. (#833)
• [x] More precise unassuming than doing an assume on a top state and joining that in? In base, this probably would be an invariant-like recursive computation; in apron, not sure if anything better can be done.
• [x] Clean up and document widening tokens.

[sim642]

As discussed in GobCon, the idea of trying to unassume hints only once can be quite problematic and thus will not be added to this. In all the reasonable cases when witnesses have true invariants and they are unassumed conservatively (which isn't currently necessarily the case), narrowing down from an overly imprecise invariant should be unnecessary.

[sim642]

This is also a fairly big PR and has changes that often conflict with other changes on master, so it would be great to also get this merged soon.

[michael-schwarz]

I think once the comments are addressed and the adaptations necessary because of the new affeq analysis are made, this is ready to be merged.