[analyzer][solver] Improve reasoning for not equal to operator

[manas]

Summary

This patch fixes certain cases where solver was not able to infer
disequality due to overlapping of values in rangeset. This case was
casting from lower signed type to bigger unsigned type.

[manas]

Rebase

[steakhal]

Thanks for going the extra mile to address this last thing. I really appreciate it.
I've got only a few minor comments and suggestions.

I'd recommend spell-checking the comments and the summary of this revision.
See my technical comments inline.

The test coverage looks good to me.

Good job.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1639

I think in this context != should achieve the same, and we usually prefer this operator for this.

1639–1640

I was thinking that maybe if (LHS.isUnsigned() && RHS.isSigned()) {} ... else if (LHS.isSigned() && RHS.isUnsigned()) results in cleaner code, as it would require one level fewer indentations.
The control-flow looks complicated already enough.

1640

Why do we need this additional condition?
If I remove these, I get no test failures, which suggests to me that we have some undertested code paths here.

1642–1647

1664–1667

I was thinking of using init-ifs, but on second thought I'm not sure if that's more readable.

if (RHS.getAPSIntType().convert(LHS.getMaxValue()) < RHS.getMinValue())
  return getTrueRange(T);

Shouldn't be too bad.

[manas]

In D140086#3998426, @steakhal wrote:

Thanks for going the extra mile to address this last thing. I really appreciate it.
I've got only a few minor comments and suggestions.

I'd recommend spell-checking the comments and the summary of this revision.
See my technical comments inline.

Thank you once again for reviewing @steakhal :)

I did the spell-checking.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1639–1640

I was thinking that maybe if (LHS.isUnsigned() && RHS.isSigned()) {} ... else if (LHS.isSigned() && RHS.isUnsigned()) results in cleaner code

I did this, and I also combined both blocks into one to remove redundant code.

1640

Why do we need this additional condition?

Bitwidth was important because we should ideally cast smaller bitwidth type to bigger bitwidth type.

Consider if we have LHS(u8), RHS(i32), then without checking for bitwidth, we would be casting RHS's maxValue to LHS's type, which will result in lose of information and will not serve our purpose.

1664–1667

I think its readable. But to combine two blocks into one, I had to use different variable names, which makes this expression bigger. Should we still go with init-ifs?

[manas]

Remove redundant branches

[steakhal]

About spellings. In the summary you used 'lesser', I think as a synonym for 'smaller' or something like that. Anyway, not important.
Great stuff.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1640

If you think we need that bitwidth check, why did you remove it?
I'd like to see test cases demonstrating what we are talking about and see if we want that behavior or not.

1640

Interesting. I like it. I'd however recommend to move this and the other variable to the beginning of this guarded block. That way it would be easier to see that the guard condition relates to this ternary condition.

[manas]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1640

This test fails.

void testfoo(unsigned char u, signed int s) {
  if (u >= 253 && u <= 255 && s < INT_MAX - 2) {
    // u: [253, 254], s: [INT_MIN, INT_MAX - 2]
    clang_analyzer_eval(u != s); // expected-warning{{UNKNOWN}}
                                 // but returns TRUE
  }
}

[steakhal]

Bitwidth was important because we should ideally cast smaller bitwidth type to bigger bitwidth type.
Consider if we have LHS(u8), RHS(i32), then without checking for bitwidth, we would be casting RHS's maxValue to LHS's type, which will result in lose of information and will not serve our purpose.

If you think we need that bitwidth check, why did you remove it?
I'd like to see test cases demonstrating what we are talking about and see if we want that behavior or not.

This test fails.

void testfoo(unsigned char u, signed int s) {
  if (u >= 253 && u <= 255 && s < INT_MAX - 2) {
    // u: [253, 254], s: [INT_MIN, INT_MAX - 2]
    clang_analyzer_eval(u != s); // expected-warning{{UNKNOWN}}
                                 // but returns TRUE
  }
}

