[clang] f0d6cb4 - [analyzer] Canonicalize SymIntExpr so the RHS is positive when possible

Balazs Benics via cfe-commits cfe-commits at lists.llvm.org
Thu May 5 08:49:04 PDT 2022


Author: Tomasz KamiƄski
Date: 2022-05-05T17:48:49+02:00
New Revision: f0d6cb4a5cf5723d7ddab2c7dab74f2f62116a6d

URL: https://github.com/llvm/llvm-project/commit/f0d6cb4a5cf5723d7ddab2c7dab74f2f62116a6d
DIFF: https://github.com/llvm/llvm-project/commit/f0d6cb4a5cf5723d7ddab2c7dab74f2f62116a6d.diff

LOG: [analyzer] Canonicalize SymIntExpr so the RHS is positive when possible

This PR changes the `SymIntExpr` so the expression that uses a
negative value as `RHS`, for example: `x +/- (-N)`, is modeled as
`x -/+ N` instead.

This avoids producing a very large `RHS` when the symbol is cased to
an unsigned number, and as consequence makes the value more robust in
presence of casts.

Note that this change is not applied if `N` is the lowest negative
value for which negation would not be representable.

Reviewed By: steakhal

Patch By: tomasz-kaminski-sonarsource!

Differential Revision: https://reviews.llvm.org/D124658

Added: 
    clang/test/Analysis/additive-op-on-sym-int-expr.c

Modified: 
    clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
    clang/test/Analysis/expr-inspection.c

Removed: 
    


################################################################################
diff  --git a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
index 65c2564637c18..27e474866c297 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -197,8 +197,27 @@ SVal SimpleSValBuilder::MakeSymIntVal(const SymExpr *LHS,
       if (RHS.isSigned() && !SymbolType->isSignedIntegerOrEnumerationType())
         ConvertedRHS = &BasicVals.Convert(SymbolType, RHS);
     }
-  } else
+  } else if (BinaryOperator::isAdditiveOp(op) && RHS.isNegative()) {
+    // Change a+(-N) into a-N, and a-(-N) into a+N
+    // Adjust addition/subtraction of negative value, to
+    // subtraction/addition of the negated value.
+    APSIntType resultIntTy = BasicVals.getAPSIntType(resultTy);
+    assert(resultIntTy.getBitWidth() >= RHS.getBitWidth() &&
+           "The result operation type must have at least the same "
+           "number of bits as its operands.");
+
+    llvm::APSInt ConvertedRHSValue = resultIntTy.convert(RHS);
+    // Check if the negation of the RHS is representable:
+    // * if resultIntTy is unsigned, then negation is always representable
+    // * if resultIntTy is signed, and RHS is not the lowest representable
+    //   signed value
+    if (resultIntTy.isUnsigned() || !ConvertedRHSValue.isMinSignedValue()) {
+      ConvertedRHS = &BasicVals.getValue(-ConvertedRHSValue);
+      op = (op == BO_Add) ? BO_Sub : BO_Add;
+    }
+  } else {
     ConvertedRHS = &BasicVals.Convert(resultTy, RHS);
+  }
 
   return makeNonLoc(LHS, op, *ConvertedRHS, resultTy);
 }
@@ -636,16 +655,27 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
               const llvm::APSInt &first = IntType.convert(symIntExpr->getRHS());
               const llvm::APSInt &second = IntType.convert(*RHSValue);
 
+              // If the op and lop agrees, then we just need to
+              // sum the constants. Otherwise, we change to operation
+              // type if substraction would produce negative value
+              // (and cause overflow for unsigned integers),
+              // as consequence x+1U-10 produces x-9U, instead
+              // of x+4294967287U, that would be produced without this
+              // additional check.
               const llvm::APSInt *newRHS;
-              if (lop == op)
+              if (lop == op) {
                 newRHS = BasicVals.evalAPSInt(BO_Add, first, second);
-              else
+              } else if (first >= second) {
                 newRHS = BasicVals.evalAPSInt(BO_Sub, first, second);
+                op = lop;
+              } else {
+                newRHS = BasicVals.evalAPSInt(BO_Sub, second, first);
+              }
 
               assert(newRHS && "Invalid operation despite common type!");
               rhs = nonloc::ConcreteInt(*newRHS);
               lhs = nonloc::SymbolVal(symIntExpr->getLHS());
-              op = lop;
+
               continue;
             }
           }

