Hacker News Reader

Comment by WalterBright | Hacker News Reader

Checked C:

    int a[5] = { 0, 1, 2, 3, 4};
    _Array_ptr<int> p : count(5) = a;  // p points to 5 elements.

My proposal for C:

    int a[5] = { 0, 1, 2, 3, 4};
    int p[..] = a;  // p points to 5 elements.

https://www.digitalmars.com/articles/C-biggest-mistake.html

https://github.com/Microsoft/checkedc/wiki/New-pointer-and-a...

View on HN

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 ;)

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

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://github.com/NASA-SW-VnV/ikos

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.

I don't know how a static analyzer could do this:

    size_t i = some_function(); // gets return value from environment
    array[i] = 3;

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.

Nearly all my use of arrays is arrays whose length cannot be known until runtime.

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

That sounds a bit like what WUFFS is doing

WUFFS: https://github.com/google/wuffs

> 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?

> You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations.

This is how sound static analyzers are advertised.

> This doesn't correspond to how static analyzers work in reality.

Of course it does not, since a normal static analyzer is not sound. However, a sound static analyzer is sound.

> 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.

I already did (and explained that while I have yet to use it, NIST did a positive review). Until you learn better reading comprehension, you will never see it. Here is a hint. Look 6 comments up.

> 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?

The theory was made 5 decades ago:

https://en.wikipedia.org/wiki/Abstract_interpretation

It has already been rolled out in aviation, nuclear power, etcetera. Even NASA is using an implementation of it:

https://www.nasa.gov/content/tech/rse/research/ikos

You, like myself a few months ago, had never heard of it. However, when was the last time you seriously looked for something like this? I have been making a major push to resolve all static analysis reports from Coverity, Clang and others in OpenZFS. I found it when looking into additional static analyzers. If it were not for that, I would still be entirely unaware.

That being said, you have a clear reading comprehension issue, since I already provided links showing that NASA has deployed software implementing that theory and NIST did a positive review of software implementing it. It is absurd to read that and think “this is not feasible”.

> 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

> 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/

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.

> 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.

This is not entirely true. Patrick Cousot‘s group, which invented the theory of abstract interpretation, kept working on it and produced Astree.

I had previously been under the impression that Astree was from the same people that made Compcert C, but upon double checking for this reply, I realized that was wrong. The two groups are both in France though. It was an easy mistake to make considering that Absint sells licenses for both.

> Trying to make static guaranties about imperative code is indeed a dead end by now.

The astree static analyzer is available from Absint. One of the inventors of both it and the theory on which it is based is also still alive:

https://en.wikipedia.org/wiki/Patrick_Cousot

His software is in use at the ESA and other places.

NASA is using software it wrote in house based on that theory:

https://www.nasa.gov/aero/ikos.html

Presumably, NASA heard about Astree from the ESA and decided to make its own tool, possibly due to NIH syndrome. I am not sure if NASA counts as academia.

This is far from a dead end, even if most researchers cannot be bothered to do things in that area. You will probably find a number of the ones that can be bothered to do things in that area at farma-c:

https://frama-c.com/

It's justified for aerospace, because failures are quite expensive there, but for usual business it will be much easier to implement automatic bound checking, like at 1% complexity of the C compiler.

I wonder what operating systems the aerospace industry uses, since failures in the operating system could be equally expensive, yet operating system developers generally do not have access to these tools.

Much of the time they build their own.

Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.

> Type checking is actually a special case of abstract interpretation.

I'm not sure about that.

Maybe in regard to type level functions? But else? I'm skeptical.

Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction.

> For all we know, it may even be that dependent types can already express many complex uses of it;

That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative.

Depended types can express anything computable. (Which also makes them undecidable in general).

In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.

He appears to be right in saying "Type checking is actually a special case of abstract interpretation". The paper that presented Abstract Interpretation to the world concludes:

"It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..."

https://www.di.ens.fr/~cousot/publications.www/CousotCousot-...

That said, abstract interpretation promises that the absence of reports proves the absence of the errors that the sound static analyzer implementing it is designed to catch. Provided that you do not abuse casts/unions, the absence of warnings/errors from a compiler's type checking on a strongly typed language should prove an absence of type errors, which does sound like what abstract interpretation promises.

Lastly, I need make time to actually read that paper. I have only read a very small part of it.

You could model C in a dependently-typed language by embedding the C abstract machine and C program expressions in it. Then you could use the Poincaré principle applied to C-program fragments to perform any "abstract interpretation" of them and derive any property you might care about. So it looks like the Poincaré's principle (as it was named by Barendegt) is the actual "missing link" that would enable you to generalize from purely syntax-based analysis (as in the traditional definition of type systems/type checks) to "interpretation" of a more general sort.

> Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.

See the paper that presented abstract interpretation to the world:

"It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..."

https://www.di.ens.fr/~cousot/publications.www/CousotCousot-...

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/

> 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.

> 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!

> 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.

> Are you sure?

No, I just picked it from the ENS web page (https://www.astree.ens.fr) but it may have not been updated for a while.

As I understand it there's been improvement on dynamic allocation with separation logic in general, TBC what Astrée supports (I've no first hand experience).

For recursion, it's a similar problem as for loops as I understand it: to handle it fully automatically the analyzer would have to prove recursion terminates and find and prove induction invariant. But safety critical code tend to forbid it anyway so it may not be a big limitation for most Astrée customers.

> > 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 [...]

A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu.

I would expect the lack of Z3 support to lead to a lot more false alarms in a FS, as the analysis with only the Clang SA build it range analysis will be basic and won't understand anything related to bit fields and operations for example.

The `llvm` package must depend on a `libz3-4` package, recent enough (on Bookworm it's 4.8.10, but IIRC anything >= 4.7 would be used). Another way to check could be to use the CodeChecker `--z3-refutation`: this is enabled by default if LLVM has the Z3 support, but if requested explicitly should fail if not (untried, TBC).

> A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu.

That was one of the first things I did. Recompiling with z3 support made little difference. That said, I thought --z3-refutation Was the default when it was available.

I will try rerunning tests with it explicitly specified, but I do not expect much from that, since running tests with --z3, which replaces the range checker with z3, did not really eliminate reports beyond those that were in files that caused clang’s static analyzer to crash when that was set.

Yes, if the LLVM toolchain has Z3 support then `--z3-refutation` will be the default. It's only useful if you want an error in case the LLVM toolchain may not have this support.

I've read somewhere that the "full Z3" mode with `--z3` is very experimental and not well maintained. It didn't crash when I tried it but was no better and way too slow: typically 15 times slower on average, but a few files took over 24 hours to check.

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?

https://en.cppreference.com/w/c/error/set_constraint_handler...

You simply have go treat that as always unsound.

This is essentially the status quo, and it's not helpful. Better is possible.

> 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?

> 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

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

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.

Here is a 4th one:

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/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. ;)

