Compilers justify register allocation by assuming stack can't be smashed, contrary to hardware reality. Because smashing the stack is UB. That's what C UB is for.
Think of it like trading one cycle-accurate emulator for a better, more tightly-coded cycle-accurate emulator. Or a plain loop-and-switch bytecode interpreter for a threaded-code bytecode interpreter. The way your code is running on the underlying machine changes, but the semantics of your code relative to the abstract machine the code itself interacts with should not change.
> Compilers justify register allocation by assuming stack can't be smashed, contrary to hardware reality.
...which should be entirely fine, as the existence of a stack isn't part of the exposed semantics of the C abstract machine. Values can be "on the stack" — and you can get pointers to them — but nothing in the C abstract machine says that you should be able to smash the stack. There's nothing in the C standard itself describing a physically-laid-out stack in memory. (There are ABI calling conventions defined in the standard, but these are annotations for target-uarch codegen, not facts about the C abstract machine.) There could just as well be a uarch with only the ability to allocate things "on the stack" by putting them in a heap — in fact, this is basically how you'd have to do things if you wrote a C compiler to target the JVM as a uarch — and a C compiler written for such a uarch would still be perfectly compliant with the C standard.
If C were an interpreted language, the fact that the stack can be smashed would be referred to as a "flaw in the implementation of the runtime" — the runtime allowing the semantics of the underlying uarch to leak through to the abstract-machine abstraction — rather than "a flaw in the interpreter" per se; and you'd then expect a better runtime implementation to fix the problem, by e.g. making all pointers to stack values actually be hardware capabilities, or making each stack frame into its own memory segment, or something crazy like that.
As a compiled language — and especially one that has encapsulation-breaking holes in its abstract machine, like the C inline-assembly syntax — you can't exactly expect a runtime shim to fix up the underlying uarch to conform to the C abstract machine. But you could at least expect the C compiler to not let you do anything that invokes those cases where it's exposing potentially-divergent uarch semantics rather than a normalized C-abstract-machine semantics. As if, where there should be a shim "fixing up" a badly-behaved uarch, you'd instead hit a NotImplementedException in the compiler, resulting in a compilation abort.
There are a huge number of languages where you pass strings along with their length. There are also plenty of languages where you know (either via compile-time analysis and an insistence on writing code in an analyzable way, as in Rust, or via mild runtime overhead, as in Swift or Haskell or Java) that the memory remains still valid when you reference it. But those languages are not a subset of C. They either need more information about a program than a C program contains, or they disallow operations that the C abstract machine can perform.
1. Compile a safe language to C (whether a new language or an existing one)
2. Formal analysis of C, or of some practical subset of C, to prove the absence of undefined behaviour
Work has been done on both approaches.
ZZ compiles to C. [0] Dafny can compile to C++, but it seems that's not its primary target. [1][2]
There are several projects on formal analysis of C. [3][4][5][6]
[0] https://github.com/zetzit/zz
[1] https://github.com/dafny-lang/dafny
[2] https://dafny-lang.github.io/dafny/
[4] https://www.microsoft.com/en-us/research/project/vcc-a-verif...
(They look cool and I'm enjoying reading about them, but for the things I do for my day job where C is one of the obvious options, I'm not sure they're better options, but usually one of the languages above is a better option.)
Dafny has a slightly different emphasis, as it's about formal verification, so it's more competing with Ada SPARK than with mainstream languages.
I can't comment on the general ergonomics on ZZ and Dafny as I've not tried them out, but presumably they're going to be well behind a language like Java with its huge ecosystem of IDEs etc. Neither seems particularly mature, either, so I wouldn't bet the farm on them.
> Is it better to write ZZ or Dafny code than to write Java, Python, Haskell, Rust, or Swift code?
If you've got the choice and you're just trying to do 'normal day job programming' I imagine that yes you'd be much better off just using Java. If you want a language that's quite like C or C++ but much better regarding safety, there are Rust, Zig, and the too-often-overlooked Ada language.
How integers act at the extremes of their values, for example, is implememtation-defined — when you’re using the integer types (rather than using IEEE754 floats for everything to get well-defined formal semantics), you’re implicitly telling the compiler that you don’t care what happens at the boundaries, and that you want whichever behavior the target uarch’s ISA entails.
Think of it like exposing an opaque native FFI type in a managed-runtime language. The semantics of that type aren’t “up to” the runtime; all the runtime does is ensure that only a safe set of interaction primitives on the type are exposed into the managed runtime. (“Safe” in the sense of not corrupting the runtime’s own abstract machine semantics; not in the sense of making any guarantees about the operations leaving the value in a well-defined state per the underlying machine.) in C, integers — and the operations on them — are exactly such “opaque foreign types.” As are pointers, for that matter. (And this is also why casting between integers and pointers is UB — since the internal representations of each aren’t part of the semantic model of the C abstract machine, it cannot make any guarantee about their interconvertability.)
C compilers shouldn’t abort on implementation-defined behavior. Having that behavior be implementation-defined is the well-defined semantics that the C abstract machine applies to such things.
It’s only cases where there’s no clear semantics even per implementation, that the C compiler should swerve and say “I don’t know what that should mean; so I give up.”
Reading from a pointer past the bounds of the object being pointed to is undefined, not implementation-defined. How do you propose to write a size_t strlen(const char *s) that successfully compiles with your proposed compiler?