DefExc.widen Excluded range to static size instead of join

[vogler]

In DefExc we currently have let widen = join.
As I see it, this causes extra iterations for little to no gain.

Consider this loop:

int main() {
  int i = 0;
  while (i < 10)
    i++;
  return i;
}

The excluded range via join already does something like a threshold widening by going through the intermediate int sizes (i++ overflows range) before reaching the static type:

i -> (0,[0,0])
i -> (Unknown int([0,7]),[0,9])
i -> (Unknown int([0,8]),[0,9])
i -> (Unknown int([0,16]),[0,9])
i -> (Unknown int([-31,31]),[0,9])
i -> (Unknown int([-31,31]),[0,9])

Instead of doing this, one can jump to the static type directly for widen and only keep this stepwise behavior for join.

$ ./goblint wp.c --html --enable ana.int.interval --trace sol2 2>&1 | grep ' solve node 79' | wc -l
11

from 15 calls to solve without this change.

I tried to find an example where you would get a less precise exclusion range.
But here for i we already have [-31,31] with widen = join:

int main () {
  for (int i = 0; i < 10; i++) {
    char j = 0;
    for (; j < 10; j++) ;
    i = j;
    j = 0;
  }
}

I guess you can construct some example where you widen some value in a loop that is not changed each iteration but only joined from some branches.
However, the saved iterations for every int loop probably outweigh this loss.

[sim642]

The let widen = join definitions actually are overall unnecessary I think, because we always call it like widen old (join old new), so the default implementation might as well just return the second argument (which is what StdCousot previously did by default as well).

This of course doesn't change anything w.r.t. the number of solves, but just avoids a useless idempotent join. But it also means that widen need not do the joining, but just widen the range to the type's directly. Correspondingly, I think one could then define narrow to simply decrease it. That should even give the precision back, no?

[vogler]

The let widen = join definitions actually are overall unnecessary I think, because we always call it like widen old (join old new), so the default implementation might as well just return the second argument (which is what StdCousot previously did by default as well).

Was that how we left it? I.e. inlined all StdCousot and made all solvers join the right argument of widen?
This claims so:

analyzer/src/domains/lattice.ml

Line 21 in ef58842

val widen: t -> t -> t (** [widen x y] assumes [leq x y]. Solvers guarantee this by calling [widen old (join old new)]. *)

However, searching widen old [^(], there's:

analyzer/src/solvers/sLR.ml

Line 68 in ef58842

if HM.mem globals x then S.Dom.widen old tmp

analyzer/src/solvers/topDown_term.ml

Line 89 in b52b784

HM.replace rho' y (S.Dom.widen old d);

This of course doesn't change anything w.r.t. the number of solves, but just avoids a useless idempotent join. But it also means that widen need not do the joining, but just widen the range to the type's directly.

Not sure the useless join is relevant. Depends on how confident we are that we (currently and in the future) enforce the join.
If you don't, it may be unsound?

Correspondingly, I think one could then define narrow to simply decrease it. That should even give the precision back, no?

Currently we have let narrow ik x y = x.
Is there an example where we lose precision?

[michael-schwarz]

Depends on how confident we are that we (currently and in the future) enforce the join. If you don't, it may be unsound?

I would leave it as it is, unless there are masisve performance benefits to removing the joins. I think it is hard to ensure that everyone does it all the time in the future.

[vogler]

So, merge like this or should we think about some example where it's less precise?

---

Sample:
./goblint -v --enable ana.int.interval ../bench/single-thread/maradns-1.4.06_zoneserver_comb.c

vars = 72285    evals = 198766
TOTAL                          140.110 s

vars = 71882    evals = 183300
TOTAL                          128.044 s

./goblint -v ../bench/single-thread/maradns-1.4.06_zoneserver_comb.c

vars = 70682    evals = 176607
TOTAL                          113.898 s

vars = 70161    evals = 168915
TOTAL                          108.063 s

[sim642]

Was that how we left it? I.e. inlined all StdCousot and made all solvers join the right argument of widen?
This claims so:

I think we didn't change it because it's what was almost always done. And we've definitely had domains which assume that, e.g. intervals: #414.
I think I added the comment to make it explicit, but maybe never checked all the usages.

I suppose to be on the safe side, we should change those two solvers to also do the join for widen, especially since there are domains assuming that.

Not sure the useless join is relevant. Depends on how confident we are that we (currently and in the future) enforce the join.
If you don't, it may be unsound?

Possibly yes. there isn't any rush to actually avoid those possibly unnecessary joins. Better safe than sorry.

Currently we have let narrow ik x y = x.
Is there an example where we lose precision?

I don't have an example, but was just thinking how this is a bit like the interval widening: the type's range is the most imprecise thing corresponding to infinity and this would widen to that. The analogous narrowing would be such that it may improve on the widening results, i.e. come back down, but only from the type's range.

Although I suppose this doesn't really matter. These ranges (especially since they're rounded to integer types) form only very short ascending chains anyway, like the ones shown in the PR description.
And the defexc ranges are a very minor piece of information, which I don't think are the deciding factor for precision anyway in almost all cases.

I think it is hard to ensure that everyone does it all the time in the future.

As I said, it has already been an implicit assumption for a very long time for some domains, so this should be enforced anyway and hence could also be assumed by all other domains. Not enforcing it is how issues like #414 happen.
It's not really that difficult to enforce: it's simply the solvers that have to call it as such.

[michael-schwarz]

I'll actually do an sv-comp run because the case where this may matter very much is for globals as we never do narrowing for them. If there is a difference there, we might want to have an option to toggle this behavior.

