New Analysis combining Linear Two-Variable Equalities with other domains

[leunam99]

This pull-request adds an analysis combining Lin2VarEq with multiple other domains: Intervals, Congruences and several options for two variable inequalities.

Lin2VarEq selects a representant for each group of variables connected by equalities. The other domains contain only information about representants and convert information about other variables from / to constraints for the respective representants.

[michael-schwarz]

We now have more tests on master, you should rename the new group to 88-....

[leunam99]

I am not sure why the regression test fail, as it runs locally. Do you have a suggestion how to debug this?

[sim642]

I am not sure why the regression test fail, as it runs locally. Do you have a suggestion how to debug this?

The CI artifact (https://github.com/goblint/analyzer/actions/runs/16374091305/artifacts/3564686204) should have the log files.

EDIT: The failing CI jobs are the pull_request ones, meaning the failure happens when this is merged with the current master.

[leunam99]

This query is what causes the regression test to output a warning:

%%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base query_evalint i % (unsigned int )(SIZE#in + 2)
  %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base eval_rv_base i % (unsigned int )(SIZE#in + 2)
    %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base eval_rv i
      %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base eval_rv_ask_evalint i
        %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base ask EvalInt i
          %%% evalint: base ask EvalInt i -> IntDomLifter(intdomtuple):8
        %%% evalint: base eval_rv_ask_evalint i -> 8
      %%% evalint: base eval_rv i -> 8
    %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base eval_rv (unsigned int )(SIZE#in + 2)
      %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base eval_rv_ask_evalint (unsigned int )(SIZE#in + 2)
        %%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  base ask EvalInt (unsigned int )(SIZE#in + 2)
          %%% evalint: base ask EvalInt (unsigned int )(SIZE#in + 2) -> IntDomLifter(intdomtuple):⊤
        %%% evalint: base eval_rv_ask_evalint (unsigned int )(SIZE#in + 2) -> ⊤
      %%% evalint: base eval_rv (unsigned int )(SIZE#in + 2) -> ⊤
[Warning][Integer > DivByZero][CWE-369] Second argument of modulo might be zero (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)
    %%% evalint: base eval_rv_base i % (unsigned int )(SIZE#in + 2) -> (Unknown int([0,32]),[0,8])
  %%% evalint: base query_evalint i % (unsigned int )(SIZE#in + 2) -> IntDomLifter(intdomtuple):(Unknown int([0,32]),[0,8])
%%% evalint: (tests/regression/88-lin2vareq_p/36-relations-overflow.c:14:3-14:17)  relation query i % (unsigned int )(SIZE#in + 2) (%(Lval(Var(i, NoOffset)), CastE(TInt(unsigned int, ), PlusA(Lval(Var(SIZE#in, NoOffset)), Const(Int(2,int,2))))))
  %%% evalint: relation st: (({rand=0 ∧ n₃₂₃=2 ∧ i₃₂₄=8 ∧ SIZE=1 }, {}, {})₄, ())
  %%% evalint: relation query i % (unsigned int )(SIZE#in + 2) -> IntDomLifter(intdomtuple):⊤

The expression contains a wrapper for a global variable, which base does not know about and (and the relational domain during the query doesn't either).
The query is almost exactly the same as in Convert.texpr1_expr_of_cil_exp. However, the simplification there never reaches the modulo expression, as the returned top-value does not pass the overflow check in the cast.
Changing the testcase to

int SIZE = 1;

int main() {
  int n=2,i=8;
  n = n + (i%SIZE); //NOWARN

  return 0;
}

lets me reproduce the error with lin2vareq as well.

I guess the solution with the most precision would be to adapt ask to work with these temporary variables.
I am also a bit surprised that AnalysisState.executing_speculative_computations does not prevent the warnings. If there is not a good reason for this, the simplest working solution could be to change that.

[sim642]

AnalysisState.executing_speculative_computations is for preventing warnings, but currently it's only checked for overflow warnings. There might be other places as well that should consider it.

[leunam99]

I would like to fix this not only for the specific circumstances here, but there are many places where similar messages could come from. Would it be a valid solution to check for this in Messages.msg (and similar)? Or would this suppress actually important things? Maybe the severity Debug should still be let through.

In addition, I think it could still be worth to come from the other direction as well: Could it be possible to modify ask so that it takes the relational domain with the added variables into account? Then at least the relational domain could answer queries that contain the global variable stand-ins instead of always using top for all globals.
I looked into it, but did not find where / how man.ask is actually created.

[sim642]

I would like to fix this not only for the specific circumstances here, but there are many places where similar messages could come from. Would it be a valid solution to check for this in Messages.msg (and similar)? Or would this suppress actually important things? Maybe the severity Debug should still be let through.

It's tempting to check AnalysisState.executing_speculative_computations at a high level, but I don't think it's a good idea. Currently the global flag is checked in a very small scope: just around producing the overflow warning (and setting the flag for SV-COMP). A similar check could be exactly around the recently-added zero-division warning.
This keeps the scope of global state as small as possible, as opposed to making it much broader as that would make it more difficult to easily get rid of it altogether at some point, e.g. in relation to our work on parallel solvers.

In addition, I think it could still be worth to come from the other direction as well: Could it be possible to modify ask so that it takes the relational domain with the added variables into account? Then at least the relational domain could answer queries that contain the global variable stand-ins instead of always using top for all globals.
I looked into it, but did not find where / how man.ask is actually created.

The man given to analyses is constructed in MCP, but that wouldn't be the right place to handle the relational-analysis renaming specifics. Rather, RelationAnalysis should maybe be creating a new wrapper ask that is given to relational domains because the analysis is what performs the mapping of globals.
Although, for example, RelationAnalysis query handles EvalInt queries by renaming the globals before using the domain. There might be other places where such things should take place. But I think generally the arguments of queries like EvalInt should not contain the in/out variables at all, because that will cause problems for other analyses.
If the relational analysis wants to query EvalInt itself on something, it might have to do the backwards mapping. If I remember correctly, read_globals_to_locals and read_globals_to_locals_inv do this in one direction or the other.

[leunam99]

I fixed the first part, and talked with Michael Petter about the second point.
We are not entirely sure if replacing the '#in' variables with the corresponding globals is completely sound.
Also, for using read_globals_to_locals_inv one would need a list of varinfos of all globals (and escaped vars). I did not yet find a good way to get them.

I hope that next week, we will be able to look into it further.