Back before I converted the back end of the D compiler from C++ to D, I ran a couple of static checkers over it. Thousands of errors were found. I was rather excited, here are lots of bugs I can fix at very low cost!

I only found one actual bug. While I was happy to get that fixed, the overall result was disappointing.

My conclusion that the best path forward was to design a language where a static analysis tool would add no value.

Which ones did you try?

The only static analyzers that I am allowed to say have stood out to me are:

* Clang's static analyzer

* GCC's static analyzer with -Wno-analyzer-malloc-leak -Wno-analyzer-use-of-uninitialized-value -Wno-analyzer-null-dereference because those three checks are uniquely buggy. `-Wanalyzer-null-dereference` fails to understand assertions. `-Wanalyzer-use-of-uninitialized-value` fails to recognize initialization from pass by pointer. `-Wanalyzer-malloc-leak` is so buggy that out of the 32 reports it made, only 1 was real, but it was right before an `exit()` call in a test suite, so it was not a particularly interesting report. Unfortunately, I do not have notes describing why that check is buggy.

Note that I am restricted by Coverity's Scan User Agreement from saying anything involving Coverity that could constitute a comparison. I suggest that you look at the public information about its use by myself and draw your own conclusions. Keep in mind, your conclusions are not things that I said.

I think it was PC-something, but it was several years ago.

I once told the Coverity staff that the purpose of D was to put Coverity out of business (!)

Was it PC-Lint?

That was probably a bad choice. John Carmack did not rate it very highly:

http://www.sevangelatos.com/john-carmack-on-static-code-anal...

No, not that one. Maybe PVS-xxxx

Here is a list of almost every known static analysis tool for C++:

https://analysis-tools.dev/tag/cpp

The only one I know to exist absent from that list is Microsoft’s /analyze.

That said, I am surprised that D only has 1 tool listed:

https://analysis-tools.dev/tag/dlang

Maintainer of the list here. Thanks for mentioning it. I have not heard of Microsoft's analyze. Could you paste a link here? I will add it to the list, then. Alternatively you could send a pull request to the repository. ;) https://github.com/analysis-tools-dev/static-analysis

It is a static analyzer built into Microsoft Visual Studio:

https://learn.microsoft.com/en-us/cpp/build/reference/analyz...

The only reason I know about it is that John Carmack rated it highly:

http://www.sevangelatos.com/john-carmack-on-static-code-anal...

Can the D compiler prove things about the code? I didn't know.

How does this work?

For one thing, it won't let you take the address of a local variable and return it, or store it in a global, or throw it as an exception, or any other way for it to survive the stack frame. It won't let you "sanitize" it by passing it through a wrapper function, either.

(This is all in functions annotated with `@safe`.)

Try it and see for yourself.

There's a long list of things like this D does. For another example, it won't allow reading from uninitialized variables. It will check your printf/scanf format string against the arguments. (This last one was a big win.)

> It will check your printf/scanf format string against the arguments. (This last one was a big win.)

Clang and GCC are able to do this on C/C++ code via the format function attribute:

https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attribute...

I agree about it being a big win. I have been dragging my feet on retrofitting the OpenZFS source code to use it since I have just not had much time to revise my pull request doing it after code review asked me to use `(u_longlong_t)` instead of PRId64 and friends and the initial attempt to retrofit the OpenZFS codebase using it did not find anything I considered to be a real bug. That might be because a number of real bugs in this area had already been identified and fixed thanks to static analyzers.

That said, there is this annoying oscillation that both GCC and Clang have where they complain that my type is long long and I should use %lld when I use %ld for uint64_t, only to complain that my type is long and I should use %ld when I use %lld for uint64_t. Using `PRId64` from stdint.h weirdly suppresses that behavior. Using a typecast to `(u_longlong_t)` also suppresses it.

I know about the function attributes. But those are extensions, not part of the language, and hence unreliable. The core language needs to be fixed.

Think of all the stupid problems arising in C from `long` not having a defined size. I can't believe all the time I've lost dealing with that. In D, a `long` is 64 bits. Period. Problems just vanish into the ether.

Just a brief erratum report since it is too late to edit my previous comment to correct the mistake, I meant to write PRIu64 for my example. Writing PRId64 was a typo.

> You are lucky if you get -Wall -Werror.

But why not for instance use a build system in some "container"?

In other language environments that's quite common. It's easy for developers, so there is no issue. I think the project could "bother" contributors with something like that, couldn't it?

> Coverity […] CodeQL […] SonarCloud

An embedded C developer I've talked with quite often on some other forum, who imho is quite competent, said that Coverity is a poor tool that generates way too much false negatives and overlooks at the same time glaring issues. He was not happy about it. Said that's mostly an issue with all OpenSource tools for static C analysis. OTOH the commercial ones are very expensive usually, with a target market of critical things like aviation of safety systems in cars and military use, places where they spend billions on projects. Nothing there for the average company, and especially not for (frankly often underfunded) OpenSource projects.

CodeQL? It's mostly an semantic search and replace tool, as I know? Is it that helpful? (I had a look, but the projects I'm working on don't require it. One would just use the IDE. No need for super large-scale refactorings, across projects, in our case).

