[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:496
 
+  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    if (SSE->getOpcode() == BO_Sub) {
----------------
With this, it sounds as if we're half-way into finally supporting the unary minus operator (:

Could you add a FIXME here: "Once SValBuilder supports unary minus, we should use SValBuilder to obtain the negated symbolic expression instead of constructing the symbol manually. This will allow us to support finding ranges of not only negated SymSymExpr-type expressions, but also of other, simpler expressions which we currently do not know how to negate."


================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:499-504
+      // If the type of A - B is the same as the type of A, then use the type of
+      // B as the type of B - A. Otherwise keep the type of A - B.
+      SymbolRef negSym = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+                                              SSE->getLHS(),
+                                              (T == SSE->getLHS()->getType()) ?
+                                              SSE->getRHS()->getType() : T);
----------------
I'm quite sure that types of `A - B` and `B - A` are always equal when it comes to integer promotion rules.

Also, due to our broken `SymbolCast` (which is often missing where it ideally should be), the type of the `A - B` symbol may not necessarily be the same as the type that you obtain by applying integer promotion rules to types of `A` and `B`.

So i think you should always take the type of `A - B` and expect to find `B - A` of the same type in the range map, otherwise give up.


================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+           SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+           SSE->getLHS()->getType()->isPointerType()) {
+          return negV->Negate(BV, F);
----------------
Pointer types are currently treated as unsigned, so i'm not sure you want them here.


================
Comment at: test/Analysis/ptr-arith.c:268-270
 //-------------------------------
 // False positives
 //-------------------------------
----------------
The tests that are now supported should be moved above this comment.


https://reviews.llvm.org/D35110