Partitioned array imprecision with int annotations in interactive

[sim642]

I just merged master into interactive and now there are two failures due to the combination of partitioned arrays and int annotations:

Expected assert, but registered unknown on 22_01-simple_array:51
    assert(a[0] == 0);
Expected assert, but registered unknown on 22_01-simple_array:52
    assert(a[7] == 0);
Expected assert, but registered unknown on 22_01-simple_array:53
    assert(a[41] == 0);
Expected assert, but registered unknown on 22_01-simple_array:107
    assert(b[0] == 0);
Expected assert, but registered unknown on 22_01-simple_array:108
    assert(b[41] == 0);
42/08 annotated-precision/22_01-simple_array failed!

Expected assert, but registered unknown on 23_01-simple_array:49
    assert(a[0] == 0);
Expected assert, but registered unknown on 23_01-simple_array:50
    assert(a[7] == 0);
Expected assert, but registered unknown on 23_01-simple_array:51
    assert(a[41] == 0);
Expected assert, but registered unknown on 23_01-simple_array:105
    assert(b[0] == 0);
Expected assert, but registered unknown on 23_01-simple_array:106
    assert(b[41] == 0);
42/15 annotated-precision/23_01-simple_array failed!

2 tests failed: ["42/08 22_01-simple_array", "42/15 23_01-simple_array"]

Tracing evalint it appears to be that inside join for partitioned arrays, the indexing expression i - 1 is evaluated using the EvalInt query, but because this isn't happening inside any transfer function, the current_loc and current_node aren't set properly and thus the int annotation lookup bases its precision on a location not corresponding to the loop head in that function.

I'm not completely sure why this issue just reveals itself on interactive, but maybe it's due to the hardened current location unsetting using Fun.protect that ensures the resetting even with exceptions. Previously on exception the current location wasn't reset properly so the following join outside of transfer functions might have accidentally happened to use an appropriate location for the tests to still pass, but this definitely shouldn't be relied on.

[sim642]

Actually, I tried printing any exceptions from tf and there were none, so my first suspicion wasn't entirely right. I think it happens because of this change: https://github.com/goblint/analyzer/pull/391/commits/8bc2c89c94c2f22a7be95f8b959894b1ca3ca764. It changes a bit how the different evals and tfs nest and this seems to be enough to change which undetermined current_node still happened to be set at that point.

I think it previously just relied on the outer tfs current_node still being set when all the current tfs unset theirs and did the join. So it was using the wrong node, but it didn't matter because it was still in the same function with the same precision attributes, so no mismatch occurred.

[jerhard]

Reverting 8bc2c89 does indeed make both test case failures disapper. Still have to investigate on how to properly fix this.

[jerhard]

Even when not using the pval passed to the tf in line 697 by uncommenting the line here: https://github.com/goblint/analyzer/blob/1cf9b408a5846678103cc96a150767a29db3ab7e/src/framework/constraints.ml#L697-L700 the early evaluation of the stricts here: https://github.com/goblint/analyzer/blob/1cf9b408a5846678103cc96a150767a29db3ab7e/src/framework/constraints.ml#L729-L730 is somehow enough to cause the imprecision in the samples.

[sim642]

The difference is that the commented out old getl (u,c) would happen inside the Fun.protect where the current node has been already changed, whereas doing it outside of that (e.g. before in system directly), the currently set node hasn't been set yet, but corresponds to something up the call stack, which isn't necessarily in the same function.

I doubt it's just a matter of setting the current node early enough. Sure, it could probably fix this specific case, but that only affects the joins made in system directly, which is where the incoming edges get joined together. But there are also joins happening inside the solver and there's no sane way to wrap each one of those with corresponding current node updating.

The deeper problem is that the lattice operations for partitioned arrays somehow want to depend on the constraints, which is kind of the wrong way around.

[sim642]

Base analysis domain uses the following function to evaluate some local expressions inside the lattice operations:

val eval_exp: t  ->  Cil.exp -> IntOps.BigIntOps.t option

where t is the base analysis local domain.

One possible way of fixing this is to put the precision inside that local domain, such that it can be accessed outside of ctx or any location. And then pass this down through all the evaluation functions to ID.create where it's really needed. That would hopefully remove the dependence eval_exp has on some global OCaml variables, which can cause such unpredictable behavior.

[michael-schwarz]

The deeper problem is that the lattice operations for partitioned arrays somehow want to depend on the constraints, which is kind of the wrong way around.

