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 then the resulting range
should be [Tmin, Tmax] as Min <= Max even after overflowing.
2. If both of them overflows, then: a. If both overflows on the same side, that
is, both wrapped around Tmax, or both wrapped around Tmin, then the range
should be [Min, Max] only. b. But if both overflowed in different sides,
supposedly Min overflowed on left and Max on right, or vice versa, then the
range will be [Tmin, Tmax].
Will it work?
================
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}}
+ clang_analyzer_eval((c + d) <= -2); // expected-warning{{UNKNOWN}}
----------------
When I pull these cases out to a separate function (say testAdditionRules2) in
constant-folding.c then algorithm is able to reason about the range correctly,
but inside testAdditionRules, it is unable to figure stuff out. Does it have
something to do with constraints being propagated which we discussed below?
@vsavchenko wrote:
> I have one note here. The fact that we don't have a testing framework and
> use this approach of inspecting the actual analysis has an interesting
> implication.
>
> ```
> if (a == 10) { // here we split path into 2 paths: one where a == 10, and one
> where a != 10;
> // one goes inside of if, one doesn't
> . . .
> }
> if (a >= 5) { // here we split into 3 paths: a == 10, a < 5, and a in [5, 9]
> and [11, INT_MAX] (aka a >= 5 and a != 10).
> // 1 path was infeasible: a == 10 and a < 5
> // Two of these paths go inside of the if, one doesn't
> . . .
> clang_analyzer_eval(a == 10); // it will produce two results: TRUE and FALSE
> }
> clang_analyzer_eval(a == 10); // it will produce three results: TRUE, FALSE,
> and FALSE
> ```
>
> We don't want to test how path splitting works in these particular tests
> (they are about solver and constant folding after all), that's why we try to
> have only one path going through each `clang_analyzer_eval(...)`
>
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D103440/new/
https://reviews.llvm.org/D103440
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
