[PATCH] D105692: [analyzer][solver][NFC] Introduce ConstraintAssignor

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko created this revision.
vsavchenko added reviewers: NoQ, xazax.hun, martong, steakhal, Szelethus, ASDenysPetrov, manas, RedDocMD.
Herald added subscribers: dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware.
vsavchenko requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D105692

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D105692.357480.patch
Type: text/x-patch
Size: 17399 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210709/767329ee/attachment-0001.bin>