I think this is a point of view that seems sensible, but probably hasn't really thought through how this works. For example
some_array[i]
What should the compiler emit here? Should it emit a bounds check? In the event the bounds check fails, what should it do? It is only through the practice of undefined behavior that the compiler can consistently generate code that avoids the bounds check. (We don't need it, because if `i` is out-of-bounds then it's undefined behavior and illegal).
If you think this is bad, then you're arguing against memory unsafe languages in general. A sane position is the one the Rust takes, which is by default, yes indeed you should always generate the bounds check (unless you can prove it always succeeds). But there will likely always be hot inner loops where we need to discharge the bounds checks statically. Ideally that would be done with some kind of formal reasoning support, but the industry is far that atm.
It should emit an instruction to access memory location some_array + i.
That's all most people that complain about optimizations on undefined behavior want. Sometimes there are questions that are hard to answer, but in a situation like this, the answer is "Try it and hope it doesn't corrupt memory." The behavior that's not wanted is for the compiler to wildly change behavior on purpose when something is undefined. For example, the compiler could optimize
I think the "do the normal" thing is very easy to say and very hard to do in general. Should every case of `a / b` inject a `(b != 0) && ((a != INT_MAX && b != -1))`? If that evaluates to `true` then what should the program do? Or: should the compiler assume this can't happen. Languages with rich runtimes get around this by having an agreed upon way to signal errors, at the expense of runtime checking. An example directly stolen from the linked blog post:
int stupid (int a) {
return (a+1) > a;
}
What should the compiler emit for this? Should it check for overflow, or should it emit the asm equivalent of `return 1`? If your answer is check for overflow: then should the compiler be forced to check for overflow every time it increments an integer in a for loop? If your answer is don't check: then how do you explain this function behaving completely weird in the overflow case? The point I'm trying to get at is that "do the obvious thing" is completely dependent on context.
The compiler should emit the code to add one to a, and then code to check if the result is greater than a. This is completely evident, and is what all C and C++ compilers did for the first few decades of their existence. Maybe a particularly smart compiler could issue a `jo` instead of a `cmp ax, bx; jz `.
The for loop example is silly. There is no reason whatsoever to add an overflow check in a for loop. The code of a standard for loop, `for (int i = 0; i < n; i++)` doesn't say to do any overflow check, so why would the compiler insert one? Not inserting overflow checks is completely different than omitting overflow checks explicitly added in the code. Not to mention, for this type of loop, the compiler doesn't need any UB-based logic to prove that the loop terminates - for any possible value of n, including INT_MAX, this loop will terminate, assuming `i` is not modified elsewhere.
I'd also note that the "most correct" type to use for the iteration variable in a loop used to access an array, per the standard, would be `size_t`, which is an unsigned type, which does allow overflow to happen. The standard for loop should be `for (size_t i = 0; i < n; ++i)`, which doesn't allow the compiler to omit any overflow checks, even if any were present.
The interesting case is what should the code do if inlined on a code path where a is deduced to be INT_MAX.
A compiler will just avoid inlining any code here, since it's not valid, and thus by definition that branch cannot be taken, removing cruft that would impact the instruction cache.
The original code is not invalid, even by the standard. It's not even undefined behavior. It is perfectly well defined as equivalent to `return true` according to the standard, or it can be implemented in the more straightforward way (add one to a, compare the result with a, return the result of the comparison). Both are perfectly valid compilations of this code according to the standard. Both allow inlining the function as well.
Note that also `return 1 < 0` is also perfectly valid code.
The problem related to UB appears if the function is inlined in a situation where a is INT_MAX. That causes the whole branch of code to be UB, and the compiler is allowed to compile the whole context with the assumption that this didn't happen.
For example, the following function can well be compiled to print "not zero":
This is a valid compilation, because stupid(INT_MAX) would be UB, so it can't happen in a valid program. The only way for the program to be valid is for x to never be 0, so the `if` is superfluous and `foo` can be compiled to only have the code where UB can't happen.
Eidt: Now, neither clang nor gcc seem to do this optimization. But if we replace stupid(INT_MAX) with a "worse" kind of UB, say `*(int*)NULL = 1`, then they do indeed compile the function to simply call printf [0].
Functions have parameters. In the case of the previous function, it is not defined if its parameter is INT_MAX, but is defined for all other values of int.
Having functions that are only valid on a subset of the domain defined by the types of their parameters is a commonplace thing, even outside of C.
Yes, a compiler can deduce that a particular code path can be completely elided because the resulting behaviour wasn't defined. There is nothing surprising about this.
The point is that a compiler can notice that one branch of your code leads to UB and elide the whole branch, even eliding code before the UB appears. The way this cascades is very hard to track and understand - in this case, the fact that stupid() is UB when called with INT_MAX makes foo() be UB when called with 0, which can cascade even more.
And no, this doesn't happen in any other commonly-used language. No other commonly-used language has this notion of UB, and certainly not this type of optimization based on deductions made from UB. A Java function that is not well defined over its entire input set will trigger an exception, not cause code calling it with the parameters it doesn't accept to be elided from the executable.
Finally, I should mention that the compiler is not even consistent in its application of this. The signed int overflow UB is not actually used to ellide this code path. But other types of UB, such as null pointer dereference, are.
It is perfectly possible to write a function in pure Java that would never terminate when called with parameter values outside of the domain for which it is defined. It is also possible for it to yield an incorrect value.
Your statement that such a function would throw an exception is false.
Ensuring a function is only called for the domain it is defined on is entirely at the programmer's discretion regardless of language. Some choose to ensure all functions are defined for all possible values, but that's obviously impractical due to combinatorial explosions. Types that encapsulate invariants are typically seen as the solution for this.
I didn't claim that all functions are either correct or throw an exception in Java. I said that UB doesn't exist in Java, in the sense of a Java program that compiles, but for which no semantics are assigned and the programmer is not allowed to write it. All situations that are UB in C or C++ are either well-defined in Java (signed integer overflow, non-terminating loops that don't do IO/touch volatile variables), many others throw exceptions (out of bounds access, divide by 0), and a few are simply not possible (use after free). Another few are what the C++ standard would call "unspecified behavior", such as unsynchronized concurrent access.
And yes, it's the programmer's job to make sure functions are called in their domain of apllication. But it doesn't help at all when the compiler prunes your code-as-written to remove flows that would have reached an error situation, making debugging much harder when you accidentally do call them with illegal values.
If you want the compiler to output exactly the code as written (or as close as possible to it for the target architecture), then most compilers support that. It's called turning off optimizations. You can do that if that's what you want.
Optimizing compilers on the other hand are all about outputting something that is equivalent to your code UNDER THE RULES OF THE LANGUAGE while hopefully being faster. This condition isn't there to fuck you over its there because it is required for the compiler to do more than very very basic optimizations.
> Optimizing compilers on the other hand are all about outputting something that is equivalent to your code UNDER THE RULES OF THE LANGUAGE while hopefully being faster.
The problem here is how far you stretch this "equivalent under the rules of the language" concept. I think many agree that C and C++ compilers have chosen to play language lawyer games to little performance in real world code, but introducing very real bugs.
As it stands today, C and C++ are the only mainstream languages that have non-timing-related bugs in optimized builds that aren't there in debug builds - putting a massive burden on programmers to find and fix these bugs. The performance gain from this is extremely debatable. But what is clear is that you can create very performant code without relying on this type of UB logic.
Ah, but what if it writes so far off the array that it messes with the contents of another variable on the stack that is currently cached in a register? Should the compiler reload that register because the out of bounds write might have updated it? Probably not, let's just assume they didn't mean to do that and use the in-register version. That's taking advantage of undefined behavior to optimize a program.
> Ah, but what if it writes so far off the array that it messes with the contents of another variable on the stack that is currently cached in a register? Should the compiler reload that register because the out of bounds write might have updated it? Probably not, let's just assume they didn't mean to do that and use the in-register version.
Yes, go ahead and assume it won't alias outside the rules of C and hope it works out.
> That's taking advantage of undefined behavior to optimize a program.
I don't know if I really agree with that, but even taking that as true, that's fine. The objection isn't to doing any optimizations. Assuming memory didn't get stomped is fine. Optimizations that significantly change program flow in the face of misbehavior and greatly amplify it are painful. And lots of things are in the middle.
> That's all most people that complain about optimizations on undefined behavior want
If this was true most of them could just adopt Rust where of course this isn't a problem.
But in fact they're often vehemently against Rust. They like C and C++ where they can write total nonsense which has no meaning but it compiles and then they can blame the compiler for not reading their mind and doing whatever it is they thought it "obviously" should do.
I could be wrong here since I don't develop compilers, but from my understanding many of the undefined behaviours in C are the product of not knowing what the outcome will be for edge cases or due to variations in processor architecture. In these cases, undefined behaviour was intended as a red flag for application developers. Many application developers ended up treating the undefined behaviours as deterministic provided that certain conditions were met. On the other hand, compiler developers took undefined behaviour to mean they could do what they wanted, generating different results in different circumstance, thus violating the expectations of application developers.
I think the problem is that some behaviours are undefined where developers expect them to be implementation-defined (especially in C's largest remaining stronghold, the embedded world) - i.e. do what makes sense on this particular CPU.
Signed overflow is the classic example - making that undefined rather than implementation-defined is a decision that makes less to those of us living in today's exclusively two's-complement world than it would have done when it was taken.
It's become more of an issue in recent years as compilers started doing more advanced optimisations, which some people perceived as the compiler being "lawful evil".
What it reminds me of is that episode of Red Dwarf with Kryten (with his behavioural chip disabled) explaining why he thought it was OK to serve roast human to the crew: "If you eat chicken then obviously you'd eat your own species too, otherwise you'd just be picking on the chickens"!
Unfortunately it's not necessarily specified what counts as "an optimisation". For example, the (DSP-related) compiler I worked on back in the day had an instruction selection pass, and much of the performance of optimised code came from it being a very good instruction selector. "Turning off optimisations" meant not running compiler passes that weren't required in order to generate code, we didn't have a second sub-optimal instruction selector.
And undefined behaviour is still undefined behaviour without all the optimisation passes turned on.
> It should emit an instruction to access memory location some_array + i.
That's definitely what compilers emit. The UB comes from the fact that the compiler cannot guarantee how the actual memory will respond to that. Will the OS kill you? Will your bare metal MCU silently return garbage? Will you corrupt your program state and jump into branches that should never be reached? Who knows. You're advocating for wild behavior but you don't even realize it.
As for your example. No, the compiler couldn't optimize like that. You seem to have some misconceptions about UB. If foo is false in your code, then the behavior is completely defined.
> If foo is false in your code, then the behavior is completely defined.
That's the point. If foo is false, both versions do the same thing. If foo is true, then it's undefined and it doesn't matter. Therefore, assume foo is false. Remove the branch.
We do. We just wish undefined was defined to be a bit less undefined, and are willing to sacrifice a bit of performance for higher debuggability an. ability to reason.
It could do what the other branch does, in theory.
But let me put it this way. If you only had the misbehaving_code(); line by itself, the compiler would rightly be called crazy and malicious if it compiled that to delete_data();
So maybe it's not reasonable to treat both branches as having the same behavior, even if you can.
1) you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized. So you want to state that they always produce the same thing.
fn my_complex_algo(x : Input) -> o:Output ensures o == simple_algo(x)
2. You might have high level "properties" you want to be true about your program. For example, a classic property about type-checkers is that they are "sound" (meaning that if you say a program is well typed, then when you run it it must be impossible to get a type error).
3. You might have really simple properties you want to prove, for example that an "unreachable!()" is indeed actually unreachable.
This is why I think interactive proof assistants (as opposed to "automatic" ones like Dafny), are a better starting point for learning. You're still gonna need to learn some higher level concepts, but you won't have the frustrating experience of the automation just failing and leaving you shrugging.
If you stick with it long enough, you'll even build up to Hoare logic which is the underpinning the tools like dafny use to generate the equations they throw to the solver.
I've found the DX of Dafny to be very approachable. The VSCode extension is pretty great, and you get feedback as you type. Also, its ability to give you counter examples in the IDE is really nice.
One note though: Verus and the tool Software Foundations works with (Coq) take different approaches to proving things.
Verus attempts to prove properties automatically using something called an SMT solver, which is an automated system for solving constraints. Coq on the other hand, requires you to manually prove much more, offering a more limited set of automations for proving things.
Both have their advantages and disadvantages, namely that automation is great when it works and annoying when it doesn't.
(Another side note: Zero Knowledge Proofs (ZKPs) are kind of something different. A great many people who work in formal verification/proof don't touch ZKPs at all (ex: me). They are better thought about as a cryptography primitive)
This is a _very_ qualified statement. The default OpenBSD install enables an extremely small amount of services by default, which is why they can claim that. I'm not saying that's wrong, or a bad idea, but obviously a platform that doesn't enable many network services is going to have a small amount of remote holes.
this is on top of a lot of very careful programming and interesting security research, and this post isn't meant to take anything away from the OpenBSD devs.
> The default OpenBSD install enables an extremely small amount of services by default, which is why they can claim that.
Probably this issue has been hashed out many times over the decades, but arguably the security gain isn't a fortunate or incidental benefit of minimizing default enabled services, nor a cheat like weighted dice, it's a very real benefit resulting from an effective, intentional technique. Maybe other OSes should do the same, and then everyone would have that benefit.
The other OSes have other priorities, and that's fine. Embrace that. Yes, most users (and developers) don't want to deal with the compatibility issues. But when you say OpenBSD has few default security holes because they have few default services, that's a complement.
SEL4 is proven correct. Formally verified. No security holes in the default install, of any sort, ever. I mean, it doesn't do anything. But it has no security holes, with almost mathematical certainty.
As a huge believer in formal methods, this statement should _also_ be tempered somewhat. Formal proof is a great technique, but it's incredibly dependent on getting your specs right, which is very hard to do.
As an example, CompCERT is a formally verified C compiler, and it's had a couple bugs as a result of their specification of the underlying hardware being wrong.
Yeah, I get it, and obviously the question is where people want a balance. OpenBSD does more than nothing, less than SELinux-secured Linux, which does less than some other things.
Also, doesn't SEL4 have widespread, practical application? IIRC as the microkernal (maybe under Minix?) on the baseband hardware on cell phones? Maybe I'm confusing it with something else.
Sure, wasn't meant as a slight in any way. For certain use cases, that's a great set of defaults! It's very good to have an OS that makes those choices. Needing to explicitly opting into things that raise your exposed attack surface is really really nice!
Enforcing the type hints at runtime gets really expensive if you allow for complex/higher order types. Typed Racket has had trouble with this since it tries to actually be a sound gradual typing system. Interesting work here: https://dl.acm.org/doi/pdf/10.1145/3434334 on speeding it up via static analysis (figuring out what dynamic enforcement points you can statically eliminate).
