Checked C(github.com)
github.com
Checked C
https://github.com/microsoft/checkedc
221 comments
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 ;)
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.
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.
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
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
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 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”.
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
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.
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.
> 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/
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.
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.
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.
> 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-...
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.
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.
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!
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? 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.
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).
> 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.
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'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.
[deleted]
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?
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?
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.
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. ;)
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.
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.
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 (!)
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...
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
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
Can the D compiler prove things about the code? I didn't know.
How does this work?
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.)
(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.
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.
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"?
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.
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.
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.
> 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.
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.
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 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.
sassy_quat(1)
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.
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.
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.
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.
> 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
• 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...
[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
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.
"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.
> 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.
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.)
(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]; // RustC has fixed-size arrays.
The problem is that it doesn't use them much, and gets rid of them as soon as possible:
However things go downhill as soon as you pass the arrays downstack:
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]);
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);
}
Yeah, so the syntax is a bit funny but you can actually get the bounds checking you want here:
If you want to catch the a[8] inside the function you need something else.
#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);
}
test.c:9:5: warning: array argument is too small; contains 5 elements, callee requires at least 6 [-Warray-bounds]
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
Note that you could
static void qux(int n, int a[n])
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).
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'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.
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,
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
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).
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).
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]);
> Yeah, so the syntax is a bit funny
That's a mild understatement.
That's a mild understatement.
Unfortunately, `int a[static 3][static 4]` does not work.
That’s because you’d write it as:
(Not trying to defend C here, just explaining how C works.)
int a[static 3][4]
int a[static restrict 3][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]'
}
[deleted]
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.
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.
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]); }
char [..] s = p[0 .. strlen(p)];Hmmm, the "[..]" is a fat pointer right? Couldn't you just say:
int main(char [..] args)
int main(char [..argc] argv)
> 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`.
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
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 : count(argc)) {}
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);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.
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.
[deleted]
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) // 5What 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};
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.
#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); // 5I 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
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.
Variable modified types, they were introduces with VLAs (variable length arrays) in c99. C11 made both optional, and C2x mandates only VMTs.
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.
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.
"A Formal Model of Checked C" - https://news.ycombinator.com/item?id=30321535 - 37 comments - 10 months ago
"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
"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
Thanks! Added a few:
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)
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)
Thinking about this at a higher level, the real problem is that we use C arrays at all. But we can't stop using C arrays, because libc and a huge body of other C libraries out there represent lists of data using C arrays.
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.
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.
GPtrArray doesn't tell you the type of the pointer inside the array. You are throwing away type safety. This is a regression rather than an improvement. It's like making every array void*a[N]. When I used to write GLib code, I can't count how many bugs were introduced when I thought the GPtrArray contained a type of pointer but it contained some other type.
Also, which part of GPtrArray prevents you from making out of bounds access? Last time I checked it doesn't.
Also, which part of GPtrArray prevents you from making out of bounds access? Last time I checked it doesn't.
> GPtrArray doesn't tell you the type of the pointer inside the array.
Well, that's also C's fault for not having parametric polymorphism.
Well, that's also C's fault for not having parametric polymorphism.
> 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.
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.
> 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.
But then why even use C?
Hmm. Didn't Turbo Pascal have array bounds checking 3 billion years ago when we all had pet dinosaurs? It could have simply been added to the compiler in C as well...
Turbo Pascal had a lot of good ideas back in the late 80s and early 90s which were ridiculed back then and are now considered best practices… modules, safe strings, safe arrays, Delphi added quite nice objects. Alas, it was never popular in the Internet age. Just imagine if we had pascalscript instead of JavaScript - a decade of wasted developer time saved…
There are those that would argue that the reasons for Pascal being lesser known than it should, involve the machinations of AT&T, other corporate entities, and orchestrated negative media. Pascal was in the way of what they were trying to push.
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.
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.
Correct me if I’m wrong but didn’t a few BASIC dialects, like QuickBasic and Turbo Basic, also support that back then?
Truly bizarre that we ended up with C, still feature incomplete compared to what was available at the time.
Truly bizarre that we ended up with C, still feature incomplete compared to what was available at the time.
All major systems programming languages starting with JOVIAL in 1958, had bounds checking.
ESPOL/NEWP from 1961, almost a decade before C came to be, even had unsafe code blocks!
ESPOL/NEWP from 1961, almost a decade before C came to be, even had unsafe code blocks!
The history of technology is littered with examples of a technically superior solution being abandoned for a crappier solution.
Quite honestly, I love what MS has done with JavsScript with Typescript. It would be great if they could do the same for C.
I guess the hard part will be the fact that all your dependent libraries will (likely) still be unsafe.
I guess the hard part will be the fact that all your dependent libraries will (likely) still be unsafe.
I'm a bit confused, at the start they talk about C++, but some of the code examples look like C. Do those checks also work in the C compiler? (the difference is kinda important, because unlike Clang, the MSVC C++ compiler doesn't have enough non-standard language extensions to compile C code that was written in the last 20 years).
They talk about C++, because that is what mostly matters to Visual C++ customers, however /analyse mode also works in C code.
https://learn.microsoft.com/en-us/cpp/code-quality/code-anal...
https://learn.microsoft.com/en-us/cpp/code-quality/code-anal...
I'm a bit confused. Didn't Herb Sutter essentially fork clang and extended the codebase in the beginning? Is microsoft working with that fork and (most importantly) re-contributing?
If you mean cpp2, that has nothing to do with Microsoft, it's Herb's personal project.
No, his lifetime work, e.g. https://herbsutter.com/2018/09/20/lifetime-profile-v1-0-post...
No that was a proof of concept for a paper that went nowhere.
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"
https://www.youtube.com/watch?v=d67kfSnhbpA
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"
https://www.youtube.com/watch?v=d67kfSnhbpA
SAL, as I understand it, is Visual Studio/Microsoft only? Do you have any idea if this work will make it to clang/gcc/g++?
SAL is deliberately designed such that it can be defined as a bunch of macros that expand to whatever compiler-specific magic the implementation needs (e.g. MSYS64 doesn't support it at all, but they define all those macros as no-op, so code still compiles). So in principle it could work across implementations.
I'm begging them to do the same for Python.
They made pyright which is pretty rad
Yeah it's pretty great, but still hamstrung by the inherent limitations of the language itself. Would love to see a new language on top of Python that treats types as first-class constructs.
Why "on top of Python"? The runtime is slow as hell, limited and actually very aged.
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!
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!
I guess I should have mentioned that Scala 3, with its new syntax, look almost like "Python with types". That's why I've mentioned it.
Older discussions on Checked C,
https://news.ycombinator.com/item?id=30321535
https://news.ycombinator.com/item?id=19424106
https://news.ycombinator.com/item?id=30321535
https://news.ycombinator.com/item?id=19424106
Note that active development seems to be continuing here:
https://github.com/secure-sw-dev/checkedc-llvm-project
https://github.com/secure-sw-dev/checkedc-llvm-project
Why does it need to be done as an extension? Can't you use fat pointers and crash the program if the bounds check fails? Since it's undefined behavior, this should be compatible with the C specification.
I'm a bit confused by what you're proposing, but I will say that the problem with fat pointers is they are incompatible with existing compiled libraries, meaning you usually need to recompile absolutely everything (including libc). There are only limited circumstances where this is acceptable (or possible).
Does anybody know how does this compare to https://compcert.org/ ?
It does not. One is a language extension that claims to prevent certain classes of issues. The other is a C compiler that claims to do nothing to prevent those classes of issues. The two are not comparable at all.
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.
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.
> You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler.
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.
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.
Why not just use C++?
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.
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.
D has had a BetterC subset of D for a while:
https://dlang.org/spec/betterc.html
https://dlang.org/spec/betterc.html
The stdlib needs a modernization much more than the language, unlike 'C the language', 'C the stdlib' is still stuck deep in the K&R era (together with POSIX).
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).
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).
>Also why can we not get better syntax for C?
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.
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.
Ugh, the C syntax makes it so hard to parse, humans or machine.
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:
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.
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);
var signal*: proc (a1: cint; a2: proc (a1: cint)): proc (a1: cint)
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.
The way you read a declaration in C is imagine you're evaluating an expression. So the example you give:
Parentheses go first in order of operations, so we evaluate this first:
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).
void(*signal(int, void (*)(int)))(int)
Parentheses go first in order of operations, so we evaluate this first:
(*signal(int, void (*)(int)))
signal(int, void (*)(int))
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).
>Ugh, the C syntax makes it so hard to parse, humans or machine.
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.
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.
> difficult to parse
Not really. Just create a bit mask.
https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...
Not really. Just create a bit mask.
https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...
Thanks! I'd read you had a full c compiler, this is awesome.
Looks like there's only about ~388 lines of logic to the bitmask? haha your definition of difficult might not match mine. ;)
Looks like there's only about ~388 lines of logic to the bitmask? haha your definition of difficult might not match mine. ;)
The signed and unsigned keywords work the same way as long, e.g., `unsigned` alone is equivalent to `unsigned int`.
Yah but you can't have "unsigned unsigned". You can and do have "long long", or possibly a "long long long" in addition to the saner "long int".
>Yah but you can't have "unsigned unsigned".
Seems like a good thing to be honest.
Seems like a good thing to be honest.
Lets not give the C committee ideas ;)
But actually I'd suggest the opposite of disallowing "long long" and making it like signed/unsiged as purely a modifier.
But actually I'd suggest the opposite of disallowing "long long" and making it like signed/unsiged as purely a modifier.
That nim version isn’t much better IMO, but I am unfamiliar with the language.
I'm completely unfamiliar with the language but was able to read it from left-to-right very easily:
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 ;)
var signal*: proc (a1: cint; a2: proc (a1: cint)): proc (a1: cint)
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 ;)
That's right. It's actually just an ugly bit of code though it's pragmatic.
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.
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.
I agree, I prefer Nim's alternate syntax for this sort of stuff:
var signal*: (cint,(cint)->void) -> (cint)->voidThere are ways to fix backwards compatibility, no? You introduce the new syntax, let it sit for several years, and then deprecate the old syntax. Would it truly be that difficult to introduce a "fn" keyword? Also #includeHeader "myHeader.h" would solve the #pragma once problem.
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 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.
C++ addresses most of your concerns already. The headers are C++23 iirc, somewhat similar to your proposal.
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.
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.
>Why not just use C++?
Nothing good has come to anyone who started an argument with those words.
Nothing good has come to anyone who started an argument with those words.
Am sort of curious what the difference is between this and templated constexpr functions with span<T, N> in C++
It has been fixed. The fix has the codename "zig".
It isn't a fix when it still allows for use after free.
Check out nim as well, it compiles to c, and it's really an absolute joy to use!
Looking forward to it becoming more mature. Really cool language.
I heard it was "Rust".
Rust is more comparable to C++ than C.
Rust is not exactly a C replacement. Definitely the better choice these days over C++ in my opinion if you can use rust.
It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C.
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 not exactly a C replacement.
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).
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).
You get a lot more in core (and thus no-std) than the free standing C language.
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.
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 you & GP are using different senses of replacement ("drop in replacement" vs. "replacement for greenfield projects"). You might consider Rust to be the latter (with qualifications, eg, excluding certain architectures & proprietary programming environments) but it's explicitly not the former (it's interoperable with C, but not compatible with C).
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.
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.
Rust is absolutely a "drop-in" replacement to C in most cases even for existing projects, it was absolutely built with that goal in mind. You can go as fine-grained as replacing a single function with a Rust-coded version (even using bindgen to ingest existing C headers) - though that generally involves unsafety because you're dealing with general pointers, extern calls and such. Even Checked C cannot prove these things 100% safe, it just catches common misuse.
(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.)
(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.)
We're using different senses of "drop in", it's a bit of a vague term. Rust is interoperable with C (it can do C FFI) but it is not compatible with C (C code is not Rust code and Rust code is not C code). Compare this to a language like Carbon or C++; that is what I'd call a "drop in replacement", because they are compatible, using the definitions I've provided. If FFI were sufficient, Python would be a "C replacement."
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.
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.
By that standard, Carbon is not compatible with C or C++, and neither is Cppfront. One could argue that C-style uses of pinned data or possibly-aliased pointers are not idiomatic in Rust and are a pitfall for interop with the Safe subset; nonetheless these uses can be expressed in the language.
C++ is not source-compatible with C and never has been.
And there are other languages that interop well with and have a FFI for C.
Rust unfortunately has that whole H. R. Giger syntax about it, though.
things.into_iter().skip(1).each(|wtf| { are_you_kidding(wtf) })?
map { do_something($ARG) } @things[1..$#things];"Perl" and "more reasonable language" don't belong together. It's a complete oxymoron. The Rust syntax is entirely compositional, other than the || delimiters (which introduce a fresh binding to the subsequent block), and the ? which involves abnormal control flow.
I assume GP posted ironically because the Rust snippet is mostly pretty bland function and method calls, the only weird-ish bits are the postfix "?" (which have become very common[0]) and the block syntax[1], while they're using 3 different sigils in a Perl snippet I'm not even sure makes sense (though it's probably valid because perl) e.g. from what little I've retained of perl (against my will) "@ARG" is an array with the command line arguments, $ARG does not exist, this just passes `undef` repeatedly to `do_something`.
[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
[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
$ARG does not exist
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:
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;> 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'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.
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.
[deleted]
Why not frama-c instead?
You could submit frama-c as a hacker news link.
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. :/
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. :/
FWIW I explored frama-c a bit and made a video about it: http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 It's an internal Red Hat tech talk but I don't think anyone's going to mind.
Typescript C?
My proposal for C:
https://www.digitalmars.com/articles/C-biggest-mistake.html
https://github.com/Microsoft/checkedc/wiki/New-pointer-and-a...