[Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions

[baloghadamsoftware]

Summary

Patch SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option) not only rearranges comparisons but also binary expressions. This latter behavior is not protected by the analyzer option. Hower, since no complexity threshold is enforced to the symbols this may result in exponential execution time if the expressions are too complex: Huge static analysis performance regression for very simple testcase. For a quick fix we extended the analyzer option to also cover the additive cases.

This is only a temporary fix, the final solution should be enforcing the complexity threshold to the symbols.

[NoQ]

I was thinking of two flags, but that'll work too.

[mikhail.ramalho]

I getting the following error when analyzing test/Analysis/plist-macros.cpp, usign z3 as constraint manager (-analyzer-constraints=z3 -DANALYZER_CM_Z3):

/home/mgadelha/llvm/tools/clang/test/Analysis/plist-macros.cpp:640:16: error: CHECK-NEXT: expected string not found in input
// CHECK-NEXT: <key>line</key><integer>36</integer>
               ^
/home/mgadelha/llvm/build/tools/clang/test/Analysis/Output/plist-macros.cpp.tmp.plist:562:2: note: scanning from here
 <key>line</key><integer>37</integer>
 ^

I bisected back to this commit. I reverted it locally and the error goes away.

Any idea why it doesn't work with z3?

[NoQ]

In D49536#1176128, @mikhail.ramalho wrote:

I getting the following error when analyzing test/Analysis/plist-macros.cpp, usign z3 as constraint manager (-analyzer-constraints=z3 -DANALYZER_CM_Z3):

/home/mgadelha/llvm/tools/clang/test/Analysis/plist-macros.cpp:640:16: error: CHECK-NEXT: expected string not found in input
// CHECK-NEXT: <key>line</key><integer>36</integer>
               ^
/home/mgadelha/llvm/build/tools/clang/test/Analysis/Output/plist-macros.cpp.tmp.plist:562:2: note: scanning from here
 <key>line</key><integer>37</integer>
 ^

I bisected back to this commit. I reverted it locally and the error goes away.

Any idea why it doesn't work with z3?

Uhm, dunno, plist/FileCheck tests are annoying. What i usually do to make sense out of them is update the tested output with the actual output and look at git diff. From that it's usually obvious what exactly happened (warnings added, warnings removed, warnings moved to a different location, intermediate diagnostics added, intermediate diagnostics removed, intermediate diagnostics moved to a different location). Could you do that and see if it makes sense or attach the diff here so that we could have a look?

[mikhail.ramalho]

Uhm, dunno, plist/FileCheck tests are annoying. What i usually do to make sense out of them is update the tested output with the actual output and look at git diff. From that it's usually obvious what exactly happened (warnings added, warnings removed, warnings moved to a different location, intermediate diagnostics added, intermediate diagnostics removed, intermediate diagnostics moved to a different location). Could you do that and see if it makes sense or attach the diff here so that we could have a look?

The diff using Z3 is the removal of all lines inserted in plist-macros.cpp by this commit. I think it's a note in the first if (assuming condition is true) of:

#define noPathNoteMacro y+y
int macroInExpressionNoNote(int *p, int y) {
  y++;
  if (5 + noPathNoteMacro)
    if (p)
      ;
  return *p; // expected-warning {{Dereference of null pointer}}
}

Maybe using Z3 as CM, the CSA finds the other path, where the condition is false?

[NoQ]

The "Assuming..." diagnostic piece isn't the same as "Taking true/false branch" diagnostic piece. The former indicates that a constraint is added. The latter indicate how the path flows between program points.

The absence of "Assuming..." indicates that Z3 didn't need to make an assumption; it already knew that the condition is true.

I understand how Z3 could figure this out. Indeed, 5 + (y + 1) + (y + 1) = 2y + 7 is an odd number, and therefore it cannot be equal to 0.

I don't understand how our rearrangement could figure this out. Might it have been an incorrect rearrangement?

In any case, it is clear that both behaviors are currently correct and the test needs to be updated to reflect the Z3's superpower. I suggest using FileCheck's -check-prefixes= to highlight the difference. See cfg-rich-constructors.cpp for an example of how to use those.

cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h

private:
   Optional<bool> WidenLoops;
 
   /// \sa shouldUnrollLoops
   Optional<bool> UnrollLoops;
 
   /// \sa shouldDisplayNotesAsEvents
   Optional<bool> DisplayNotesAsEvents;
 
