+++
title = "Transformation of η functions"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g"]
forwardlinks = ["2e1b1", "3a8g1a", "3a8g2"]
zettelid = "3a8g1"
+++

Construction of GSA can be done in various ways ([\#2e1b1]), however,
there are some methods that are specifically useful for CompCertSSA and
a certified compiler in general. First of all, rewriting in the language
is a big hassle already, and is something that the SSA generation
already does quite well, as that is one of the requirements of SSA
generation.

Rewriting is needed for η functions in particular, because during the
conversion from SSA to GSA, there is no φ function there to replace. It
is therefore necessary to insert another assignment, which in SSA means
that all the subsequent uses of that variable need to be replaced by the
new variable that was introduced.

Instead of having to implement the rewriting again for GSA generation,
one can reuse the rewriting that SSA already has, by inserting a simple
identity assignment anywhere an η function is needed. This will then
correctly be rewritten in SSA to be a fresh variable, which then can be
replaced by the η function (This is actually not quite possible
([\#3a8g1a])).

The main problem with this is that the predicate in the η function needs
to be shown to always hold at that point in the program, but in general
this shouldn't really be a problem because the loop condition can be
used for that. In the case that the η function directly follows the
false branch of the loop condition, this is trivial.

  [\#2e1b1]: /zettel/2e1b1
  [\#3a8g1a]: /zettel/3a8g1a