Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[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
- Loading branch information