SonarCloud, hmm… This one I've used (around web development though). But am not a fan of. It bundles other "scanner" tools, with varying quality and utility. At least what they had for the languages I've actively used it was mostly about "style issues". And when it showed real errors, the IDE would do the same… (The question then is how this could be committed in the first place. But OK, some people just don't care. For them you need additional checks like SonarCloud I guess.)

> Clang’s static analyzer

Heard good things about that one!

Wouldn't it be easy to add at least this to the build by using some "build container"?

> So you understand my pain.

Well, that's why I think something equivalent to `-Wall -Werror` should be switched on before writing the first line of code, in any language.

But as I just checked whether `-Werror` really does what I've expected I came across this here:

https://embeddedartistry.com/blog/2017/05/22/werror-is-not-y...

I have to admit that in the context of C/C++ development they have a point there.

One more reason for "Solution 2.: Capturing the build environment", I guess.

> I submitted a paper to Asia BSDCon 2023 explaining this.

Oh, cool! Good luck with that!

> You should look at the coverity scan results for the Linux kernel. They are far worse.

I've heard the rumors… (The C dude form above was also always talking about that).

But I didn't want to go into that as Linux code quality is a quite loaded topic sometimes.

> I am not aware of another major filesystem that does that much QA. Let me know if you find one.

OK, you have a point here.

I've never looked to close to be honest. Firstly, I have a very hard time reading C. Secondly, I don't want to get scared. And C code always scares me… (Likely because I'm mostly doing Scala, and especially the FP thing. So I get scared most of the time even by occasional `var`s)

> 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.

Sure an option to consider.

But I guess I will stay with engraving my data into solid rock. Proven for at least hundred thousand years.

At least someone needs to preserve the cat pictures and meme of our current human era for the cockroach people of the distant future. I'm not sure they will have a compatible Linux kernel and compiler available to build the ZFS drivers, or even punch card readers…

> But why not for instance use a build system in some "container"?

I am not sure how this helps.

> I think the project could "bother" contributors with something like that, couldn't it?

Which project?

> An embedded C developer I've talked with quite often on some other forum, who imho is quite competent, said that Coverity is a poor tool that generates way too much false negatives and overlooks at the same time glaring issues.

He likely violated a license agreement with Coverity, since no one is allowed to say anything comparing Coverity to anything else.

> Said that's mostly an issue with all OpenSource tools for static C analysis.

I have been filing bug reports.

> OTOH the commercial ones are very expensive usually, with a target market of critical things like aviation of safety systems in cars and military use, places where they spend billions on projects. Nothing there for the average company, and especially not for (frankly often underfunded) OpenSource projects.

So you understand my pain.

To be more specific, OpenZFS is decently funded since its developers can get employment to work on it. However, I suspect that funding for tools like Abstree and PVS Studio is not there.

Interestingly, PVS Studio claims to be free for open source projects, but then restricts the projects that may use it to hobbyist projects:

https://pvs-studio.com/en/order/open-source-license/

I really doubt funding would be there for PVS Studio given that its blog suggests that companies purchase licenses for all developers. They did that with Google at the following link, in a way that suggested (as per my reading) that Google pay for licenses for Chrome developers working at other companies:

https://pvs-studio.com/en/blog/posts/cpp/0559/

Getting 1 company to volunteer to pay for the licenses of all developers that work on an open source project is not a feasible proposition, since even if it were willing to pay for licenses, it would only be willing to pay for ones for its own developers. This conflicts with the idea that an OSS project should integrate static analyzers into continuous integration infrastructure to make defect reports available to all developers through pull requests.

1 developer handling all reports like we currently have with Coverity might seem like it would work around that, but it is a huge burden on that 1 developer. I know because I am currently that 1 developer. Their blog speaks fairly strongly against large groups getting a license for 1 developer who is responsible for all of the reports, so that seems unlikely to happen even if I were masochistic enough to volunteer to be that 1 developer:

https://pvs-studio.com/en/blog/posts/0135/

That said, I have not yet finished processing reports from the free tools, so when I do, I would be pleasantly surprised should:

1. I try free trials of paid tools (mainly astree and PVS Studio)

2. I find that they are worthwhile to continue using.

3. I ask the community about obtaining funding to obtain those tools for our continuous integration infrastructure.

4. It actually happens.

I strongly expect both Astree and PVS Studio to ask for astronomical numbers that the community is not going to fund. That is also why I keep delaying the use of their free trials, since I want to use them during a period where I am certain that I can make the most of them. I won't be able to make the most of them if I am still working on reports from other static analyzers, especially since those same reports might also be made by Astree and PVS Studio.

> CodeQL? It's mostly an semantic search and replace tool, as I know? Is it that helpful? (I had a look, but the projects I'm working on don't require it. One would just use the IDE. No need for super large-scale refactorings, across projects, in our case).

I have never heard about a semantic search and replace function in CodeQL. Perhaps you are thinking of Coccinelle?

CodeQL is a static analyzer whose checks are written in the CodeQL language. However, it is very immature. When github acquired it, they banished the less reliable checks to the extended-and-security suite, leaving it only with about ~50 checks for C/C++ code. Those catch very little, although in the rare instances that they do catch things, the things caught are somewhat amazing. Unfortunately, at least one of those checks provides technically correct, yet difficult to understand, explanations of the problem, so most developers would dismiss its reports as false positives despite it being correct:

https://github.com/github/codeql/issues/11744

There are probably more issues like that, but I have yet to see and report them.

> SonarCloud, hmm… This one I've used (around web development though). But am not a fan of. It bundles other "scanner" tools, with varying quality and utility. At least what they had for the languages I've actively used it was mostly about "style issues". And when it showed real errors, the IDE would do the same… (The question then is how this could be committed in the first place. But OK, some people just don't care. For them you need additional checks like SonarCloud I guess.)

It is supposed to be able to integrate into github's code scanning feature, so any newly detected issues are reported in the PR that generated them. Anyway, it is something that I am considering. I wanted to use it much sooner, but it required authorization to make changes to github on my behalf, which made me cautious about the manner in which I try it. It is basically at the bottom of my todo list right now.

> Wouldn't it be easy to add at least this to the build by using some "build container"?

I do not understand your question. To use it, we need a few things:

1. To be able to show any newly introduced defect reports in the PR that generated them shortly after it was filed.

2. To be able to scan the kernel modules since right now, it cannot due to a bad interaction between the build system and how compiler interposition is done. As of a few days ago, I have a bunch of hacks locally that enable kernel module scans, but this needs more work.

3. An easy way to mark false positives without doing commits.

Without those things in place, it is a dead on arrival proposition. OpenZFS already tried using CPPCheck without #1 and #3 in place and it was so painful that the project reversed course. That happened while I was on a multi-year sabbatical from the project, so I only know about it from seeing traces of it in the repository and asking others who were around for it about what happened.

> Well, that's why I think something equivalent to `-Wall -Werror` should be switched on before writing the first line of code, in any language.

OpenZFS has had that in place for more than a decade. I do not know precisely when it was first used (although I could look if anyone is particularly interested), but my guess is 2008 when ZFSOnLinux started. Perhaps it was done at Sun before then, but both events predate me. I became involved in 2012 and it is amazing to think that I am now considered one of the early OpenZFS contributors.

Interestingly, the earliest commits in the OpenZFS repository referencing static analysis are from 2009 (with the oldest commit being from 2008 when ZFSOnLinux started). Those commits are ports of changes from OpenSolaris based on defect reports made by Coverity. There would be no more commits mentioning static analysis until 2014 when I wrote patches fixing things reported by Clang's static analyzer. Coverity was (re)introduced in 2016.

As far as the current OpenZFS repository is concerned, knowledge of static analysis died with OpenSolaris and we lost an entire form of QA until we rediscovered it during attempts to improve QA years later.

That said, if you have suggestions to improve QA, I am willing to listen to them, although keep in mind that it takes time for me to do things, even if I think they are good ideas, and I already have a large number of ideas to implement since returning to the project earlier this year.

> But I guess I will stay with engraving my data into solid rock. Proven for at least hundred thousand years.

That method is no longer reliable due to acid rain. You would need to bury it in a tomb to protect it from acid rain. That has the pesky problem of the pointers being lost over time.

> At least someone needs to preserve the cat pictures and meme of our current human era for the cockroach people of the distant future. I'm not sure they will have a compatible Linux kernel and compiler available to build the ZFS drivers, or even punch card readers…

Github's code vault found a solution for that, although they used it on source code:

https://github.com/github/archive-program/blob/master/GUIDE....

I vaguely recall another effort trying to include the needed hardware in time capsules, but I could be misremembering.

> since no one is allowed to say anything comparing Coverity to anything else

A product where the company is afraid of comparative reviews implies it just isn't a competitive product.

Feel free to compare D with any other programming language.

> > But why not for instance use a build system in some "container"?

> I am not sure how this helps.

> > I think the project could "bother" contributors with something like that, couldn't it?

> Which project?

OpenZFS. But this is kind of a misunderstanding on my side. I thought you were talking about convince for local developers. But you're talking about a CI system? Did I now understand correctly?

But still a local developer needs a local build environment that is similar to the one on the CI which will do the checks later on. It's a common practice to bundle the whole tool-chain and all kind of checkers and scanners in a "build container". You can run it than locally as on the CI.

But how to do bare metal tests on GitHub I actually don't know. Kernel divers are something special I guess. Not the usual workload that can be completely put into a container. One needs at least some VM setup. Never did that on GitHub.

> > An embedded C developer I've talked with quite often on some other forum, who imho is quite competent, said that Coverity is a poor tool that generates way too much false negatives and overlooks at the same time glaring issues.

> He likely violated a license agreement with Coverity, since no one is allowed to say anything comparing Coverity to anything else.

LOL

> I have never heard about this function. It is a static analyzer whose checks are written in the CodeQL language.

Need to take a second look I guess. I had it differently in mind, but OK.

Thanks for the pointer.

> That said, if you have suggestions on QA, I am willing to listen to them, although keep in mind that it takes time for me to do things, even if I think they are good ideas, and I already have a large number of ideas to implement since returning to the project earlier this year.

I'm not sure I can say much without having actually deeper insides into issues with the current QA setup.

It sounded like it would be difficult to introduce tools for static analysis. But I'm not completely sure whether this is more a technical issue or a developer convenience and workflow thingy.

At least some of such tools can be integrated into a fully packaged build tool-chain, like I said. This way you can rule out for example that someone commits stuff that triggers false positives in some code analysis tool that you can run also against your local build. Of course you still need checks on the CI in place. But those checks should actually never trigger by something that someone should have seen and resolved already locally (and if it does trigger this needs investigation usually anyway as the local build does not mirror the CI build in every aspect any more). This would relief the need to "ignore" checks on the CI without commits, I guess. Just do the checks you can do locally locally. Deliver the tools to do so in a convenient "package" ("container", VM image / config, whatever; you know, something like Vagrant).

Showing test results in PRs or even outright reject PRs based on test results can be done in GitHub with Actions. One can also trigger Actions by special comments, useful for example for checks and benchmarks that only need to run occasionally when something related changes. But I guess you know all that… :-)

Regarding code analysis: I think the stuff that Microsoft Research does is also interesting, and wasn't mentioned yet. But I'm not sure how practically relevant this is (especially in Unix land). They have at least on paper some tools for C code analysis. But no clue how stuff works in reality. Never heard directly from anybody who used this things.

> OpenZFS. But this is kind of a misunderstanding on my side. I thought you were talking about convince for local developers. But you're talking about a CI system? Did I now understand correctly?

I was actually asked by another OpenZFS developer about a good local tool for this. I did not have an answer then and I still do not have a great answer for it now, but I am getting closer to one. Some build system patches + Clang's static analyzer + codechecker seems to be the most promising combination since that would not only be able to cross translation unit analysis, but also be able to do differential reporting so only new reports are visible, but I still need to figure out all of the details.

Also, I suspect the end result will be far less useful in practice than it sounds because of just how long the analysis takes. We would need a way to do incremental analysis like we can do incremental builds for it to be truly useful, and I currently do not have an answer for incremental analysis, although I suspect maybe something could be done in CodeChecker based on filesystem time stamps.

Supposedly PVS Studio can do that, but as I explained my previous comment (in an edit that I probably made after you initially read it), PVS Studio is unlikely to be an option beyond its free trial period.

That said, QA would be better achieved by integrating these tools into our continuous integration infrastructure so that they could be run whenever a pull request is done so that all newly reported issues are made available to all reviewers and we can avoid merging things that introduce regressions that static analyzers can catch in the first place.

> But still a local developer needs a local build environment that is similar to the one on the CI which will do the checks later on. It's a common practice to bundle the whole tool-chain and all kind of checkers and scanners in a "build container". You can run it than locally as on the CI.

It is easy to do builds on any Linux / FreeBSD machine. The test suite really should be run in a VM since running experimental code on your kernel is not advisable and is not always feasible. Machines that have root on ZFS cannot have that code loaded into the running kernel without significant inconveniences, which include breaking the system if you mess up in a way that completely breaks the driver. You can still use the ZFS stochastic testing tool called ztest. That does testing on a userland version of ZFS, although it is different from running the test suite.

> But how to do bare metal tests on GitHub I actually don't know. Kernel divers are something special I guess. Not the usual workload that can be completely put into a container. One needs at least some VM setup. Never did that on GitHub.

I think we are talking about different things here. github can integrate with buildbots and has its own runners that you can use via github workflows, but running the test suite has nothing to do with static analyzers, which I thought were the focus of the discussion.

> Need to take a second look I guess. I had it differently in mind, but OK.

I revised my response to ask if you had mistaken CodeQL for Coccinelle.

> It sounded like it would be difficult to introduce tools for static analysis.

It is infrastructure work. It is doable, but it takes time. I have been working on it. The addition of CodeQL to github pull requests was the first thing to come out of that.

> But I'm not completely sure whether this is more a technical issue or a developer convenience and workflow thingy.

If the developer is inundated with reports, it is useless. That is why we need to ensure that developers only see new reports from their code changes. We also need to be able to mark existing reports as false positives so that we do not have a bunch of unresolved reports.

> At least some of such tools can be integrated into a fully packaged build tool-chain, like I said. This way you can rule out for example that someone commits stuff that triggers false positives in some code analysis tool that you can run also against your local build.

Commits can only be done by a select few people and they are only done following code review. Asking the reviewers to download the code locally to redundantly run all of these tools on their local machines (which also implies inundating them with reports from pre-existing issues) is a fantastic way to cause developer burn out. That might sound silly, but real problems occur when you require developers to do menial tasks that require them to process huge amounts of mostly useless information.

I have been through all of that myself and the burnout problem hit me. Excessive local testing is also a productivity killer, which becomes a morale killer when you put your tested patch in a pull request and then the buildbot not only finds a problem with it, but then demonstrates that all of your local testing was a waste of time since you now need to start from the beginning in retesting everything.

It is far better to have the tools' reports added to the pull request by a machine for the reviewers to see in the PR, with pre-existing issues filtered from those reports. It avoids the "please end my suffering now" part of the development process that occurs when developers manually run all of the things they can locally every single time they make a small change, only to have the continuous integration infrastructure tell them to start over.

> Of course you still need checks on the CI in place. But those checks should actually never trigger by something that someone should have seen and resolved already locally (and if it does trigger this needs investigation usually anyway as the local build does not mirror the CI build in every aspect any more).

They do all the time. You simply cannot test all of the architectures, OS version combinations, etcetera locally that are tested by the continuous integration infrastructure.

> This would relief the need to "ignore" checks on the CI without commits, I guess.

I do not understand.

> Just do the checks you can do locally locally.

I used to do this. My productivity was several times lower, I still missed things that the continuous integration software caught and I burned myself out doing menial work by needing to manually run all of this. I really do not recommend it.

Now I do much less of this and rely on the buildbot to do the menial work.

> Deliver the tools to do so in a convenient "package" ("container", VM image / config, whatever; you know, something like Vagrant).

I have a suspicion nobody would use it since everything they need is already fairly simple to setup.

> Showing test results in PRs or even outright reject PRs based on test results can be done in GitHub with Actions.

OpenZFS already does this.

> One can also trigger Actions by special comments, useful for example for checks and benchmarks that only need to run occasionally when something related changes. But I guess you know all that…

I did not know that part, but I find it to be more useful to always run all tests all the time.

> Regarding code analysis: I think the stuff that Microsoft Research does is also interesting, and wasn't mentioned yet. But I'm not sure how practically relevant this is (especially in Unix land). They have at least on paper some tools for C code analysis. But no clue how stuff works in reality. Never heard directly from anybody who used this things.

If they published them for third party use, I would be willing to look.

> Some build system patches + Clang's static analyzer + codechecker seems to be the most promising combination since that would not only be able to cross translation unit analysis, but also be able to do differential reporting so only new reports are visible, but I still need to figure out all of the details. Also, I suspect the end result will be far less useful in practice than it sounds because of just how long the analysis takes. We would need a way to do incremental analysis like we can do incremental builds for it to be truly useful, and I currently do not have an answer for incremental analysis, although I suspect maybe something could be done in CodeChecker based on filesystem time stamps.

I use CodeChecker with ClangSA, CTU enabled and with Z3 for refutation. The code base is smaller so incremental checking is less a concern to me.

Still, we had a look. CC allows taking a list of files, and updating those files analysis only while keeping the existing results for other non listed files.

But unless something has changed this partial analysis just do what it's told, analyzing only the files given on the CLI. With CTU this may miss side effects: a modified file may impact other files using its function for example. It's possible to use CC own CTU info to derive these dependencies and extend the list of files.

Then there are modified header files, with the usual inclusion dependencies.

So if it's not provided "out of the box", it should be possible to have a layer on top taking a list of changed files, extending it with both CTU and header dependencies, and passing the extended list to CC for a safe update.

> An embedded C developer I've talked with quite often on some other forum, > who imho is quite competent, said that Coverity is a poor tool that > generates way too much false negatives and overlooks at the same time > glaring issues. He was not happy about it. Said that's mostly an issue > with all OpenSource tools for static C analysis. OTOH the commercial ones > are very expensive usually, with a target market of critical things like > aviation of safety systems in cars and military use, places where they > spend billions on projects. Nothing there for the average company, and > especially not for (frankly often underfunded) OpenSource projects.

I don't have any experience with Coverity, but used another commercial static analyzer (SA) that I won't name in case there are similar legal limitations as with Coverity ;)

With the commercial tool I have the same problem you mention: too many false alarms. Most reports are a waste of time really. In the end, people tend to ignore the tool.

The best results I get with Clang SA, used through CodeChecker. Very few false alarms, and usually at least code smells. It's not sound of course, but is free and could spot a few nasty bugs. I recommend trying CC+ClangSA.

One important point is the ability to do cross files analysis. It is very common to use a value from a function in another file. With a "one file at a time" analysis no assumption can be made on this value range, so the analyzer must be conservative. This leads to a lot of false alarms in practice.

With cross file analysis (called "cross translation units" or CTU analysis in Clang SA), the SA can propagate constraints along paths traversing multiple files. This makes a huge difference in my experience. As I explained in another comment, this is well suited for an application: all paths come from `main`. For a library the result will depend on the test application(s) provided to the SA: the call to the library under test must cover all the function domains for the analysis not to miss some issue. Otherwise, it may use too restrictive constraints from the UT that are not relevant to real life use.

But it may not be enough: the commercial tool I use do make cross file analysis. It seems more limited than Clang SA though, and misses a lot.

Another thing that help IMHO is the use of Z3 as a checker. ClangSA uses a simple and fast range based analysis. As far as SA goes, this is a bit primitive and not as powerful as polyhedral analysis for example (which is more expensive).

But when Clang SA range analysis finds an issue, it is cross checked with the Z3 SMT solver, which can deal with more complex constraints, and possible rejected there. I do embedded development, and Z3 can understand bit fields and bit operations for example (trivial for a SMT solver with bit vectors). I never tried with and without using Z3 in this way, but I assume it helps.

In any case, I'm very happy with the results I get from ClangSA+CC with CTU and Z3 enabled (check your LLVM toolchain for Z3 support, OK in Debian stable for example). It's much better in practice than the costly commercial tool we still use, for now.

For cross compilation, there may be a few Clang/GCC differences to work-around. CodeChecker already handle some, but maybe not all. It's been manageable in our case. For Linux based development CC should work fine out of the box.

I think attributes provide the flexibility to avoid dealing with ISO. Stay tuned. :-X

> 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

A quick test with `clang -std=c89 -pedantic` says it was in C99. Amazingly, it seems that almost nobody knew about it.

Not the same thing at all, that only works with compile-time known sizes.

Pascal arrays were fixed at compile time, which I quickly discovered made Pascal rather useless without extensions.

The example was for compile-time known sizes.

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.

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.

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).

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.

