Integrate formal SMT-based methods

[FrNecas]

This PR introduces an SMT-based comparison of short sequential snippets using Z3 solver. The general approach can be described as follows:

• when we find a difference and no pattern is applicable, try to check equivalence using an SMT solver
• the differing code snippets to be analyzed are determined based on searching for a synchronization point, i.e. a pair of instructions after which the code can be synchronized until the end of the basic block
• we construct a formula expressing the equivalence of the identified snippets -- if the inputs are the same and the blocks are executed, the outputs of the blocks must be the same. Since checking satisfiability is a hard problem, we apply a timeout.
• furthermore, the extension facilitates inverse-branching-condition pattern, e.g. it can detect a more complex change such as icmp slt %1, 101 being an inverse of icmp sgt %1, 100 if %1 is an integer.

Something to discuss:

• The new component is off by default and must be enabled using --use-smt. Do we always want to build this extension? The problem is that it introduces z3 as a dependency which is quite significant. However, since SMTBlockComparator is tightly coupled with DifferentialFunctionComparator, trying to exclude it from the build unless explicitly turned on would require quite a lot of preprocessor if-s. Furthermore, even if it was conditionally removed from simpll, it would still be part of the python frontend CLI which could be quite confusing.

Depends on: #323 #325 (needed for correct functionality in some more complicated cases, e.g. the KABI experiment)

[FrNecas]

Hm, trying to run this on the KABI experiments results in a segfault... I guess more debugging time :/

[lenticularis39]

Since LLVM is built for performance, it usually just segfaults when something goes wrong, one needs to extensively use GDB :D

[viktormalik]

• The new component is off by default and must be enabled using --use-smt. Do we always want to build this extension? The problem is that it introduces z3 as a dependency which is quite significant. However, since SMTBlockComparator is tightly coupled with DifferentialFunctionComparator, trying to exclude it from the build unless explicitly turned on would require quite a lot of preprocessor if-s. Furthermore, even if it was conditionally removed from simpll, it would still be part of the python frontend CLI which could be quite confusing.

I would say, let's not complicate things now and always build the extension in. If we wanted to make the z3 dependency optional, probably the easiest way is to have an alternative (ifdef-ed) version of SMTBlockComparator which has empty implementations of the exported functions.

FWIW, I would also love to make it on by default but IIRC, the overhead is still quite high, especially due to finding the snippets.

[FrNecas]

I've rebased the PR and addressed the comments (hopefully all of them, other than the more high-level comment if this should be a pattern or an option -- which we probably need to discuss more closely). This is probably ready to be reviewed again.