[analyzer] Condition optimization improvements for RangeConstraintManager

Hi, CSA ​community.

I got an idea how to make RangeConstraintManager​ more sofisticated.

I want you speak out, share your vision about this idea.

Actually this bug https://bugs.llvm.org/show_bug.cgi?id=13426 pushed me to these thoughts.

Let’s consider the next snippet:

int foo(int y, int x) {
int x;

if (y == z) {

x = 0;
}

if (y != z) {
x = 1;
}

return x;

}

Finally CSA reports you:

warning: Undefined or garbage value returned to caller
[core.uninitialized.UndefReturn]
return x;

But as a human you know that x has definitely been initialized.

As you can see CSA builds paths without relying on previous conditions (except the case {A-B} {B-A}m it is already done).

The same behavior appears when:

(y > z) (y <= z)

(y <= z) (y > z)​

(y == z) (z != y)​
etc.
I made a solution for this but have not upload it for review yet.

I also have some more thoughts about optimization such:
if (y < z) {}

if (y <= z) {} // which is a subset of (y < z)

I can continue to do this improvement and show you the result soon.

The ranged based constraint manager is kinda weak, we all know that.

To circumvent such infeasible bugreports, I highly recommend enabling the Z3 refutation (-analyzer-config crosscheck-with-z3=true)
which validates the constraints on the bugpath. Invalidates the bugreport if the constraints are UnSAT.
This option would suppress this report for sure.

Another solution is to make the constraint manager smarter, to reason about sym-sym comparisons, at least for the obvious ones.

My patch under review is partially solving this (still in WIP): D77792

Note that this limitation is well known and understood.
Introducing sym-sym comparisons seems to be valuable, though I’m not entirely sure how would fit into our model.
It would cover some sym-sym-comparisons, but potentially not all of them.
Debugging why a certain comparison evaluated to true/false would be a somewhat cumbersome process even if we dump the ExplodedGraph.

Imagine this example:
void transitivity(int x, int y, int z) {
if (x >= y)
return;
// x < y for sure
if (y >= z)
return;
// y < z for sure
clang_analyzer_eval(x < z); // ?
}

Regards,

Balazs

Denis Petrov via cfe-dev <cfe-dev@lists.llvm.org> ezt írta (időpont: 2020. ápr. 22., Sze, 22:55):