HomePhabricator

[Analyzer][solver] Simplify existing eq classes and constraints when a new…

Authored by martong on May 28 2021, 6:18 AM.

Description

[Analyzer][solver] Simplify existing eq classes and constraints when a new constraint is added

Update setConstraint to simplify existing equivalence classes when a
new constraint is added. In this patch we iterate over all existing
equivalence classes and constraints and try to simplfy them with
simplifySVal. This solves problematic cases where we have two symbols in
the tree, e.g.:

int test_rhs_further_constrained(int x, int y) {
  if (x + y != 0)
    return 0;
  if (y != 0)
    return 0;
  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
  return 0;
}

Differential Revision: https://reviews.llvm.org/D103314