[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
Loading
Please sign in to comment