[all-commits] [llvm/llvm-project] f26deb: [analyzer][solver][NFC] Introduce ConstraintAssignor

[Valeriy Savchenko via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: f26deb4e6ba7e00c57b4be888c4d20c95a881154
      https://github.com/llvm/llvm-project/commit/f26deb4e6ba7e00c57b4be888c4d20c95a881154
  Author: Valeriy Savchenko <vsavchenko at apple.com>
  Date:   2021-07-13 (Tue, 13 Jul 2021)

  Changed paths:
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

  Log Message:
  -----------
  [analyzer][solver][NFC] Introduce ConstraintAssignor

The new component is a symmetric response to SymbolicRangeInferrer.
While the latter is the unified component, which answers all the
questions what does the solver knows about a particular symbolic
expression, assignor associates new constraints (aka "assumes")
with symbolic expressions and can imply additional knowledge that
the solver can extract and use later on.

- Why do we need it and why is SymbolicRangeInferrer not enough?

As it is noted before, the inferrer only helps us to get the most
precise range information based on the existing knowledge and on the
mathematical foundations of different operations that symbolic
expressions actually represent.  It doesn't introduce new constraints.

The assignor, on the other hand, can impose constraints on other
symbols using the same domain knowledge.

- But for some expressions, SymbolicRangeInferrer looks into constraints
  for similar expressions, why can't we do that for all the cases?

That's correct!  But in order to do something like this, we should
have a finite number of possible "similar expressions".

Let's say we are asked about `$a - $b` and we know something about
`$b - $a`.  The inferrer can invert this expression and check
constraints for `$b - $a`.  This is simple!
But let's say we are asked about `$a` and we know that `$a * $b != 0`.
In this situation, we can imply that `$a != 0`, but the inferrer shouldn't
try every possible symbolic expression `X` to check if `$a * X` or
`X * $a` is constrained to non-zero.

With the assignor mechanism, we can catch this implication right at
the moment we associate `$a * $b` with non-zero range, and set similar
constraints for `$a` and `$b` as well.

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


  Commit: 60bd8cbc0c84a41146b1ad6c832fa75f48cd2568
      https://github.com/llvm/llvm-project/commit/60bd8cbc0c84a41146b1ad6c832fa75f48cd2568
  Author: Valeriy Savchenko <vsavchenko at apple.com>
  Date:   2021-07-13 (Tue, 13 Jul 2021)

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

  Log Message:
  -----------
  [analyzer][solver][NFC] Refactor how we detect (dis)equalities

This patch simplifies the way we deal with (dis)equalities.
Due to the symmetry between constraint handler and range inferrer,
we can have very similar implementations of logic handling
questions about (dis)equality and assumptions involving (dis)equality.

It also helps us to remove one more visitor, and removes uncertainty
that we got all the right places to put `trackNE` and `trackEQ`.

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


Compare: https://github.com/llvm/llvm-project/compare/2bc07083a258...60bd8cbc0c84