-  /// \sa shouldAggressivelySimplifyRelationalComparison
-  Optional<bool> AggressiveRelationalComparisonSimplification;
+  /// \sa shouldAggressivelySimplifyBinaryOperation
+  Optional<bool> AggressiveBinaryOperationSimplification;
 
   /// \sa getCTUDir
   Optional<StringRef> CTUDir;
 
   /// \sa getCTUIndexName
   Optional<StringRef> CTUIndexName;
 
   /// \sa naiveCTUEnabled
public:
   /// Returns true if the bug reporter should transparently treat extra note
   /// diagnostic pieces as event diagnostic pieces. Useful when the diagnostic
   /// consumer doesn't support the extra note pieces.
   ///
   /// This is controlled by the 'extra-notes-as-events' option, which defaults
   /// to false when unset.
   bool shouldDisplayNotesAsEvents();
 
-  /// Returns true if SValBuilder should rearrange comparisons of symbolic
-  /// expressions which consist of a sum of a symbol and a concrete integer
-  /// into the format where symbols are on the left-hand side and the integer
-  /// is on the right. This is only done if both symbols and both concrete
-  /// integers are signed, greater than or equal to the quarter of the minimum
-  /// value of the type and less than or equal to the quarter of the maximum
-  /// value of that type.
-  ///
-  /// A + n <REL> B + m becomes A - B <REL> m - n, where A and B symbolic,
-  /// n and m are integers. <REL> is any of '==', '!=', '<', '<=', '>' or '>='.
-  /// The rearrangement also happens with '-' instead of '+' on either or both
-  /// side and also if any or both integers are missing.
-  bool shouldAggressivelySimplifyRelationalComparison();
+  /// Returns true if SValBuilder should rearrange comparisons and additive
+  /// operations of symbolic expressions which consist of a sum of a symbol and
+  /// a concrete integer into the format where symbols are on the left-hand
+  /// side and the integer is on the right. This is only done if both symbols
+  /// and both concrete integers are signed, greater than or equal to the
+  /// quarter of the minimum value of the type and less than or equal to the
+  /// quarter of the maximum value of that type.
+  ///
+  /// A + n <OP> B + m becomes A - B <OP> m - n, where A and B symbolic,
+  /// n and m are integers. <OP> is any of '==', '!=', '<', '<=', '>', '>=',
+  /// '+' or '-'. The rearrangement also happens with '-' instead of '+' on
+  // either or both side and also if any or both integers are missing.
+  bool shouldAggressivelySimplifyBinaryOperation();
 
   /// Returns the directory containing the CTU related files.
   StringRef getCTUDir();
 
   /// Returns the name of the file containing the CTU index of functions.
   StringRef getCTUIndexName();
 
   /// Returns true when naive cross translation unit analysis is enabled.

cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp

 
 bool AnalyzerOptions::shouldDisplayNotesAsEvents() {
   if (!DisplayNotesAsEvents.hasValue())
     DisplayNotesAsEvents =
         getBooleanOption("notes-as-events", /*Default=*/false);
   return DisplayNotesAsEvents.getValue();
 }
 
-bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() {
-  if (!AggressiveRelationalComparisonSimplification.hasValue())
-    AggressiveRelationalComparisonSimplification =
-      getBooleanOption("aggressive-relational-comparison-simplification",
+bool AnalyzerOptions::shouldAggressivelySimplifyBinaryOperation() {
+  if (!AggressiveBinaryOperationSimplification.hasValue())
+    AggressiveBinaryOperationSimplification =
+      getBooleanOption("aggressive-binary-operation-simplification",
                        /*Default=*/false);
-  return AggressiveRelationalComparisonSimplification.getValue();
+  return AggressiveBinaryOperationSimplification.getValue();
 }
 
 StringRef AnalyzerOptions::getCTUDir() {
   if (!CTUDir.hasValue()) {
     CTUDir = getOptionAsString("ctu-dir", "");
     if (!llvm::sys::fs::is_directory(*CTUDir))
       CTUDir = "";
   }

cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

static Optional<NonLoc> tryRearrange(ProgramStateRef State,
   SValBuilder &SVB = StateMgr.getSValBuilder();
 
   // We expect everything to be of the same type - this type.
   QualType SingleTy;
 
   auto &Opts =
     StateMgr.getOwningEngine()->getAnalysisManager().getAnalyzerOptions();
 
+  // FIXME: After putting complexity threshold to the symbols we can always
+  //        rearrange additive operations but rearrange comparisons only if
+  //        option is set.
+  if(!Opts.shouldAggressivelySimplifyBinaryOperation())
+    return None;
+
   SymbolRef LSym = Lhs.getAsSymbol();
   if (!LSym)
     return None;
 
-  // Always rearrange additive operations but rearrange comparisons only if
-  // option is set.
-  if (BinaryOperator::isComparisonOp(Op) &&
-      Opts.shouldAggressivelySimplifyRelationalComparison()) {
+  if (BinaryOperator::isComparisonOp(Op)) {
     SingleTy = LSym->getType();
     if (ResultTy != SVB.getConditionType())
       return None;
     // Initialize SingleTy later with a symbol's type.
   } else if (BinaryOperator::isAdditiveOp(Op)) {
     SingleTy = ResultTy;
     if (LSym->getType() != SingleTy)
       return None;

cfe/trunk/test/Analysis/constraint_manager_negate_difference.c

-// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-binary-operation-simplification=true -verify %s
 
 void clang_analyzer_eval(int);
 
 void exit(int);
 
 #define UINT_MAX (~0U)
 #define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
 #define INT_MIN (UINT_MAX & ~(UINT_MAX >> 1))

cfe/trunk/test/Analysis/iterator-range.cpp

-// RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,alpha.cplusplus.IteratorRange -analyzer-eagerly-assume -analyzer-config aggressive-relational-comparison-simplification=true -analyzer-config c++-container-inlining=false %s -verify
-// RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,alpha.cplusplus.IteratorRange -analyzer-eagerly-assume -analyzer-config aggressive-relational-comparison-simplification=true -analyzer-config c++-container-inlining=true -DINLINE=1 %s -verify
+// RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,alpha.cplusplus.IteratorRange -analyzer-eagerly-assume -analyzer-config aggressive-binary-operation-simplification=true -analyzer-config c++-container-inlining=false %s -verify
+// RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,alpha.cplusplus.IteratorRange -analyzer-eagerly-assume -analyzer-config aggressive-binary-operation-simplification=true -analyzer-config c++-container-inlining=true -DINLINE=1 %s -verify
 
 #include "Inputs/system-header-simulator-cxx.h"
 
 void clang_analyzer_warnIfReached();
 
 void simple_good_end(const std::vector<int> &v) {
   auto i = v.end();
   if (i != v.end()) {

cfe/trunk/test/Analysis/plist-macros.cpp

 // CHECK-NEXT:            <key>line</key><integer>36</integer>
 // CHECK-NEXT:            <key>col</key><integer>4</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:          </array>
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:        </dict>
+// CHECK-NEXT:       </array>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>event</string>
+// CHECK-NEXT:      <key>location</key>
+// CHECK-NEXT:      <dict>
+// CHECK-NEXT:       <key>line</key><integer>36</integer>
+// CHECK-NEXT:       <key>col</key><integer>7</integer>
+// CHECK-NEXT:       <key>file</key><integer>0</integer>
+// CHECK-NEXT:      </dict>
+// CHECK-NEXT:      <key>ranges</key>
+// CHECK-NEXT:      <array>
+// CHECK-NEXT:        <array>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>36</integer>
+// CHECK-NEXT:          <key>col</key><integer>7</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>36</integer>
+// CHECK-NEXT:          <key>col</key><integer>25</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:        </array>
+// CHECK-NEXT:      </array>
+// CHECK-NEXT:      <key>depth</key><integer>0</integer>
+// CHECK-NEXT:      <key>extended_message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:      <key>message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>control</string>
+// CHECK-NEXT:      <key>edges</key>
+// CHECK-NEXT:       <array>
+// CHECK-NEXT:        <dict>
+// CHECK-NEXT:         <key>start</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:         <key>end</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
 // CHECK-NEXT:            <key>line</key><integer>37</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
 // CHECK-NEXT:            <key>line</key><integer>37</integer>
 // CHECK-NEXT:            <key>col</key><integer>6</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>

cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c

-// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-binary-operation-simplification=true -verify %s
 
 void clang_analyzer_dump(int x);
 void clang_analyzer_eval(int x);
 
 void exit(int);
 
 #define UINT_MAX (~0U)
 #define INT_MAX (UINT_MAX & (UINT_MAX >> 1))