This patch adds a new Static Analyzer checker for the correct use of spin locks in the Magenta kernel. The checker checks that a lock is not locked twice in a row, nor unlocked twice in a row.
The checker was authored by Farid Molazem Tabrizi.
Differential D26340
[analyzer] Add SpinLockChecker for the Magenta kernel khazem on Nov 6 2016, 6:32 PM. Authored by
Details
This patch adds a new Static Analyzer checker for the correct use of spin locks in the Magenta kernel. The checker checks that a lock is not locked twice in a row, nor unlocked twice in a row. The checker was authored by Farid Molazem Tabrizi.
Diff Detail Event TimelineComment Actions Thanks for upstreaming this! (And it was great to meet you at the developer conference.)
Comment Actions Good to meet you too, thanks for the useful comments and pointers to helpful examples! I'm going to update the diff twice: the first one to address your first two comments, and the second one to address your last two. Comment Actions The strings for Spin{Unl,L}ockFuncName and LockErrorCategory are now initialized when constructing a SpinLockChecker object rather than being static globals, in order to avoid adverse effects on startup time. Also, the Spin*FuncName variables are now of type CallDescription. This is to enable pointer rather than string comparisons of the function name. Comment Actions If a double-lock or double-release is detected, path notes are now emitted on the _first_ lock or release event. Also updated the tests to check for these notes. Comment Actions Devin, based on Artem's review of the other checker that I have posted [1] I am wondering about merging both this SpinLockChecker and the MutexChecker into PthreadLockChecker. Do you think it is still worth landing this SpinLockChecker, or do you suppose that abandoning this patch and working on merging all the checkers would be a good idea? I've noted how the checkers might be merged in my reply to Artem: [2]. [1] https://reviews.llvm.org/D26342 Comment Actions Thanks for adding the path notes and adopting CallDescription. I've added some additional comments inline, which are mostly minor nits. Two additional important changes -- and I should have noted these in the initial review -- is that it would be good to remove a MemRegion mapping from the program state when a MemRegion escapes and also when it becomes dead. These should both be small changes. Escaping void foo(lock_t *l) { spin_lock(l); ... do_stuff_and_unlock(l); .. spin_lock(); } If do_stuff_and_unlock() is in another translation unit the analyzer won't see the unlock and so will report a false positive if you don't remove the mapping when the lock escapes. If you remove the mapping when the lock escapes, the analyzer will optimistically assume the best-case scenario the next time it sees a lock or unlock operation. There is an example of how to do this in ObjCContainersChecker::checkPointerEscape() Removing Dead Symbols
Comment Actions Merging seems reasonable to me. It is also a good way to make it less likely that the Magenta checkers accidentally regress since the main logic of the checker will be exercised when checking a much more common API. |
Nit: I think it would good to add a little bit more context to disambiguate so that future maintainers will be able to do a web search to learn about what these checkers are for. For example, maybe something like "Checkers for the Magenta kernel"?