There's a few things in C that are not in C++ that MSVC added. Designated initializers and type-generic macros are two features that come to mind, and I believe MSVC also supports C99 restrict. The only non-optional C11 feature I can think of that MSVC doesn't support these days is _Atomic.

That is an amazing change of heart on Microsoft's part.

> MSVC supports a substantial amount of C99, C11, and C17, (...)

Supporting only some features of a spec means that they do not conform with the spec.

Msvc is still stuck with C89, and it won't budge.

Funny, Microsoft seems to disagree with you: https://devblogs.microsoft.com/cppblog/c11-and-c17-standard-...

> For many years Visual Studio has only supported C to the extent of it being required for C++. Things are about to change now that a conformant token-based preprocessor has been added to the compiler. With the advent of two new compiler switches, /std:c11 and /std:c17, we are officially supporting the latest ISO C language standards.

> All the required features of C11 and C17 are supported.

The spec has made those features optional, compliance doesn't require optional features, that is why they are optional.

SQL Server on Linux runs on Drawbridge, with NTUM and all.

No, since Visual Studio 2015 Microsoft have been making efforts to support C11 and C17.

I don't think the comment you are replying to is talking about MSFT's Checked C?

Many people have been down this road, including me.[1] Back in my 2012 paper, I listed prior art:

