Symbolically propagate assertions inside a basic block

[elazarg]

This is not going to be merged soon (if ever), it's just a demonstration of #258.

Assertion constraints are propagated backwards inside each basic block, with the ultimate goal of putting them at the start of the block. If this will be achieved, the checking phase will only involve checking them, and the analysis phase will never see them (unless --assume-assert is on).

In the process, many assertions (60% on average) are simply resolved, and many more can be resolved with more sophisticated propagation - for example, tracking cells as if they were registers, or using general expression instead of only registers and constants.

Ideally we'll simply use a constraint language instead of ebpf-specific assertions, and then implement symbolic simplification and join operations, but that would be even a larger change.