No, not really. They actually only really depend on the entire CPA instead of on only the values inside. So in some sense, the proper domain here is the CPA for which it is totally reasonable that the lattice operations are not defined purely per-element. That this is then somehow delegated into these array domains is purely a question of our implementation.

I think as you pointed out the bigger problem is precision_from_node_or_config making assumptions about when it is called that do not actually hold.

[sim642]

I think as you pointed out the bigger problem is precision_from_node_or_config making assumptions about when it is called that do not actually hold.

That's what I meant by the lattice operation depending on the constraints: the current node is something related to a particular edge in the transfer function, rather than the abstract values we compute for them. This dependence is just very roundabout: instead of directly passing something from ctx to join, it's put into a global OCaml variable and then read on the other side.

[jerhard]

This dependence is just very roundabout: instead of directly passing something from ctx to join, it's put into a global OCaml variable and then read on the other side.

If we modify the join and meet to take a precision for the int domains, we would have to modify the signature of partial orders, or at least of the ValueDomain elements, and pass a precision on every join/meet. Or am I missing something?

[sim642]

I think that wouldn't be necessary, because it isn't ID.join, etc that need to know the precision (they already know the precision from their arguments!), but rather eval_* in the base analysis that doesn't. If the current precision is another component in the base analysis D, then it could directly be looked up from there in the base analysis, where the ID.create, which tries to access the precision from the current node, is used.

[jerhard]

What precision should the queries and e.g. the apron analysis use? In both, some IntDomTuple values are constructed. If one adapts the IntDomTuple to take a precision for all operations that create new values (of_int, of_bool etc.), then the precision would either have to be passed around in all analysis that use some IntDomTuple or one could go for some default precision (e.g. the globally configures one) that is then used everywhere except for the Base analysis.

[sim642]

Don't queries (Queries.ID) use the global precision currently anyway? Probably could just keep doing that. I think apron analysis only uses intdomains for responding to queries.

[jerhard]

If there is a current_node set, and annotation.int.enabled is enabled, the values constructed by the IntDomTuple will have the precision of the function the node is part of. That also holds for queries.

[jerhard]

@sim642 I had a look at trying to fix this with the approach of passing a precicision to all IntDomTuple functions that create new values (of_int, of_excl_list, of_interval, top_of ...), but this would require to change many of the ValueDomain functions (top_value, bot_value, zeroinit_value), take a precision as well, and to thread the precision basically everywhere through in the Base analysis. Making the precision so prominent throughout the code seems a bit excessive.

@michael-schwarz and I discussed this and had a longer look at the first example. When the join at the head of the loop in function example2 is performed, the current_node is set to the call site of example2 within main. The eval_int that is called by the smart_join within the partitioned array domain then evaluates whether i - 1 == 0. i has an integer value that come from the state of example2, with only the interval domain active, while the abstract value for 1 is freshly created, with only the DefExc domain active, as the current_node is set to a node in main. The computations on these abstract values yield an IntDomTuple-element with all domains being inactive, i.e. (None, None, None, None). Due to this value, the partitioned arrays do not know that it can do a precise join.

[jerhard]

It seems to me, that it would be more suited to ensure that the current_node is set correctly on a join than to pass the precision around in so many places.

[sim642]

It seems to me, that it would be more suited to ensure that the current_node is set correctly on a join than to pass the precision around in so many places.

It should be relatively easy to change this for the incoming edges join in FromSpec, because that's done explicitly there in the constraint system construction, no leaky abstraction.

But doing it for all the other joins, widens and leqs that the solvers call, this would require bunch of hacks in the solver, because only it knows which node (i.e. the left-hand side constraint variable) the domain elements it's currently joining correspond to.

[sim642]

The eval_int that is called by the smart_join within the partitioned array domain then evaluates whether i - 1 == 0. i has an integer value that come from the state of example2, with only the interval domain active, while the abstract value for 1 is freshly created, with only the DefExc domain active, as the current_node is set to a node in main. The computations on these abstract values yield an IntDomTuple-element with all domains being inactive, i.e. (None, None, None, None).

Maybe it would suffice for invariant to just create new constants with maximum (/global) precision and have the IntDomTuple operations project them down to whatever is actually used by the other values that have been created with the correct precision during the actual transfer functions, not during the joins. Since these precision projections already exist for making things compatible in combine, they could just be used for all the operations, no? And that would be completely based on the abstract values, not any information about the current node.