• Microsoft source code annotation language (SAL)

• Cyclone (AT&T research language)

• SCC, the Safe C compiler.

• Ccured

• MemSafe

The breakthrough will come when someone can create an automated system to convert unsafe C into safe something. AI may be far enough along to do that now. Every array in a valid C program has a size, defined by some expression known to the programmer. All you have to do is find that expression and tell the language about it. Most of the time this is easy. Sometimes it's hard. Sometimes it's impossible, in which case the program is probably a buffer overflow waiting to happen.

[1] http://animats.com/papers/languages/safearraysforc43.pdf

What about Fail-Safe C [1] and SoftBound [2]:

[1] https://staff.aist.go.jp/y.oiwa/FailSafeC/index-en.html

[2] https://people.cs.rutgers.edu/~sn349/softbound/

The former apparently implements full ANSI C, and the latter apparently has a memory safety proof in Coq.

The group that did [1] also did an ANSI C to Java compiler.

It seems to me that we could really use a safe ABI (x86_64_safe, etc.) for C/C++, and that it should be supported by clang and gcc.

Maybe CHERI will catch on someday...

> The breakthrough will come when someone can create an automated system to convert unsafe C into safe something

https://dl.acm.org/doi/abs/10.1145/3527322

Now that's real progress.

"We find that typ3c automatically converted 67.9% of pointers in our benchmark programs to checked types, which improves on the 48.4% inferred by unification-style algorithms used in prior work. boun3c was able to infer bounds for 77.3% of pointers that required them."

