Page MenuHomePhabricator

[Analyzer] Basic support for multiplication and division in the constraint manager (for == and != only)
Needs ReviewPublic

Authored by baloghadamsoftware on Aug 3 2018, 8:11 AM.



Currently, the default (range-based) constraint manager supports symbolic expressions of the format symbol + integer or symbol - integer to compare them to another integer. However, multiplication and division is not supported yet.

An example where multiplication (and division) could be useful is the checking whether a pointer operation or an array index is out of the bounds of the memory region. The index is often a first-degree expression of the format a*x + b (e.g. for special sparse matrices, such as triangular ones).

In this patch we only support multiplication and division for two kinds of symbolic comparisons: the == and the != operators. The rest is to follow in a subsequent patch. Negative multipliers and divisors are not supported yet.

Diff Detail

Event Timeline

whisperity edited the summary of this revision. (Show Details)Aug 3 2018, 8:45 AM
whisperity set the repository for this revision to rC Clang.
MTC added a subscriber: MTC.Aug 5 2018, 7:18 PM

@NoQ Any comments/concerns regarding this solution?

Tests updated to the now default eagerly assume mode. Range scaling fixed.

NoQ added a comment.Nov 29 2018, 4:09 PM

I guess that's roughly the way to go if we want to expand RangeConstraintManager with more math.

One important thing to test here, that doesn't seem to be tested, is what happens when the integer and the scale value are of different types. This may occur because we don't have any representation for integral casts and therefore the type of the symbol itself isn't necessarily the type of the unknown value it represents. As usual, that complicates this sort of work.

I think it's a good idea to organize the constraint manager and SValBuilder a bit better, so that it was easier to understand the algorithmic complexity of the newly implemented stuff by looking at small parts of their code.

Also i'd really appreciate if someone refactors SValBuilder and/or RangeConstraintManager so that it was easier to navigate. The current ad-hoc code structure makes it too hard to figure out what the contract of every function is and how do the changes affect algorithmic complexity of the whole thing. But for this patch it doesn't seem to be that bad.


I believe that this code should be moved directly into getRange(). If it's about looking at a single symbol and figuring out what range information about it do we already have, it should go into getRange(). This way we don't need to duplicate it in all the assume...() functions, and also it's exactly what getRange() is supposed to accomplish.


Mmm, what if Scale.Val is veeeeeeeery large?

baloghadamsoftware marked 2 inline comments as done.Dec 4 2018, 5:59 AM

Thank you for reviewing this patch!


getRange() retrieves the existing range for the symbol. However, similarly to the Adjustment we use the Scale to change the right side of the relation, not the left one.

I also dislike code multiplication. Maybe we should use the Strategy pattern here and create a function that does the loop. However, if you take a look at D49074 you will see that the body of the loop may look quite different.


That is a real problem. We either have to limit this functionality for small numbers (for the short term, maybe) or find a better algorithm (for the long term).

baloghadamsoftware marked 2 inline comments as done.Feb 20 2019, 6:11 AM
baloghadamsoftware added inline comments.

I took a look again at all the loops including D49074, but only the loop conditions match. There are no other similarities between the loop bodies. I can move the loop into another function taking a lambda as the loop body but it does not simplify the code so I see no point in it.


Any suggestion for the limit? Maybe 256?

Multipliers limited to less or equal to 255.

Intersecting an empty set caused an assertion. Early return inserted to prevent this.

baloghadamsoftware retitled this revision from [Analyzer] [WIP] Basic support for multiplication and division in the constraint manager (for == and != only) to [Analyzer] Basic support for multiplication and division in the constraint manager (for == and != only).Jul 26 2019, 7:10 AM
NoQ added inline comments.Jul 26 2019, 3:51 PM

Something's not right here. All three can potentially be true, because both 1/2 == 0 and (-1)/2 == 0.

Fixed error when the result of an integer division is compared to zero.

baloghadamsoftware marked 2 inline comments as done.Jul 29 2019, 5:16 AM
baloghadamsoftware added inline comments.

Thank you for noticing this! It is strange that I forgot about 0 for == and != but not for the rest of the comparison operators in my subsequent patch. Now I fixed it.