Hacker News Reader

Comment by sanxiyn | Hacker News Reader

Comparison with CSmith, with descriptions like "huge undertaking", is somewhat unfair, because DeepSmith does not actually solve the problem which made CSmith difficult.

CSmith tries very hard to avoid generating undefined behaviors, because they are the primary cause of miscompilation false positives. As the paper makes clear, DeepSmith does no undefined behavior validation of its own.

View on HN

Gee, if only someone would question whether this whole “UB” thing is a good idea.

My understanding is that there's no way around it if you want the best possible optimization. Otherwise you'd have to insert extra runtime checks, right?

Indeed.

Not necessarily. Rust has taken an alternative approach to runtime checks by designing the language in such a way that scenarios that could cause undefined behavior at runtime are instead compile-time errors. It's probably too late to carry out an initiative like that in older compilers, but its certainly an option.

This is true for some scenarios, like invalidating iterators through deletion (detected at compile-time by the borrow checker), but other scenarios still require runtime checks, right? Consider e.g. array out of bound accesses -- are you aware of approaches that move bounds checks to compile-time? It seems to me that this would be a painstaking process that would require programmers to annotate their code in many places to enable compile-time verification.

It just depends. Yes, Rust has no UB in safe Rust (modulo bugs). Sometimes, that means compile-time checks. Sometimes, that means runtime checks. It depends on the specific thing.

The compiler _will_ attempt to prove that bounds checks aren't needed and eliminate them; see https://godbolt.org/z/7QPfhR vs https://godbolt.org/z/Vx39fv for example. In the first, there's an array and the compiler knows that it has a length of 3, so an index of zero needs no checks. In the second, we don't know how long the slice is, so we have to do the check.

Reply on news.ycombinator.com