[StaticAnalyzer] Try to calculate arithmetic result when operand has a range of possible values

[danielmarjamaki]

Summary

This is a fix for https://bugs.llvm.org/show_bug.cgi?id=32911

In the code below the division result should be a value between 5 and 25.

if (a >= 10 && a <= 50) {
  int b = a / 2;
}

This patch will calculate results for additions, subtractions and divisions.

I intentionally do not try to handle all possible cases that can be handled. I want to know if my approach is ok.

[xazax.hun]

Can't you reuse somehow some machinery already available to evaluate the arithmetic operators? Those should already handle most of your TODOs and overflows.

[danielmarjamaki]

A minor code cleanup. No functional change.

[danielmarjamaki]

In D36471#835410, @xazax.hun wrote:

Can't you reuse somehow some machinery already available to evaluate the arithmetic operators? Those should already handle most of your TODOs and overflows.

Sounds good.. I have not seen that machinery.. I will look around.

To me it seems it would be nice if this machinery was builtin in APSInt so I could calculate (x+y) even if x and y did not have the same signedness and that the result would be unsigned.

[danielmarjamaki]

Refactoring, use BasicValueFactory::evalAPSInt

[danielmarjamaki]

Should evalAPSInt() have machinery to do standard sign/type promotions? I suggest that I add one more argument bool promote = false, do you think that sounds good?

[danielmarjamaki]

minor code cleanup

[danielmarjamaki]

ping

[danielmarjamaki]

ping

[danielmarjamaki]

ping

[danielmarjamaki]

ping

[xazax.hun]

I think this change is very useful but it is also important to get these changes right.
I think one of the main reason you did not get review comments yet is that it is not easy to verify that these changes are sound.

In general, there are false positives in the analyzer due to limits in the constraint manager (or missing parts in modeling the language). But in general, we try to avoid having false positives due to unsound assumptions (apart from some cases like assuming const methods will not change the fields of a class).

While the change you introduced is indeed very useful the soundness probably depends on the details of how promotions, conversions, and other corner cases are handled.
In order to introduce a change like this, we need to have those cases covered to ensure that we have the soundness we want and this needs to be verified with test cases.
Also once the solution is sound it would be great to measure the performance to ensure that we did not regress too much.

I understand that you do not want to work on something that might not get accepted but also with the available information it might be hard to decide whether this is a good approach to the problem or not.
But of course, I am just guessing here, @dcoughlin, @zaks.anna, @NoQ might have a different opinion.

A bit more technical comment: did you consider using SValBuilder's evalBinOpNN? I believe it already handles at least some of the conversions you did not cover here.

[danielmarjamaki]

I have updated the patch so it uses evalBinOpNN. This seems to work properly.

I have a number of TODOs in the test cases that should be fixed. Truncations are not handled properly.

Here is a short example code:

void f(unsigned char X) {
  if (X >= 10 && X <= 50) {
    unsigned char Y = X + 0x100; // truncation
    clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
  }
}

The expected-warning should be TRUE but currently FALSE is written.

When the "Y >= 10" condition is evaluated the ProgramState is:

Store (direct and default bindings), 0x222ab0fe5f8 :
 (Y,0,direct) : (unsigned char) ((reg_$0<unsigned char X>) + 256)

Expressions:
 (0x222a96d6050,0x222ab0eb930) X + 256 : (unsigned char) ((reg_$0<unsigned char X>) + 256)
 (0x222a96d6050,0x222ab0eb960) clang_analyzer_eval : &code{clang_analyzer_eval}
 (0x222a96d6050,0x222ab0eb988) Y : &Y
 (0x222a96d6050,0x222ab0eb9d8) Y : (unsigned char) ((reg_$0<unsigned char X>) + 256)
 (0x222a96d6050,0x222ab0eb9f0) Y : (unsigned char) ((reg_$0<unsigned char X>) + 256)
 (0x222a96d6050,0x222ab0eba08) Y >= 10 : ((unsigned char) ((reg_$0<unsigned char X>) + 256)) >= 10
 (0x222a96d6050,0x222ab0ebb28) clang_analyzer_eval : &code{clang_analyzer_eval}
Ranges of symbol values:
 reg_$0<unsigned char X> : { [10, 50] }
 (reg_$0<unsigned char X>) + 256 : { [10, 50] }

It seems to me that the symbol initialization does not handle the range properly. Imho there is nothing wrong with the calculation. What you think about adding a range like below?

(unsigned char) ((reg_$0<unsigned char X>) + 256) : { [10, 50] }

[danielmarjamaki]

I will not continue working on this. Feel free to take over the patch or write a new patch.

