[analyzer][solver] Compute adjustment for unsupported symbols as well

[vsavchenko]

Summary

When the solver sees conditions like a +/- INT cmp INT, it disassembles
such expressions and uses the first integer constant as a so-called "Adjustment".
So it's easier later on to reason about the range of the symbol (a
in this case).

However, conditions of form a +/- INT are not treated the same way,
and we might end up with contradictory constraints.

This patch resolves this issue and extracts "Adjustment" for the
latter case as well.

[steakhal]

Seems reasonable to me. Let's wait for someone else as well.
This is a really elegant patch, I should tell!

[vsavchenko]

In D107636#2931302, @steakhal wrote:

Seems reasonable to me. Let's wait for someone else as well.

Sure, NP.

This is a really elegant patch, I should tell!

Thanks! I guess my take on this, that this path to the solver just got forgotten and that's what produced this inconsistency.

[ASDenysPetrov]

I checked the tests file on the latest sources. It passes even without your changes. Maybe this patch is already outdated.

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

82–86

Do we need the same changes here as below?

[martong]

I am not sure if this patch makes sense at all because the adjustment handling logic is restricted to handle SymInt expressions only.

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

82–86

I believe, the adjustment is deliberately Zero here. This is because we are dealing with a SymSym expr, and the adjustment logic is capable of handling only a SymInt expr.

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

if (BinaryOperator::isEqualityOp(Op)) {
       SymbolRef CanonicalEquality =
           SymMgr.getSymSymExpr(SSE->getLHS(), BO_EQ, SSE->getRHS(), ExprType);
 
       bool WasEqual = SSE->getOpcode() == BO_EQ;
       bool IsExpectedEqual = WasEqual == Assumption;
 
       const llvm::APSInt &Zero = getBasicVals().getValue(0, ExprType);
 
       if (IsExpectedEqual) {
         return assumeSymNE(State, CanonicalEquality, Zero, Zero);
       }
 
       return assumeSymEQ(State, CanonicalEquality, Zero, Zero);
     }
   }
 
   // If we get here, there's nothing else we can do but treat the symbol as
   // opaque.
   return assumeSymUnsupported(State, Sym, Assumption);
 }
 
RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
   QualType T = Sym->getType();
 
   // Non-integer types are not supported.
   if (!T->isIntegralOrEnumerationType())
     return State;
 
   // Reverse the operation and add directly to state.
   const llvm::APSInt &Zero = BVF.getValue(0, T);
+  llvm::APSInt Adjustment = Zero;
+  computeAdjustment(Sym, Adjustment);
+
   if (Assumption)
-    return assumeSymNE(State, Sym, Zero, Zero);
-  else
-    return assumeSymEQ(State, Sym, Zero, Zero);
+    return assumeSymNE(State, Sym, Zero, Adjustment);
+
+  return assumeSymEQ(State, Sym, Zero, Adjustment);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
                                                       SymbolRef Sym,
                                                       BinaryOperator::Opcode Op,
                                                       const llvm::APSInt &Int) {
   assert(BinaryOperator::isComparisonOp(Op) &&
          "Non-comparison ops should be rewritten as comparisons to zero.");

clang/test/Analysis/infeasible_paths.c

+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+
+// expected-no-diagnostics
+
+void clang_analyzer_warnIfReached();
+
+void unsupportedSymAssumption_1(int a) {
+  int b = a + 1;
+  if (b + 1)
+    return;
+  // At this point, b == -1, a == -2
+  // and this condition is always true.
+  if (b < 1)
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+}
+
+void unsupportedSymAssumption_2(int a) {
+  int b = a - 1;
+  if (!b)
+    return;
+  if (b)
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+}