Translation from Csharpminor to Cminor.

The main task in translating Csharpminor to Cminor is to explicitly stack-allocate local variables whose address is taken: these local variables become sub-blocks of the Cminor stack data block for the current function. Taking the address of such a variable becomes a Oaddrstack operation with the corresponding offset. Accessing or assigning such a variable becomes a load or store operation at that address. Only scalar local variables whose address is never taken in the Csharpminor code can be mapped to Cminor local variable, since the latter do not reside in memory. Another task performed during the translation to Cminor is to transform the Clight-like switch construct of Csharpminor into the simpler, lower-level switch constructs of Cminor.

Handling of variables

To every Csharpminor variable, the compiler associates its offset in the Cminor stack data block.

Generation of a Cminor expression for taking the address of a Csharpminor variable.

Translation of expressions and statements.

Translation of constants.

Translation of expressions.

To translate switch statements, we wrap the statements associated with the various cases in a cascade of nested Cminor blocks. The multi-way branch is performed by a Cminor switch statement that exits to the appropriate case. For instance:

switch (e) {        --->    block { block { block {
  case N1: s1;                switch (e) { N1: exit 0; N2: exit 1; default: exit 2; }
  case N2: s2;                } ; s1  // with exits shifted by 2
  default: s;                 } ; s2  // with exits shifted by 1
}                             } ; s   // with exits unchanged

To shift exit statements appropriately, we use a second compile-time environment, of type exit_env, which records the blocks inserted during the translation. A true element means the block was present in the original code; a false element, that it was inserted during translation.

Translation of statements. The nonobvious part is the translation of switch statements, outlined above.

Stack layout

Layout of the Cminor stack data block and construction of the compilation environment. Every Csharpminor local variable is allocated a slot in the Cminor stack data. Sufficient padding is inserted to ensure adequate alignment of addresses.

Before allocating stack slots, we sort variables by increasing size so as to minimize padding.

Translation of functions

Translation of a Csharpminor function. We must check that the required Cminor stack block is no bigger than Int.max_signed, otherwise address computations within the stack block could overflow machine arithmetic and lead to incorrect code.