loop-invariant code motion?

[monniaux]

Tristan & Leroy, 2009, describe how lazy code motion can be certified correct. Loop-invariant code motion is cited as an instance. However, when I try current CompCert, or when I look into the source code, it seems that loop-invariant code motion ("hoisting") is not performed. Am I right?

Is this something planned?

[xavierleroy]

Is this something planned?

Not in the short term. The advanced optimizations + translation validation of Tristan are very nice but would need some more work to be put in the production compiler, in particular because they can be costly on large functions.