]> granicus.if.org Git - clang/commitdiff
[Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
authorAdam Balogh <adam.balogh@ericsson.com>
Wed, 11 Apr 2018 06:21:12 +0000 (06:21 +0000)
committerAdam Balogh <adam.balogh@ericsson.com>
Wed, 11 Apr 2018 06:21:12 +0000 (06:21 +0000)
Since the range-based constraint manager (default) is weak in handling comparisons where symbols are on both sides it is wise to rearrange them to have symbols only on the left side. Thus e.g. A + n >= B + m becomes A - B >= m - n which enables the constraint manager to store a range m - n .. MAX_VALUE for the symbolic expression A - B. This can be used later to check whether e.g. A + k == B + l can be true, which is also rearranged to A - B == l - k so the constraint manager can check whether l - k is in the range (thus greater than or equal to m - n).

The restriction in this version is the the rearrangement happens only if both the symbols and the concrete integers are within the range [min/4 .. max/4] where min and max are the minimal and maximal values of their type.

The rearrangement is not enabled by default. It has to be enabled by using -analyzer-config aggressive-relational-comparison-simplification=true.

Co-author of this patch is Artem Dergachev (NoQ).

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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@329780 91177308-0d34-0410-b5e6-96231b3b80d8

include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/conditional-path-notes.c
test/Analysis/explain-svals.cpp
test/Analysis/svalbuilder-rearrange-comparisons.c [new file with mode: 0644]

index 17c5c59bccbcf372b4e18aa9104f38cbda089142..ee9419a8a094a8c9ed12ccbafef245976a38709e 100644 (file)
@@ -312,6 +312,9 @@ private:
   /// \sa shouldDisplayNotesAsEvents
   Optional<bool> DisplayNotesAsEvents;
 
+  /// \sa shouldAggressivelySimplifyRelationalComparison
+  Optional<bool> AggressiveRelationalComparisonSimplification;
+
   /// \sa getCTUDir
   Optional<StringRef> CTUDir;
 
@@ -666,6 +669,20 @@ public:
   /// 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 the directory containing the CTU related files.
   StringRef getCTUDir();
 
index 65231ea8ce7880b941d9e3278ea84dc8e4b5e2b5..33e482dd40773ffc91e1adbc16256b5314be2eca 100644 (file)
@@ -445,6 +445,14 @@ bool AnalyzerOptions::shouldDisplayNotesAsEvents() {
   return DisplayNotesAsEvents.getValue();
 }
 
+bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() {
+  if (!AggressiveRelationalComparisonSimplification.hasValue())
+    AggressiveRelationalComparisonSimplification =
+      getBooleanOption("aggressive-relational-comparison-simplification",
+                       /*Default=*/false);
+  return AggressiveRelationalComparisonSimplification.getValue();
+}
+
 StringRef AnalyzerOptions::getCTUDir() {
   if (!CTUDir.hasValue()) {
     CTUDir = getOptionAsString("ctu-dir", "");
index 0ec4a81af3e6b546507e402341efdd34d3f6c7b5..b2224b5495b7fa70e0df8f760d29031c07e1bfdc 100644 (file)
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 
 using namespace clang;
@@ -307,6 +309,192 @@ SVal SimpleSValBuilder::MakeSymIntVal(const SymExpr *LHS,
   return makeNonLoc(LHS, op, *ConvertedRHS, resultTy);
 }
 
+// See if Sym is known to be a relation Rel with Bound.
+static bool isInRelation(BinaryOperator::Opcode Rel, SymbolRef Sym,
+                         llvm::APSInt Bound, ProgramStateRef State) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  SVal Result =
+      SVB.evalBinOpNN(State, Rel, nonloc::SymbolVal(Sym),
+                      nonloc::ConcreteInt(Bound), SVB.getConditionType());
+  if (auto DV = Result.getAs<DefinedSVal>()) {
+    return !State->assume(*DV, false);
+  }
+  return false;
+}
+
+// See if Sym is known to be within [min/4, max/4], where min and max
+// are the bounds of the symbol's integral type. With such symbols,
+// some manipulations can be performed without the risk of overflow.
+// assume() doesn't cause infinite recursion because we should be dealing
+// with simpler symbols on every recursive call.
+static bool isWithinConstantOverflowBounds(SymbolRef Sym,
+                                           ProgramStateRef State) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  BasicValueFactory &BV = SVB.getBasicValueFactory();
+
+  QualType T = Sym->getType();
+  assert(T->isSignedIntegerOrEnumerationType() &&
+         "This only works with signed integers!");
+  APSIntType AT = BV.getAPSIntType(T);
+
+  llvm::APSInt Max = AT.getMaxValue() / AT.getValue(4), Min = -Max;
+  return isInRelation(BO_LE, Sym, Max, State) &&
+         isInRelation(BO_GE, Sym, Min, State);
+}
+
+// Same for the concrete integers: see if I is within [min/4, max/4].
+static bool isWithinConstantOverflowBounds(llvm::APSInt I) {
+  APSIntType AT(I);
+  assert(!AT.isUnsigned() &&
+         "This only works with signed integers!");
+
+  llvm::APSInt Max = AT.getMaxValue() / AT.getValue(4), Min = -Max;
+  return (I <= Max) && (I >= -Max);
+}
+
+static std::pair<SymbolRef, llvm::APSInt>
+decomposeSymbol(SymbolRef Sym, BasicValueFactory &BV) {
+  if (const auto *SymInt = dyn_cast<SymIntExpr>(Sym))
+    if (BinaryOperator::isAdditiveOp(SymInt->getOpcode()))
+      return std::make_pair(SymInt->getLHS(),
+                            (SymInt->getOpcode() == BO_Add) ?
+                            (SymInt->getRHS()) :
+                            (-SymInt->getRHS()));
+
+  // Fail to decompose: "reduce" the problem to the "$x + 0" case.
+  return std::make_pair(Sym, BV.getValue(0, Sym->getType()));
+}
+
+// Simplify "(LSym + LInt) Op (RSym + RInt)" assuming all values are of the
+// same signed integral type and no overflows occur (which should be checked
+// by the caller).
+static NonLoc doRearrangeUnchecked(ProgramStateRef State,
+                                   BinaryOperator::Opcode Op,
+                                   SymbolRef LSym, llvm::APSInt LInt,
+                                   SymbolRef RSym, llvm::APSInt RInt) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  BasicValueFactory &BV = SVB.getBasicValueFactory();
+  SymbolManager &SymMgr = SVB.getSymbolManager();
+
+  QualType SymTy = LSym->getType();
+  assert(SymTy == RSym->getType() &&
+         "Symbols are not of the same type!");
+  assert(APSIntType(LInt) == BV.getAPSIntType(SymTy) &&
+         "Integers are not of the same type as symbols!");
+  assert(APSIntType(RInt) == BV.getAPSIntType(SymTy) &&
+         "Integers are not of the same type as symbols!");
+
+  QualType ResultTy;
+  if (BinaryOperator::isComparisonOp(Op))
+    ResultTy = SVB.getConditionType();
+  else if (BinaryOperator::isAdditiveOp(Op))
+    ResultTy = SymTy;
+  else
+    llvm_unreachable("Operation not suitable for unchecked rearrangement!");
+
+  // FIXME: Can we use assume() without getting into an infinite recursion?
+  if (LSym == RSym)
+    return SVB.evalBinOpNN(State, Op, nonloc::ConcreteInt(LInt),
+                           nonloc::ConcreteInt(RInt), ResultTy)
+        .castAs<NonLoc>();
+
+  SymbolRef ResultSym = nullptr;
+  BinaryOperator::Opcode ResultOp;
+  llvm::APSInt ResultInt;
+  if (BinaryOperator::isComparisonOp(Op)) {
+    // Prefer comparing to a non-negative number.
+    // FIXME: Maybe it'd be better to have consistency in
+    // "$x - $y" vs. "$y - $x" because those are solver's keys.
+    if (LInt > RInt) {
+      ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy);
+      ResultOp = BinaryOperator::reverseComparisonOp(Op);
+      ResultInt = LInt - RInt; // Opposite order!
+    } else {
+      ResultSym = SymMgr.getSymSymExpr(LSym, BO_Sub, RSym, SymTy);
+      ResultOp = Op;
+      ResultInt = RInt - LInt; // Opposite order!
+    }
+  } else {
+    ResultSym = SymMgr.getSymSymExpr(LSym, Op, RSym, SymTy);
+    ResultInt = (Op == BO_Add) ? (LInt + RInt) : (LInt - RInt);
+    ResultOp = BO_Add;
+    // Bring back the cosmetic difference.
+    if (ResultInt < 0) {
+      ResultInt = -ResultInt;
+      ResultOp = BO_Sub;
+    } else if (ResultInt == 0) {
+      // Shortcut: Simplify "$x + 0" to "$x".
+      return nonloc::SymbolVal(ResultSym);
+    }
+  }
+  const llvm::APSInt &PersistentResultInt = BV.getValue(ResultInt);
+  return nonloc::SymbolVal(
+      SymMgr.getSymIntExpr(ResultSym, ResultOp, PersistentResultInt, ResultTy));
+}
+
+// Rearrange if symbol type matches the result type and if the operator is a
+// comparison operator, both symbol and constant must be within constant
+// overflow bounds.
+static bool shouldRearrange(ProgramStateRef State, BinaryOperator::Opcode Op,
+                            SymbolRef Sym, llvm::APSInt Int, QualType Ty) {
+  return Sym->getType() == Ty &&
+    (!BinaryOperator::isComparisonOp(Op) ||
+     (isWithinConstantOverflowBounds(Sym, State) && 
+      isWithinConstantOverflowBounds(Int)));
+}
+
+static Optional<NonLoc> tryRearrange(ProgramStateRef State,
+                                     BinaryOperator::Opcode Op, NonLoc Lhs,
+                                     NonLoc Rhs, QualType ResultTy) {
+  ProgramStateManager &StateMgr = State->getStateManager();
+  SValBuilder &SVB = StateMgr.getSValBuilder();
+
+  // We expect everything to be of the same type - this type.
+  QualType SingleTy;
+
+  auto &Opts =
+    StateMgr.getOwningEngine()->getAnalysisManager().getAnalyzerOptions();
+
+  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()) {
+    SingleTy = LSym->getType();
+    if (ResultTy != SVB.getConditionType())
+      return None;
+    // Initialize SingleTy later with a symbol's type.
+  } else if (BinaryOperator::isAdditiveOp(Op)) {
+    SingleTy = ResultTy;
+    // Substracting unsigned integers is a nightmare.
+    if (!SingleTy->isSignedIntegerOrEnumerationType())
+      return None;
+  } else {
+    // Don't rearrange other operations.
+    return None;
+  }
+
+  assert(!SingleTy.isNull() && "We should have figured out the type by now!");
+
+  SymbolRef RSym = Rhs.getAsSymbol();
+  if (!RSym || RSym->getType() != SingleTy)
+    return None;
+
+  BasicValueFactory &BV = State->getBasicVals();
+  llvm::APSInt LInt, RInt;
+  std::tie(LSym, LInt) = decomposeSymbol(LSym, BV);
+  std::tie(RSym, RInt) = decomposeSymbol(RSym, BV);
+  if (!shouldRearrange(State, Op, LSym, LInt, SingleTy) ||
+      !shouldRearrange(State, Op, RSym, RInt, SingleTy))
+    return None;
+
+  // 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,
@@ -559,6 +747,9 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
       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.
       return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
     }
