Checked C
github.com
github.com
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.htmlhttps://github.com/Microsoft/checkedc/wiki/New-pointer-and-a...
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.
At least there's BetterC ;)
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.
size_t i = some_function(); // gets return value from environment
array[i] = 3;If it has a limitation that prevents it from finding a proof, it will complain about the lines that could not be proven safe.
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:
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?
Here's a list:
https://en.wikipedia.org/wiki/Symbolic_execution#Tools
Also related:
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/
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.
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.
"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.
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-...
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:
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”.
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?
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/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.
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!
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.
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.
> 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).
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.
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.
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.
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. ;)
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.
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 once told the Coverity staff that the purpose of D was to put Coverity out of business (!)
That was probably a bad choice. John Carmack did not rate it very highly:
http://www.sevangelatos.com/john-carmack-on-static-code-anal...
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://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...
How does this work?
(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.)
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.
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.
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…
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.
> 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.
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.
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.
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.
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.
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.
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.
> 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.
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.
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.
int main(int argc, char **argv) { return myMain(argv[0 .. argc]); }
Strings can be done like this: char [..] s = p[0 .. strlen(p)]; 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?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`.
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.
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.
char *strncpy(char * restrict dest : count(n),
const char * restrict src : count(n),
size_t n) : bounds(dest, (_Array_ptr<char>)dest + n); 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);
} 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);
} a := [5]int32{0, 1, 2, 3, 4} // Go
let mut array: [i32; 5] = [0, 1, 2, 3, 4]; // RustThe 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". #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.
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.)
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.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).
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.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).
T[3][4][..] a;
> length a.lengthI'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.
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.
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.That's a mild understatement.
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.ABEL = "Advanced Boolean Expression Language", a language for programming PLDs (Programmable Logic Devices) which was a core business for Data I/O.
• 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
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.
(Who invented array slices? It was a concept that came along much later than one might have expected.)
[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...
> 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.
"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.
#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#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.
Variable modified types, they were introduces with VLAs (variable length arrays) in c99. C11 made both optional, and C2x mandates only VMTs.
"Checked C" - https://news.ycombinator.com/item?id=26190403 - 133 comments - 2021
"Refactoring the FreeBSD Kernel with Checked C" - https://news.ycombinator.com/item?id=25989115 - 41 comments - 2021
"Achieving Safety Incrementally with Checked C" - https://news.ycombinator.com/item?id=19424106 - 21 comments - 2019
"Checked C: Making C Safer by Extension" - https://news.ycombinator.com/item?id=17939537 - 55 comments - 2018
"Checked C: extension to C that adds static and dynamic checking" - https://news.ycombinator.com/item?id=16588483 - 92 comments - 2018
"Checked C" - https://news.ycombinator.com/item?id=11899925 - 156 comments - 2016
C to Checked C by 3C - https://news.ycombinator.com/item?id=30857289 - March 2022 (1 comment)
A Formal Model of Checked C - https://news.ycombinator.com/item?id=30321535 - Feb 2022 (37 comments)
Why Checked C when there was Verona? - https://news.ycombinator.com/item?id=26499846 - March 2021 (2 comments)
Checked C - https://news.ycombinator.com/item?id=26190403 - Feb 2021 (133 comments)
Refactoring the FreeBSD Kernel with Checked C [pdf] - https://news.ycombinator.com/item?id=25989115 - Feb 2021 (41 comments)
Refactoring the FreeBSD Kernel with Checked C [pdf] - https://news.ycombinator.com/item?id=24019185 - Aug 2020 (13 comments)
Achieving Safety Incrementally with Checked C - https://news.ycombinator.com/item?id=19424106 - March 2019 (21 comments)
Checked C: Making C Safer by Extension - https://news.ycombinator.com/item?id=17939537 - Sept 2018 (55 comments)
Checked C: extension to C that adds static and dynamic checking - https://news.ycombinator.com/item?id=16588483 - March 2018 (92 comments)
Checked C - https://news.ycombinator.com/item?id=12049548 - July 2016 (3 comments)
Checked C – A Safer C/C++ from Microsoft - https://news.ycombinator.com/item?id=11936418 - June 2016 (3 comments)
Checked C - https://news.ycombinator.com/item?id=11899925 - June 2016 (156 comments)
As a useful counterexample, glib has GArray, GPtrArray, and GList, along with functions that you use to manipulate the lists. Those functions are presumably implemented correctly, and will prevent you from making out-of-bounds accesses.
But of course those things are not widely adopted, because they're not standardized, they're not in libc, and libc has not been reimagined such that all of its APIs take and return these safer list primitives instead of bare C arrays.
(And sure, GArray etc. are not necessarily suitable everywhere, as they require heap allocations. But I could imagine a safe abstraction that could allow for using stack or static allocations to back it.)
So I see something like Checked C as a band-aid, when the language and stdlib just needs a complete overhaul. Obviously that's incredibly unlikely to ever happen, so something like Checked C is a decent compromise, I guess.
> But of course those things are not widely adopted, because they're not standardized, they're not in libc, and libc has not been reimagined such that all of its APIs take and return these safer list primitives instead of bare C arrays.
I'm really not sure why the second thing is regarded by C programmers as such an insuperable barrier to the first thing.
I absolutely understand that there are circumstances where extreme portability is a major requirement. That, and C's ability to operate in highly constrained environments are among its most laudable features.
But many of us (including me) write user-facing C applications that have neither requirement and where Glib is either already installed or easy to install. Why not just go ahead and use it? If you're trying to get it to run on a tiny embedded system or in some land without Glib . . . well, this isn't the program for you!
I feel like this is more of a weird cultural prejudice than a technical matter. People run programs in JavaScript (or Haskell, or Python) with hundreds of dependencies, and while some find that annoying, I don't hear people in these communities objecting to idea of dependencies the way people do with C.
Could the standard library be better? Of course. But there's something to be said for not including a lot of batteries in the standard and just using the third-party tools that are available.
Also, which part of GPtrArray prevents you from making out of bounds access? Last time I checked it doesn't.
Well, that's also C's fault for not having parametric polymorphism.
Truly bizarre that we ended up with C, still feature incomplete compared to what was available at the time.
ESPOL/NEWP from 1961, almost a decade before C came to be, even had unsafe code blocks!
And if people look deeper, there are some surprising elements of Pascal in newer languages, more than many realize. At some point, sanity and common sense will sneak through.
I guess the hard part will be the fact that all your dependent libraries will (likely) still be unsafe.
https://learn.microsoft.com/en-us/cpp/code-quality/code-anal...
VC++ analysis builds up on SAL infrastructure.
https://learn.microsoft.com/en-us/cpp/code-quality/understan...
"Closing the Gap between Rust and C++ Using Principles of Static Analysis - CppCon 2020"
https://www.youtube.com/watch?v=_pQGRr4P16w
There is also a clang work on lifetimes, but little progress has happened since 2019.
"Lifetime analysis for everyone - CppCon 2019"
But there are better modern alternatives.
https://docs.scala-lang.org/scala3/book/scala-for-python-dev...
Types in Scala are not only "first-class". You can even program with them like in TS.
https://blog.rockthejvm.com/type-level-programming-scala-3/
(Type level functions are correctness proves, BTW.)
Enjoy!
You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler.
https://www.absint.com/astree/index.htm
Astree claims to be able to prove the absence of use-after-free, which the checked C documentation says that checked C does not prevent.
You would need to check to see if Astree can prove the absence of all of the issues that checked C is intended to prevent, but at a glance that seems possible. In theory, Astree can be used to fix all of them by doing fixes until it stops complaining.
I was wrong to write this. They were written by different groups in France, but licenses for both of them are being sold by the same company, which made it easy to mistake the creators as the same group. I realized my misunderstanding several hours after making that comment and could not edit to correct the error.
Also why can we not get better syntax for C? Function pointer syntax is so bad that people actively avoid using them. #pragma once is a hack. Every string library function is actively dangerous in addition to puts/gets.
I know that nobody wants to be the one to mess with the core language and ruin it but this is awfully low-hanging fruit that hasn’t been fixed in 50 years.
It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C.
Rust is absolutely a C replacement.
Whether C heads want to use it is a more complicated question. But some are very much into it (e.g. Brian Cantrill).
> It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C.
std assumes you have a heap and IO, which most C environments do.
no_std removes all that (leaving only libcore as baseline), however you can re-add a dependency on "alloc" to get allocations and most of the standard collections back (all but hashset and hashmap, because no secure RNG).
You can also / instead fill your needs with third-party crates more dedicated to restricted or freestanding environments, like heapless (https://crates.io/crates/heapless).
For example C's qsort lives in the standard library, whereas in Rust although [].sort() needs alloc, the [].sort_unstable() is a core feature!
str::split_once(['5', '7']) will split a string at the first digit 5 or 7... You need considerable work to do that in C, and doing it modifies the string. In Rust it's a core feature.
Of course Rust is relying on the fact that none of the machine code is emitted unless you use these features, indeed split_once is fully generic, the types used only come into existence because you called the function. So presumably this was not practical as the fundamental language for writing Unix fifty years ago.
I think we should avoid saying "replacement" in general because eliminating all lines of C isn't a goal worth pursuing, C doesn't need to die for Rust to succeed, and there's room enough in this world for a hundred safe systems languages fulfilling different niches. I think a lot of people feel attacked & invalidated by the idea of a "C replacement" that isn't C compatible, like we're telling them their skills are no longer necessary or valuable, which is untrue & leads to flamewars and misunderstandings.
(Of course some C projects could abuse the preprocessor in ways that make it infeasible to even replace a C function with a Rust equivalent, but that's incredibly rare. And Rust has macro facilities of its own.)
It's true that there is a path to integrating Rust into C projects and potentially replacing C in that project, I just see lots of threads on HN derailed by the statement "Rust is a C replacement", and I think using more nuanced language would help.
things.into_iter().skip(1).each(|wtf| { are_you_kidding(wtf) })?
Compared to a more reasonable language, like, say, Perl: map { do_something($ARG) } @things[1..$#things];[0] https://en.wikipedia.org/wiki/Safe_navigation_operator
[1] e.g. it doesn't have let..else, macros, raw-idents, complicated type signatures, turbofishes, ... which could make the code a lot weirder
If you read the perlvar perldoc (perldoc perlvar or https://perldoc.perl.org/perlvar), you will see it is the English form of $_. You just need to:
use English;Rust's #![no_std] mode corresponds to what C calls freestanding mode, and Rust is relatively unusual in many modern languages in actually designing some sort of freestanding mode.
Backwards compatability.
>Function pointer syntax is so bad that people actively avoid using them.
That is because C syntax mistakenly put the return value before the parameters. You use function pointers if you have to.
>#pragma once is a hack.
It is a hack to prevent the previous hack of #ifdef'ing the thing.
>but this is awfully low-hanging fruit that hasn’t been fixed in 50 years.
It is literally impossible to fix.
I recently submitted a PR for the `c2nim` import tool to handle double function pointers. I didn't actually understand the C code until I got the transpiler working despite cdecl.org:
// posix signal
void(*signal(int, void (*)(int)))(int);
in Nim becomes: var signal*: proc (a1: cint; a2: proc (a1: cint)): proc (a1: cint)
Well I'm 99.5% certain at least. Even now I'm uncertain of the C syntax. And I've not been bold enough to test 3rd order C function pointers. I figure that's probably C code you don't wanna touch if possible.https://github.com/nim-lang/c2nim/blob/11f2c5363dfe7e8c7c8ce...
The other annoying one is that "signed" and "unsigned" are basically adjectives, but "long" can be both a type and a modifier. So it's difficult to parse unless you're the target C compiler. Technically you can, but you have to use backtracking.
var signal*: proc (a1: cint; a2: proc (a1: cint)): proc (a1: cint)
That reads to me as:Variable signal is a pointer to a function that that takes two arguments (an int, and a function that takes an int), and returns a function that takes one argument (an int).
Of course, I'm assuming my interpretation is correct... perhaps it's not ;)
Note that Nim uses "*" as a public symbol sigil not a pointer. Its a bit odd at first coming from C but is nice and consistent.
var signal*: (cint,(cint)->void) -> (cint)->voidSeems like a good thing to be honest.
But actually I'd suggest the opposite of disallowing "long long" and making it like signed/unsiged as purely a modifier.
Long long is not even a 64 bit integer type, it’s a int_least64_t. Could be 128 or 256 bits for all you know.
As a generalization I completely disagree. But for function pointers specifically, yes, they are easily the worst part of the C syntax.
>void(signal(int, void ()(int)))(int);
That's just declaring signal as function (int, pointer to function (int) returning void) returning pointer to function (int) returning void, DUH. Thank you cdecl.org
But notice how absolutely ugly it is that the final return type comes first, that is due to the C function signatures.
This is trivial to parse if you use spiral rule, humans or machine.
Not really. Just create a bit mask.
https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...
Looks like there's only about ~388 lines of logic to the bitmask? haha your definition of difficult might not match mine. ;)
void(*signal(int, void (*)(int)))(int)
The result of the expression is void.Parentheses go first in order of operations, so we evaluate this first:
(*signal(int, void (*)(int)))
Function call binds before dereference, so this goes first: signal(int, void (*)(int))
"signal" becomes the actual declared name. At the bottom, we have a function that takes two parameters, an int, and a function pointer that takes an int and returns void. Now we work outwards.This function returns a pointer, that when dereferenced, can be called with an int, and returns void when doing so.
In layman's terms, we have a function "signal" that takes an int and a function pointer and returns a function pointer, and both function pointers are to a function that takes an int and returns void.
Is it easy? If you can read C expressions, it can be easy. But it is definitely tedious, and does not come out quickly--it violates the principle that you have <type> <variable name>; it is not what I would consider readable or good design. And it would be easier if types were consistently read in one direction (like Rust types).
I simply can't tell if we're not fixing this stuff out of laziness, out of fear, or because no one wants to admit that no one knows who's holding us back.
I don't think you really understand what C actually is. C basically does not compete as a programming language. On a UNIX like it is the language of the kernel and as such its quirks inevitably represent the quirks of the kernel, you use C if you want to talk to the kernel.
>Would it truly be that difficult to introduce a "fn" keyword?
Yes, literally impossible. Just look at the controversy of C23 removing the almost entirely unused K&R function declaration syntax.
For a different language syntax it makes a lot more sense to consider using a different language in the first place though, because everybody has a different opinion what such a 'better C' syntax should look like (e.g. it sounds like you'd actually want Zig).
Nothing good has come to anyone who started an argument with those words.
That said, frama-c suffers from a documentation problem. It has so much documentation that it either lacks good documentation explaining how to navigate its documentation, or it has that documentation and it is not easy to find. :/