[all-commits] [llvm/llvm-project] f531c1: [analyzer] Introduce small improvements to the sol...

[Valeriy Savchenko via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: f531c1c7c0d5850c824333518ff32708730d775b
      https://github.com/llvm/llvm-project/commit/f531c1c7c0d5850c824333518ff32708730d775b
  Author: Valeriy Savchenko <vsavchenko at apple.com>
  Date:   2020-07-22 (Wed, 22 Jul 2020)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

  Log Message:
  -----------
  [analyzer] Introduce small improvements to the solver infra

Summary:
* Add a new function to delete points from range sets.
* Introduce an internal generic interface for range set intersections.
* Remove unnecessary bits from a couple of solver functions.
* Add in-code sections.

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


  Commit: b13d9878b8dcef4354ddfc86f382ca9b537e65aa
      https://github.com/llvm/llvm-project/commit/b13d9878b8dcef4354ddfc86f382ca9b537e65aa
  Author: Valeriy Savchenko <vsavchenko at apple.com>
  Date:   2020-07-22 (Wed, 22 Jul 2020)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
    M clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    M clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
    A clang/test/Analysis/equality_tracking.c

  Log Message:
  -----------
  [analyzer][solver] Track symbol equivalence

Summary:
For the most cases, we try to reason about symbol either based on the
information we know about that symbol in particular or about its
composite parts.  This is faster and eliminates costly brute force
searches through existing constraints.

However, we do want to support some cases that are widespread enough
and involve reasoning about different existing constraints at once.
These include:
  * resoning about 'a - b' based on what we know about 'b - a'
  * reasoning about 'a <= b' based on what we know about 'a > b' or 'a < b'

This commit expands on that part by tracking symbols known to be equal
while still avoiding brute force searches.  It changes the way we track
constraints for individual symbols.  If we know for a fact that 'a == b'
then there is no need in tracking constraints for both 'a' and 'b' especially
if these constraints are different.  This additional relationship makes
dead/live logic for constraints harder as we want to maintain as much
information on the equivalence class as possible, but we still won't
carry the information that we don't need anymore.

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


  Commit: e63b488f2755f91e8147fd678ed525cf6ba007cc
      https://github.com/llvm/llvm-project/commit/e63b488f2755f91e8147fd678ed525cf6ba007cc
  Author: Valeriy Savchenko <vsavchenko at apple.com>
  Date:   2020-07-22 (Wed, 22 Jul 2020)

  Changed paths:
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    M clang/test/Analysis/equality_tracking.c
    A clang/test/Analysis/mutually_exclusive_null_fp.cpp

  Log Message:
  -----------
  [analyzer][solver] Track symbol disequalities

Summary:
This commmit adds another relation that we can track separately from
range constraints.  Symbol disequality can help us understand that
two equivalence classes are not equal to each other.  We can generalize
this knowledge to classes because for every a,b,c, and d that
a == b, c == d, and b != c it is true that a != d.

As a result, we can reason about other equalities/disequalities of symbols
that we know nothing else about, i.e. no constraint ranges associated
with them.  However, we also benefit from the knowledge of disequal
symbols by following the rule:
  if a != b and b == C where C is a constant, a != C
This information can refine associated ranges for different classes
and reduce the number of false positives and paths to explore.

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


Compare: https://github.com/llvm/llvm-project/compare/e00645cc7878...e63b488f2755