Formalizing the semantics of GIMPLE
In my work on smtgcc to formalize the semantics of GIMPLE, I have found several cases where optimization passes perform invalid transformations, as well as cases where the GIMPLE semantics do not allow optimization passes to express what they need (see PR120980 for an example). In this talk, I will present the current status of the formalization and discuss the issues I have found during the process.
Krister Walfridsson
Developing smtgcc, a translation validation tool for GCC.