include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

#endif
   virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
                                         SymbolRef sym) const {
     return nullptr;
   }
 
   /// Scan all symbols referenced by the constraints. If the symbol is not
   /// alive, remove it.
   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
-                                                 SymbolReaper& SymReaper) = 0;
+                                             SymbolReaper &SymReaper) = 0;
 
-  virtual void print(ProgramStateRef state,
-                     raw_ostream &Out,
-                     const char* nl,
+  virtual void print(ProgramStateRef state, raw_ostream &Out, const char *nl,
                      const char *sep) = 0;
 
+  virtual ProgramStateRef evalRangeOp(ProgramStateRef state, SVal V) {
+    return nullptr;
+  }
+
   virtual void EndPath(ProgramStateRef state) {}
 
   /// Convenience method to query the state to see if a symbol is null or
   /// not null, or if neither assumption can be made.
   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
 
     return checkNull(State, Sym);

include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h

 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 
 namespace clang {
 
 namespace ento {
 
 class SimpleConstraintManager : public ConstraintManager {
   SubEngine *SU;
+
+protected:
   SValBuilder &SVB;
 
 public:
   SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
       : SU(subengine), SVB(SB) {}
 
   ~SimpleConstraintManager() override;
 

lib/StaticAnalyzer/Core/ExprEngineC.cpp

if (!B->isAssignmentOp()) {
       if (B->getOpcode() == BO_PtrMemD)
         state = createTemporaryRegionIfNeeded(state, LCtx, LHS);
 
       // Process non-assignments except commas or short-circuited
       // logical expressions (LAnd and LOr).
       SVal Result = evalBinOp(state, Op, LeftV, RightV, B->getType());
       if (!Result.isUnknown()) {
         state = state->BindExpr(B, LCtx, Result);
+        ProgramStateRef state2 =
+            getConstraintManager().evalRangeOp(state, Result);
+        Bldr.generateNode(B, *it, state2 ? state2 : state);
+      } else {
+        Bldr.generateNode(B, *it, state);
       }
 
-      Bldr.generateNode(B, *it, state);
       continue;
     }
 
     assert (B->isCompoundAssignmentOp());
 
     switch (Op) {
       default:
         llvm_unreachable("Invalid opcode for compound assignment.");

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override;
 
   ProgramStateRef removeDeadBindings(ProgramStateRef State,
                                      SymbolReaper &SymReaper) override;
 
   void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
              const char *sep) override;
 
+  ProgramStateRef evalRangeOp(ProgramStateRef state, SVal V) override;
+
   //===------------------------------------------------------------------===//
   // Implementation for interface from RangedConstraintManager.
   //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
 
void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
   Out << nl << sep << "Ranges of symbol values:";
   for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
        ++I) {
     Out << nl << ' ' << I.getKey() << " : ";
     I.getData().print(Out);
   }
   Out << nl;
 }
+
+ProgramStateRef RangeConstraintManager::evalRangeOp(ProgramStateRef St,
+                                                    SVal V) {
+  const SymExpr *SE = V.getAsSymExpr();
+  if (!SE)
+    return nullptr;
+
+  const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE);
+  if (!SIE)
+    return nullptr;
+
+  const clang::BinaryOperatorKind Opc = SIE->getOpcode();
+
+  if (Opc != BO_Add && Opc != BO_Sub && Opc != BO_Div)
+    return nullptr;
+
+  const SymExpr *LHS = SIE->getLHS();
+  const llvm::APSInt &RHS = SIE->getRHS();
+
+  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
+  for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
+       ++I) {
+    if (LHS != I.getKey())
+      continue;
+    const auto D = I.getData();
+    for (auto I = D.begin(); I != D.end(); ++I) {
+      NonLoc FromN = SVB.makeIntVal(I->From()).castAs<NonLoc>();
+      NonLoc ToN = SVB.makeIntVal(I->To()).castAs<NonLoc>();
+      NonLoc RHSN = SVB.makeIntVal(RHS).castAs<NonLoc>();
+
+      // Calculate Lower value.
+      SVal Tmp = SVB.evalBinOpNN(St, Opc, FromN, RHSN, LHS->getType());
+      const llvm::APSInt &Lower = Tmp.castAs<nonloc::ConcreteInt>().getValue();
+
+      // Calculate Upper value.
+      Tmp = SVB.evalBinOpNN(St, Opc, ToN, RHSN, LHS->getType());
+      const llvm::APSInt &Upper = Tmp.castAs<nonloc::ConcreteInt>().getValue();
+
+      // TODO: Handle truncations better
+      if (Lower > Upper)
+        continue;
+
+      // Set Range for symbol.
+      SymbolRef Sym = V.getAsSymbol();
+      RangeSet RS =
+          getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+      // TODO: This only evaluates the first range. Evaluate all ranges.
+      return RS.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, RS);
+    }
+  }
+  return nullptr;
+}

