[analyzer] Fix constraint being dropped when analyzing a program without taint tracking enabled

[mikhail.ramalho]

Summary

This patch removes the constraint dropping when taint tracking is disabled.

It also voids the crash reported in D28953 by treating a SymSymExpr with non pointer symbols as an opaque expression.

Updated the regressions and verifying the big projects now; I'll update here when they're done.

Based on the discussion on the mailing list and the patches by @ddcc.

[NoQ]

+Adam because that's a lot of stuff he's interested in and his tests are affected.

Do we need a complexity threshold like in the original revision?:

// Use a lower bound to avoid recursive blowup, e.g. on PR24184.cpp
if (V.getSymbol()->computeComplexity() > 10)
  ...

I.e., could the same test be rewritten to cause performance problems on the current patch?

[ddcc]

I don't see any #ifdef for the tests. Do they pass both with and without z3? I recall needing to case out the expected test output before.

Because he's not extending the SValBuilder visitors, it's possible the complexity threshold won't be a problem. But regardless, I think it would be good practice to allow runtime configuration of the complexity threshold.

For reference, my stale version is D35450. I haven't rebased yet to remove the APSInt fixes that have been merged.

[baloghadamsoftware]

Do the tests pass now because of rL333670?

[mikhail.ramalho]

In D48650#1146592, @baloghadamsoftware wrote:

Do the tests pass now because of rL333670?

Actually, one test is crashing because of D32642. The following cast in lib/StaticAnalyzer/Checkers/IteratorChecker.cpp:1168:

return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);

A SymExpr object is reaching that call and the cast fails.

[baloghadamsoftware]

In D48650#1146720, @mikhail.ramalho wrote:

Actually, one test is crashing because of D32642. The following cast in lib/StaticAnalyzer/Checkers/IteratorChecker.cpp:1168:

return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);

A SymExpr object is reaching that call and the cast fails.

Thank you for pointing me this! The iterator checker may have worked incorrectly (but did not crash) without your patch. Now I fixed that, it works correctly and does not crash with your patch. I added my patch as parent revision for yours.

[mikhail.ramalho]

In D48650#1147755, @baloghadamsoftware wrote:

In D48650#1146720, @mikhail.ramalho wrote:

Actually, one test is crashing because of D32642. The following cast in lib/StaticAnalyzer/Checkers/IteratorChecker.cpp:1168:

return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);

A SymExpr object is reaching that call and the cast fails.

Thank you for pointing me this! The iterator checker may have worked incorrectly (but did not crash) without your patch. Now I fixed that, it works correctly and does not crash with your patch. I added my patch as parent revision for yours.

Nice, thanks for fixing it.

[mikhail.ramalho]

Just found a test where this patch removes a true positive: test/Analysis/PR37855.c.

The path that leads to the second bug:

n[1].node->s; // expected-warning {{Dereference of undefined pointer value}}

is removed because the CSA is removing the branch where the loop termination condition node != l is false, which is the one that leads to the bug.

[george.karpenkov]

Just found a test where this patch

@mikhail.ramalho I don't really follow your description, could you clarify?

[mikhail.ramalho]

In D48650#1148091, @george.karpenkov wrote:

Just found a test where this patch

@mikhail.ramalho I don't really follow your description, could you clarify?

Ok, this is the test:

typedef struct o p;
struct o {
  struct {
  } s;
};

void q(*r, p2) { r < p2; }

void k(l, node) {
  struct {
    p *node;
  } * n, *nodep, path[sizeof(void)];
  path->node = l;
  for (n = path; node != l;) {
    q(node, n->node);
    nodep = n;
  }
  if (nodep)
    n[1].node->s; // warning: Dereference of undefined pointer value
}

Without this patch, the graph shows that the bugs is found when the loop is unrolled once and terminates. When this happens, nodep contains a valid value n (which is path), so a new core.NullDereference node is created to check the expression n[1].node->s;.

With this patch, since the constraints are not being dropped, it knows that neither node nor l change, so the loop doesn't terminate after the first iteration and the CSA doesn't evaluate anything after the loop.

