This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Correctly add assumptions based on array bounds.
ClosedPublic

Authored by xazax.hun on Aug 3 2016, 3:19 AM.

Details

Diff Detail

Repository
rL LLVM

Event Timeline

xazax.hun updated this revision to Diff 66635.Aug 3 2016, 3:19 AM
xazax.hun retitled this revision from to [analyzer] Correctly add assumptions based on array bounds..
xazax.hun updated this object.
xazax.hun added reviewers: zaks.anna, dcoughlin, NoQ.
xazax.hun added a subscriber: cfe-commits.
NoQ edited edge metadata.Aug 3 2016, 7:20 AM

Nice catch!

Now, this needs a test. How about this one:

// enable the debug.ExprInspection checker?
void clang_analyzer_eval(int);

void test_asume_after_access(unsigned long x) {
  char buf[100];
  buf[x] = 1;
  clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
}

By the way, if we replace char with int, this test fails even with your patch. The reason is, the assumption is added on (4 * x) rather than on x, and the constraint manager explodes. Does anybody volunteer to fix this (eg. on the checker side - throw easier equations at the solver)?

xazax.hun updated this revision to Diff 67135.Aug 8 2016, 2:23 AM
xazax.hun edited edge metadata.
  • Address review comments.

I am not sure that the checker is the appropriate way to fix the remaining issue with this checker. I think generating simpler constraints without loosing any generality is non trivial.

NoQ accepted this revision.Aug 8 2016, 11:35 AM
NoQ edited edge metadata.
NoQ added inline comments.
test/Analysis/out-of-bounds.c
153 ↗(On Diff #67135)

Yay, there already was a test for this.

/asume/assume/ here and below?

This revision is now accepted and ready to land.Aug 8 2016, 11:35 AM
NoQ added a comment.Aug 10 2016, 3:12 AM

Whoops, forgot to answer:

I am not sure that the checker is the appropriate way to fix the remaining issue with this checker.

Yeah, there are anyway more problems that require this functionality in the RangeConstraintManager (the code throws complicated equations into it anyway, and there are false positives reported), so i think we should try to fix it there anyway, some day.

xazax.hun updated this revision to Diff 68023.Aug 15 2016, 5:31 AM
xazax.hun edited edge metadata.
  • Simplifiy generated constraints.

I added a (proof of concept?) implementation to simplify the constraints in the checker. I wonder what do you think.

NoQ added a comment.Aug 18 2016, 5:32 AM

On second thought, in RangeConstraintManager we need a different functionality. In particular, from 4 * x < 1000 it does not follow that x < 250 in the general case (due to possible overflows). But in the case of this checker, it doesn't matter - we are always sure that any valid array address is never overflowing even when converted to bytes.

That said, it is still boilerplate. Some day i wish to consider adding the non-overflowing versions of common operations into the SValBuilder's evalBinOp(), so that it could help checkers simplify various symbolic expressions. In my opinion, evalBinOp() should be as user-friendly as possible.

But that's another story, your approach looks good to me!

This revision was automatically updated to reflect the committed changes.