Actually, we should probably always have that toggle (see #459).

[vogler]

I'll actually do an sv-comp run because the case where this may matter very much is for globals as we never do narrowing for them. If there is a difference there, we might want to have an option to toggle this behavior.

Was there some noticeable difference?

[michael-schwarz]

When comparing between e75f7d7 and cb439e0 we loose a total of 12 points, and the runtimes of some of the tests go from a few seconds to timing out after 15min. Conversely, for some tests runtimes improve a bit.

Also, for some of those, what is very strange is that we have a quite low number of variables that are all uncovered very quickly and then the number of evals keeps going up without any new variables being discovered:

E.g. for 32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--leds--leds-pca9633.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml we now have

runtime: 00:00:10.127
vars: 280, evals: 6605

|rho|=280
|called|=12
|stable|=254
|infl|=272
|wpoint|=7
Found 47 contexts for 18 functions. Top 5 functions:

and then after 15min

runtime: 00:14:52.603
vars: 280, evals: 538640

|rho|=280
|called|=18
|stable|=264
|infl|=272
|wpoint|=7
Found 47 contexts for 18 functions. Top 5 functions:

Before, it terminated in 3s.
Something that came to mind is the refinement, but that is disabled in this configuration. So I'm not sure what causes this but we should investigate it.

All the details are here:

e75f7d-vs-cb439e0.zip

Of course there now is #495 in between, so some of the changes may be due to that, but seems a bit unlikely that this would cause an issue with evals going up and the number of vars remaining constant.
I'll also start a run of that later today.

[vogler]

Pretty wide graph 😄


Best to compare it to its predecessor e81b1a1.

The eval thing is interesting. Sounds like it could be address-related, but then you'd expect the context/vars to go up as well.

[michael-schwarz]

Pretty wide graph

Yup, it sure is, but it's mostly other things that then diverged, it is only like 5 commits in between (and those are from #495).
I started a run with e81b1a1 this morning, should be done in a few hours.

[vesalvojdani]

Also getting a timeout on ./goblint --set dbg.timeout 90 ../bench/pthread/knot_comb.c. This used to run under 6 seconds. Just doing a git revert cb439e0 on top of current master makes it work again.

[sim642]

This also seems to be the reason for this OpenSSL nontermination: goblint/bench#7 (comment). Now that we have an option for this, I'm going to just toggle it on master to get the old behavior by default, since there's some regression with this.

[vogler]

We can just not use it, but it's somehow indicative of some other issue, no?
At least I don't understand how widening to some bigger value immediately could lead to timeouts.
Most likely the passed ikind is wrong in those cases.

[sim642]

Indeed, I don't see anything conceptually wrong with quicker widening, so there must be some issue worth looking into. Probably easiest to minimize one of the SV-COMP programs as opposed to knot_comb or openssl.

[michael-schwarz]

I already started on knot before lunch. I have it down to 400 lines and will continue with it this afternoon.

[vesalvojdani]

This example is based on knot: 3a6491a, and I've tried manually to simplify it, but if you remove any of the structs or pointers, the problem disappears.

[michael-schwarz]

👍 The example I have thus far is single threaded and has two functions only, trying to narrow it down to only one at the moment. Maybe having two small examples is also insightful.

[sim642]

Sorry, I forgot about that already minimized example. If it happens just with structs and pointers, then it might have something to do with widening of indices in offsets of addresses. Maybe there's another point where widen is applied incorrectly (second argument is not a join).

[michael-schwarz]

int main(int argc , char **argv )
{
    char buf[512];
    int top;
    char *start ;

    while (1) {
        start = & buf[top];
    }
    return 0;
}

Here is another minimal example. What is interesting is that the widen Unknown int([-31,31]) Unknown int([-31,31]) is Unknown int([-63,63]). The value in the offset of start comes from top and that is in fact from [-31,31] and that is reestablished in the loop when start is assigned.

If I change widen such that widen x x = x, we get termination.

However, it is very strange that we have non-termination otherwise, because the widen should be able to arbitrarily go to larger values without risking non-termination (there is no narrowing for def_exc here). Julian and I were wondering if this might have to do with the removal of widening points that was added recently @vogler ?

[sim642]

The widening point removal is far from new I think. Thanks for minimizing the problem down to such small program. I traced it too and beyond what you mention, this happens:

%%% ad: (initfun:0:0)  widen {buf[def_exc:Unknown int([-31,31])], NULL, ?} {buf[def_exc:Unknown int([-31,31])], NULL, ?}
  %%% ad: -> {buf[def_exc:Unknown int([-63,63])], NULL, ?}
%%% ad: (initfun:0:0)  widen {buf[def_exc:Unknown int([-63,63])], NULL, ?} {buf[def_exc:Unknown int([-63,63])], NULL, ?}
  %%% ad: -> {buf[def_exc:Unknown int([-63,63])], NULL, ?}
%%% ad: (initfun:0:0)  widen {buf[def_exc:Unknown int([-63,63])], NULL, ?} {buf[def_exc:Unknown int([-31,31])], NULL, ?}
  %%% ad: -> {buf[def_exc:Unknown int([-31,31])], NULL, ?}

The problem is the last line where widen is indeed called somehow incorrectly and makes the result more precise.

EDIT: I think I found the culprit, opening a PR in a moment.

[michael-schwarz]

But that is not even so wrong, because it is called from a narrow.

[vogler]

Fix for Adress Domain widen: #534

Maybe post the bench results here then. Hopefully better than the results above #502 (comment).

The initial motivation for the change was to have shorter traces for small programs, but for big loops with many function calls inside (that's why I tried maradns-1.4.06_zoneserver_comb.c) this should have some significant enough speed-up.

[vogler]

Seems to work on the interactive benches. It also makes smtprc almost 2x faster compared to the version that widens via joins:

• no_widen_by_join (with this fix)
• widen_by_join

Originally posted by @vesalvojdani in #534 (review)