However, there is another path that triggers the bug, when node != l holds, the loop body is not evaluated and, if nodep happens to be not null, n[1].node->s is a real bug. This path is not evaluated by the CSA, I only see a core.uninitialized.branch node and the analysis stops there. Am I correct to assume that, since if (nodep) is undefined behaviour in this path (nodep is uninitialized), the static analyzer doesn't evaluate it?

[george.karpenkov]

Am I correct to assume that, since if (nodep) is undefined behaviour in this path (nodep is uninitialized), the static analyzer doesn't evaluate it?

Yeah, so once we reach if (nodep) we are already reading from an uninitialized variable, and that should be reported as a bug.
So you see it in the exploded graph, but not in the analyzer report?

[mikhail.ramalho]

In D48650#1148173, @george.karpenkov wrote:

Am I correct to assume that, since if (nodep) is undefined behaviour in this path (nodep is uninitialized), the static analyzer doesn't evaluate it?

Yeah, so once we reach if (nodep) we are already reading from an uninitialized variable, and that should be reported as a bug.
So you see it in the exploded graph, but not in the analyzer report?

The CSA correctly reports:

arena.c:18:7: warning: Branch condition evaluates to a garbage value
  if (nodep)
      ^~~~~

but not:

arena.c:19:5: warning: Dereference of undefined pointer value
    n[1].node->s; // warning: Dereference of undefined pointer value
    ^~~~~~~~~~~~

[george.karpenkov]

but not:

That's expected, since the above error message is fatal, and the path is killed.
I'm fine with changing the test.
@NoQ any objections?

[george.karpenkov]

test/Analysis/svalbuilder-rearrange-comparisons.c

563 ↗

