[PATCH] D81061: [Analyzer][VLASizeChecker] Fix problem with zero index assumption.

Wed Jun 3 08:45:02 PDT 2020

balazske marked 2 inline comments as done.
balazske added inline comments.

================
Comment at: clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp:127-129
+        // Despite the previous assumptions for non-zero and positiveness,
+        // this value might be zero or negative.
+        // At least check for zero again.
----------------
NoQ wrote:
> 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.
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).

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D81061/new/

https://reviews.llvm.org/D81061