index d842b7fc6eefd2541337d1c39e6768d01396ee7f..0ccf40f4cd1a3932e839f80773c755d86d7c7746 100644 (file)
@@ -78,6 +78,7 @@ void testDiagnosableBranchLogical(int a, int b) {
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
     // expected-note@-1 {{Taking true branch}}
+    // expected-note@-2 {{Assuming the condition is true}}
     *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
     // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>79</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>79</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>79</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>79</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>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>11</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>79</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>79</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>82</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>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1594,12 +1658,12 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:         <key>start</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</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>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1607,12 +1671,12 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1624,7 +1688,7 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:      <key>kind</key><string>event</string>
 // CHECK-NEXT:      <key>location</key>
 // CHECK-NEXT:      <dict>
-// CHECK-NEXT:       <key>line</key><integer>81</integer>
+// CHECK-NEXT:       <key>line</key><integer>82</integer>
 // CHECK-NEXT:       <key>col</key><integer>24</integer>
 // CHECK-NEXT:       <key>file</key><integer>0</integer>
 // CHECK-NEXT:      </dict>
@@ -1632,12 +1696,12 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:      <array>
 // CHECK-NEXT:        <array>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</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>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>26</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
@@ -1658,10 +1722,10 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:    <key>issue_hash_content_of_line_in_context</key><string>f56671e5f67c73abef619b56f7c29fa4</string>
 // CHECK-NEXT:   <key>issue_context_kind</key><string>function</string>
 // CHECK-NEXT:   <key>issue_context</key><string>testNonDiagnosableBranchArithmetic</string>
-// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>3</string>
+// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>4</string>
 // CHECK-NEXT:   <key>location</key>
 // CHECK-NEXT:   <dict>
-// CHECK-NEXT:    <key>line</key><integer>81</integer>
+// CHECK-NEXT:    <key>line</key><integer>82</integer>
 // CHECK-NEXT:    <key>col</key><integer>24</integer>
 // CHECK-NEXT:    <key>file</key><integer>0</integer>
 // CHECK-NEXT:   </dict>
index ecb5af1f8efb0aad1ec3a89846f004bcb26f7223..c1b5200eb8e924766a8166c4e1d45762ffef05df 100644 (file)
@@ -69,7 +69,7 @@ void test_4(int x, int y) {
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re{{{{^\(argument 'x'\) \+ 1$}}}}
   clang_analyzer_explain(1 + y); // expected-warning-re{{{{^\(argument 'y'\) \+ 1$}}}}
-  clang_analyzer_explain(x + y); // expected-warning-re{{{{^unknown value$}}}}
+  clang_analyzer_explain(x + y); // expected-warning-re{{{{^\(argument 'x'\) \+ \(argument 'y'\)$}}}}
   clang_analyzer_explain(z); // expected-warning-re{{{{^undefined value$}}}}
   clang_analyzer_explain(&z); // expected-warning-re{{{{^pointer to local variable 'z'$}}}}
   clang_analyzer_explain(stat); // expected-warning-re{{{{^signed 32-bit integer '0'$}}}}
diff --git a/test/Analysis/svalbuilder-rearrange-comparisons.c b/test/Analysis/svalbuilder-rearrange-comparisons.c
new file mode 100644 (file)
index 0000000..47366d2
--- /dev/null
@@ -0,0 +1,931 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-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))
+
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+    unsigned int __line, __const char *__function)
+     __attribute__ ((__noreturn__));
+#define assert(expr) \
+  ((expr)  ? (void)(0)  : __assert_fail (#expr, __FILE__, __LINE__, __func__))
+
+int g();
+int f() {
+  int x = g();
+  // Assert that no overflows occur in this test file.
+  // Assuming that concrete integers are also within that range.
+  assert(x <= ((int)INT_MAX / 4));
+  assert(x >= -((int)INT_MAX / 4));
+  return x;
+}
+
+void compare_different_symbol_equal() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_same_symbol_equal() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_equal() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_int_equal() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less_or_equal() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_same_symbol_less() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_int_less() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_int_less() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_right_int_less() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_right_int_less() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_different_symbol_equal_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_same_symbol_equal_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_equal_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_equal_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less_or_equal_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_same_symbol_less_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_int_less_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void overflow(signed char n, signed char m) {
+  if (n + 0 > m + 0) {
+    clang_analyzer_eval(n - 126 == m + 3); // expected-warning{{UNKNOWN}}
+  }
+}