That's reasonably good. The real goal is to convert all pointers to either run-time checked pointers (slower) or compile-time checked pointers. It's already possible to convert everything to "fat pointers". GCC used to have that as an option. But the goal is to eliminate the need for that for code that's frequently executed. That is, inner loops. It's good to see activity in this area.

The output code is kind of clunky looking, but that could be fixed.

I can already see it:

> This C code is guaranteed to be safe. We had an AI go through it and make it safe.

No, thanks. That sounds more like a problem than a solution.

> an automated system to convert unsafe C into safe something

Can't we just make macros to redefine types as some 'safe' type variant system, and #include "safetypes.h" or something? It's ugly, but searching your source code for 'int a[5]' and replacing it with 'INT(a,5)' might be dumb enough to work.

Statically allocated/sized arrays are relatively easy. The problem is dynamically allocated/sized arrays coupled with pointer "interface", which supports type casting.

Something smart enough to convert pointer arithmetic to slice expressions is needed. Most C pointer arithmetic is really just slice access.

(Who invented array slices? It was a concept that came along much later than one might have expected.)

Yes, needing a fixed-sized array seems like a fairly common need to me.

    a := [5]int32{0, 1, 2, 3, 4} // Go

    let mut array: [i32; 5] = [0, 1, 2, 3, 4]; // Rust

C has fixed-size arrays.

The problem is that it doesn't use them much, and gets rid of them as soon as possible:

  int a[5] = {1, 2, 3, 4, 5, 6};

  printf("%d\n", a[8]);

in clang, this warns, by default, on both misuse sites "excess elements in array initializer" and "array index is past the end of the array". Which is good.

However things go downhill as soon as you pass the arrays downstack:

    #include <stdio.h>

    static void foo(int *a) {
        printf("%d\n", a[8]);
    }
    static void bar(int a[]){
        printf("%d\n", a[8]);
    }
    static void qux(int a[6]){
        printf("%d\n", a[8]);
    }

    int main() {
        int a[5] = {1, 2, 3, 4, 5};

        foo(a);
        bar(a);
        qux(a);
    }

no warning anywhere, even under "-Wall -Weverything".

Yeah, so the syntax is a bit funny but you can actually get the bounds checking you want here:

  #include <stdio.h>

  static void qux(int a[static 6]){
    printf("%d\n", a[8]);
  }

  int main() {
    int a[5] = {1, 2, 3, 4, 5};
    qux(a);
  }

