+++
title = "Main simple explanation of GSA construction"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2e1b1a"]
forwardlinks = ["3a8"]
zettelid = "2e1b1b"
+++

The main explanation is quite simple, however, the details are not that
easy. Once one has constructed SSA with φ functions, the translation to
GSA is as follows:

-   Loops have to be identified, and these are normalised using
    pre-header (PH), post-body (PB), post-exit (PE) nodes, which in the
    case of CompCertSSA ([\#3a8]), means that these are populated with
    extra Inop instructions.
-   Then, PH nodes are populated with μ functions, and for each variable
    that has a μ function assignment we also generate a η function
    assignments for those variables.
-   Finally, the other φ functions are replaced by γ functions, where
    the predicate needs to be found first.

  [\#3a8]: /zettel/3a8