Linear Two-Variable Equalities Analysis

This pull request introduces an analysis for linear two variable equalities (ref: A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities). The structure of the analysis implementation is mostly based on the affine equality analysis (affeq).

The supported equalities are of the form x = y + c, where x is a variable and c is a constant. We also perform partial evaluation in some cases, e.g. when there is an assignment of the form x_1 = x_2 + x_3 - x_4 and we know that x_3 == x_2 and x_4 == x_2, then it follows that x_1 == x_2.

To enable the analysis, the parameter --set ana.activated[+] lin2vareq needs to be added.

Domain

Abstract states in this domain are represented by structs containing an optional array and an apron environment.
The bottom element is represented by a struct with "None" instead of the array.

The arrays are modeled as proposed in the paper: Each variable is assigned to an index and each array element represents a linear relationship that must hold at the corresponding program point.
The apron environment is used to organize the order of columns and variables.

The length of the array always corresponds to the number of variables in the environment.
If for example in the array at index j we store the element (Some i, k), this means that our analysis found out that x_i = x_j + k. If the array entry at index j is (None, k), it means that x_j = k, where k is a constant and x_i and x_j are variables.

Overflow handling

The overflow handling in affeq was spread over multiple files and wasn't very precise. We rewrote it in a more readable way and we exploited the interval analysis to check if there is an overflow in a certain expression.

The query MaySignedOverflow was added to the base analysis to handle possible overflow of signed integer expressions. Each subexpression is analyzed to see if an overflow happened. For each operator in the expression, we use the query EvalInt to approximate the bounds of each operand and we compute if in the worst case there could be an overflow.

This query is used by the domains affeq and lin2vareq in order to find expressions that possibly contain an overflow.

Casting

We found a bug in the analysis affeq, where casts where not properly handled. We fixed the bug for affeq and for our domain.

Refactoring of affeq

In order to have less code duplication, we moved some functions from affineEqualityDomain to sharedFunctions, such that affineEqualityDomain and our linearTwoVarEqualityDomain can both use them.