This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Simplify values in binary operations more aggressively
ClosedPublic

Authored by NoQ on Apr 10 2017, 8:08 AM.

Details

Summary

SValBuilder tries to constant-fold symbols in the left-hand side of the symbolic expression whenever it fails to evaluate the expression directly. However, it only constant-folds them when they are atomic expressions, not when they are complicated expressions themselves. This patch adds recursive constant-folding to the left-hand side expression (there's a lack of symmetry because we're trying to have symbols on the left and constants on the right). As an example, we'd now be able to handle operations similar to "$x + 1 < $y", when $x is constrained to a constant.

The constant-folding procedure, which i put into SValBuilder::simplifySVal(), is reusable, and i suspect that there are numerous places around SValBuilder, ConstraintManager, and our checkers, where it could be useful, but this patch tries to be relatively careful.

I'm still to see how it affects performance.

Diff Detail

Repository
rL LLVM

Event Timeline

NoQ created this revision.Apr 10 2017, 8:08 AM
xazax.hun edited edge metadata.Apr 10 2017, 11:30 AM

This is a very welcome addition. I hope the performance will be still good :)

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
1023 ↗(On Diff #94670)

We do not expect to see IntSymExpr? Maybe it is worth to document why.

1024 ↗(On Diff #94670)

Maybe worth to have this as a member instead of query it every time?

1027 ↗(On Diff #94670)

Why are these ops special?

1033 ↗(On Diff #94670)

Maybe this can be hoisted?

danielmarjamaki added inline comments.
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
49 ↗(On Diff #94670)

thier => their

NoQ updated this revision to Diff 94955.Apr 12 2017, 5:23 AM
NoQ marked 5 inline comments as done.

Thanks for the comments! Updated.

Performance didn't degrade in my test runs.

xazax.hun accepted this revision.Apr 12 2017, 6:45 AM

LGTM! Thank you for working on this!

This revision is now accepted and ready to land.Apr 12 2017, 6:45 AM

One last question: maybe we want to skip this kind of simplification in case of Z3?
Probably the constraint managers could have a flag like "wantsSimplifiedConstraints"?
Maybe somehow the checkers that are doing their own simplification could respect this flag as well somehow?

NoQ added a comment.Apr 12 2017, 9:04 AM

maybe we want to skip this kind of simplification in case of Z3?

Hmm, that depends on how would we want to use it eventually.

  • If Z3 acts all alone and fires only over actual bug reports, then yeah, it turns this simplification procedure into a dry-run no-op. However, the much bigger performance problem would be the increased path explosion from not removing infeasible paths early on.
  • If we try to filter out infeasible paths continuously, either by employing RangeConstraintManager as a filter, or by employing Z3 as a filter, then Z3 would anyway benefit from simpler symbolic expressions. In the worst case ("that's what Z3 would have done itself anyway), we'd, i guess, have little effect on quality *or* performance

Generally, i've a feeling that simplifying SVals is a safe thing to do.

This revision was automatically updated to reflect the committed changes.
dkrupp added a subscriber: dkrupp.May 3 2017, 9:01 AM