(On Diff #153094)

Those FIXME's could probably be dropped.
@baloghadamsoftware Comments?

[mikhail.ramalho]

test/Analysis/svalbuilder-rearrange-comparisons.c

563 ↗

(On Diff #153094)

I left them there because there are several cases in this file that are simplified to either TRUE or FALSE.

[george.karpenkov]

@mikhail.ramalho But they are clearly neither true nor false, right?

[mikhail.ramalho]

In D48650#1148254, @george.karpenkov wrote:

@mikhail.ramalho But they are clearly neither true nor false, right?

Indeed, most of them are something like conj_$2{int} == conj_$2{int} or conj_$2{int} < conj_$2{int}.

[NoQ]

Am I correct to assume that, since if (nodep) is undefined behaviour in this path (nodep is uninitialized), the static analyzer doesn't evaluate it?

Yep. Even if it wasn't undefined behavior but only unspecified value, we would still interrupt the analysis because otherwise we'd just get a bunch of duplicate warnings about the same uninitialized value used all over the place.

test/Analysis/svalbuilder-rearrange-comparisons.c

563 ↗

(On Diff #153094)

I guess the ultimate purpose of the test is to simplify "(x + 1) == x" to "1 == 0".

[george.karpenkov]

test/Analysis/svalbuilder-rearrange-comparisons.c

563 ↗

(On Diff #153094)

Ah right, I see. Z3 should be able to do that here.

[NoQ]

test/Analysis/svalbuilder-rearrange-comparisons.c

563 ↗

(On Diff #153094)

Not here, but ultimately yeah it'd help with the original problem.

[mikhail.ramalho]

Update test case

[george.karpenkov]

Oh sorry I've referenced wrong revision in the commit. Re-opening.

[mikhail.ramalho]

Revert back to the previous diff.

[george.karpenkov]

@mikhail.ramalho please resubmit with -U999

[mikhail.ramalho]

Update diff with -U99999

[mikhail.ramalho]

Decreased default complexity threshold to 25 as it finds the same amount of bugs as 10000 in the following projects: tmux, git, openssl, postgresql, redis, sqlite3, tmux and twin. Going < 25, and a number of bugs stop being reported.

Also, removed the FIXMEs from the test.

[george.karpenkov]

@mikhail.ramalho Could you also state how different values affect the effectivity of refutation?

[mikhail.ramalho]

In D48650#1157689, @george.karpenkov wrote:

@mikhail.ramalho Could you also state how different values affect the effectivity of refutation?

Hi, the same bugs are removed, with threshold 25 and 10000:

• redis: 1 removed
• openssl: 2 removed
• git: 11 removed
• postgresql: 5 removed
• sqlite3: 14 removed

With complexity 10000, however, the verification time of openSSL went from 260s to 1500s. The other were roughly the same (~20s slower at most).

[mikhail.ramalho]

Fix expected warning locations

[george.karpenkov]

LGTM with a nit. We'll watch the bots after this is merged.

test/Analysis/bitwise-ops.c

11 ↗

(On Diff #154861)

I think this comment can be dropped.

[mikhail.ramalho]

Removed comment.

[NoQ]

This commit causes an assertion failure on void foo(int a, int *b) { (int)b < a; }

Run-line: clang -cc1 -analyze -analyzer-checker=core -analyzer-eagerly-assume test.c

So it kinda frustrates RangeConstraintManager with a SymSymExpr that expresses a comparison between a Loc and a NonLoc symbol.

I'll think a bit more on how do i want to address that.

[Ka-Ka]

In D48650#1165966, @NoQ wrote:

This commit causes an assertion failure on void foo(int a, int *b) { (int)b < a; }

Run-line: clang -cc1 -analyze -analyzer-checker=core -analyzer-eagerly-assume test.c

So it kinda frustrates RangeConstraintManager with a SymSymExpr that expresses a comparison between a Loc and a NonLoc symbol.

I'll think a bit more on how do i want to address that.

Earlier today I created an issue in bugzilla for this problem.
https://bugs.llvm.org/show_bug.cgi?id=38273
However, the reproducer presented here is smaller and much nicer. I will update the issue in bugzilla.

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

 unsigned AnalyzerOptions::getGraphTrimInterval() {
   if (!GraphTrimInterval.hasValue())
     GraphTrimInterval = getOptionAsInteger("graph-trim-interval", 1000);
   return GraphTrimInterval.getValue();
 }
 
 unsigned AnalyzerOptions::getMaxSymbolComplexity() {
   if (!MaxSymbolComplexity.hasValue())
-    MaxSymbolComplexity = getOptionAsInteger("max-symbol-complexity", 10000);
+    MaxSymbolComplexity = getOptionAsInteger("max-symbol-complexity", 25);
   return MaxSymbolComplexity.getValue();
 }
 
 unsigned AnalyzerOptions::getMaxTimesInlineLarge() {
   if (!MaxTimesInlineLarge.hasValue())
     MaxTimesInlineLarge = getOptionAsInteger("max-times-inline-large", 32);
   return MaxTimesInlineLarge.getValue();
 }

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

if (isa<SymbolData>(Sym)) {
     // calculations ("end - begin"). The more correct thing to do would be to
     // canonicalize "a - b" and "b - a", which would allow us to treat
     // "a != b" and "b != a" the same.
     SymbolManager &SymMgr = getSymbolManager();
     BinaryOperator::Opcode Op = SSE->getOpcode();
     assert(BinaryOperator::isComparisonOp(Op));
 
     // For now, we only support comparing pointers.
-    assert(Loc::isLocType(SSE->getLHS()->getType()));
-    assert(Loc::isLocType(SSE->getRHS()->getType()));
+    if (Loc::isLocType(SSE->getLHS()->getType()) &&
+        Loc::isLocType(SSE->getRHS()->getType())) {
       QualType DiffTy = SymMgr.getContext().getPointerDiffType();
       SymbolRef Subtraction =
           SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
 
       const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
       Op = BinaryOperator::reverseComparisonOp(Op);
       if (!Assumption)
         Op = BinaryOperator::negateComparisonOp(Op);
       return assumeSymRel(State, Subtraction, Op, Zero);
     }
+  }
 
   // If we get here, there's nothing else we can do but treat the symbol as
   // opaque.
   return assumeSymUnsupported(State, Sym, Assumption);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,

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

Optional<SVal> SValBuilder::getConstantVal(const Expr *E) {
   }
   }
 }
 
 SVal SValBuilder::makeSymExprValNN(ProgramStateRef State,
                                    BinaryOperator::Opcode Op,
                                    NonLoc LHS, NonLoc RHS,
                                    QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-    return UnknownVal();
-
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();
+
   // TODO: When the Max Complexity is reached, we should conjure a symbol
   // instead of generating an Unknown value and propagate the taint info to it.
   const unsigned MaxComp = StateMgr.getOwningEngine()
                                ->getAnalysisManager()
                                .options.getMaxSymbolComplexity();
 
   if (symLHS && symRHS &&
       (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)

cfe/trunk/test/Analysis/PR37855.c

struct {
     p *node;
   } * n, *nodep, path[sizeof(void)];
   path->node = l;
   for (n = path; node != l;) {
     q(node, n->node);
     nodep = n;
   }
   if (nodep) // expected-warning {{Branch condition evaluates to a garbage value}}
-    n[1].node->s; // expected-warning {{Dereference of undefined pointer value}}
+    n[1].node->s;
 }

cfe/trunk/test/Analysis/bitwise-ops.c

 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -triple x86_64-apple-darwin13 -Wno-shift-count-overflow -verify %s
 
 void clang_analyzer_eval(int);
 #define CHECK(expr) if (!(expr)) return; clang_analyzer_eval(expr)
 
 void testPersistentConstraints(int x, int y) {
   // Sanity check
   CHECK(x); // expected-warning{{TRUE}}
   CHECK(x & 1); // expected-warning{{TRUE}}
   
-  // False positives due to SValBuilder giving up on certain kinds of exprs.
-  CHECK(1 - x); // expected-warning{{UNKNOWN}}
-  CHECK(x & y); // expected-warning{{UNKNOWN}}
+  CHECK(1 - x); // expected-warning{{TRUE}}
+  CHECK(x & y); // expected-warning{{TRUE}}
 }
 
 int testConstantShifts_PR18073(int which) {
   // FIXME: We should have a checker that actually specifically checks bitwise
   // shifts against the width of the LHS's /static/ type, rather than just
   // having BasicValueFactory return "undefined" when dealing with two constant
   // operands.
   switch (which) {

cfe/trunk/test/Analysis/std-c-library-functions.c

 size_t fread(void *, size_t, size_t, FILE *);
 size_t fwrite(const void *restrict, size_t, size_t, FILE *restrict);
 void test_fread_fwrite(FILE *fp, int *buf) {
   size_t x = fwrite(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(x <= 10); // expected-warning{{TRUE}}
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
 void test_getline(FILE *fp) {
   char *line = 0;
   size_t n = 0;
   ssize_t len;
   while ((len = getline(&line, &n, fp)) != -1) {

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

 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) + 1U) == (conj_$2{int})}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) - 1U) == (conj_$2{int})}}
 }
 
 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?
+  // expected-warning@-1{{(conj_$2{int}) == ((conj_$2{int}) + 1U)}}
 }
 
 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?
+  // expected-warning@-1{{(conj_$2{int}) == ((conj_$2{int}) - 1U)}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) + 1U) == ((conj_$2{int}) - 1U)}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) - 1U) == ((conj_$2{int}) + 1U)}}
 }
 
 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);

 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) + 1U) <= (conj_$2{int})}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) - 1U) <= (conj_$2{int})}}
 }
 
 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?
+  // expected-warning@-1{{(conj_$2{int}) <= ((conj_$2{int}) + 1U)}}
 }
 
 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?
+  // expected-warning@-1{{(conj_$2{int}) <= ((conj_$2{int}) - 1U)}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) + 1U) <= ((conj_$2{int}) - 1U)}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) - 1U) <= ((conj_$2{int}) + 1U)}}
 }
 
 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);

 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) + 1U) < (conj_$2{int})}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) - 1U) < (conj_$2{int})}}
 }
 
 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?
+  // expected-warning@-1{{(conj_$2{int}) < ((conj_$2{int}) + 1U)}}
 }
 
 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?
+  // expected-warning@-1{{(conj_$2{int}) < ((conj_$2{int}) - 1U)}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) + 1U) < ((conj_$2{int}) - 1U)}}
 }
 
 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?
+  // expected-warning@-1{{((conj_$2{int}) - 1U) < ((conj_$2{int}) + 1U)}}
 }
 
 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);