[PATCH] D49703: [analyzer] pr38273: Admit that we can't handle the newly produced Loc<>NonLoc comparisons.

[Artem Dergachev via Phabricator via cfe-commits]

NoQ created this revision.
NoQ added reviewers: dcoughlin, xazax.hun, a.sidorin, george.karpenkov, szepet, rnkovacs, mikhail.ramalho.
Herald added subscribers: cfe-commits, baloghadamsoftware.

This patch fixes the crash caused by https://reviews.llvm.org/D48650 and reported as https://bugs.llvm.org/show_bug.cgi?id=38273 by removing the assertion.

`SValBuilder` now produces a lot more `SymSymExpr` symbolic expressions, some of which the rest of the Analyzer has never seen before. Moreover, for some of them, we've never made a conscious decision on how exactly do we want them to be represented in our `SVal`/`SymExpr`/`MemRegion` hierarchy.

This patch deals with the results of comparing a `nonloc::LocAsInteger` to an integer-type symbol, which through the emergent behavior introduced in https://reviews.llvm.org/D48650 results in a `SymSymExpr` that has its LHS and RHS have different `Loc`-ness. This behavior discards the information contained in both `nonloc::LocAsInteger` and `SymbolicRegion` for the `Loc`-typed side and probably more information if there are wrapper regions around the `SymbolicRegion` (i //hope// it works correctly, but i didn't check).

So the bigger problem here is where exactly do we want to move with the `nonloc::LocAsInteger` thing as it repeatedly gets in our way. If we want to keep it, we want to make some sort of `SymLocAsIntegerExpr` (and `LocAsIntegerSymExpr` respectively) that would represent results of such operations, and then the assertion would need to be brought back.

If we want to remove `nonloc::LocAsInteger` entirely, it'd simplify our hierarchy of values quite a bit, and i think it's a good thing, but it immediately strikes us with a bigger problem: our symbolic expressions and our region offsets represent the same thing but in completely different manners, so every conversion from `Loc` to `NonLoc` and vice versa would require us to convert one representation to the other (eg., `element{SymRegion{$p}, $i, int}` <=> `$p + ($i * 4)`). The whole idea behind `LocAsInteger` is to kinda hide this problem, but in any case we can't really avoid it.


Repository:
  rC Clang

https://reviews.llvm.org/D49703

Files:
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  test/Analysis/casts.c


Index: test/Analysis/casts.c
===================================================================
--- test/Analysis/casts.c
+++ test/Analysis/casts.c
@@ -171,3 +171,7 @@
   (*((int *)(&x))) = (int)(unsigned *)getVoidPtr();
   *x = 1; // no-crash
 }
+
+void testLocNonLocSymbolAssume(int a, int *b) {
+  if ((int)b < a) {}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -343,9 +343,11 @@
       if (BinaryOperator::isEqualityOp(SSE->getOpcode()) ||
           BinaryOperator::isRelationalOp(SSE->getOpcode())) {
         // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+        // We've recently started producing Loc <> NonLoc comparisons (that
+        // result from casts of one of the operands between eg. intptr_t and
+        // void *), but we can't reason about them yet.
         if (Loc::isLocType(SSE->getLHS()->getType())) {
-          assert(Loc::isLocType(SSE->getRHS()->getType()));
-          return true;
+          return Loc::isLocType(SSE->getRHS()->getType());
         }
       }
     }


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D49703.156891.patch
Type: text/x-patch
Size: 1224 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180723/7d3b2c14/attachment.bin>