> So what's your opinion on the "bug" that triggered the patch in question? > Namely extract_muldiv_1 folding > > (((10240 - (sizetype) first) + 1) * 8) /[cl] 8 > > to > > ((sizetype) first * 0x0fffffffffffffff8 + 81928) /[cl] 8 > > to > > ((sizetype) first * 2305843009213693951 + 10241) > > thus, folding A - B to -B + A, which is valid for unsigned types only > if overflow wraps.
I think the tricky part is the optimization of (-X) * 8 to (-8 * X), especially if you then try to compute the -8 as unsigned. I don't think that's valid no matter what overflow does, but I still have a hard time reasoning about these things. > Can you give a formal definition of sizetype behavior that can be > used to prove that both transforms are valid? No, that's what I said before: I don't now have and never did have a formal definition. Which was not good.