Page MenuHomePhabricator

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

Authored by pgousseau on Sep 16 2015, 4:37 AM.

Details

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

Diff Detail

Repository
rL LLVM

Event Timeline

pgousseau updated this revision to Diff 34882.Sep 16 2015, 4:37 AM
pgousseau retitled this revision from to [Static Analyzer] Intersecting ranges and 64 bit to 32 bit truncations causing "System is over constrained." assertions..
pgousseau updated this object.
pgousseau added a subscriber: cfe-commits.
pgousseau updated this object.Sep 16 2015, 8:42 AM
pgousseau updated this revision to Diff 34900.Sep 16 2015, 9:49 AM

Added some comments.

xazax.hun edited edge metadata.Sep 18 2015, 10:47 AM

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?

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 updated this revision to Diff 35604.Sep 24 2015, 4:07 AM
pgousseau edited edge metadata.

Following Gabor's review:

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

Let me know if this looks reasonable ?

Regards,

Pierre

pgousseau retitled this revision from [Static Analyzer] Intersecting ranges and 64 bit to 32 bit truncations causing "System is over constrained." assertions. to [Static Analyzer] Assertion "System is over constrained" after truncating 64 bits integers to 32 bits. (PR25078).Oct 6 2015, 10:18 AM
zaks.anna edited edge metadata.Oct 7 2015, 3:26 PM

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

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 updated this revision to Diff 43120.Dec 17 2015, 4:13 AM
pgousseau updated this object.
pgousseau edited edge metadata.

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

NoQ added a subscriber: NoQ.Dec 17 2015, 5:46 AM

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 ↗(On Diff #43120)

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."

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 ↗(On Diff #43120)

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 accepted this revision.Jan 11 2016, 10:08 AM
zaks.anna edited edge metadata.

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

Thanks!
Anna.

This revision is now accepted and ready to land.Jan 11 2016, 10:08 AM
This revision was automatically updated to reflect the committed changes.