I get,

  test.c:9:5: warning: array argument is too small; contains 5 elements, callee requires at least 6 [-Warray-bounds]

I did not enable any warning flags at all, this is just default Clang on a Mac.

If you want to catch the a[8] inside the function you need something else.

It appears that Clang will warn even without this syntax while GCC does not warn unless it has this syntax. At least, it did when I dropped the `static 6` from the example.

The explicit "6" is a problem if you aren't using fixed size arrays.

Yes, this was in direct response to someone talking about fixed-size arrays. Think of this as just “one small way in which C does not happen to be broken” rather than some kind of endorsement of C!

Note that you could

  static void qux(int n, int a[n])

but this changes the interface somewhat and there are lots of reasons why you might want to avoid VLAs in C.

The problem with that syntax is you have to repeat it every time `a` is forwarded to another function. The array data and length need to be combined into a single semantic entity.

Yes, but I don't think a deeper discussion about the flaws of array handling C is really going to illuminate anything here. The conclusions generally go in one of three ways--either you choose to use a different language, choose to deal with C (with tools like static analyzers or instrumentation), or choose to make proposals to the C committee.

Proper array types are not present in C and they're unlikely to be added at any point in the future, so if the conversation is "the array data and length need to be combined into a single semantic entity", then the conversation is no longer about C, but the starting point for choosing another language.

The int a[static 6] syntax made it into the language because it's a small enough change that it's not disruptive to existing uses of C, but it still has some benefit (I've used it, I've seen its benefits).

I really want C to have a slice/fat-pointer-array type, because C is the least common denominator for ABIs and any kind of FFI, and since it doesn't have something like that, it complicates FFI from languages that have a more sane way of handling arrays.

I'd even be happy if the standard just included a macro like:

#define ARRAY(T) struct { T *ptr, size_t len }

Along with a few functions for working with such types.

Although that would be kind of unwieldy to use in C, since you would need a typedef to actually use any specific types.

I am relatively sure we will end up adding a fat pointer next round.

So long, you can look at my experiments using a struct type here: https://github.com/uecker/noplate/

The typedef thing will go away with C2X where you do this in place.

My proposal is backwards compatible and will not disrupt existing use.

Do you have a more complete write-up somewhere? At face value, it looks like something that wouldn’t make it into the C standard, because VLAs were too much for the standard to bear. It’s also unclear how multidimensional arrays would work—presumably, you would want that to be possible, and distinct from fat-pointer-to-fat-pointer-array.

No, that's all I got, although since it is lifted directly from D, you can get a complete treatment there.

VLAs had a poor cost/benefit because they're just too awkward to use. 20 years experience with D shows that the [] syntax knocks it out of the park.

Any combination of static/fat arrays can be made for multidimensionality. For example,

    [..][3]   array of 3 fat pointers
    [3][..]   fat pointer to 3 element array
    [3][3]    array of 3 3-element arrays
    [..][..]  fat pointer to array of 3 fat pointers

etc.

I guess what I would want is to be able to have a fat pointer to a multidimensional array, like I can do in Fortran, NumPy, etc. Why is the 1D case special, here?

My other questions are how do you create one of these fat pointers, how do you get the length, etc. This sounds to me like VLAs, but with a bigger change to the language, but unable to handle multidimensional arrays. VLAs, for all their faults, at least fit into the language for users well enough that people accidentally use them all the time (not necessarily a good thing).

> a fat pointer to a multidimensional array

    T[3][4][..] a;

> length

    a.length

That does not change the interface of the function. Function type compatibility looks at the adjusted parameter types, so the parameter is always treated as a simple pointer. Therefore, all of these declarations could be used to refer to the function:

  static void qux(int n, int *a);
  static void qux(int n, int a[]);
  static void qux(int n, int a[*]);
  static void qux(int n, int a[n]);
  static void qux(int n, int a[12345]);

Weird interface problems mainly come when you have VLA types behind pointers.

> Yeah, so the syntax is a bit funny

That's a mild understatement.

Unfortunately, `int a[static 3][static 4]` does not work.

That’s because you’d write it as:

  int a[static 3][4]

You only need to put static on the outermost type, the one that decays into a pointer. Same thing applies if you need restrict:

  int a[static restrict 3][4]

which is ugly but gets the job done. Think of int a[3][4], when used as a function parameter, as “pointer to int[4]” (the 3 disappears completely), and think of int a[static 3][4] as “pointer to first of at least 3 int[4]”.

(Not trying to defend C here, just explaining how C works.)

To pass fixed-size arrays in a way that preserves the type and allows checking their bounds, you can use pointers-to-arrays:

   static void foo(int (*a)[6]) {
     printf("%d\n", (*a)[8]);  // warning: array index 8 is past the end of the array (which contains 6 elements)
   }

   int main() {
     int a[5] = {1, 2, 3, 4, 5};
     foo(&a); // warning: incompatible pointer types passing 'int (*)[5]' to parameter of type 'int (*)[6]'
   }

This is all vanilla C89, so it works even with very old compilers, so long as they're conformant.

I like your version, but how do you annotate the size from existing things like "main(int *argv, argc)" to know that the size is argc?

There was a proposal during the C23 process to make "main(int argc, char *argv[argc])" work as one would expect, as well as some similar changes elsewhere, such as with structure members. They went through several revisions but never made the cut, I think partially because they all required at least some minimal backward incompatibility.

IMO, if GCC or clang implemented and ran with those proposed changes, they'd probably be accepted for the next C revision, and become popular long before then. This is mostly a matter of time and motivation; corporate funded developer time seems to be mostly focused on half measures; e.g. type attributes, rather than fundamentally improving pointer and array semantics. But if someone put in enough time and effort, including going through the rigmarole of integration into mainline, this could happen.

"main(int argc, char *argv[argc])" should already work with C99, shouldn't it? Or was the proposal to make some of the VLA support mandatory again?

The syntax is accepted (almost as a fluke), but doesn't work the way anyone would expect because any use of argv still decays to a pointer, even with sizeof. That's in contrast to 'char *argv[argc]' declared as an automatic variable where sizeof computes at runtime the proper array size: 'sizeof (char *) * argc'.

