# [WIP][analyzer] Introduce range-based reasoning for addition operatorNeeds ReviewPublicActions

Authored by manas on Jun 1 2021, 1:38 AM.

# Details

Reviewers
 teemperor vsavchenko NoQ xazax.hun
Summary

# Diff Detail

### Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes
manas updated this revision to Diff 349796.Jun 4 2021, 2:30 AM

Fix for cases involving residual paths and add case for overflowing range near extremum of a type

xazax.hun added a comment.EditedJun 4 2021, 11:38 AM

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 ( _ BitVec 32 ))

; Assume 0 <= a, b, <= 5
(assert (bvsge a #x00000000))
(assert (bvsge b #x00000000))
(assert (bvsle a #x00000005))
(assert (bvsle b #x00000005))

; Check if 0 <= a + b  <= 10
(assert (not (and (bvsle (bvadd a b) #x0000000A) (bvsge (bvadd a b) #x00000000))))

(check-sat)```

Of course, the example above is obvious, but with overflows and other corner cases it is great to have a tool doublecheck our assumptions, and share how to reproduce the results.

manas added a comment.Jun 4 2021, 3:23 PM

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?

We are looking forward to design a unit-test framework for the solver which can compact the test cases and make them much more manageable (unlike constant-folding.c). Perhaps, we can incorporate the Z3 proves in that framework, corresponding to test cases.

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 ( _ BitVec 32 ))

; Assume 0 <= a, b, <= 5
(assert (bvsge a #x00000000))
(assert (bvsge b #x00000000))
(assert (bvsle a #x00000005))
(assert (bvsle b #x00000005))

; Check if 0 <= a + b  <= 10
(assert (not (and (bvsle (bvadd a b) #x0000000A) (bvsge (bvadd a b) #x00000000))))

(check-sat)```

Of course, the example above is obvious, but with overflows and other corner cases it is great to have a tool doublecheck our assumptions, and share how to reproduce the results.

I usually add things like this not about the tests, but about the implementation. I think it provides a bit more generality. But usually I do it as a comment to the patchset, maybe it is also good to put it in the code as well.

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?

We are looking forward to design a unit-test framework for the solver which can compact the test cases and make them much more manageable (unlike constant-folding.c). Perhaps, we can incorporate the Z3 proves in that framework, corresponding to test cases.

Hmm, so you mean we can check if the analyzer was compiled with Z3 and if so, verify the same things by it?

manas added a comment.EditedJun 5 2021, 7:02 AM

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?

We are looking forward to design a unit-test framework for the solver which can compact the test cases and make them much more manageable (unlike constant-folding.c). Perhaps, we can incorporate the Z3 proves in that framework, corresponding to test cases.

Hmm, so you mean we can check if the analyzer was compiled with Z3 and if so, verify the same things by it?

Yeah in some sense. But I think that having proof for every test case may become redundant for certain cases.

For e.g., consider two test cases for addition and subtraction operator:

1. c == [0, 10] and d == [-10, 0] will result in (c + d) == [-10, 10]
2. c == d == [0, 10] will result in (c - d) == [-10, 10]

But the first test case can be modeled as c - (- d)equivalently c - D, that is,

• usage of subtraction binary operator : (c - D), and
• symmetrical inversion of range around origin (- d) for symbol d. This will shift the range from [-10, 0] to [0, 10].

Considering having proof for every test case will make the proof for test-case 1 kind of redundant in comparison to test-case 2.

So, I think we should go with @vsavchenko 's method of adding Z3 proof with the implementation (in code), instead of test cases themselves.

manas updated this revision to Diff 352283.Jun 15 2021, 4:05 PM
manas edited the summary of this revision. (Show Details)

Herald added a subscriber: martong. Jun 15 2021, 4:05 PM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1403–1404

I changed the logic from using getCrucialPoints (which I mentioned in the e-mail thread) to simple checks to determine overflows using signedness. But the failed assertions again popped up. And I was unable to pin-point the issue here. Can someone help me?

Although, I am thinking of revising the above logic by using bitwise methods to detect overflows.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1399

This clause is exactly the same as the previous one, it is a mistake.
And I think we should have a test that could've shown that.
Also, since you are checking for overflows for both the beginning and the end, we should have tests where both overflow.

1403–1404

This is actually one place that I won't expect an assertion failure.
Can we get a bit more detail on it? Is it again From > To (which will indeed be weird) or something different?

NOTE: Asking for help (either here or on StackOverflow) is a lot like filing a bug report, try to put as much information as possible, try to structure this information so it is easy to follow. It's also good to tell people what you tried, instead of saying that you tried something and it didn't work.
1411–1417

I thought we talked quite a lot that there is nothing bad with overflows and here we have that if ANY overflow happened, we bail out and don't give any result.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1403–1404

It complains about different bit-width for ranges that the analyzer tries to intersect. What I checked next: what are those ranges, so I took begin() from one of them and checked what are From and To there.
Here is one of them:

```(const llvm::APSInt) \$8 = {
llvm::APInt = {
U = {
VAL = 22
pVal = 0x0000000000000016
}
BitWidth = 4022311424
}
IsUnsigned = true
}```

Woah, this BitWidth seems ridiculous! What does it tell us? It definitely didn't get there as part of any reasonable logic, right? So, what can it be instead? Only one answer here - garbage. We have some sort of memory issue with integers that we use as part of our ranges! So, let's see what type of information Range class actually stores:

```class Range {
public:
Range(const llvm::APSInt &From, const llvm::APSInt &To) : Impl(&From, &To) {
assert(From <= To);
}

...

private:
std::pair<const llvm::APSInt *, const llvm::APSInt *> Impl;
};```

What we have here is a pair of pointers, and you have:

```llvm::APSInt Min = LHS.From() + RHS.From();
llvm::APSInt Max = LHS.To() + RHS.To();
llvm::APSInt Tmin = ValueFactory.getMinValue(ResultType);
llvm::APSInt Tmax = ValueFactory.getMaxValue(ResultType);```

These are ALL stack variables. So, pointer to those point to adequate data ONLY while we are inside of our functions. When we call another function, these pointers point into some data from some other function in the call stack, it doesn't point to anything even remotely resembling llvm::APSInt and we get BitWidth = 4022311424.

OK, we figured out the problem, what about a solution? If you look at other implementations, you can notice a couple of interesting things.
When you do:

`llvm::APSInt Tmin = ValueFactory.getMinValue(ResultType);`

other code does something like:

`const llvm::APSInt &Tmin = ValueFactory.getMinValue(ResultType);`

Or when you do:

`Range Second = Range(Min, Tmax);`

The sibling code does:

`return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};`

It looks like ValueFactory is the key here! It actually manages the lifetime of those integers for you and, whenever you ask it about values, it gives you llvm::APSInt & (note the reference part) that will have the correct lifetime.

I hope this gives you some insight into how you can debug things like this on your own and how you can reason about what you see.

Another piece of advice is to look around, other VisitBinaryOperator methods have all the information you actually needed. If you don't understand why we need ValueFactory, - experiment, ask us! It's bad to just ignore it.

1407–1408

Why not just return RangeFactory.add(ResultRangeSet, Second)?

NOTE: variables with integers in their names is a big no-no.
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1399

Understood! I will add tests to check each OR part of these conditionals in these cases.

1403–1404

Got it! I am working on fixing this.

1407–1408

Right! I assumed I have to refactor this part so I used this temporarily.

1411–1417

Understood! Should I replace it with code returning EmptySet()?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1411–1417

Why EmptySet()? EmptySet() means that this can never happen, this path is infeasible. Is that the case?
Let's say we have: [INT_MAX - 20, INT_MAX - 10] + [30, 40] what happens in this case?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1411–1417

Right! That will not be the case.

In this particular case, the range will be [INT_MIN + 9, INT_MIN + 29] which is far smaller than [Tmin, Tmax].

Also, I think I misunderstood the part of bailing out and not giving any result as returning empty.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1411–1417

Gotcha!

Because of cases like this, you need to re-think that part about Min > Max and maybe count the number of overflows on each side?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1411–1417

That's right. If it is able to deduce how many times overflows are occurring then it can reason about whether it will be MaxRangeSet or a subset of it. Fixing it!

manas updated this revision to Diff 353168.Jun 18 2021, 11:14 PM

Reason about cases where Min > Max

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?

clang/test/Analysis/constant-folding.c
280–281

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(...)

manas marked 11 inline comments as done.Jun 20 2021, 10:08 PM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1387

I commented on this part previously, you shouldn't get fixated on Min > Max because Max >= Min doesn't imply that overflow didn't happen (less important) and that the range [Min, Max] is correct (more important). Recall one of the examples that I had in that email.

There is an interesting pattern about results that we can use:

• no overflows happened -> [Min, Max] (should be always true)
• 1 overflow happened -> we need to invert the range, but there are two different cases:
• Min > Max, perfect, that's what we expected -> [Tmin, Max] ∪ [Min, Tmax]
• Max >= Min, we overflowed and wrapped the whole range -> [Tmin, Tmax]
• 2 overflows happened on one side -> [Min, Max]
• 2 overflows happened on both sides -> [Tmin, Tmax]

You need to think of this problem in terms of what really happens and not in terms of combating with assertions.

1403

What if LHS.From() is Tmin for signed T?
What if T is unsigned? Does Tmin - LHS.From() (aka 0 - LHS.From()) make sense?

1440–1443

Speaking of unsigned T, does it work for unsigned overflows? Do we have tests for that?

clang/test/Analysis/constant-folding.c
280–281

It might be that or it might be something different. Just by looking at this example, the previous if statement shouldn't add more paths that go inside of this if, so it shouldn't be the root cause.
Whenever you encounter problems and you want to tell other people, please, provide more detail. Did you notice it when running the test case? What was the output? What did you try? How did you extract it into a separate function?

clang/test/Analysis/constant-folding.c
280–281

I put a new test function in constant-folding.c as:

```void testAdditionRulesNew(int c, int d) {
if (c < 0 && c != INT_MIN && d < 0) {
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
}
}```

I tested this specific function as:

`./build/bin/clang -cc1 -analyze -analyzer-checker=core,debug.ExprInspection -analyze-function=testAdditionRulesNew constant-folding.c`

And I got the following output:

```../clang/test/Analysis/constant-folding.c:338:5: warning: FALSE [debug.ExprInspection]
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}```

which is correct.

But when I ran the same test inside testAdditionRules, using:

`./build/bin/clang -cc1 -analyze -analyzer-checker=core,debug.ExprInspection -analyze-function=testAdditionRules constant-folding.c`

then I got:

```../clang/test/Analysis/constant-folding.c:281:5: warning: FALSE [debug.ExprInspection]
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
../clang/test/Analysis/constant-folding.c:281:5: warning: TRUE [debug.ExprInspection]
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~```

Here, c = [INT_MIN + 1, -1] and d = [INT_MIN, 0], so c + d = [INT_MIN, -2] U [1, INT_MAX]. So c + d == 0 should be false. But in latter case, it is reasoning c + d == 0 to be UNKNOWN.

Also, the error arises in c + d == 0 case only and not in c + d == -1 case. I mistakenly highlighted that case while commenting.

clang/test/Analysis/constant-folding.c
280–281

Hmm, I don't know what can be the reason.

There are three reasonable approaches:

2. Print-based: use clang_analyzer_printState inside of this if. Among other things it will print you all constraints that we know about, you can check if they match your expectations. Also, if it is indeed because of residual paths, you will get another print from residual path.
3. Reduction: add the whole testAdditionRules into testAdditionRulesNew and start removing parts of it. At some point problem should disappear (based on your previous observations). That "minimal" reproducer can give you insight into what's going on.

These are not mutually exclusive, so you can try them in combination.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1403

Even if LHS.From() is Tmin for signed T the reasoning would be correct. As, CrucialPoint will be Zero and hence RHS will be divided into two parts: BeforeZero ([RHS.From, Zero]) and AfterAndIncludingZero ([Zero, RHS.To]).

And if the BeforeZero subrange (which will be responsible for overflowing, contains Tmin + Tmax then we can ensure that the final range will be [Tmin, Tmax]. And if it does not, (and assuming there is no overflow on the right side), then 1432:1434 will reason the range to be [Tmin, Max] U [Min, Tmax].

For unsigned types, actually we are asking the wrong question because an addition of unsigned integers can never overflow from the left side. So in that case, the code deducing the overflows from left-side will not be applicable. And therefore, 0 - LHS.From() will never give us anything. I was thinking to checked T before applying these rules.

1440–1443

This was not going to make into the patch as it does not solve the case mentioned in FIXME(:1437).

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].
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1387

I think I agree with you. This pattern (and the code following this pattern) makes much more sense, and easier to follow. I think I will refactor the patch accordingly.

clang/test/Analysis/constant-folding.c
280–281

I tried print the ProgramState as in both the cases like:

```if (c < 0 && c != INT_MIN && d < 0) {
clang_analyzer_printState();
clang_analyzer_eval(...);
...
}```
1. During testAdditionRulesNew, when I added clang_analyzer_printState just before doing any clang_analyzer_eval calls, I got the following constraints (these are as expected):
```"constraints": [
{ "symbol": "reg_\$0<int c>", "range": "{ [-2147483647, -1] }" },
{ "symbol": "reg_\$1<int d>", "range": "{ [-2147483648, -1] }" }
],```
```"constraints": [
{ "symbol": "reg_\$2<int c>", "range": "{ [-2147483647, -1] }" },
{ "symbol": "reg_\$3<int d>", "range": "{ [-2147483648, -1] }" },
{ "symbol": "(reg_\$2<int c>) + (reg_\$3<int d>)", "range": "{ [0, 2147483647] }" }
],

"constraints": [
{ "symbol": "reg_\$2<int c>", "range": "{ [-2147483647, -1] }" },
{ "symbol": "reg_\$3<int d>", "range": "{ [-2147483648, -1] }" },
{ "symbol": "(reg_\$2<int c>) + (reg_\$3<int d>)", "range": "{ [-2147483648, -2] }" }
],```

A point to note is that this ProgramState is before any clang_analyzer_eval calls have been made. So, the third constraint, in both sets of constraints (for c + d) should not exist there, that is,

```a. { "symbol": "(reg_\$2<int c>) + (reg_\$3<int d>)", "range": "{ [0, 2147483647] }" }
b. { "symbol": "(reg_\$2<int c>) + (reg_\$3<int d>)", "range": "{ [-2147483648, -2] }" }```

should not be in the constraints set.

And as obvious, the UNKNOWN reasoning for c + d == 0 in testAdditionRules is arising from constraint (a) above, which is a wrong reasoning (it ideally should be [1, INT_MAX] and not [0, INT_MAX]).

clang/test/Analysis/constant-folding.c
280–281

@vsavchenko wrote:

1. Reduction: add the whole testAdditionRules into testAdditionRulesNew and start removing parts of it. At some point problem should disappear (based on your previous observations). That "minimal" reproducer can give you insight into what's going on.

Trying this, I was able to deduce that the following snippet is causing UNKNOWN triggers:

```void testAdditionRulesNew(unsigned int a, unsigned int b, int c, int d) {
if (c < 0 && d < 0) {
clang_analyzer_printState();
clang_analyzer_eval((c + d) < 0); // expected-warning{{UNKNOWN}}
clang_analyzer_printState();
}

if (c < 0 && c != INT_MIN && d < 0) {
clang_analyzer_printState();
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
clang_analyzer_printState();
}
}```

The output warnings are as follows:

```<snipped-ProgramStates>
../clang/test/Analysis/constant-folding.c:341:5: warning: FALSE [debug.ExprInspection]
clang_analyzer_eval((c + d) < 0); // expected-warning{{UNKNOWN}}
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
../clang/test/Analysis/constant-folding.c:341:5: warning: TRUE [debug.ExprInspection]
clang_analyzer_eval((c + d) < 0); // expected-warning{{UNKNOWN}}
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
../clang/test/Analysis/constant-folding.c:347:5: warning: FALSE [debug.ExprInspection]
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
../clang/test/Analysis/constant-folding.c:347:5: warning: TRUE [debug.ExprInspection]
clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4 warnings generated.```

The second evaluation is leading to wrong reasoning. I think the constraints are being propagated somehow from first conditional (c < 0 && d < 0) to the second conditional (c < 0 && c != INT_MIN && d < 0).

I have added a pastebin using clang_analyzer_printState here: https://pastebin.com/0E8hmTWh

clang/test/Analysis/constant-folding.c
280–281

Ooof, OK. I know what's going on here.

clang_analyzer_eval actually assumes its condition. So it works as expected when the result is TRUE or FALSE, but actually splits the path when UNKNOWN.
This being said, the first conditional doesn't affect you (it is weaker than the second condition), clang_analyzer_eval((c + d) < 0); // expected-warning{{UNKNOWN}} does.
After that point, you have two states: one where c + d >= 0 (you called it a.) and the other with c + d < 0 (b.).

Another important point here is located in SymbolicRangeInferrer::infer(SymbolRef Sym). You can see that there are three returns in that function. Your functionality lives in the very last one, namely in Visit(Sym). What it means is that we ALWAYS give preference to existing constraints. And if we don't have any, we start traversing symbolic expressions to get something from that level.
This logic is flawed because we can be in a situation like you encountered now. Where we believe that c + d >= 0, but if we look at c and d, we can see that this is actually impossible.
It can be solved by always doing Visit(Sym) and intersecting results from ALL available sources. It has a simple implementation, but requires additional performance testing.

Long story short, that's not your problem. Try to avoid it/rewrite the test.

manas updated this revision to Diff 353825.Jun 22 2021, 4:57 PM

Added updated logic for reasoning using number of overflows. Also, changed a couple of tests which were leading to unwanted constriants being propagated further.

manas marked 7 inline comments as done.Jun 22 2021, 4:59 PM
manas added a comment.Jun 22 2021, 5:05 PM

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.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1067–1068

We should have these specific functions for other BO as well. Because they will lead us to reason about when Operand1 binop Operand2 can overflow or not. I was thinking in the direction of having a simpler class which works for this.

manas marked an inline comment as not done.Jun 22 2021, 6:29 PM

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:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1067–1068

I searched through a codebase a bit and here are the couple of functions (from APInt.h) that can come in handy:

```// Operations that return overflow indicators.
APInt sadd_ov(const APInt &RHS, bool &Overflow) const;
APInt uadd_ov(const APInt &RHS, bool &Overflow) const;
APInt ssub_ov(const APInt &RHS, bool &Overflow) const;
APInt usub_ov(const APInt &RHS, bool &Overflow) const;
APInt sdiv_ov(const APInt &RHS, bool &Overflow) const;
APInt smul_ov(const APInt &RHS, bool &Overflow) const;
APInt umul_ov(const APInt &RHS, bool &Overflow) const;
APInt sshl_ov(const APInt &Amt, bool &Overflow) const;
APInt ushl_ov(const APInt &Amt, bool &Overflow) const;```

APSInt is derived from APInt, so we can totally use these.

clang/test/Analysis/constant-folding.c
269

They are already unsigned, we don't need a >= 0 and b >= 0

330

I don't see the cases where we overflow on both ends and the case where we overflow on one end, but Min > Max.

manas added a comment.EditedJun 23 2021, 1:53 AM

I am working on debugging those 3 cases.

Thanks @vsavchenko and everyone for helping! :)

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1067–1068

That's great! I will incorporate those in the code instead of custom functions.

clang/test/Analysis/constant-folding.c
269

Right! I will remove those constraints.

330

manas updated this revision to Diff 354154.Jun 23 2021, 10:25 PM

Fix issues involving cases for unsigned type and add tests

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

Using uadd_ov (and sadd_ov), we can get the added value as well as whether overflow occurred or not. A point is that these functions return APInt instead of APSInt.

But when I tried just using:

```Min = LHS.From().uadd_ov(RHS.From(), HasMinOverflowed);

```Min = LHS.From() + RHS.From();
Max = LHS.To() + RHS.To();```

just for the added value, then the following tests failed (these tests and all other tests pass when I use the latter method to get Min/Max):

```Clang :: Analysis/PR3991.m
Clang :: Analysis/global-region-invalidation.c
Clang :: Analysis/malloc-overflow2.c
Clang :: Analysis/out-of-bounds-new.cpp
Clang :: Analysis/taint-generic.c```

I am working on fixing this part.

manas marked 3 inline comments as done.Jun 23 2021, 11:03 PM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

You can easily construct APSInt from APInt using APSInt ::APSInt(APInt I, bool isUnsigned) constructor.

manas marked an inline comment as not done.Jun 24 2021, 1:52 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

Okay. I will try with using uadd_ov only then. And check whether those tests pass or not.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

Hmm, why only uadd_ov? What about those tests? How do they fail? Try to look at the reasons and not brute-force by trying different solutions blindly.
Those tests are your friends, it's much better to get failures right now then getting them later when you land the patch.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

I meant related functions as well.

Most of them were failing due to Error evaluating statements. Although, I have rebased my tree so I will re-check again.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

Error evaluating statements just tells you when we crashed (for the context and fast insight).
Below this message is usually the real reason (and the last time I checked, it was assertion From > To failure).

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1392

My bad. I took a look and found, it was signed mismatch!

manas updated this revision to Diff 354424.Thu, Jun 24, 7:54 PM

Fix issues involving usage of uadd_ov and family of functions

manas marked 3 inline comments as done.Thu, Jun 24, 7:55 PM
clang/test/Analysis/constant-folding.c
264–266

We need a test with ranges and unsigned overflow

330

This comment is marked as "Done", but I still don't these cases.

manas updated this revision to Diff 354441.Thu, Jun 24, 11:58 PM

Add tests for overflows on both ends

clang/test/Analysis/constant-folding.c
330

Amended. From line 260 and later.

manas updated this revision to Diff 355825.Thu, Jul 1, 3:57 AM

manas updated this revision to Diff 356250.Fri, Jul 2, 12:43 PM

Replace literal-value 0 with APSInt Zero

manas marked 2 inline comments as done.Tue, Jul 20, 3:17 PM

Here is the proof of correctness of the algorithm using Z3: https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25

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 need to resolve. I left my comments there.

clang/test/Analysis/constant-folding.c
260

This looks like an overflow on one end (we couldn't have them on both ends with addition and unsigned integers) and wrapping around surpassing the beginning of the range.