This is an archive of the discontinued LLVM Phabricator instance.

[Analyzer] Model STL Algoirthms to improve the iterator checkers
ClosedPublic

Authored by baloghadamsoftware on Nov 28 2019, 6:12 AM.

Details

Summary

STL Algorithms are usually implemented in a tricky for performance reasons which is too complicated for the analyzer. Furthermore inlining them is costly. Instead of inlining we should model their behavior according to the specifications.

This patch is the first step towards STL Algorithm modeling. It models all the find()-like functions in a simple way: the result is either found or not. In the future it can be extended to only return success if container modeling is also extended in a way the it keeps track of trivial insertions and deletions.

Diff Detail

Event Timeline

NoQ added a comment.Feb 3 2020, 8:15 AM

Other than the packaging debate, i think this check looks good!

clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
620

STL algorithm modeling, as such, doesn't need to be opt-in.

That said, as i mentioned, i strongly prefer the state split on std::find to be opt-in, because there's usually no obvious indication in the code that the search is expected to fail.

Let's move the checker to cplusplus and add an option to it ("aggressive std::find modeling" or something like that) that'll enable exploration of the failure branch. I prefer it as an option because there definitely is a chance that we'll actually want it on by default (like we did with the move-checker for locals - it's still wonky but it seems to work really well in practice), and if we do that, i'd prefer not to have to rename a checker.

clang/lib/StaticAnalyzer/Checkers/STLAlgorithmModeling.cpp
28–33

Dead code?

127

Typo: *ahead.

139–140

Is this because you only have atomic conjured symbols in your map? Because otherwise the assertion will fail every time we reach a maximum symbol complexity during evalBinOp.

I'd rather make the code defensive and handle the UnknownVal case. That said, you can be sure it's not UndefinedVal.

Szelethus added inline comments.Feb 5 2020, 5:59 AM
clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
654

This checker should be Hidden.

clang/lib/StaticAnalyzer/Checkers/STLAlgorithmModeling.cpp
38–39

Prefer using. D67706#inline-614013

68

= default;

127

Hold on, isn't it the other way around?

[_|_|x|_|_|_|_|y|_|_|_|z|_]

Suppose in the range [x, z) I'm looking for y. The range-end argument would be z, isn't y behind it? The following code and the test cases seem to be correct, so I guess its the comment?

130–131

What if the range-end iterator is a reverse iterator? Wouldn't it mess with the relative position of the found element?

[_|_|x|_|_|_|_|y|_|_|_|z|_]

std::find(z, x, y);

Suppose I'm searching in the (x, z] range for y, where x, z are reverse iterators. Here, you'll create a forward iterator for y, if I'm not mistaken, and you'd say that its behind x? Are these things correctly modeled in IteratorChecker?

Also, I really like this patch, its well documented, small and very well tested!

Updated: checker moved to alpha.cplusplus (until at least one of the iterator-related checkers gets out of alpha state or a new non-alpha container checker is created). Error-branch is protected by an option. New constraint added for the non-error branch: the found value is not behind the parameter denoting the beginning of the lookup range.

baloghadamsoftware marked 3 inline comments as done.Feb 5 2020, 7:17 AM
baloghadamsoftware added inline comments.
clang/lib/StaticAnalyzer/Checkers/STLAlgorithmModeling.cpp
139–140

In the map we either have atomic conjured symbols or an atomic conjured symbol plus/minus a concrete integer. It should not reach a maximum symbol complexity. The assertion is a copy from IteratorModeling.

NoQ accepted this revision.Feb 5 2020, 7:22 AM

Thanks! Tests for the other value of the option are welcome (:

This revision is now accepted and ready to land.Feb 5 2020, 7:22 AM
This revision was automatically updated to reflect the committed changes.

I dont think any of my comments were addressed -- could you follow up?

baloghadamsoftware marked 5 inline comments as done.Feb 5 2020, 10:37 AM

I dont think any of my comments were addressed -- could you follow up?

I addressed two, added fixme for another one. Now I explained why I did not address the rest.

clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
654

When this checker gets enabled by default, it should be hidden. However, now nothing depends on it, it is not enabled by default thus making it hidden now is the same as making it nonexistent.

clang/lib/StaticAnalyzer/Checkers/STLAlgorithmModeling.cpp
127

z is ahead of y. y is behind z.

130–131

FIXME added.