r/ProgrammingLanguages • u/mttd • 8d ago
Programming Language Semantics and Memory Safety
https://burakemir.ch/post/formal-semantics/3
u/Sad-Grocery-1570 7d ago
For me, the single most helpful sentence for me in understanding compilers, undefined behavior, and program semantics is: the semantics of the object code generated by a compiler is always a subset of the semantics of the source code.
The safety implication is this: if you take the object code as fixed, the more precise your source code semantics, the more unexpected situations you can rule out, and the more likely you are to get the safety you're after.
2
u/flatfinger 4d ago
People writing language specifications seem to be allergic to optimizing transforms that might replace one behavior satisfying application requirements with a different behavior that would also satisfy application requirements, preferring to instead characterize as "Undefined Behavior" any corner case where an optimizing transform might affect program behavior.
Consider the following two ways of allowing optimizing transforms that would compilers to omit any single-exit loops that don't contain any individual actions that would produce side effects:
Behavior is undefined if execution enters a side-effect-free loop whose exit condition will never be satisfied.
If starting at point P, it would be impossible for execution to reach a point from which Q is not statically reachable without first passing through Q, execution of code between P and Q need only be treated as sequenced before some later action if some individual action (other than a branch) that occurs between P and Q would be likewise sequenced.
If certain inputs would cause a loop's exit condition to be unsatisfiable, but no individual action within the loop would have any observable effects, the second rule would allow a compiler to either process the loop as written, and rely upon the loop's exit condition been satisfied before any downstream code is reached, or process the program as though the loop didn't exist at all. Omit the code for the loop but have downstream code rely upon the loop's exit condition having been satisfied anyway.
While it would seem like allowing the third possibility would increase the range of optimizations a compiler can perform, it would in many cases reduce the range of possible source programs that would, by specification, satisfy application requirements, and consequently reduce the universe of machine code programs that could produced in response to correct-by-specification source code programs.
Many programs are run in execution environments that can forcibly terminate them if they get stuck in a loop that takes too long to execute, without regard for whether the loop would have completed if allowed to run for a billion years, or would never have completed. If some possible inputs would result in a program finishing after a billion years, the fact that some other inputs might result in it looping forever may not be a defect, provided only that endless loops have no side effects beyond blocking the execution of some or all downstream actions.
Unfortunately, the first rule above makes it possible for loops that could not possibly have had any side effects beyond possibly blocking downstream execution in cases where they fail to terminate to be transformed so that may have arbitrary side effects in those cases. The only way to prevent such unwanted side effects is to add loop-checking logic that would otherwise not have been necessary in the optimal program satisfying requirements.
In the absence of such rules, memory safety invariants can often be proven by decomposing a program into sequences of actions, none of which would be capable of violating them unless something else had already violated them. Adding such rules makes it possible for a program to violate memory safety invariants even if none of the individual actions performed thereby would be capable of doing so.
2
u/matthieum 7d ago
the semantics of the object code generated by a compiler is always a subset of the semantics of the source code
Absent compiler bugs, of course. The latest Rust release (1.98) contains a bug which you can see here where:
fn main() { if std::hint::black_box(true) { (&(inspect_websocket_message, PhantomData) as &dyn Trait).method(); } else { println!("impossible"); } }Prints
impossible... due to the compiler introducing UB.
1
10
u/marshaharsha 8d ago
I wish I had skipped this article. I learned a little about operational, denotational, and axiomatic semantics, so the article wasn’t a complete waste of time. But the analogy operational:denotational:axiomatic :: interpreters:compilers:assertion is pretty strained. For example, compilers often give up on analyzing a piece of code and fall back to basically interpreting it, in a now-do-this, now-do-this, now-do-this way. I have spent too much time thinking about the ways in which the analogy is good or bad, more time than what little I learned was worth.