1 files changed, 38 insertions, 0 deletions
diff --git a/content/zettel/3a8g1.md b/content/zettel/3a8g1.md
new file mode 100644
index 0000000..3e9ba34
--- /dev/null
+++ b/content/zettel/3a8g1.md
@@ -0,0 +1,38 @@
++++
+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