[analyzer] Translate "a != b" to "(b - a) != 0" in the constraint manager.

Canonicalizing these two forms allows us to better model containers like
std::vector, which use "m_start != m_finish" to implement empty() but
"m_finish - m_start" to implement size(). The analyzer should have a
consistent interpretation of these two symbolic expressions, even though
it's not properly reasoning about either one yet.

The other unfortunate thing is that while the size() expression will only
ever be written "m_finish - m_start", the comparison may be written
"m_finish == m_start" or "m_start == m_finish". Right now the analyzer does
not attempt to canonicalize those two expressions, since it doesn't know
which length expression to pick. Doing this correctly will probably require
implementing unary minus as a new SymExpr kind (<rdar://problem/12351075>).

For now, the analyzer inverts the order of arguments in the comparison to
build the subtraction, on the assumption that "begin() != end()" is
written more often than "end() != begin()". This is purely speculation.

<rdar://problem/13239003>

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

1 files changed, 3 insertions, 3 deletions

diff --git a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index d397e47224..216fb3d4b0 100644
--- a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -285,8 +285,8 @@ namespace {
 class RangeConstraintManager : public SimpleConstraintManager{
   RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
 public:
-  RangeConstraintManager(SubEngine *subengine, BasicValueFactory &BVF)
-    : SimpleConstraintManager(subengine, BVF) {}
+  RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
+    : SimpleConstraintManager(subengine, SVB) {}
 
   ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
                              const llvm::APSInt& Int,
@@ -328,7 +328,7 @@ private:
 
 ConstraintManager *
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
-  return new RangeConstraintManager(Eng, StMgr.getBasicVals());
+  return new RangeConstraintManager(Eng, StMgr.getSValBuilder());
 }
 
 const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,