5 ms·

With "cross translation units" (CTU) analysis a static analyzer could derive a constraint on `some_function` return value and check this against the array size

• ryao 4y ago
  > The Clang static analyzer [1], used through CodeChecker (CC) [2], do support CTU (enabled with `--ctu`). I'm very happy with the result on the code I'm working on. I have done some preliminary testing with this on the OpenZFS codebase and I am less than happy with the result since I receive many reports of subtle variations of the same thing on top of Clang already reporting a decent number of false positives. That turned around 80 mostly false positive reports from scan-build into 300 to 400 mostly false positive reports (I forget which offhand). This is in part because I started with around 240 reports from scan-build and fixed many of the actually fixable reports, which has gotten it down to around ~80 in my local branch that has some experimental header annotations for improving Clang’s static analyzer’s analysis that I have yet to upstream. Interestingly, the additional reports from CSA CTU analysis duplicating scan-build reports far outweigh the additional reports from CSA CTU analysis reporting new things. I have not yet tried using the differential reports, but I suspect it will make this more useful for evaluating patches. Also, codechecker uses clang tidy by default, which has problematic bugprone-assignment-in-if-condition rule. While there are ways to miswrite that pattern, it is better in my opinion to write checks for those. This pattern makes code cleaner and easier to read. Coincidentally, it is used all over the ZFS codebase with the addition of extra parentheses to tell GCC’s diagnostics “yes, I really meant to use assignment in a conditional expression here”. Just that alone should suppress this, but it does not (and perhaps I should file a bug report), so I had to disable it in my runs of codechecker, since it turned a list with hundreds of reports into a list of ~3000 reports, with all of the additional reports that I managed to check being perfectly fine code. Not only Clang + CC is not sound static analysis, but I know for a fact that it does miss bugs that other tools have caught. Going a step further based on bug reports filed against OpenZFS, I say with certainty that a number of bugs that static analyzers should catch were never reported to me by any static analyzer. This has me considering the sound options for a next step as a way to get the missing reports after I am finished processing reports from the conventional static analyzers that I use. > The other limitation is that there's only a limited complexity budget the analyzer can handle, so it cannot track all constraints on all paths. Depending on how the approximation is done it can lead to missed detection or false alarms. I really should start looking into how to find statistics on unnecessarily pruned paths and look at knobs I can turn to reduce that. Also, Clang’s static analyzer has an issue where it cannot understand even simple cases of reference counting. It also fails to understand error checking of libc functions (off the top of my head, it involved errno). No amount of knob turning will fix that sadly. There are a other bugs in how it’s checkers work too, although I will refrain from enumerating them off the top of my head since I do not remember them well at the moment. > IKOS (last time I checked) does not support CTU, it's doing "a file at a time" analysis. As far as open source tools go the Clang static analyzer is the only one I know with a working support for CTU (best used through CC). I there are other ones I missed I'd be happy to learn about them and try them out. I had not known that IKOS did not do cross translation unit analysis. Thanks for telling me about that. There is always the hack of concatenating all C files via the C preprocessor and static analyzing that. I have yet to be desperate enough to use that hack with a static analyzer to bolt on CTU analysis, so it remains an untested possibility. Perhaps I will finally deploy that hack when I try IKOS.
  • yaantc 4y ago
    > This has me considering the sound options for a next step [...] I'm definitely not an expert but look into SA a bit out of curiosity. Sound analysis normally comes with significant restrictions. For example Astrée does not support dynamic memory allocation nor recursion (not too bad for embedded). There's likely more. Let's consider the case of an iteration, with a number of loops unknown at compile/analysis time. What an unsound SA will typically do is unroll the loop a fixed number of times (5 by default for CC/ClangSA from memory). Obviously this could miss bugs if less than the actual number of loops. To do better, a fully automatic sound analyzer would have to derive the relevant loop invariants and the associated induction proofs automatically, not to have to make any guess on the number of iterations. As far as I know this is still a research topic. Or alternatively, enforce a known, small enough bounds for any loop. In general, either the sound SA must be able to derive quite complex proofs for the characteristics to enforce (research topic), or it must enforce simplicity to make the problem manageable automatically. An alternative is a tool like frama-C that can kick the ball back to a human, to do the correctness proof manually using a proof assistant for automatic verification, if automation fails. And that can be a hard job. The more constrained the application, the more realistic sound analysis should be. I don't know where a filesystem like OpenZFS sits here. Best of luck in any case!
    • ryao 4y ago
      > For example Astrée does not support dynamic memory allocation nor recursion (not too bad for embedded). Are you sure? Around 2019, they seem to have overcome those limitations, since they removed mention of them from their website. Another OpenZFS developer found that on an old university page and pointed it out to me, but that webpage was made well before then. I wonder if you read the same page that he did. I plan to look into that when I am using the free trial. > To do better, a fully automatic sound analyzer would have to derive the relevant loop invariants and the associated induction proofs automatically, not to have to make any guess on the number of iterations. As far as I know this is still a research topic. Or alternatively, enforce a known, small enough bounds for any loop. I plan to look into this when I try using sound static analyzers, since if they cannot do induction proofs on loops to prove loop correctness, it would either invalidate their claims of soundness, or at the very least limit the scope of such claims, which would mean that I would not be able to semi-formally verify ZFS using them. I know that frama-c’s Eva is specifically documented as not being able to do this.