diff  --git a/clang/test/Analysis/additive-op-on-sym-int-expr.c b/clang/test/Analysis/additive-op-on-sym-int-expr.c
new file mode 100644
index 0000000000000..c9385f58c980f
--- /dev/null
+++ b/clang/test/Analysis/additive-op-on-sym-int-expr.c
@@ -0,0 +1,58 @@
+// RUN: %clang_analyze_cc1 -triple=x86_64-unknown-linux -analyzer-checker=core,debug.ExprInspection -analyzer-config eagerly-assume=false -verify %s
+
+void clang_analyzer_dump(int);
+void clang_analyzer_dumpL(long);
+void clang_analyzer_warnIfReached();
+
+void testInspect(int x) {
+  if ((x < 10) || (x > 100)) {
+    return;
+  }
+  // x: [10, 100]
+
+  int i = x + 1;
+  long l = i - 10U;
+  clang_analyzer_dump(i);       // expected-warning-re {{(reg_${{[0-9]+}}<int x>) + 1 }}
+  clang_analyzer_dumpL(l);      // expected-warning-re {{(reg_${{[0-9]+}}<int x>) - 9U }} instead of + 4294967287U
+  clang_analyzer_dumpL(l + 0L); // expected-warning-re {{(reg_${{[0-9]+}}<int x>) - 9 }}  instead of + 4294967287
+
+  if ((l - 1000) > 0) {
+    clang_analyzer_warnIfReached(); // no-warning
+  }
+  if (l > 1000) {
+    clang_analyzer_warnIfReached(); // no-warning
+  }
+  if (l > 1000L) {
+    clang_analyzer_warnIfReached(); // no-warning
+  }
+  if ((l + 0L) > 1000) {
+    clang_analyzer_warnIfReached(); // no-warning
+  }
+
+  i = x - 1;
+  l = i + 10U;
+  clang_analyzer_dumpL(l); // expected-warning-re {{(reg_${{[0-9]+}}<int x>) + 9U }} instead of - 4294967287U
+
+  i = x + (-1);
+  l = i - 10U;
+  clang_analyzer_dumpL(l); // expected-warning-re {{(reg_${{[0-9]+}}<int x>) - 11U }} instead of + 4294967285U
+
+  i = x + 1U;
+  l = i - 10U;
+  clang_analyzer_dumpL(l); // expected-warning-re {{(reg_${{[0-9]+}}<int x>) - 9U }} instead of + 4294967287U
+}
+
+void testMin(int i, long l) {
+  clang_analyzer_dump(i + (-1));  // expected-warning-re {{(reg_${{[0-9]+}}<int i>) - 1 }} instead of + -1
+  clang_analyzer_dump(i - (-1));  // expected-warning-re {{(reg_${{[0-9]+}}<int i>) + 1 }} instead of - -1
+  clang_analyzer_dumpL(l + (-1)); // expected-warning-re {{(reg_${{[0-9]+}}<long l>) - 1 }} instead of + -1
+  clang_analyzer_dumpL(l - (-1)); // expected-warning-re {{(reg_${{[0-9]+}}<long l>) + 1 }} instead of - -1
+
+  int intMin = 1 << (sizeof(int) * 8 - 1); // INT_MIN, negative value is not representable
+  // Do not normalize representation if negation would not be representable
+  clang_analyzer_dump(i + intMin); // expected-warning-re {{(reg_${{[0-9]+}}<int i>) + -2147483648 }}
+  clang_analyzer_dump(i - intMin); // expected-warning-re {{(reg_${{[0-9]+}}<int i>) - -2147483648 }}
+  // Produced value has higher bit with (long) so negation if representable
+  clang_analyzer_dumpL(l + intMin); // expected-warning-re {{(reg_${{[0-9]+}}<long l>) - 2147483648 }} instead of + -2147483648
+  clang_analyzer_dumpL(l - intMin); // expected-warning-re {{(reg_${{[0-9]+}}<long l>) + 2147483648 }} instead of - -2147483648
+}

diff  --git a/clang/test/Analysis/expr-inspection.c b/clang/test/Analysis/expr-inspection.c
index bd05b2b3c3251..33c90f95bc782 100644
--- a/clang/test/Analysis/expr-inspection.c
+++ b/clang/test/Analysis/expr-inspection.c
@@ -11,7 +11,7 @@ void clang_analyzer_numTimesReached(void);
 
 void foo(int x) {
   clang_analyzer_dump(x); // expected-warning{{reg_$0<int x>}}
-  clang_analyzer_dump(x + (-1)); // expected-warning{{(reg_$0<int x>) + -1}}
+  clang_analyzer_dump(x + (-1)); // expected-warning{{(reg_$0<int x>) - 1}}
   int y = 1;
   for (; y < 3; ++y) {
     clang_analyzer_numTimesReached(); // expected-warning{{2}}


        


More information about the cfe-commits mailing list