[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas marked an inline comment as done. manas added a comment. I have updated the proof for Add: https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25 Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 363742. manas added a comment. Fix unrelated commits mess up! Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/utils/analyzer/Dockerfile:15-22 RUN apt-get update && apt-get install -y \ git=1:2.17.1* \ gettext=0.19.8.1* \ python3=3.6.7-1~18.04 \ python3-pip=9.0.1-2.3* \ -cmake=3.20.5* \ -ninja-build=1.8.2-1 +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/utils/analyzer/Dockerfile:15-22 RUN apt-get update && apt-get install -y \ git=1:2.17.1* \ gettext=0.19.8.1* \ python3=3.6.7-1~18.04 \ python3-pip=9.0.1-2.3* \ -cmake=3.20.5* \ -ninja-build=1.8.2-1

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 363734. manas added a comment. Fix test comments Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. In D103440#2891915 , @manas wrote: > Here is the proof of correctness of the algorithm using Z3: > https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25 There is a couple of fundamental problems there that you

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. Here is the proof of correctness of the algorithm using Z3: https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25 Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 356256. manas added a comment. Rebase Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 356250. manas added a comment. Replace literal-value 0 with APSInt Zero Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 355825. manas added a comment. Reformat comments Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/test/Analysis/constant-folding.c:330 +clang_analyzer_eval((c + d) == INT_MAX - 22); // expected-warning{{FALSE}} + } +} vsavchenko wrote: > manas wrote: > > vsavchenko wrote: > > > I don't see the cases where

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 354441. manas added a comment. Add tests for overflows on both ends Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/test/Analysis/constant-folding.c:264-266 + if (a == UINT_MAX && b == UINT_MAX) { +clang_analyzer_eval((a + b) == UINT_MAX - 1); // expected-warning{{TRUE}} + } We need a test with ranges and unsigned

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 354424. manas added a comment. Fix issues involving usage of `uadd_ov` and family of functions Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(), HasMaxOverflowed); vsavchenko wrote: >

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(), HasMaxOverflowed); manas wrote: >

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(), HasMaxOverflowed); vsavchenko wrote: >

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(), HasMaxOverflowed); manas wrote: >

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas marked an inline comment as not done. manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(),

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(), HasMaxOverflowed); manas wrote: >

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 354167. manas added a comment. Rebase Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1400 + if (ResultType.isUnsigned()) { +LHS.From().uadd_ov(RHS.From(), HasMinOverflowed); +LHS.To().uadd_ov(RHS.To(), HasMaxOverflowed); Using `uadd_ov`

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 354154. manas added a comment. Fix issues involving cases for unsigned type and add tests Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. Thanks @vsavchenko and everyone for helping! :) Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1075-1076 + /// LHSOpd binop RHSOpd == Result, where binop is any binary operation + bool hasOverflowed(llvm::APSInt LHSOpd,

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. Hey, it looks like we are finally converging on this one! Great job! NOTE: I don't know if you noticed, but I want to point out that there are three failing tests: F17553262: Screen Shot 2021-06-23 at 11.35.49.png

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. Regarding the tweakings in `constant-folding.c`, I have refrained from using cases which were resulting in `UNKNOWN` assertions as they were the primary reason for constraints being propagated. Comment at:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 353825. manas added a comment. Added updated logic for reasoning using number of overflows. Also, changed a couple of tests which were leading to unwanted constriants being propagated further. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/test/Analysis/constant-folding.c:280-281 + if (c < 0 && c != INT_MIN && d < 0) { +clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}} +clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}} +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/test/Analysis/constant-folding.c:280-281 + if (c < 0 && c != INT_MIN && d < 0) { +clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}} +clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}} +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/test/Analysis/constant-folding.c:280-281 + if (c < 0 && c != INT_MIN && d < 0) { +clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}} +clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}} +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1395 + + if (Min > Max) { +// This implies that an overflow has occured as either boundary would have vsavchenko wrote: > I commented on this part previously,

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1411 +if ((LHS.From() < 0 && RHS.From() < 0)) { + llvm::APSInt CrucialPoint = Tmin - LHS.From(); + if (RHS.Includes(CrucialPoint)) { vsavchenko wrote:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/test/Analysis/constant-folding.c:280-281 + if (c < 0 && c != INT_MIN && d < 0) { +clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}} +clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}} +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/test/Analysis/constant-folding.c:280-281 + if (c < 0 && c != INT_MIN && d < 0) { +clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}} +clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}} +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1395 + + if (Min > Max) { +// This implies that an overflow has occured as either boundary would have I commented on this part previously, you shouldn't

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. The diff fixes all invalid assertion issues and also reasons about the cases where Min > Max. One thing which is stuck for me is the case where Min <= Max but it overflows. I could reason about that in this way: 1. If one of Min/Max overflows while the other doesn't

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 353168. manas added a comment. Reason about cases where Min > Max Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1409-1415 + if ((LHS.From() > 0 && RHS.From() > 0 && Min < 0) || + (LHS.From() < 0 && RHS.From() < 0 && Min > 0) || + (LHS.To() > 0 && RHS.To() > 0 && Max < 0) || +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1409-1415 + if ((LHS.From() > 0 && RHS.From() > 0 && Min < 0) || + (LHS.From() < 0 && RHS.From() < 0 && Min > 0) || + (LHS.To() > 0 && RHS.To() > 0 && Max < 0) || +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1409-1415 + if ((LHS.From() > 0 && RHS.From() > 0 && Min < 0) || + (LHS.From() < 0 && RHS.From() < 0 && Min > 0) || + (LHS.To() > 0 && RHS.To() > 0 && Max < 0) || +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1409-1415 + if ((LHS.From() > 0 && RHS.From() > 0 && Min < 0) || + (LHS.From() < 0 && RHS.From() < 0 && Min > 0) || + (LHS.To() > 0 && RHS.To() > 0 && Max < 0) || +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1397 +(LHS.To() < 0 && RHS.To() < 0 && Max > 0) || +(LHS.To() < 0 && RHS.To() < 0 && Max > 0)) { + return {RangeFactory, Tmin, Tmax};

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1401-1402 + +// FIXME: This case in particular is resulting in failed assertion. +Range First = Range(Tmin, Max); +Range Second = Range(Min, Tmax);

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1397 +(LHS.To() < 0 && RHS.To() < 0 && Max > 0) || +(LHS.To() < 0 && RHS.To() < 0 && Max > 0)) { + return {RangeFactory, Tmin, Tmax}; This

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1401-1402 + +// FIXME: This case in particular is resulting in failed assertion. +Range First = Range(Tmin, Max); +Range Second = Range(Min, Tmax); I

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 352283. manas edited the summary of this revision. manas added a comment. Herald added a subscriber: martong. Add logic for computing rangeset for an expression containing BO_Add. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. In D103440#2800710 , @vsavchenko wrote: > In D103440#2800122 , @manas wrote: > >> In D103440#2799629 , @xazax.hun >> wrote: >> >>> I was

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. In D103440#2799629 , @xazax.hun wrote: > I was wondering, if we could try something new with the tests. To increase > our confidence that the expected behavior is correct, how about including a > Z3 proof with each of the

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. In D103440#2799629 , @xazax.hun wrote: > I was wondering, if we could try something new with the tests. To increase > our confidence that the expected behavior is correct, how about including a > Z3 proof with each of the test

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

xazax.hun added a comment. I was wondering, if we could try something new with the tests. To increase our confidence that the expected behavior is correct, how about including a Z3 proof with each of the test cases? For example: (declare-const a ( _ BitVec 32 )) (declare-const b ( _

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 349796. manas added a comment. Fix for cases involving residual paths and add case for overflowing range near extremum of a type Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/test/Analysis/constant-folding.c:282 + +if (c >= -20 && d >= -40) { + clang_analyzer_eval((c + d) < -1); // expected-warning{{TRUE}} vsavchenko wrote: > manas wrote: > > vsavchenko wrote: > > > Great, it's

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. In D103440#2797991 , @manas wrote: >> I also would like to see tests where the ranges are not going all the way to >> either INT_MIN or INT_MAX (if we talk about int), but overflow still might >> happen, and cases where

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added inline comments. Comment at: clang/test/Analysis/constant-folding.c:282 + +if (c >= -20 && d >= -40) { + clang_analyzer_eval((c + d) < -1); // expected-warning{{TRUE}} manas wrote: > vsavchenko wrote: > > Great, it's good to check

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 349749. manas added a comment. Added tests for residual paths and negation of certain values, and fixed expected warnings for UNKNOWN cases. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. > I also would like to see tests where the ranges are not going all the way to > either INT_MIN or INT_MAX (if we talk about int), but overflow still might > happen, and cases where overflow might happen, but we still can identify the > overflowing results precisely

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. I also would like to see tests where the ranges are not going all the way to either `INT_MIN` or `INT_MAX` (if we talk about `int`), but overflow still might happen, and cases where overflow might happen, but we still can identify the overflowing results precisely

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas updated this revision to Diff 349225. manas added a comment. Fixed test cases expecting wrong assertions and added few more test cases. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 Files:

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. In D103440#2792814 , @NoQ wrote: > Our pre-commit testing shows that the new tests fail, eg.: > > https://buildkite.com/llvm-project/premerge-checks/builds/41391#b557c86c-0587-4aee-a06b-8a4de6d771c4 > > Failed Tests (1): >

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added inline comments. Comment at: clang/test/Analysis/constant-folding.c:282 + if (a == UINT_MAX && b == UINT_MAX) { +clang_analyzer_eval((a + b) >= 0); // expected-warning{{FALSE}} + } manas wrote: > xazax.hun wrote: > > I think `UINT_MAX +

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas added a comment. @NoQ I figured out the tests but while testing against Z3, I mixed up constraints. I am changing those. Comment at: clang/test/Analysis/constant-folding.c:265 +if (a > INT_MAX) { + clang_analyzer_eval((a + b) <= 0); // expected-warning{{FALSE}}

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

NoQ added a comment. Our pre-commit testing shows that the new tests fail, eg.: https://buildkite.com/llvm-project/premerge-checks/builds/41391#b557c86c-0587-4aee-a06b-8a4de6d771c4 Failed Tests (1): Clang :: Analysis/constant-folding.c Did you figure out how to *run* the tests locally?

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

xazax.hun added inline comments. Comment at: clang/test/Analysis/constant-folding.c:265 +if (a > INT_MAX) { + clang_analyzer_eval((a + b) <= 0); // expected-warning{{FALSE}} + clang_analyzer_eval((a + b) > 0); // expected-warning{{FALSE}} Since

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

vsavchenko added a comment. Hey, great start! I added my comments inline and other mentors as reviewers. Comment at: clang/test/Analysis/constant-folding.c:275 + +if (a <= UINT_MAX && b <= UINT_MAX) { + clang_analyzer_eval((a + b) < 0); // expected-warning{{UNKNOWN}}

[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

manas created this revision. Herald added subscribers: steakhal, ASDenysPetrov, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, xazax.hun. Herald added a reviewer: teemperor. manas requested review of this revision. Herald added a project: clang. Herald