I feel like we have something to talk about.
When I do the review pro bono, I'd like to focus on higher-level issues and let the submitter deal with the smaller concerns.
That's why I'm expecting the submitter to:

• Explain in the summary what the patch aims to solve (aka. why did your work on it)
• What & how it implemented it
• What obstacles you had when you tried to implement it? Because the reviewer will most likely think the same way, it's better to highlight what you tried and why you failed that way.
• Most importantly, attach the test cases you uncovered during development about the edge-cases of the previous point.

I'm also expecting that the change compiles, works, and is well-tested. This generally means that tests are covering all the branches in the modified parts and the change runs and are capable of analyzing non-trivial projects without crashing or producing unacceptable reports.
In particular, the Core and the range-based solver are the foundation of the engine, hence even more rigorous testing is required, so correctness is a must in these contexts.

Coming back to this review, I don't want to validate the correctness of the math. I trust you to do this, which you prove by tests or (Z3 solution in addition to that).
Getting more concrete, returning Unknown is fine, but returning the wrong answer like True for cases where we should not be able to deduce it, it's a serious issue.

I hope it helps to align us.

[manas]

Re-introduce bitwidth comparison

[manas]

In D140086#4010175, @steakhal wrote:

This test fails.

void testfoo(unsigned char u, signed int s) {
  if (u >= 253 && u <= 255 && s < INT_MAX - 2) {
    // u: [253, 254], s: [INT_MIN, INT_MAX - 2]
    clang_analyzer_eval(u != s); // expected-warning{{UNKNOWN}}
                                 // but returns TRUE
  }
}

I feel like we have something to talk about.
When I do the review pro bono, I'd like to focus on higher-level issues and let the submitter deal with the smaller concerns.

I think there has been some miscommunication. When I mentioned the failing example, I didn't mean to leave/delegate the pending work.

Nonetheless, I fixed it by re-introducing bitwidth comparison. Here is a Z3 proof https://gist.github.com/weirdsmiley/a9917815e71e4ec09e076522df039841

[manas]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1641–1642

I combined the two conditionals as they both were returning TrueRange. Is it readable?

[steakhal]

Sorry, I don't have the time this week.

[manas]

Gentle ping.

[steakhal]

Looks good. Thanks.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(RangeSet LHS,
                                                            RangeSet RHS,
                                                            QualType T) {
   assert(!LHS.isEmpty() && !RHS.isEmpty());
 
   if (LHS.getAPSIntType() == RHS.getAPSIntType()) {
     if (intersect(RangeFactory, LHS, RHS).isEmpty())
       return getTrueRange(T);
+
   } else {
+    // We can only lose information if we are casting smaller signed type to
+    // bigger unsigned type. For e.g.,
+    //    LHS (unsigned short): [2, USHRT_MAX]
+    //    RHS   (signed short): [SHRT_MIN, 0]
+    //
+    // Casting RHS to LHS type will leave us with overlapping values
+    //    CastedRHS : [0, 0] U [SHRT_MAX + 1, USHRT_MAX]
+    //
+    // We can avoid this by checking if signed type's maximum value is lesser
+    // than unsigned type's minimum value.
+
+    // If both have different signs then only we can get more information.
+    if (LHS.isUnsigned() != RHS.isUnsigned()) {
+      if (LHS.isUnsigned() && (LHS.getBitWidth() >= RHS.getBitWidth())) {
+        if (RHS.getMaxValue().isNegative() ||
+            LHS.getAPSIntType().convert(RHS.getMaxValue()) < LHS.getMinValue())
+          return getTrueRange(T);
+
+      } else if (RHS.isUnsigned() && (LHS.getBitWidth() <= RHS.getBitWidth())) {
+        if (LHS.getMaxValue().isNegative() ||
+            RHS.getAPSIntType().convert(LHS.getMaxValue()) < RHS.getMinValue())
+          return getTrueRange(T);
+      }
+    }
+
     // Both RangeSets should be casted to bigger unsigned type.
     APSIntType CastingType(std::max(LHS.getBitWidth(), RHS.getBitWidth()),
                            LHS.isUnsigned() || RHS.isUnsigned());
 
     RangeSet CastedLHS = RangeFactory.castTo(LHS, CastingType);
     RangeSet CastedRHS = RangeFactory.castTo(RHS, CastingType);
 
     if (intersect(RangeFactory, CastedLHS, CastedRHS).isEmpty())
       return getTrueRange(T);
   }
 
   // In all other cases, the resulting range cannot be deduced.
   return infer(T);
 }
 
 template <>
 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
                                                            QualType T) {
   APSIntType ResultType = ValueFactory.getAPSIntType(T);
   llvm::APSInt Zero = ResultType.getZeroValue();
 
   bool IsLHSPositiveOrZero = LHS.From() >= Zero;
   bool IsRHSPositiveOrZero = RHS.From() >= Zero;
 
[[nodiscard]] std::optional<bool> interpreteAsBool(RangeSet Constraint) {
     return std::nullopt;
   }
 
   ProgramStateRef State;
   SValBuilder &Builder;
   RangeSet::Factory &RangeFactory;
 };
 
