10 ms·

It's a shame this will never get through the insane bureaucracy that is the C standards committee. Had they listened to you all the way back in 2009, C11 might

It's a shame this will never get through the insane bureaucracy that is the C standards committee. Had they listened to you all the way back in 2009, C11 might have been a game changer the same way C++11 was. Alas. At least there's BetterC ;)

WalterBright 4y ago
This proposal could very well save C, as array bounds overflows are consistently the #1 cause of corruption bugs in shipped C software.
- ryao 4y ago
  In theory, sound static analyzers could be another method by which this is achieved in existing projects. They claim to be able to catch all instances of this. Some examples of sound static analyzers include: https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos https://github.com/static-analysis-engineering/CodeHawk-C https://github.com/static-analysis-engineering/CodeHawk-C I have planned to try using them on OpenZFS for a while, but I am still busy reviewing and fixing reports made by conventional static analyzers. I plan to look into these next. That said, at least one of them claims to be able to prove the absence of issues in C that checked C’s documentation explicitly says it cannot prevent. The obvious one is use-after-free.
  - WalterBright 4y ago
    I don't know how a static analyzer could do this: size_t i = some_function(); // gets return value from environment array[i] = 3;
    - deleted 4y ago
      [deleted]
    - ryao 4y ago
      A sound static analyzer in theory can check the safety of that by examining all code paths and complain whenever any exist where it is possible to go out of bounds. It is called sound because the absence of a complaint means it has proven the absence of the issues it is meant to catch. If it has a limitation that prevents it from finding a proof, it will complain about the lines that could not be proven safe.
      - WalterBright 4y ago
        Nearly all my use of arrays is arrays whose length cannot be known until runtime.
        ryao 4y ago
        Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. At least, that is the theory. I have yet to use one. I plan to try the ones I mentioned next year. That said, NIST gave astree a good review in 2020: https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf
        simplotek 4y ago
        > Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations. This doesn't correspond to how static analyzers work in reality. Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
        still_grokking 4y ago
        > Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. Here's a list: https://en.wikipedia.org/wiki/Symbolic_execution#Tools https://en.wikipedia.org/wiki/Symbolic_execution#Tools Also related: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? Depends on how you define "feasible". Abstract interpretation and symbolic execution are crazy complex¹. Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. Trying to make static guaranties about imperative code is indeed a dead end by now. The problem is that proving any properties of imperative code needs much more effort (and therefore code) than what is expressed by the code that needs proves, so it's actually likely that you haven than bugs in the code that proves things. So this approach is not really "feasible" in the end. --- ¹ Just have a look at the documentation around the KeY tool used to prove things about Java programs. https://www.key-project.org/thebook2/ https://www.key-project.org/thebook2/ That's the most complex stuff I've ever seen! Depended type systems are "trivially simple" in contrast, no joke. But this is just about a "simple language" like Java… The complexity of C is much much higher.
    - ZiiS 4y ago
      You simply have go treat that as always unsound.
      - 95014_refugee 4y ago
        This is essentially the status quo, and it's not helpful. Better is possible.
        ryao 4y ago
        > This is essentially the status quo, and it's not helpful. Better is possible. It is helpful, since if you address all of the complaints, then your code will be proven to be free of the issues that the sound static analyzer can detect. In theory, you can produce C code that is proven to be memory safe by doing that, which effectively makes it semi-formally verified code. Unlike other methods of doing semi-formal verification, this method is actually usable by an average programmer. Would you explain to me how that is the status quo? How would you do better?
    - abcd_f 4y ago
      I am with you wrt fat pointers for arrays, but what difference would it make here? Will it result in a bounds check and a run-time failure point?
      - GoblinSlayer 4y ago
        https://en.cppreference.com/w/c/error/set_constraint_handler_s https://en.cppreference.com/w/c/error/set_constraint_handler...
    - yaantc 4y ago
      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 to detect a possible bug. 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. Of course this is not magic, and it's important to understand the limitations. The CTU analysis is well suited for an application: there is a `main` function, and all the paths from there can (in theory) be analyzed through the code base files. But if the code to analyze is a library, then the CTU analysis will be done from one or more unit test applications and the paths constraints analysis will only be as good as the unit tests. To avoid this one can analyze without CTU, but then the above code will always trigger a report as the static analyzer has no information on `some_function` return value and must assume the worst. 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. 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. Clang SA + CC is a really nice combo. It's not sound (the limited complexity budget above), so can miss issues. Still, with CTU and the use of Z3 to cross check alarms (very nice when using bitfield) it is a nice user experience with very few false alarms, which matters to make the tool more acceptable (people tend to ignore tools with too many false alarms after a while IME). Still some rough edges for people doing embedded cross compiled development but manageable. [1] https://clang-analyzer.llvm.org/ [2] https://codechecker.readthedocs.io/en/latest/
      - 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.
  - still_grokking 4y ago
    > https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm This looks interesting. It's based on abstract interpretation which is more or less the most powerful approach for imperative code available. (Because the way it works it's likely slow as hell though, I guess). But it's closed source. One of this kind of products where you need to asks for the price… I think we all know what this means: It'll be laughably expensive. I don't see any offer for OpenSource projects frankly. > https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos Also abstract interpretation based. Looks less polished than the first one at first glance. It's under some questionable license. According to OSI it's OpenSource. According to the FSF it's not. (The FSF argument sounds strong. They're right in my opinion. This NASA license does not look like OpenSource). But an OpenSource project could use it for free I assume. > https://github.com/static-analysis-engineering/CodeHawk-C https://github.com/static-analysis-engineering/CodeHawk-C Much more constrained in scope than the other ones. But looks a little bit "too academic" imho: Uses its own C parser and such. At least it's OpenSource under MIT license. Thanks for the links either way! Good to know about some tools in case one would need them at some point. > I have planned to try using them on OpenZFS for a while, but I am still busy reviewing and fixing reports made by conventional static analyzers. Stupid question about usual C development practices (as I don't have much contact with that): Aren't analyzers today part of the build pipeline form the get go? Especially as C is known to be full of booby traps. Imho it shouldn't be even possible to push anything that has issues discovered by tools. This should be the lowest barrier as most code analyzers are at most able to spot quite obvious problems (the commercial one above is likely an exception to this "rule"). When even the usual "stupid analyzer" sees issues than the code is very likely in a very bad shape. Adding such tools later on in the development is like activating warnings post factum: You'll get drowned in issues. Especially in such critical domains as file-systems I would actually expect that the developers are using "the best tools money can buy" (or at least the best OpenSource tools available). "Still fixing bugs found by some code analyzer" doesn't sound like someone should have much trust with their data in something like ZFS, to be honest… The statement sounds actually quite scary to me.
    - ryao 4y ago
      Here is a 4th one: https://frama-c.com/ https://frama-c.com/ It is more of a bunch of different things for working out source code correctness glued together and the EVA code that is a static analyzer has limitations, but it can be used to write proofs of the correctness of C code, so it is basically a tool to investigate after I have investigated the others. Be warned that it is the first project that I have ever seen that has so much documentation that it needs documentation on how to browse the documentation. > Aren't analyzers today part of the build pipeline form the get go? Especially as C is known to be full of booby traps. No, since developers generally cannot be bothered to do that. You are lucky if you get -Wall -Werror. OpenZFS uses that, but many other projects cannot be bothered to do even that much. I have been working on improving this in OpenZFS. Unfortunately, Coverity’s scan service is incompatible with PRs due to it not supporting branches and having weekly scan limits, but CodeQL was integrated a few months ago and I have plans to integrate Clang’s static analyzer. I am also looking into SonarCloud. > Adding such tools later on in the development is like activating warnings post factum: You'll get drowned in issues. So you understand my pain. > Especially in such critical domains as file-systems I would actually expect that the developers are using "the best tools money can buy" (or at least the best OpenSource tools available). I submitted a paper to Asia BSDCon 2023 titled “Lessons from Static Analysis of OpenZFS” that explains the extent to which these tools are used in OpenZFS, which might interest you. Assuming it is accepted, I will be giving a talk there. I would post the paper for others to read, but I still have 2 months before the final paper is due and I want to make some additional improvements to it before then. Also, they would still need to accept the paper; I will be informed of their decision next month. > "Still fixing bugs found by some code analyzer" doesn't sound like someone should have much trust with their data in something like ZFS, to be honest… The statement sounds actually quite scary to me. You should look at the coverity scan results for the Linux kernel. They are far worse. https://scan.coverity.com/projects/linux https://scan.coverity.com/projects/linux https://scan.coverity.com/projects/openzfs-zfs https://scan.coverity.com/projects/openzfs-zfs At present, the ZFS Linux kernel module is at 0.14 unresolved defects per thousand lines. That is better than it’s in tree competitors: * btrfs: 0.90 * ext*: 0.87 * jfs: 1.78 * reiserfs: 1.12 * xfs: 0.79 At the time of writing, the overall Linux kernel is at 0.48 while the entire OpenZFS tree is at 0.09, but sure, be worried about ZFS. Ignore Linux, which has a number of obvious unfixed bugs being reported by Coverity (and this does not even consider other static analyzers). I would send patches for some of them if mainline Linux did not have an annoying habit of ignoring many of the patches that I send. They have ignored enough that I have stopped sending patches since it is often a waste of time. Anyway, static analysis has the benefit of checking little used execution paths, but it also has the downside of checking never used execution paths. It is often hard to reliably tell which are little used and which are never used. Also, not every defect report is a bug in the code and not every bug in the code is a potential data loss bug. Many are relatively benign things that do not negatively impact the safety of data. For example, if our test suite is not using cryptographically secure random numbers (and it is not), certain static analyzers will complain, but that is not a real bug. I might even write patches changing to /dev/urandom just for the sake of making the various static analyzers shut up so I do not have to write explanations of why it is wrong for every defect single report. That does not mean that the code had real bugs in it. Most of the static analysis fixes being done lately are fixing things not known to affect end users (no one reported issues that resemble what the static analyzers are finding lately) and the fixes are just being done either for good measure or because I and others think changing the code in a way that gets the static analyzer to shut up makes the code easier to read. It is wrong to glance at a summary of static analyzer reports, or even a list of fixes done based on those reports, and think the code itself is bad at data integrity. It is not so simple. That said, most of the remaining defect reports that I had yet to handle in the various static analyzers that I use are not even real issues. I just have not yet gotten around to writing an explanation of why something is a false positive or rewriting code in which a non-issue was reported where I felt some minor revision would make the code better while silencing the static analyzer. There might be a few remaining real bugs, which is why I am going through every single report. Look at how developers of other software projects handle static analyzer scan reports and you will be horrified. The only others I know that are this rigorous with static analysis reports are grub and libreoffice. The rest are far less rigorous (and GCC’s 1.59 defects per thousand lines reported by coverity that the GCC developers try to hide is just plain frightening). In addition, ZFS has plenty of other QA techniques that it employs, such as a test suite, stochastic testing and code review. All three are done on every pull request. I am not aware of another major filesystem that does that much QA. Let me know if you find one. Also, you do have a point. My suggestion is that you go back to punched cards, and keep them in triplicate at different geographically distinct facilities under climate control. Ideally, those facilities will have armed security and be on different continents in places that are known to have low seismic activity. That should keep your data safer than it is on a single ZFS pool. ;)
  - sassy_quat 4y ago
    [flagged]
    - dang 4y ago
      Yikes, you can't attack others like this here. Since you've done this before (https://news.ycombinator.com/item?id=31980833 https://news.ycombinator.com/item?id=31980833), I've banned the account. If you don't want to be banned, you're welcome to email hn@ycombinator.com and give us reason to believe that you'll follow the rules in the future. They're here: https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html.
- ndesaulniers 4y ago
  I think attributes provide the flexibility to avoid dealing with ISO. Stay tuned. :-X
jeffybefffy519 4y ago
It doesnt need to get through any committees to have impact. Microsoft just has to use it (which i assume they are given they are the authors) and then its had impact.
- adastra22 4y ago
  I don't think the comment you are replying to is talking about MSFT's Checked C?
- ryao 4y ago
  Do they still refuse to update their compiler to support any version of C beyond C89? Unless they have changed course, it seems more likely that Microsoft will drop NT for a UNIX kernel than Microsoft would put this into their compiler. I assume that this is by Microsoft Research and work by Microsoft Research is almost never used by Microsoft. The only exception I know is Drawbridge, which they reportedly used in Azure.
  - my123 4y ago
    SQL Server on Linux runs on Drawbridge, with NTUM and all.
  - jcranmer 4y ago
    MSVC supports a substantial amount of C99, C11, and C17, but they don't support the features that were made optional in C11 (i.e., variable-length arrays).
    - ryao 4y ago
      By a substantial amount, do you mean the parts that overlap with C++? I recall reading something about Microsoft only caring about C++ support, such that anything in C that is not in C++ is unlikely to ever be implemented in their compiler, despite other compilers having no issue doing this.
      - jcranmer 4y ago
ryao 4y ago
> It's a shame this will never get through the insane bureaucracy that is the C standards committee. Had they listened to you all the way back in 2009, C11 might have been a game changer the same way C++11 was. Alas. This comment did not age well: https://news.ycombinator.com/item?id=34086304 https://news.ycombinator.com/item?id=34086304 A quick test with `clang -std=c89 -pedantic` says it was in C99. Amazingly, it seems that almost nobody knew about it.
- sirwhinesalot 4y ago
  Not the same thing at all, that only works with compile-time known sizes.
  - WalterBright 4y ago
    Pascal arrays were fixed at compile time, which I quickly discovered made Pascal rather useless without extensions.
  - ryao 4y ago
    The example was for compile-time known sizes.

WalterBright 4y ago

This proposal could very well save C, as array bounds overflows are consistently the #1 cause of corruption bugs in shipped C software.

ryao 4y ago
In theory, sound static analyzers could be another method by which this is achieved in existing projects. They claim to be able to catch all instances of this. Some examples of sound static analyzers include: https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos https://github.com/static-analysis-engineering/CodeHawk-C https://github.com/static-analysis-engineering/CodeHawk-C I have planned to try using them on OpenZFS for a while, but I am still busy reviewing and fixing reports made by conventional static analyzers. I plan to look into these next. That said, at least one of them claims to be able to prove the absence of issues in C that checked C’s documentation explicitly says it cannot prevent. The obvious one is use-after-free.
- WalterBright 4y ago
  I don't know how a static analyzer could do this: size_t i = some_function(); // gets return value from environment array[i] = 3;
  - deleted 4y ago
    [deleted]
  - ryao 4y ago
    A sound static analyzer in theory can check the safety of that by examining all code paths and complain whenever any exist where it is possible to go out of bounds. It is called sound because the absence of a complaint means it has proven the absence of the issues it is meant to catch. If it has a limitation that prevents it from finding a proof, it will complain about the lines that could not be proven safe.
    - WalterBright 4y ago
      Nearly all my use of arrays is arrays whose length cannot be known until runtime.
      - ryao 4y ago
        Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. At least, that is the theory. I have yet to use one. I plan to try the ones I mentioned next year. That said, NIST gave astree a good review in 2020: https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf
        simplotek 4y ago
        > Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations. This doesn't correspond to how static analyzers work in reality. Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
        still_grokking 4y ago
        > Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. Here's a list: https://en.wikipedia.org/wiki/Symbolic_execution#Tools https://en.wikipedia.org/wiki/Symbolic_execution#Tools Also related: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? Depends on how you define "feasible". Abstract interpretation and symbolic execution are crazy complex¹. Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. Trying to make static guaranties about imperative code is indeed a dead end by now. The problem is that proving any properties of imperative code needs much more effort (and therefore code) than what is expressed by the code that needs proves, so it's actually likely that you haven than bugs in the code that proves things. So this approach is not really "feasible" in the end. --- ¹ Just have a look at the documentation around the KeY tool used to prove things about Java programs. https://www.key-project.org/thebook2/ https://www.key-project.org/thebook2/ That's the most complex stuff I've ever seen! Depended type systems are "trivially simple" in contrast, no joke. But this is just about a "simple language" like Java… The complexity of C is much much higher.
  - ZiiS 4y ago
    You simply have go treat that as always unsound.
    - 95014_refugee 4y ago
      This is essentially the status quo, and it's not helpful. Better is possible.
      - ryao 4y ago
        > This is essentially the status quo, and it's not helpful. Better is possible. It is helpful, since if you address all of the complaints, then your code will be proven to be free of the issues that the sound static analyzer can detect. In theory, you can produce C code that is proven to be memory safe by doing that, which effectively makes it semi-formally verified code. Unlike other methods of doing semi-formal verification, this method is actually usable by an average programmer. Would you explain to me how that is the status quo? How would you do better?
  - abcd_f 4y ago
    I am with you wrt fat pointers for arrays, but what difference would it make here? Will it result in a bounds check and a run-time failure point?
    - GoblinSlayer 4y ago
      https://en.cppreference.com/w/c/error/set_constraint_handler_s https://en.cppreference.com/w/c/error/set_constraint_handler...
  - yaantc 4y ago
    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 to detect a possible bug. 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. Of course this is not magic, and it's important to understand the limitations. The CTU analysis is well suited for an application: there is a `main` function, and all the paths from there can (in theory) be analyzed through the code base files. But if the code to analyze is a library, then the CTU analysis will be done from one or more unit test applications and the paths constraints analysis will only be as good as the unit tests. To avoid this one can analyze without CTU, but then the above code will always trigger a report as the static analyzer has no information on `some_function` return value and must assume the worst. 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. 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. Clang SA + CC is a really nice combo. It's not sound (the limited complexity budget above), so can miss issues. Still, with CTU and the use of Z3 to cross check alarms (very nice when using bitfield) it is a nice user experience with very few false alarms, which matters to make the tool more acceptable (people tend to ignore tools with too many false alarms after a while IME). Still some rough edges for people doing embedded cross compiled development but manageable. [1] https://clang-analyzer.llvm.org/ [2] https://codechecker.readthedocs.io/en/latest/
    - 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.
- still_grokking 4y ago
  > https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm This looks interesting. It's based on abstract interpretation which is more or less the most powerful approach for imperative code available. (Because the way it works it's likely slow as hell though, I guess). But it's closed source. One of this kind of products where you need to asks for the price… I think we all know what this means: It'll be laughably expensive. I don't see any offer for OpenSource projects frankly. > https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos Also abstract interpretation based. Looks less polished than the first one at first glance. It's under some questionable license. According to OSI it's OpenSource. According to the FSF it's not. (The FSF argument sounds strong. They're right in my opinion. This NASA license does not look like OpenSource). But an OpenSource project could use it for free I assume. > https://github.com/static-analysis-engineering/CodeHawk-C https://github.com/static-analysis-engineering/CodeHawk-C Much more constrained in scope than the other ones. But looks a little bit "too academic" imho: Uses its own C parser and such. At least it's OpenSource under MIT license. Thanks for the links either way! Good to know about some tools in case one would need them at some point. > I have planned to try using them on OpenZFS for a while, but I am still busy reviewing and fixing reports made by conventional static analyzers. Stupid question about usual C development practices (as I don't have much contact with that): Aren't analyzers today part of the build pipeline form the get go? Especially as C is known to be full of booby traps. Imho it shouldn't be even possible to push anything that has issues discovered by tools. This should be the lowest barrier as most code analyzers are at most able to spot quite obvious problems (the commercial one above is likely an exception to this "rule"). When even the usual "stupid analyzer" sees issues than the code is very likely in a very bad shape. Adding such tools later on in the development is like activating warnings post factum: You'll get drowned in issues. Especially in such critical domains as file-systems I would actually expect that the developers are using "the best tools money can buy" (or at least the best OpenSource tools available). "Still fixing bugs found by some code analyzer" doesn't sound like someone should have much trust with their data in something like ZFS, to be honest… The statement sounds actually quite scary to me.
  - ryao 4y ago
    Here is a 4th one: https://frama-c.com/ https://frama-c.com/ It is more of a bunch of different things for working out source code correctness glued together and the EVA code that is a static analyzer has limitations, but it can be used to write proofs of the correctness of C code, so it is basically a tool to investigate after I have investigated the others. Be warned that it is the first project that I have ever seen that has so much documentation that it needs documentation on how to browse the documentation. > Aren't analyzers today part of the build pipeline form the get go? Especially as C is known to be full of booby traps. No, since developers generally cannot be bothered to do that. You are lucky if you get -Wall -Werror. OpenZFS uses that, but many other projects cannot be bothered to do even that much. I have been working on improving this in OpenZFS. Unfortunately, Coverity’s scan service is incompatible with PRs due to it not supporting branches and having weekly scan limits, but CodeQL was integrated a few months ago and I have plans to integrate Clang’s static analyzer. I am also looking into SonarCloud. > Adding such tools later on in the development is like activating warnings post factum: You'll get drowned in issues. So you understand my pain. > Especially in such critical domains as file-systems I would actually expect that the developers are using "the best tools money can buy" (or at least the best OpenSource tools available). I submitted a paper to Asia BSDCon 2023 titled “Lessons from Static Analysis of OpenZFS” that explains the extent to which these tools are used in OpenZFS, which might interest you. Assuming it is accepted, I will be giving a talk there. I would post the paper for others to read, but I still have 2 months before the final paper is due and I want to make some additional improvements to it before then. Also, they would still need to accept the paper; I will be informed of their decision next month. > "Still fixing bugs found by some code analyzer" doesn't sound like someone should have much trust with their data in something like ZFS, to be honest… The statement sounds actually quite scary to me. You should look at the coverity scan results for the Linux kernel. They are far worse. https://scan.coverity.com/projects/linux https://scan.coverity.com/projects/linux https://scan.coverity.com/projects/openzfs-zfs https://scan.coverity.com/projects/openzfs-zfs At present, the ZFS Linux kernel module is at 0.14 unresolved defects per thousand lines. That is better than it’s in tree competitors: * btrfs: 0.90 * ext*: 0.87 * jfs: 1.78 * reiserfs: 1.12 * xfs: 0.79 At the time of writing, the overall Linux kernel is at 0.48 while the entire OpenZFS tree is at 0.09, but sure, be worried about ZFS. Ignore Linux, which has a number of obvious unfixed bugs being reported by Coverity (and this does not even consider other static analyzers). I would send patches for some of them if mainline Linux did not have an annoying habit of ignoring many of the patches that I send. They have ignored enough that I have stopped sending patches since it is often a waste of time. Anyway, static analysis has the benefit of checking little used execution paths, but it also has the downside of checking never used execution paths. It is often hard to reliably tell which are little used and which are never used. Also, not every defect report is a bug in the code and not every bug in the code is a potential data loss bug. Many are relatively benign things that do not negatively impact the safety of data. For example, if our test suite is not using cryptographically secure random numbers (and it is not), certain static analyzers will complain, but that is not a real bug. I might even write patches changing to /dev/urandom just for the sake of making the various static analyzers shut up so I do not have to write explanations of why it is wrong for every defect single report. That does not mean that the code had real bugs in it. Most of the static analysis fixes being done lately are fixing things not known to affect end users (no one reported issues that resemble what the static analyzers are finding lately) and the fixes are just being done either for good measure or because I and others think changing the code in a way that gets the static analyzer to shut up makes the code easier to read. It is wrong to glance at a summary of static analyzer reports, or even a list of fixes done based on those reports, and think the code itself is bad at data integrity. It is not so simple. That said, most of the remaining defect reports that I had yet to handle in the various static analyzers that I use are not even real issues. I just have not yet gotten around to writing an explanation of why something is a false positive or rewriting code in which a non-issue was reported where I felt some minor revision would make the code better while silencing the static analyzer. There might be a few remaining real bugs, which is why I am going through every single report. Look at how developers of other software projects handle static analyzer scan reports and you will be horrified. The only others I know that are this rigorous with static analysis reports are grub and libreoffice. The rest are far less rigorous (and GCC’s 1.59 defects per thousand lines reported by coverity that the GCC developers try to hide is just plain frightening). In addition, ZFS has plenty of other QA techniques that it employs, such as a test suite, stochastic testing and code review. All three are done on every pull request. I am not aware of another major filesystem that does that much QA. Let me know if you find one. Also, you do have a point. My suggestion is that you go back to punched cards, and keep them in triplicate at different geographically distinct facilities under climate control. Ideally, those facilities will have armed security and be on different continents in places that are known to have low seismic activity. That should keep your data safer than it is on a single ZFS pool. ;)
- sassy_quat 4y ago
  [flagged]
  - dang 4y ago
    Yikes, you can't attack others like this here. Since you've done this before (https://news.ycombinator.com/item?id=31980833 https://news.ycombinator.com/item?id=31980833), I've banned the account. If you don't want to be banned, you're welcome to email hn@ycombinator.com and give us reason to believe that you'll follow the rules in the future. They're here: https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html.
ndesaulniers 4y ago
I think attributes provide the flexibility to avoid dealing with ISO. Stay tuned. :-X

jeffybefffy519 4y ago

It doesnt need to get through any committees to have impact. Microsoft just has to use it (which i assume they are given they are the authors) and then its had impact.

adastra22 4y ago
I don't think the comment you are replying to is talking about MSFT's Checked C?
ryao 4y ago
Do they still refuse to update their compiler to support any version of C beyond C89? Unless they have changed course, it seems more likely that Microsoft will drop NT for a UNIX kernel than Microsoft would put this into their compiler. I assume that this is by Microsoft Research and work by Microsoft Research is almost never used by Microsoft. The only exception I know is Drawbridge, which they reportedly used in Azure.
- my123 4y ago
  SQL Server on Linux runs on Drawbridge, with NTUM and all.
- jcranmer 4y ago
  MSVC supports a substantial amount of C99, C11, and C17, but they don't support the features that were made optional in C11 (i.e., variable-length arrays).
  - ryao 4y ago
    By a substantial amount, do you mean the parts that overlap with C++? I recall reading something about Microsoft only caring about C++ support, such that anything in C that is not in C++ is unlikely to ever be implemented in their compiler, despite other compilers having no issue doing this.
    - jcranmer 4y ago

ryao 4y ago

> It's a shame this will never get through the insane bureaucracy that is the C standards committee. Had they listened to you all the way back in 2009, C11 might have been a game changer the same way C++11 was. Alas. This comment did not age well: https://news.ycombinator.com/item?id=34086304 https://news.ycombinator.com/item?id=34086304 A quick test with `clang -std=c89 -pedantic` says it was in C99. Amazingly, it seems that almost nobody knew about it.

sirwhinesalot 4y ago
Not the same thing at all, that only works with compile-time known sizes.
- WalterBright 4y ago
  Pascal arrays were fixed at compile time, which I quickly discovered made Pascal rather useless without extensions.
- ryao 4y ago
  The example was for compile-time known sizes.