The proposals would make function VLA syntax work the same as for automatic variables. In theory it could break existing code, but in practice nobody actually uses this in the wild because the semantics are useless and downright confusing. There's also a related proposal to enhance flexible array members in the manner of VLAs, e.g. 'struct foo { size_t n; int arr[n]; }'. IIRC, the latter syntax is accidentally supported by GCC as a side-effect of another extension, yet GCC wouldn't have minded breaking it even though there's more production code at risk than with the function argument change.

Create an adapter:

    int main(int argc, char **argv) { return myMain(argv[0 .. argc]); }

Strings can be done like this:

    char [..] s = p[0 .. strlen(p)];

Hmmm, the "[..]" is a fat pointer right? Couldn't you just say:

    int main(char [..] args)

Maybe with some way to tell the compiler the correct parameter order if needed? Perhaps:

    int main(char [..argc] argv)

I'm curious if ELF and other formats have enough info to figure that mapping out?

> the "[..]" is a fat pointer right?

yes

> if ELF and other formats have enough info to figure that mapping out?

No, as there is no semantic connection between `argc` and `argv`.

You just... annotate it? Like, I don't see what the issue is. You just write

    int main(int argc, char **argv : count(argc)) {}

If you're already creating an extension for C, then it's fine to "change" its signature in this way. Or am I misunderstanding your objection?

Sure, the compiler can't verify that argv does indeed have argc elements, but hopefully we can rely on the kernel and C runtime to populate things properly. If not, I would say it doesn't matter that the compiler can't help you here; your system is screwed beyond repair already.

At the very least, the compiler can emit bounds checking to ensure that you don't try to access past argc elements in that array, which is still valuable.

Edit: it occurs to me that you were talking about WalterBright's version, not the version in Checked C. But I think my comment still applies: if you're changing how things work, then you just keep changing how things work to cover cases like this.

You might show an example of how to use D's templates (if it's possible) to emulate the more complex example of computing the bounds from an input argument

  char *strncpy(char * restrict dest : count(n),
              const char * restrict src : count(n),
              size_t n) : bounds(dest, (_Array_ptr<char>)dest + n);

https://news.ycombinator.com/item?id=34085835

I meant something more like this (although this doesn't QUITE compile, but it's close I think):

    static ubyte* [n*2] requires_ptr_twice_as_large_as_input(n : uint)
    (
        ubyte*[n] input,
        ubyte*[n*2] output,
    ) {
        output[0..n] = input[0..n];
        output[n..2*n] = input[0..n];
        return output;
    }

    void main()
    {
        ubyte[10] input = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
        ubyte[20] output = new ubyte[20];
        requires_ptr_twice_as_large_as_input!(10)(&input, &output);
    }

This compiles:

    ref ubyte[n*2] requires_ptr_twice_as_large_as_input(uint n)
    (
        const ref ubyte[n] input,
        ref ubyte[n*2] output,
    ) {
        output[0..n] = input[0..n];
        output[n..2*n] = input[0..n];
        return output;
    }

    void main()
    {
        ubyte[10] input = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
        ubyte[20] output;
        requires_ptr_twice_as_large_as_input!(10)(input, output);

        import std.stdio;
        writeln(output);
        assert(output == input ~ input);
    }

Thank you, neat to see it could be done (I had a hunch!)

Elegant, but of course it would be. It’s like you’re a trained professional or something ;)

not my first rodeo! ABEL was the first language I designed (for Data I/O) back in the 80s.

ABEL = "Advanced Boolean Expression Language", a language for programming PLDs (Programmable Logic Devices) which was a core business for Data I/O.

There's no substitute for decades of having programmers giving you (and shouting at you) blunt feedback on your programming language proposals.

People have never been shy with criticism!

I did not know who you were at first. Would you have any thoughts on why another group made Golang when D already existed that you would be willing to share?

Because Go designers don't like OOP and didn't want low-level system programming as core features. They also were not keen on generic programming. Basically they wanted a simpler language. (Then they realized generics are useful, ironically their constraints add complexity). Also they wanted a segmented stack and coroutines + channels as language features.

Because Google saves us all.

btw C can already do this with VMTs:

    #define ARR_LEN(a) (sizeof (a) / sizeof *(a))

    int a[5] = { 0, 1, 2, 3, 4};
    int (*p)[ARR_LEN(a)] = &a;
    ARR_LEN(*p) // 5

What does VMT mean? Virtual Method Table? When was this introduced to C? It looks like it was either in C89 or earlier according to both GCC and Clang.

#define ARR_LEN(a) (sizeof (a) / sizeof (a))

int main(void) { int a[5] = {0, 1, 2, 3, 4};

        int (*p)[ARR_LEN(a)] = &a;
        (*p)[6] = 1;
        return ARR_LEN(*p); // 5

}

I had no idea this was possible in C. It is unfortunate that GCC seems to ignore this information. Clang on the other hand uses it.

You need to use UBSan, then you get the bounds checking in GCC. I added this in 2015.

https://godbolt.org/z/8ncEK3K5b

If you add warnings, it will also tell you that the ARR_LEN macro is wrong...

> What does VMT mean?

Variable modified types, they were introduces with VLAs (variable length arrays) in c99. C11 made both optional, and C2x mandates only VMTs.

About gcc ignoring it: gcc doesn't check array bounds at all, even `int x[2]; x[9] = 1;` doesn't produce a warning.

Oddly, it does catch it for the static example posted by someone else, but that is the only place where it catches it.

Fat pointers are a good idea, but I think it’d be a better idea to store the start and evd pointers instead of a pointer to the first element and a size_t.

I've never heard of a good argument for this as compared to a capacity, length, and data struct.

If you have a start and end pointer and you move either one, you don't know what the original size of the allocation was.

D doesn't store capacity in each slice. This allows a slice to fit in registers more often. Instead for GC allocated slices, the GC will store metadata before the first element of the allocation. That does make it slower to access, particularly when the slice points past the first element, but it is cached to speed up repeated accesses to the same allocation. Repeated appending can be further speeded up by using a dedicated Appender type.

Why?

I'd guess it's because that's what C++ does. Though it's unclear to me that C++-style iteration (where you increment a running pointer until you reach an EOI pointer) is much used in C.

Storing two pointers into the same array is a memory safety problem. It's hard to implement a borrow checker when there are two live mutable pointers into the same memory object.

I would expect the borrow checker to treat a slice as a logical pointer to all elements that are addressable through it, regardless of how it's implemented under the hood.

This pattern originated in C; C++ iterators were specifically designed to fit it when it was already established.

Reply on news.ycombinator.com