Make oct-Apron context sensitive

[michael-schwarz]

oct-Apron currently either has a bottom context or the entire local state for exp.full-context. The following things should probably be improved:

• Why do we have a bottom context by default instead of a top context?
• Unless we have exp.addr-context or exp.no-int-context or exp.no-interval-context, we should probably be context sensitive? Or at least have the possibility to be?

[sim642]

Without full context, it doesn't really matter if all octApron contexts are bottom or top. They're all just the same and that's all what matters at that point.

The philosophical question is what should octApron contexts achieve? Unlike base, octApron actually constructs function summaries: the return node has a relation between the formal arguments and the return value. And combine instantiates those formal arguments with the relation between arguments from the call site. Passing the same data also in as contexts doesn't make much of a difference in many cases I think.

I haven't tested it with full context, so I cannot vouch for that actually working sensibly, but that could be fixed if it doesn't. A separate question is if there's any sensible partial context sensitivity possible for octApron.

[michael-schwarz]

They're all just the same and that's all what matters at that point.

Indeed. But I think that would be more obvious if we had top instead of bot here.

And combine instantiates those formal arguments with the relation between arguments from the call site. Passing the same data also in as contexts doesn't make much of a difference in many cases I think.

Really? To me it seems like there is some additional things going on in enter#:

https://github.com/goblint/analyzer/blob/d9c4818ad7c8993170d953b8881f4294a47716e2/src/analyses/apron/octApron.apron.ml#L146-L166

Also, if it only really computed function summaries, the resulting summary would always be the same. Then, this test which fails with x <= y because it does not lead to different contexts in the base analysis, would also fail if I replace that with x<y (where it currently doesn't because base distinguishes these calls), and so we get different analysis results for octApron in different contexts. Maybe this distinguishing of contexts should not just happen in some sort of hap-hazard way via base sometimes, but independent of it?

// SKIP PARAM: --sets ana.activated[+] octApron --enable ana.int.interval
#include <assert.h>

int oct(int x, int y) {
    int s;
    if(x > y) {
        s = -1;
    } else {
        s = 0;
    }
    return s;
}

void main() {
  int x, y;
  if (x <= y) {
    int res = oct(x,y);
    assert(res == 0); // FAIL (with x <= y); succeeds with x<y
  }

  int res = oct(x,y);
}

[sim642]

Indeed. But I think that would be more obvious if we had top instead of bot here.

The domain with heterogeneous environments which is currently used there doesn't have a top though. And the bottom of it is just the top value over an empty environment, so it is top in a way as well.

Really? To me it seems like there is some additional things going on in enter#:

You're right, I must've forgotten about this. The primary function there is to pass the global invariant and remove the local scope variables, but indeed it also preserves the relation between the formal arguments. And without full context they just get joined together, like in the type of example you gave.

So yes, there's additional precision to octApron contexts and exp.full-context should give you that. Although I think the bigger issue here is that exp.full-context is kind of overloaded in terms of what it does, because its central objective is in FromSpec where it determines how function call constraints are set up (without or with side effects, only the latter allows partial context sensitivity). The context sensitivity of octApron probably should be a separate option, so one could use partial context sensitivity (e.g. for base) and have context sensitivity for octApron at the same time.

A possibility of octApron partial context sensitivity would be related to #193, because one might also want to keep the number of octApron contexts down by just separating calls by argument relations and remove all global relations

[michael-schwarz]

The domain with heterogeneous environments which is currently used there doesn't have a top though.

That's a good point! Maybe we can add a comment to that effect.

Although I think the bigger issue here is that exp.full-context is kind of overloaded in terms of what it does, because its central objective is in FromSpec where it determines how function call constraints are set up (without or with side effects, only the latter allows partial context sensitivity).

I would argue that this should be the only point of full-context. full-context does in fact not give you more context than the default options, it really only differs in how original values arrive at start points of programs.

• Via c \leq [u,c]: full-context
• Or via a side-effect [u,c] -> c to that program point: no full-context

Unless one has one of these partial context settings activated (which can not be active at the same time as full-context), this still leads to the same local value at the startpoint. So probably full-context should just be side-entry with default value true and one gets full-context with side-entry set to false?

[sim642]

I'll consider this done after #322 and https://github.com/goblint/analyzer/commit/c08813c39173c49201477ca266f3c833c10c4f8f. Now there's a separate option ana.octapron.no-context and it's false by default, so octApron is context-sensitive.

If intermediate context-sensitivity levels are needed (e.g. no globals, etc), then they can easily be added as well.