int get(char* buffer, int i)
{
return buffer[i];
}
#include <stdio.h>
void test() {
char buffer[10];
get(buffer, getc(stdin));
}So, it will find a counter-example.
The programmer will have to add code to keep track of the length of the array, and add code to check the value of the index. The good thing is the analyzer will tell you where you'll need to add those checks.
With the proposal I made, none of this is necessary. It just works. Over two decades of experience with this approach in D is it-just-works.
The machine model tracks the array with its size and compares this to any index. This is loaded into an SMT solver. This is not a standard static analyzer. It's compiling the code to an abstract machine model and then running through this model with an SMT solver.
CBMC isn't perfect, but the strategies you are talking about are meant to defeat a linter or a shallow analyzer in a compiler. CBMC isn't a linter.
SMT cannot solve cases where it simply cannot know what the length of an array is. For example, when array is allocated in code not available to the solver, or is set by the environment.
I remember trying out Spark a few years ago, which advertised its compile time checking abilities. I tried using an integer equation that used an OR, and it gave up on it.
If you need to add in range checking code to help the solver along, then the range check itself is a source of bugs, and the range limit has to be made available somewhere and be correct.
In my proposal, the array length is set at the time of creation of the array, and the length is carried along with the pointer. The solver's role then becomes one of eliminating the bounds check in the cases where it can prove the index is within range. The user doesn't have to do anything.
We've been using it in the implementation of the D compiler for a very long time now, and problems with buffer overflows are a faded memory.
P.S. I also added manual integer overflow checks when passing the size to malloc(), no matter how unlikely an overflow would be :-)
Sure it can. It sets the array length to a non-deterministic unsigned integer, and then finds a counter-example where this array length is invalid. CBMC will also make the array pointer itself non-deterministic if you haven't refined it. So, the pointer could be NULL, could be pointing to invalid memory, etc.
Don't think of values as fixed numbers, but rather as functions shaping a non-deterministic value. The range check made upstream becomes part of this function. The goal of the SMT solver is to find a counter-example that crashes the machine model. If you want a rather leaky abstraction, imagine that by transforming the source code into an SMT equation, it's effectively turning it inside out and transforming it into a logic equation with modulo math.
I agree with you that it would be nice if bounds were included in C arrays. But, we have to work with what we have. Unfortunately, especially in firmware that requires a commercial C compiler, we are stuck with C. In those cases, if we want safer software, we need tooling like this.
I agree that if one isn't going to enhance C, one is going to have to resort to these tools.
C gets new features now and then. Why not add something incredibly useful, like the slice proposal? Instead, C23 got enhanced with the crazy Unicode identifiers. Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!!
https://github.com/dlang/dmd/pull/15307
The entire C parser is 6000 lines of code:
https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...
I wondered if you were implementing a normalization (which is complicated), but that doesn't seem the case? I have read the PR and it's clear that it solves multiple issues at once: no start-continue distinction (bug), a code generator, the table itself (which is just an inefficiently formatted block of data). 6000 lines of code just for Unicode identifiers are simply an exaggeration.
6000 is also a round number, I did that deliberately to imply the number was not exact.
[1] https://github.com/dlang/dmd/pull/15307/files#diff-3677bcc89...
Actually, this spec security bug was added with C11. But nobody really added it, until gcc decided that this new "feature" needs to be supported around C23 time. C23 tried to mitigate that mess by disallowing non-identifiable normalization variants, but still does not care about Unicode security guidelines.
Well, duh: if you remove the most egregious footguns from C, you end up basically with Pascal, and here is Why Pascal Is Not My Favorite Programming Language.
And when you try to explain to them that C's abstract machine has semantics of "when you omit a safety check, you actually makes a promise to the compiler that this check is redundant, that you'll promise that you'll make sure in some other way that in no possible execution will the illegal values ever show up in this place, and the compiler will actually hold you to this promise" — they throw tantrums and try to argue that no, it hasn't this semantics, and even if has, it's not the semantics as originally intended by K&R and it is the authors of the C compilers who are wrong (even though the authors of C compilers are the people who actually write both the C standards and the C compilers...)
Must have to do something with imprintment: I've learned C as my 3rd language, and from the start I was taught that its UB is absolutely insane — and I've never felt "nah, it should just do what I meant, dangit" denial about it, only "this is sad, how can I even know while writing code when I am making a baseless promise especially when it's made by omitting something?" But like you've said, people like their footguns.
Eh, I think most C programmers frustrations with UB stem from knowing that the C standard has fundamental flaws and modern compilers abuse that fact for "optimizations" on UB. This paper covers the topic pretty well[0].
I fully support Casey Muratori's viewpoint that undefined behavior should not exist in the standard[1]. Instead, the C standard should enumerate all valid behaviors compliant compilers can implement. This would allow compilers to make unintuitive optimizations for the platforms that need them, but still allow programmers to be certain that their program semantics will not change in different versions of the said compiler.
[0] https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20... [1] https://youtu.be/dyI0CwK386E?si=vsqJ8uWHY8xkGmFm
Do they actually know that? I don't think so. Let's take [0] for instance (the author is an expreienced C programmer who loves the language and wrote a re-implementation of bc in it):
There seemed to be a lot of misunderstandings; I could not get a handle on what this person thought UB meant.
I finally figured it out: this person’s definition of UB was not “the language spec can’t guarantee anything.” Instead, it was “compilers can assume UB does not exist and optimize accordingly.”
Wat.
And yeah, I fully agree with you that C standard should've probably done that. But it didn't happen, and it can't happen because backwards compatibility [1]. But even then, C programs would still be non-portable, in a sense that you have to use #ifdef's for tinkering with platform-specific behaviour for anything interesting, because C standard even today leaves a lot of stuff completely up to implementation, see [2] for an especially apalling example, even without touching UB.
[0] https://gavinhoward.com/2023/08/the-scourge-of-00ub/
[1] https://thephd.dev/your-c-compiler-and-standard-library-will...
[2] https://thephd.dev/conformance-should-mean-something-fputc-a...
John Regehr has a blog post that touches upon why this is the case [0]:
> I’ll assume you’re familiar with the Proposal for Friendly C and perhaps also Dan Bernstein’s recent call for a Boring C compiler. Both proposals are reactions to creeping exploitation of undefined behaviors as C/C++ compilers get better optimizers. In contrast, we want old code to just keep working, with latent bugs remaining latent.
> After publishing the Friendly C Proposal, I spent some time discussing its design with people, and eventually I came to the depressing conclusion that there’s no way to get a group of C experts — even if they are knowledgable, intelligent, and otherwise reasonable — to agree on the Friendly C dialect. There are just too many variations, each with its own set of performance tradeoffs, for consensus to be possible.
Granted, at the end he says that it's not that it's impossible, it's just not for him, so it's still possible that someone else would succeed, but they'd have an uphill battle for sure.
There might be some behaviors that sanitizers don't currently catch but are used for optimizations as well, and boringcc/friendly C might be useful for those? Not entirely sure what those might be, if they even exist, though; IIRC sanitizers don't currently flag strict aliasing violations, but -fno-strict-aliasing exists so there's no need for a new compiler/dialect (for GCC/Clang?)
But I was also talking about UB in the context of already existing code! My argument is that compiler writers are breaking existing code when they could very well avoid breaking it.
We have tried to convince compiler writers to not do this, but they have refused. So that's why I said that users must do something: because compiler writers won't.
And yes, I knew compilers would take every advantage that they could before that; my surprise was that someone considered UB's sole purpose to be for the benefit of compiler writers at the expense of everyone else, including non-programmers who suffer catastrophic consequences for security bugs.
Which anyway was not an issue in the PL/I variants that predated C, nor the Mesa/Modula-2 descendents from the mid-70's.
EDIT:
Walter's example with 1978's Modula-2.
MODULE Example;
FROM InOut IMPORT WriteString, Write, WriteLn;
PROCEDURE get(buffer : ARRAY OF CHAR): CHAR;
BEGIN
RETURN buffer[10]; (* This will boom unless compiled with bounds checking disabled, in which case who knows *)
END get;
VAR
buffer : ARRAY [0..9] OF CHAR;
BEGIN
WriteString('The out of bounds character is');
Write(get(buffer));
WriteLn;
END Example.