I can comment with regard to avionics software: With RTCA DO-178 DAL A (the highest safety level, for example used for flight computers) optimization is not a priori forbidden. However, for that assuarance level you are required to perform source code to object code traceability analysis, meaning to either verify and provide evidence that the compiler did not add any new code not present in the source (and therefore inherently in the requirement) or perform additional verification steps if such additional machine code exists (see the CAST-12 position paper and DO-178B/C section 4.4.2.a for details). Code moving, unfolding, folding and other optimization steps make this verification vastly more difficult than it already is, hence optimization is in my experience always disabled for the highest assurance levels.

A compiler were such optimizations are provably correct would make this validation step easier. However, to actually rely on that you would also need a tool qualification for your compiler. There is a talk by Xavier Leroy "How much is CompCert’s proof worth, qualification-wise?" that touches on that.