[Static Analyzer] Assertion "System is over constrained" after truncating 64 bits integers to 32 bits. (PR25078)

[pgousseau]

Summary

Dear All,

I would like to propose a patch to fix an assertion.

Given the following test case:
----------------------------->

void f1(long foo)
{
  unsigned index = -1;
  if (index < foo) index = foo;
  if (index + 1 == 0) // -> "system over constrained" assertion
    clang_analyzer_warnIfReached(); // -> never reached but should be
  else
    clang_analyzer_warnIfReached();
}

<-----------------------------

Using a debug build:
----------------------------->

$ clang -cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,debug.ExprInspection test.cpp
clang: ../tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:86: clang::ento::ConstraintManager::ProgramStatePair clang::ento::ConstraintManager::assumeDual(clang::ento::ProgramStateRef,

clang::ento::DefinedSVal): Assertion `assume(State, Cond, false) && "System is over constrained."' failed.
<-----------------------------

When evaluating the condition "index + 1 == 0", the analyzer checks if the range of 'index' can intersect the value UINT_MAX.
Unfortunately ranges do not get updated on assignments, the range of index is the 64 bit signed range of 'foo' which is [UINT_MAX + 1; LONG_MAX] which does not intersect [UINT_MAX; UINT_MAX] or [0; UINT_MAX - 1], hence causing the assertion.

Can you let me know if this seems a reasonable change and eventually commit it for me?

Regards,

Pierre Gousseau
SN Systems - Sony Computer Entertainment

[pgousseau]

Added some comments.

[xazax.hun]

Hi!

Thank you for the patch!

What happens if you factor the "index + 1" expression out into a separate variable?
E.g.: unsigned temp = index + 1; and use temp in the condition?

My impression is that, the ranges does not model the overflow behavior correctly (which is well defined for unsigned values). I wondering why do you think that, the right way to solve this is to modify assumeSymNE and assumeSymEQ? Wouldn't it be better to actually handle the ranges properly on assignments and other operations (such as +), so assumeSymNE and assumeSymEQ can remain unmodified?

[pgousseau]

In D12901#248842, @xazax.hun wrote:

Hi!

Thank you for the patch!

Thanks for reviewing !

What happens if you factor the "index + 1" expression out into a separate variable?
E.g.: unsigned temp = index + 1; and use temp in the condition?

In this case the symbol 'temp' is still considered by the analyzer as a 'Sym + Int' symbol so the same code path is followed.
I will add the test case thanks !

My impression is that, the ranges does not model the overflow behavior correctly (which is well defined for unsigned values). I wondering why do you think that, the right way to solve this is to modify assumeSymNE and assumeSymEQ? Wouldn't it be better to actually handle the ranges properly on assignments and other operations (such as +), so assumeSymNE and assumeSymEQ can remain unmodified?

Yes handling ranges properly would be better! I am trying to fix the assertion without having to do too much re-engineering, I agree that changing assumeSymNE/assumeSymEQ's interfaces is not ideal but it has I hope the advantage of making the purpose of the change clearer and easier to revert should modelling of truncations/promotions be added ? Any ideas on how I could avoid changing the interface?

Regards,

Pierre

[pgousseau]

Following Gabor's review:

Add a test factoring 'index + 1' in an extra variable.

Let me know if this looks reasonable ?

Regards,

Pierre

[pgousseau]

Ping !

[zaks.anna]

I agree with Gabor. We should investigate how we can model the overflow on a cast correctly.

[pgousseau]

In D12901#262270, @zaks.anna wrote:

I agree with Gabor. We should investigate how we can model the overflow on a cast correctly.

Yes I agree with Gabor too. I meant this change as a temporary workaround only, I will investigate the modelling route and let you know.

Thanks!

[pgousseau]

Following Gabor and Anna's advice:

• Instead of modifying assumeSymNE and assumeSymEQ, this patch adds a new method 'SValBuilder::evalIntegralCast'.

The current workaround for truncations not being modelled is that the evaluation of integer to integer casts are simply bypassed and so the original symbol is used as the new casted symbol (cf SimpleSValBuilder::evalCastFromNonLoc).
This lead to the issue described above, as the RangeConstraintManager associates ranges with symbols.

The new evalIntegralCast method added by this patch wont bypass the cast if it finds the range of the symbol to be greater than the maximum value of the target type.

This patch also fixes a bug in 'RangeSet::pin' causing single value ranges to not be considered conventionally ordered.

The patch has been tested with openssl-1.0.0d-src and bullet-2.82-r2704 with no regressions observed.

Please let me know if this an acceptable change?

Regards,

Pierre Gousseau
SN Systems - Sony Computer Entertainment

[zaks.anna]

This patch also fixes a bug in 'RangeSet::pin' causing single value ranges to not be considered conventionally ordered.

Can that fix be submitted as a separate patch? Is there a test for it?

lib/StaticAnalyzer/Core/ExprEngineC.cpp

351

SValBuilder::evalCast and SimpleSValBuilder::evalCastFromNonLoc perform a lot of special casing. I am not sure we are not loosing anything if we bypass them. For example, there is special handling of Booleans. We might want to add this smarter handling of the integral conversions inside SimpleSValBuilder::evalCastFromNonLoc, where you see the comment starting with "If the types are the same or both are integers, ignore the cast."

[pgousseau]

In D12901#320680, @zaks.anna wrote:

This patch also fixes a bug in 'RangeSet::pin' causing single value ranges to not be considered conventionally ordered.

Can that fix be submitted as a separate patch? Is there a test for it?

Yes I will look at creating a separate review for it.
Tests at lines 81, 111, 131 fail without the fix to RangeSet::pin.

lib/StaticAnalyzer/Core/ExprEngineC.cpp

351

Yes I initially looked at making the change in 'evalCastFromNonLoc' but the problem is that the change requires access to the ProgramState, so to avoid changing the interface of evalCast (used in around 50 places) I made the change here.
Looking at evalCast it does not seem to add any special handling to casts of type 'CK_IntegralCast' before calling 'evalCastFromNonLoc'?
Booleans casts should be associated with another type of cast than 'CK_IntegralCast' and the new 'evalIntegralCast' will call 'evalCast' if it does not detect a truncation so it should be ok, what do you think?

[zaks.anna]

Sounds good. Please, split this into 2 patches (each fixing the separate problem) and commit.

Thanks!
Anna.

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

bool haveSameType(QualType Ty1, QualType Ty2) {
     // FIXME: Remove the second disjunct when we support symbolic
     // truncation/extension.
     return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
             (Ty1->isIntegralOrEnumerationType() &&
              Ty2->isIntegralOrEnumerationType()));
   }
 
   SVal evalCast(SVal val, QualType castTy, QualType originalType);
-  
+  // Handles casts of type CK_IntegralCast.
+  SVal evalIntegralCast(ProgramStateRef state, SVal val, QualType castTy,
+                        QualType originalType);
+
   virtual SVal evalMinus(NonLoc val) = 0;
 
   virtual SVal evalComplement(NonLoc val) = 0;
 
   /// Create a new value which represents a binary expression with two non-
   /// location operands.
   virtual SVal evalBinOpNN(ProgramStateRef state, BinaryOperator::Opcode op,
                            NonLoc lhs, NonLoc rhs, QualType resultTy) = 0;

lib/StaticAnalyzer/Core/ExprEngineC.cpp

switch (CastE->getCastKind()) {
       }
       case CK_MemberPointerToBoolean:
         // FIXME: For now, member pointers are represented by void *.
         // FALLTHROUGH
       case CK_Dependent:
       case CK_ArrayToPointerDecay:
       case CK_BitCast:
       case CK_AddressSpaceConversion:
-      case CK_IntegralCast:
       case CK_NullToPointer:
       case CK_IntegralToPointer:
       case CK_PointerToIntegral:
       case CK_PointerToBoolean:
       case CK_IntegralToBoolean:
       case CK_IntegralToFloating:
       case CK_FloatingToIntegral:
       case CK_FloatingToBoolean:
switch (CastE->getCastKind()) {
       case CK_LValueBitCast: {
         // Delegate to SValBuilder to process.
         SVal V = state->getSVal(Ex, LCtx);
         V = svalBuilder.evalCast(V, T, ExTy);
         state = state->BindExpr(CastE, LCtx, V);
         Bldr.generateNode(CastE, Pred, state);
         continue;
       }
+      case CK_IntegralCast: {
+        // Delegate to SValBuilder to process.
+        SVal V = state->getSVal(Ex, LCtx);
+        V = svalBuilder.evalIntegralCast(state, V, T, ExTy);
+        state = state->BindExpr(CastE, LCtx, V);
+        Bldr.generateNode(CastE, Pred, state);
+        continue;
+      }
       case CK_DerivedToBase:
       case CK_UncheckedDerivedToBase: {
         // For DerivedToBase cast, delegate to the store manager.
         SVal val = state->getSVal(Ex, LCtx);
         val = getStoreManager().evalDerivedToBase(val, CastE);
         state = state->BindExpr(CastE, LCtx, val);
         Bldr.generateNode(CastE, Pred, state);
         continue;

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
     APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
 
     switch (LowerTest) {
     case APSIntType::RTR_Below:
       switch (UpperTest) {
       case APSIntType::RTR_Below:
         // The entire range is outside the symbol's set of possible values.
         // If this is a conventionally-ordered range, the state is infeasible.
-        if (Lower < Upper)
+        if (Lower <= Upper)
           return false;
 
         // However, if the range wraps around, it spans all possible values.
         Lower = Type.getMinValue();
         Upper = Type.getMaxValue();
         break;
       case APSIntType::RTR_Within:
         // The range starts below what's possible but ends within it. Pin.
case APSIntType::RTR_Above:
       case APSIntType::RTR_Within:
         // The range starts above what's possible but ends within it (wrap).
         Lower = Type.getMinValue();
         Type.apply(Upper);
         break;
       case APSIntType::RTR_Above:
         // The entire range is outside the symbol's set of possible values.
         // If this is a conventionally-ordered range, the state is infeasible.
-        if (Lower < Upper)
+        if (Lower <= Upper)
           return false;
 
         // However, if the range wraps around, it spans all possible values.
         Lower = Type.getMinValue();
         Upper = Type.getMaxValue();
         break;
       }
       break;

lib/StaticAnalyzer/Core/SValBuilder.cpp

if (ToTy->isVoidType())
     return true;
 
   if (ToTy != FromTy)
     return false;
 
   return true;
 }
 
+// Handles casts of type CK_IntegralCast.
+// At the moment, this function will redirect to evalCast, except when the range
+// of the original value is known to be greater than the max of the target type.
+SVal SValBuilder::evalIntegralCast(ProgramStateRef state, SVal val,
+                                   QualType castTy, QualType originalTy) {
+
+  // No truncations if target type is big enough.
+  if (getContext().getTypeSize(castTy) >= getContext().getTypeSize(originalTy))
+    return evalCast(val, castTy, originalTy);
+
+  const SymExpr *se = val.getAsSymbolicExpression();
+  if (!se) // Let evalCast handle non symbolic expressions.
+    return evalCast(val, castTy, originalTy);
+
+  // Find the maximum value of the target type.
+  APSIntType ToType(getContext().getTypeSize(castTy),
+                    castTy->isUnsignedIntegerType());
+  llvm::APSInt ToTypeMax = ToType.getMaxValue();
+  NonLoc ToTypeMaxVal =
+      makeIntVal(ToTypeMax.isUnsigned() ? ToTypeMax.getZExtValue()
+                                        : ToTypeMax.getSExtValue(),
+                 castTy)
+          .castAs<NonLoc>();
+  // Check the range of the symbol being casted against the maximum value of the
+  // target type.
+  NonLoc FromVal = val.castAs<NonLoc>();
+  QualType CmpTy = getConditionType();
+  NonLoc CompVal =
+      evalBinOpNN(state, BO_LT, FromVal, ToTypeMaxVal, CmpTy).castAs<NonLoc>();
+  ProgramStateRef IsNotTruncated, IsTruncated;
+  std::tie(IsNotTruncated, IsTruncated) = state->assume(CompVal);
+  if (!IsNotTruncated && IsTruncated) {
+    // Symbol is truncated so we evaluate it as a cast.
+    NonLoc CastVal = makeNonLoc(se, originalTy, castTy);
+    return CastVal;
+  }
+  return evalCast(val, castTy, originalTy);
+}
+
 // FIXME: should rewrite according to the cast kind.
 SVal SValBuilder::evalCast(SVal val, QualType castTy, QualType originalTy) {
   castTy = Context.getCanonicalType(castTy);
   originalTy = Context.getCanonicalType(originalTy);
   if (val.isUnknownOrUndef() || castTy == originalTy)
     return val;
 
   if (castTy->isBooleanType()) {

test/Analysis/range_casts.c

+// This test checks that intersecting ranges does not cause 'system is over constrained' assertions in the case of eg: 32 bits unsigned integers getting their range from 64 bits signed integers.
+// RUN: %clang_cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,debug.ExprInspection -analyzer-store=region -verify %s
+
+void clang_analyzer_warnIfReached();
+
+void f1(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index + 1 == 0) // because of foo range, index is in range [0; UINT_MAX]
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f2(unsigned long foo)
+{
+  int index = -1;
+  if (index < foo) index = foo; // index equals ULONG_MAX
+  if (index + 1 == 0)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // no-warning
+}
+
+void f3(unsigned long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index + 1 == 0)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f4(long foo)
+{
+  int index = -1;
+  if (index < foo) index = foo;
+  if (index + 1 == 0)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f5(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index == -1)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f6(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index == -1)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f7(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index - 1 == 0) // Was not reached prior fix.
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f8(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index + 1L == 0L)
+    clang_analyzer_warnIfReached(); // no-warning
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f9(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index - 1L == 0L) // Was not reached prior fix.
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f10(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index + 1 == 0L)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f11(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index + 1UL == 0L)
+    clang_analyzer_warnIfReached(); // no-warning
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f12(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  if (index - 1UL == 0L) // Was not reached prior fix.
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f13(int foo)
+{
+  unsigned short index = -1;
+  if (index < foo) index = foo;
+  if (index + 1 == 0)
+    clang_analyzer_warnIfReached(); // no-warning
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f14(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  long bar = foo;
+  if (index + 1 == 0)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f15(long foo)
+{
+  unsigned index = -1;
+  if (index < foo) index = foo;
+  unsigned int tmp = index + 1;
+  if (tmp == 0)
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  else
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}