Linear Two-Variable Equalities Analysis

[alina-weber]

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.

[michael-schwarz]

For unreach-call, we gain 3 successful tasks and lose 3. One of the ones we lose is of this form:

// PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none --enable ana.int.interval
#include <goblint.h>

int main() {
    unsigned int n, r;
    r = n;

    __goblint_check(r == n); // works
    __goblint_check(-n + r == 0); // does not work

    return 0;
}

This seems justified, as there is an overflow coded into the assertion and our relational analysis in general is not overflow fit.

[michael-schwarz]

For valid-memsafety we lose 3 tasks.

[michael-schwarz]

I have now started a run for this on server01 so we can verify that we fixed the issue globally. After this, I think it would be a very good idea to land this.

done