Page MenuHomePhabricator

[analyzer] RangeConstraintManager: Apply constraint ranges of bitwise operations
Needs ReviewPublic

Authored by Charusso on Jul 24 2019, 12:37 PM.



We do not support evaluating bitwise operations, so that when we check for
their results being null we create a new assumption whether the current new
symbol is null or non-null. If we are on the non-null assumption's branch
we need to check the left-hand side operand's constraint range informations:

  • It if contradicts with the forming new constraint ranges then we create a null state as it is an impossible condition.
  • Otherwise we need to remove the nullability from its ranges as we know that it cannot be null on that branch (except bitwise OR).

Diff Detail

Event Timeline

Charusso created this revision.Jul 24 2019, 12:37 PM
NoQ added a comment.Jul 24 2019, 1:09 PM

Aha, great, the overall structure of the code is correct!


Let's do some math.

Suppose $x is in range [2, 3]. In this case the true range for $x & 1 is [0, 1] (because 2 & 1 == 0 and 3 & 1 == 1).

The range for $x & 8 would be [0, 0].

The range for $x | 8 would be [10, 11].

The range for $x << 1 would be [4, 4], [6, 6].

The range for $x >> 1 would be [0, 1].

None of these ranges are contained within [2, 3]. In fact, none of them even contain either 2 or 3. However, when you intersect the resulting range with [2, 3], you make sure that the resulting range is contained within [2, 3]. I don't think that's correct.


You're only taking a single segment out of the range. The range may be a union of multiple segments. You should intersect with the whole range instead.

Charusso updated this revision to Diff 211956.Jul 26 2019, 9:16 AM
Charusso edited the summary of this revision. (Show Details)
  • Restrict the generic contradiction-based range evaluation to only affect that left-hand side operands which constraint range are concrete zero.
Charusso marked 3 inline comments as done.Jul 26 2019, 9:20 AM
In D65239#1599889, @NoQ wrote:

Aha, great, the overall structure of the code is correct!

Thanks! Now it is more formal. The only problem it does not change anything on LLVM reports, where we are working with the test_non_null_lhs_range_to_null_result_feasible test case.


I have added a test case to see how bad our evaluation at the moment. That is why I saw that we are just narrowing ranges and the contradiction only could happen at concrete zero range based.

NoQ added inline comments.Jul 29 2019, 7:17 PM

Instead of "we know that the value is null", we should write "we don't know that the value is non-null". I.e. if we're not sure, we must still do an early return.


This loop doesn't make sense. When your expression looks like (((a + b) + c) + d) & (e + f), you don't want to iterate separately over a, b, c, d, e, f; but that's what this loop would do. You should only look at the LHS and the RHS. If you want to descend further, do so recursively, so that to keep track of the overall structure of the symbolic expression as you're traversing it, rather than traversing sub-expressions in an essentially random order.


This test accidentally tests debug prints. We don't want to test debug prints here. I suggest:

clang_analyzer_eval(X >= 2 && X <= 3); // expected-warning{{TRUE}}
Charusso updated this revision to Diff 212440.Jul 30 2019, 2:25 PM
Charusso marked 6 inline comments as done.
  • Fix.

Oh, fail. Thanks!


It is rather sequential in the bitwise world, but I think if you would look only at the LHS SymExpr, it should be enough. Also I would like to avoid extra overhead, that symbols() business was large enough. Thanks!

NoQ added inline comments.Aug 21 2019, 11:24 AM

I suspect we have problems with bitwise OR here, which (unlike other bitwise/shift ops) may be true when the LHS is 0.


The LHS of || is always false here, regardless of the value of A or constraints on it. This test tests something strange.


The LHS of || is equivalent to C == 1.


This check is trivially true regardless of the value of D or constraints on it.


Same here.

Charusso updated this revision to Diff 216731.Aug 22 2019, 4:15 PM
Charusso marked 7 inline comments as done.
Charusso edited the summary of this revision. (Show Details)
  • Fix.

In overall I wanted to keep the [A, B] shape of the tests, but now they are more precise, thanks!


Whoops, thanks!


Hm, yes. I felt like D equals to E, but that test fails, so I have just removed them.

NoQ added inline comments.Aug 30 2019, 3:14 PM

I recommend making this method non-static, so that not to have to pass BV and F around.


If there's no current range in the map, it doesn't mean that there's no current range at all. Instead it means that the symbol is completely unconstrained and its range is equal to the whole domain of the type's possible values. You should use RangeConstraintManager::getRange() instead to retrieve the "default" range for the symbol. It would also always exist, so no need to check.


Aaand at this point you might as well call applyBitwiseRanges() recursively. Or even call assume() recursively. This will be the better way to implement your loop idea, because now it's gonna be correct on all recursion depth levels.