-
 bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
                                               const llvm::APSInt &Constraint) {
   llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
   // Iterate over all equivalence classes and try to simplify them.
   ClassMembersTy Members = State->get<ClassMembers>();
   for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
     EquivalenceClass Class = ClassToSymbolSet.first;
     State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);

clang/test/Analysis/constant-folding.c

if (u1 >= INT_MIN && u1 <= INT_MIN + 2 &&
       s1 > INT_MIN + 2 && s1 < INT_MIN + 4) {
     // u1: [INT_MAX+1, INT_MAX+1]U[INT_MAX+4, INT_MAX+4],
     // s1: [INT_MIN+3, INT_MIN+3]
     clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
   }
 
   if (s1 < 0 && s1 > -4 && u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
     // s1: [-3, -1], u1: [UINT_MAX - 3, UINT_MAX - 2]
-    clang_analyzer_eval(u1 != s1); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
+    clang_analyzer_eval(s1 != u1); // expected-warning{{TRUE}}
   }
 
   if (s1 < 1 && s1 > -6 && s1 != -4 && s1 != -3 &&
       u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
     // s1: [-5, -5]U[-2, 0], u1: [UINT_MAX - 3, UINT_MAX - 2]
     clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
   }
 
void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
   }
 
   // Checks for char-uchar types
   if (uch >= 1 && sch <= 1) {
     // uch: [1, UCHAR_MAX], sch: [SCHAR_MIN, 1]
     clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
   }
 
-  // FIXME: Casting smaller signed types to unsigned one may leave us with
-  // overlapping values, falsely indicating UNKNOWN, where it is possible to
-  // assert TRUE.
   if (uch > 1 && sch < 1) {
     // uch: [2, UCHAR_MAX], sch: [SCHAR_MIN, 0]
-    clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(uch != sch); // expected-warning{{TRUE}}
+    clang_analyzer_eval(sch != uch); // expected-warning{{TRUE}}
   }
 
   if (uch <= 1 && uch >= 1 && sch <= 1 && sch >= 1) {
     // uch: [1, 1], sch: [1, 1]
     clang_analyzer_eval(uch != sch); // expected-warning{{FALSE}}
   }
 
   // Checks for short-ushort types
   if (ush >= 1 && ssh <= 1) {
     // ush: [1, USHRT_MAX], ssh: [SHRT_MIN, 1]
     clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
   }
 
-  // FIXME: Casting leave us with overlapping values. Should be TRUE.
   if (ush > 1 && ssh < 1) {
     // ush: [2, USHRT_MAX], ssh: [SHRT_MIN, 0]
-    clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(ush != ssh); // expected-warning{{TRUE}}
   }
 
   if (ush <= 1 && ush >= 1 && ssh <= 1 && ssh >= 1) {
     // ush: [1, 1], ssh: [1, 1]
     clang_analyzer_eval(ush != ssh); // expected-warning{{FALSE}}
   }
 }