[Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[martong]

Summary

Make the SValBuilder capable to simplify existing
SVals based on a newly added constraints when evaluating a BinOp.

Before this patch, we called simplify only in some edge cases.
However, we can and should investigate the constraints in all cases.

[steakhal]

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

378

It seems like you simplify the rhs as well. Could we have a test for that?

clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp

14

Please declare x in this statement.

[martong]

I'm attaching the coverage of the new test file for the related change:

375             :   // Constraints may have changed since the creation of a bound SVal. Check if
376             :   // the values can be simplified based on those new constraints.
377          12 :   SVal simplifiedLhs = simplifySVal(state, lhs);
378          12 :   SVal simplifiedRhs = simplifySVal(state, rhs);
379          12 :   if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs<NonLoc>())
380          12 :     lhs = *simplifiedLhsAsNonLoc;
381          12 :   if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs<NonLoc>())
382          12 :     rhs = *simplifiedRhsAsNonLoc;
383             :

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

378

Ok, I've added a new test case and reworked the existing a bit.

[martong]

• Add new test case

[steakhal]

Awesome!

[martong]

I'm attaching the coverage of the new test file for the related change:

375             :   // Constraints may have changed since the creation of a bound SVal. Check if
376             :   // the values can be simplified based on those new constraints.
377          12 :   SVal simplifiedLhs = simplifySVal(state, lhs);
378          12 :   SVal simplifiedRhs = simplifySVal(state, rhs);
379          12 :   if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs<NonLoc>())
380          12 :     lhs = *simplifiedLhsAsNonLoc;
381          12 :   if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs<NonLoc>())
382          12 :     rhs = *simplifiedRhsAsNonLoc;
383             :

[bjope]

This seem to cause some weird results.

Given this input:

bar(short k) {
  k++;
  for (short f = 0; f < k; f++)
    ;
  (long)k << 16;
}

we get

> clang  --analyze --target=x86_64 'bbi-63538.c'
bbi-63538.c:5:11: warning: The result of the left shift is undefined due to shifting '1' by '16', which is unrepresentable in the unsigned version of the return type 'long' [core.UndefinedBinaryOperatorResult]
  (long)k << 16;
  ~~~~~~~ ^
bbi-63538.c:5:11: warning: The result of the left shift is undefined due to shifting '2' by '16', which is unrepresentable in the unsigned version of the return type 'long' [core.UndefinedBinaryOperatorResult]
  (long)k << 16;
  ~~~~~~~ ^
bbi-63538.c:5:11: warning: The result of the left shift is undefined due to shifting '3' by '16', which is unrepresentable in the unsigned version of the return type 'long' [core.UndefinedBinaryOperatorResult]
  (long)k << 16;
  ~~~~~~~ ^
3 warnings generated.

[steakhal]

In D113753#3156270, @bjope wrote:

This seem to cause some weird results.

Given this input:

bar(short k) {
  k++;
  for (short f = 0; f < k; f++)
    ;
  (long)k << 16;
}

we get

> clang  --analyze --target=x86_64 'bbi-63538.c'
bbi-63538.c:5:11: warning: The result of the left shift is undefined due to shifting '1' by '16', which is unrepresentable in the unsigned version of the return type 'long' [core.UndefinedBinaryOperatorResult]
  (long)k << 16;
  ~~~~~~~ ^
bbi-63538.c:5:11: warning: The result of the left shift is undefined due to shifting '2' by '16', which is unrepresentable in the unsigned version of the return type 'long' [core.UndefinedBinaryOperatorResult]
  (long)k << 16;
  ~~~~~~~ ^
bbi-63538.c:5:11: warning: The result of the left shift is undefined due to shifting '3' by '16', which is unrepresentable in the unsigned version of the return type 'long' [core.UndefinedBinaryOperatorResult]
  (long)k << 16;
  ~~~~~~~ ^
3 warnings generated.

Good catch @bjope !
Here is an example without the loop: https://godbolt.org/z/z3rqMz4bs
We'll have a closer look.

[martong]

Here is a smaller reproducer:

void bar(short k) {
  ++k;             // k1 = k0 + 1
  assert(k == 1);  // k1 == 1 --> k0 == 0
  (long)k << 16;   // k0 + 1 <<  16
}

And the explanation is the following. With this patch, when the analyzer evaluates the (long)k << 16 expression then it can properly deduce the value of k being 1. However, it was not possible in the baseline. Since we do not model neither promotion nor explicit casts we get the false positive report. This issue highlights the importance of the patch stack to implement the modeling of casts (starting with https://reviews.llvm.org/D99797).

[steakhal]

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

372

@martong, you simplified the operands, but you overwrite only the lhs and rhs. Shouldnt you overwite these as well?
What is the purpose of these variables, do you know?

[martong]

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

372

@martong, you simplified the operands, but you overwrite only the lhs and rhs. Shouldnt you overwite these as well?
What is the purpose of these variables, do you know?

They are used exclusively to create SymExprs with makeSymExprValNN when both lhs and rhs are symbols. If we were to simplify the Input variables then it might happen that we end up with a non symbol (i.e. a concrete int) and then makeSymExprValNN would fail miserably (would assert I guess).

[steakhal]

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

372

I see. Although, it still seems suboptimal.

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

static Optional<NonLoc> tryRearrange(ProgramStateRef State,
   // We know that no overflows can occur anymore.
   return doRearrangeUnchecked(State, Op, LSym, LInt, RSym, RInt);
 }
 
 SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
                                   BinaryOperator::Opcode op,
                                   NonLoc lhs, NonLoc rhs,
                                   QualType resultTy)  {
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs<NonLoc>())
+    lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs<NonLoc>())
+    rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
     switch (op) {
       default:
         break;
       case BO_EQ:
       case BO_LE:
       case BO_GE:
case nonloc::SymbolValKind: {
             }
           }
 
           // Otherwise, make a SymIntExpr out of the expression.
           return MakeSymIntVal(symIntExpr, op, *RHSValue, resultTy);
         }
       }
 
-      // Does the symbolic expression simplify to a constant?
-      // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
-      // and try again.
-      SVal simplifiedLhs = simplifySVal(state, lhs);
-      if (simplifiedLhs != lhs)
-        if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs<NonLoc>()) {
-          lhs = *simplifiedLhsAsNonLoc;
-          continue;
-        }
-
       // Is the RHS a constant?
       if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
         return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
 
       if (Optional<NonLoc> V = tryRearrange(state, op, lhs, rhs, resultTy))
         return *V;
 
       // Give up -- this is not a symbolic expression we can handle.

clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp

+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies_lhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+    return;
+
+  // Below `x` is the LHS being simplified.
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
+
+void test_evalBinOp_simplifies_rhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+    return;
+
+  // Below `x` is the RHS being simplified.
+  clang_analyzer_eval(1 == x); // expected-warning{{TRUE}}
+  (void)(x * y);
+}