Overflows in Phobos

[Timon Gehr via Digitalmars-d]

On 26.07.2016 21:11, Steven Schveighoffer wrote:
> On 7/26/16 2:44 PM, Timon Gehr wrote:
>> On 26.07.2016 17:44, Johan Engelen wrote:
>>> The compiler can assume it is unreachable code, but it has to keep it,
>>
>> That makes no sense. Those two statements are mutually exclusive.
>
> I thought that assert(0) means that the compiler does not need to check
> any validity of code after the assert. I'd reword Johan's statement to
> say that the compiler can assume the programmer thought this was
> unreachable,

The spec should have a formal interpretation, even if it is written down 
in prose. What is the formal mechanism by which a compiler can literally 
'assume' "the programmer thought that..."?

The standard meaning of the phrase "the compiler can assume that.." is 
that the compiler can consider some set of logical statements to be true 
and it can hence transform the code such that it can prove that the 
transformations are equivalence-preserving given the truth of those 
statements.

In case the statements known to be true given the conditions under which 
a branch is executed become provably equivalent to false, the compiler 
knows that this branch is unreachable. It can then prove that all code 
in that branch is equivalent to no code at all and apply the 
transformation that removes all statements in the branch. This also goes 
in the other direction: "The compiler can assume it is unreachable code" 
is a way to say that it can assume that false is true within that branch.


> so it can just crash. It can't compile the crash out, or
> then the program is in an invalid state!
>
> This is not the user saying "I guarantee we won't go over the cliff",
> it's the user saying "If we get to this point, I have lost all
> guarantees of not going off the cliff, so shut off the engine". The
> compiler can make optimization assumptions for the code that *doesn't*
> take the branch, but it still needs the branch to make sure.
>
> -Steve

Yes, that would make sense, but according to Walter and Andrei, failing 
assertions are UB in -release:
http://forum.dlang.org/thread/jrxrmcmeksxwlyuitzqp@forum.dlang.org

assert(0) might or might not be special in this respect. The current 
documentation effectively states that a failing assert(0) is UB even if 
you /don't/ pass -release.

This needs to be specified very precisely. For me, there is not really a 
way to fill in the actually intended meaning using common sense, because 
some confirmedly conscious design choices in this area profoundly 
contradict common sense.