analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

`var_eq` doesn't remove unreachable variables in `enter`

Open sim642 opened this issue 2 years ago • 2 comments

Here's enter for var_eq analysis: https://github.com/goblint/analyzer/blob/5614dd34bb45e3bb7f960bfddd512d00106aa4aa/src/analyses/varEq.ml#L412-L430 The comment claims it tries to remove unreachable variables but nowhere does it actually do that.

This means that the analysis keeps around equalities from the entire call stack, which makes them large (and thus less efficient to manipulate). It also means more unnecessary contexts for the called function because it can in no way observe those variables. Finally, in my unassume benchmarking and tracing, I've noticed it can cause extra widening iterations in the called function due to equations on unreachable variables being invalidated.

Example

// PARAM: ---set ana.activated[+] "'var_eq'"
void foo() {
  // var_eq has x == y here
}

int main() {
  int x;
  int y;
  y = x;
  foo();
  return 0;
}

sim642 avatar Aug 04 '23 14:08 sim642