Page MenuHomePhabricator

[Analyzer][VLASizeChecker] Fix problem with zero index assumption.
Needs ReviewPublic

Authored by balazske on Jun 3 2020, 1:15 AM.



The crash was caused by incorect assumptions on a and a + 1
that resulted in knowing something about a (that it is exactly -1)
and only knowing about a + 1 that it is non-zero.

"constraints": [
  { "symbol": "reg_$0<int a>", "range": "{ [-1, -1] }" },
  { "symbol": "(reg_$0<int a>) + 1", "range": "{ [-2147483648, -1], [1, 2147483647] }" }

The problem was fixed by replacing plain assume on symbol with assume on
binary operator (test for "a==0" instead of "a").
An additional check was inserted at place of the assertion to prevent
similar crashes.

A test that triggers this last case is missing now.
The added test causes no problem because at start of the second loop
"c" can not be zero because the previous assumption made by the checker
(that did not work correct before the fix).

Diff Detail

Event Timeline

balazske created this revision.Jun 3 2020, 1:15 AM

There may be still a problem somewhere else. I think assume of "a" and "a==0" should have the same results.

NoQ added inline comments.Jun 3 2020, 4:30 AM

If we aim for a better fix, can we reduce the number of assumptions we make from 2 to 1? Like, it's ok if it's imperfect; 1 imperfect assumption is better than 2 imperfect assumptions.

The mental model i'm following here is that every path-sensitive bug can be thought of as a single formula over symbolic expressions. Eg., division by zero is the formula "$denominator == 0" is definitely true, double close is "is_closed($file_being_closed)", division by tainted value is "$denominator == 0" is possibly true AND "is_tainted($denominator)". I'd like you to write down the single formula that represents your bug and perform a single assume() over that and use the result of such assume as an ultimate source of truth. If such assume is not working correctly, let's think how to fix the assume rather than pile up more assumes in every checker to manually cross-check each other.

balazske updated this revision to Diff 268216.Jun 3 2020, 8:33 AM

Improved assumption on array size.

balazske marked 2 inline comments as done.Jun 3 2020, 8:40 AM
balazske added inline comments.

Based on this the assumptions could be really simplified. Now the check is made only for positive array size.
One question is if it is good to leave the assert here. This condition shows internal inconsistency, it may be better to abort the checker instead of making probably bad state changes (in the bad case array extent was changed to a nonzero but probably negative value range).

NoQ added inline comments.Jun 8 2020, 5:50 AM

Why not do the same in checkVLAIndexSize then?


The type of binary operator >= is bool, not size_t.

balazske marked 2 inline comments as done.Jun 9 2020, 1:31 AM
balazske added inline comments.

The only reason for this is was that at this place the known index value is already computed but not in checkVLAIndexSize.

balazske updated this revision to Diff 272361.Jun 22 2020, 2:49 AM
  • Rebase
  • Using condition type for evalBinOp
  • Comments updated
balazske marked an inline comment as done.Jun 29 2020, 12:20 AM

This is a better fix for the previous problem, and makes the code better too.

I don't have much to say here, this goes a bit outside my expertise. @NoQ?