test/Analysis/range_calc.c

+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+#define INT_MAX    ((signed int)((~0U)>>1))
+#define INT_MIN    ((signed int)(~((~0U)>>1)))
+
+void addInts(int X)
+{
+  if (X >= 10 && X <= 50) {
+    int Y = X + 2;
+    clang_analyzer_eval(Y >= 12 && Y <= 52); // expected-warning{{TRUE}}
+  }
+  
+  if (X < 5) {
+    int Y = X + 1;
+    clang_analyzer_eval(Y < 6); // expected-warning{{TRUE}}
+  }
+
+  if (X >= 1000) {
+    int Y = X + 1; // might overflow
+    clang_analyzer_eval(Y >= 1001); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(Y == INT_MIN); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(Y == INT_MIN || Y >= 1001); // expected-warning{{TRUE}}
+  }
+}
+
+void addU8(unsigned char X)
+{
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = X + 2;
+    clang_analyzer_eval(Y >= 12 && Y <= 52); // expected-warning{{TRUE}}
+  }
+  
+  if (X < 5) {
+    unsigned char Y = X + 1;
+    clang_analyzer_eval(Y < 6); // expected-warning{{TRUE}}
+  }
+
+  // TODO
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = X + (-256); // truncation
+    clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
+  }
+
+  // TODO
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = X + 256; // truncation
+    clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}} expected-warning{{UNKNOWN}}
+  }
+
+  // TODO
+  if (X >= 100) {
+    unsigned char Y = X + 1; // truncation
+  clang_analyzer_eval(Y == 0); // expected-warning{{FALSE}}}}
+  clang_analyzer_eval(Y >= 101); // expected-warning{{TRUE}}
+    clang_analyzer_eval(Y == 0 || Y >= 101); // expected-warning{{TRUE}}
+  }
+
+  if (X >= 100) {
+    unsigned short Y = X + 1;
+    clang_analyzer_eval(Y >= 101 && Y <= 256); // expected-warning{{TRUE}}
+  }
+}
+
+void sub1(int X)
+{
+  if (X >= 10 && X <= 50) {
+    int Y = X - 2;
+    clang_analyzer_eval(Y >= 8 && Y <= 48); // expected-warning{{TRUE}}
+  }
+
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = (unsigned int)X - 20; // truncation
+    clang_analyzer_eval(Y <= 30 || Y >= 246); // expected-warning{{TRUE}}
+  }
+
+  // TODO
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = (unsigned int)X - 256; // truncation
+    clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}} expected-warning{{UNKNOWN}}
+  }
+
+  if (X < 5) {
+    int Y = X - 1; // might overflow
+    clang_analyzer_eval(Y < 4); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(Y == INT_MAX); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(Y == INT_MAX || Y < 4); // expected-warning{{TRUE}}
+  }
+
+  if (X >= 1000) {
+    int Y = X - 1;
+    clang_analyzer_eval(Y >= 999); // expected-warning{{TRUE}}
+  }
+}
+
+void subU8(unsigned char X)
+{
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = X - 2;
+    clang_analyzer_eval(Y >= 8 && Y <= 48); // expected-warning{{TRUE}}
+  }
+  
+  if (X >= 100) {
+    unsigned char Y = X - 1;
+    clang_analyzer_eval(Y >= 99 && Y <= 254); // expected-warning{{TRUE}}
+  }
+
+  if (X < 5) {
+    unsigned char Y = X - 1; // overflow
+    clang_analyzer_eval(Y < 4 || Y == 255); // expected-warning{{TRUE}}
+  }
+
+  // TODO
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = X - (-256); // truncation
+    clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}} expected-warning{{UNKNOWN}}
+  }
+
+  // TODO
+  if (X >= 10 && X <= 50) {
+    unsigned char Y = X - 256; // truncation
+    clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
+  }
+
+  if (X >= 100) {
+    unsigned short Y = X + 1;
+    clang_analyzer_eval(Y >= 101 && Y <= 256); // expected-warning{{TRUE}}
+  }
+}
+
+void div(int X)
+{
+  if (X >= 10 && X <= 50) {
+    int Y = X / 2;
+    clang_analyzer_eval(Y >= 5); // expected-warning{{TRUE}}
+    clang_analyzer_eval(Y <= 25); // expected-warning{{TRUE}}
+  }
+  
+  // No overflows
+}
+
+