NoQ added a comment. In https://reviews.llvm.org/D35109#837723, @NoQ wrote:
> It's something similar to assuming that the string length is within range [0, > INT_MAX/4] in CStringChecker: we can easily assume that no overflow is > happening in computations involving string lengths or iterator positions, but > not on generic integers. Which lead me to believing that we could maintain a > no-overflow variant of evalBinOp (questionable). > > Would anything go wrong if we only enable this code when both symbols are > known to be within range [-max/4, max/4]? And in the checker, add the > respective assumption. I believe it's a very clear way to express that no > overflow is happening. In fact, in the program state we can add an API > `ProgramStateRef assumeNoOverflow(SVal, QualType)`, which tries to assume > that the value is within range [-max/4, max/4] for signed types or [0, max/4] > for unsigned types (and fails when such assumption is known be violated), so > that to avoid duplicating similar trick in every checker. I had a quick look into actually implementing this solution, and i generally liked how it looks. Instead of the checker saying "I know that these symbols won't overflow on any operations, so let me do whatever I want", it says "I know that these symbols are small" and the core handles the rest. I managed to get this patch and https://reviews.llvm.org/D35110 and https://reviews.llvm.org/D32642 running on top of my solution in a fairly straightforward manner. I did not see if there is any impact on performance; if there is, in the worst case we may want to expose the "unsafe" functions to the checkers to optimize out repeated checks. A bit of cleanup may be necessary after me (eg. turn static functions into methods where appropriate). Unsigned integers are not supported, because their overflows are harder to avoid; however, as far as i understand you are only interested in signed integers. For signed integers, rearrangement only kicks in when all symbols and concrete integers are of the same type `T` and are constrained within `[-max/4, max/4]`, where `max` is the maximum value of `T`. Here are my patches: - On top of https://reviews.llvm.org/D35109: F5459988: Max4Rearrangements.patch <https://reviews.llvm.org/F5459988> - On top of https://reviews.llvm.org/D35110: F5459990: Max4Negations.patch <https://reviews.llvm.org/F5459990> - On top of https://reviews.llvm.org/D35110: F5459991: Max4Iterators.patch <https://reviews.llvm.org/F5459991> All tests should pass when all 6 patches are applied. Could you see if this works for you? https://reviews.llvm.org/D35109 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
