This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Add checker to model builtin functions
ClosedPublic

Authored by xazax.hun on May 11 2017, 2:56 AM.

Details

Summary

Model __builtin_assume. The motivation behind using __builtin_assume from the analyzers point of view is to add assumptions. The conventional way to express invariants is to use asserts (with correct annotations for noreturn functions). However on some platform the users do not want to pay the price of an assert, even in the debug build (especially in a hot code). This way we can express these invariants to the analyzer without runtime overhead. Also it is good to use these constraints even if they are only there to aid the optimizer.

What do you think?

Diff Detail

Repository
rL LLVM

Event Timeline

xazax.hun created this revision.May 11 2017, 2:56 AM
NoQ edited edge metadata.May 11 2017, 3:04 AM

Hmm, shouldn't this be part of BuiltinFunctionChecker aka core.builtin.BuiltinFunctions? We already have __builtin_assume_aligned here (though it doesn't seem to assume anything because that particular assumption is hard to model).

lib/StaticAnalyzer/Checkers/ModelBuiltinChecker.cpp
49 ↗(On Diff #98602)

We could also pretend we modeled the call, so that to avoid invalidation.

xazax.hun updated this revision to Diff 98609.May 11 2017, 4:16 AM
xazax.hun marked an inline comment as done.
xazax.hun edited the summary of this revision. (Show Details)
  • Move this to the right checker.
In D33092#752039, @NoQ wrote:

Hmm, shouldn't this be part of BuiltinFunctionChecker aka core.builtin.BuiltinFunctions? We already have __builtin_assume_aligned here (though it doesn't seem to assume anything because that particular assumption is hard to model).

You are completely right! I do not know how could I miss that. :)

NoQ accepted this revision.May 11 2017, 10:42 PM

Great, thanks!

lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
51 ↗(On Diff #98609)

That's a good question, because assume(false) seems much more broken than assert(false).

But because we are overaggressive on branching as compared to only relying on presumption of code liveness (eg. splitting void foo(x, y) { if (x) ...; if (y) ...; } into 4 paths is unsafe - all code may be live without all paths being feasible - but we do that anyway, same with loops and eager assumptions and our aliasing approach and the whole inlining thing), i think we'd rather not warn.

I mean, due to the above, it is much more likely that the assumption is valid and the branch on which it fails is infeasible due to some function contract we dont' see, than that the assumption is actually violated. We may do well about null dereferences and such, but generally the static analyzer should try to avoid parts of code that have been carefully thought out :) We may probably want to catch cases when the assumption fails on all paths reaching it, but we shouldn't use symbolic execution for all-paths warnings.

This revision is now accepted and ready to land.May 11 2017, 10:42 PM
This revision was automatically updated to reflect the committed changes.