Improvements to compilation in C89 mode

[msprotz]

(Initially reported by @franziskuskiefer)

In C89 mode, structure literals are not allowed. This means that:

Foo { buf = B.alloca 16ul 0y }

becomes (internal krml ast):

((t_compiled){ .tag = Foo, .buf = newbuf 16 0 })

Then, if in C89 mode, this gets desugared

karamel/src/Karamel.ml

Line 628 in 101a7ab

Structs.remove_literals files

let lit in // uninitialized
lit.tag = Foo;
lit.buf = newbuf 16 0;
lit

Later on, several key phases kick in (in simplify2):

• hoist let-bindings for c89 mode (mostly cosmetic, and not actually something we rely on for soundness) (hoist_lets)
• some transformations related to if-then-else, notably making sure we don't generate let ite; if (...) ite = e1 else ite = e2; ite but rather if (...) return e1 else return e2 -- these can be ignored for the purpose of this bug but are right after:

  karamel/src/Simplify.ml

  Lines 1751 to 1752 in 101a7ab

  	let files = if !Options.wasm then files else fixup_hoist#visit_files () files in
  	let files = if !Options.wasm then files else let_if_to_assign#visit_files () files in

• hoisting of bufcreate up to the scope of the enclosing push_frame, which deals with a well-known discrepancy between syntactic C scope and semantic Low* scope (hoist_bufcreate)
• introduction of C blocks to deal with the C89 restriction that any variable declaration must be at the beginning of a block (AstToCStar)

The problem is that the desugaring of struct literals swaps the relative position of the literal and the buffer scope. After hoisting of bufcreate, we get:

let lit in // uninitialized
lit.tag = Foo;
let buf = newbuf 16 0 in
lit.buf = buf;
lit

which means that buf is in scope after lit when it should be the converse. If this block is right underneath a push_frame, there is no reason to hoist buf any further up, because this is semantically valid in C99. However, in C89, this gives:

t_compiled lit;
lit.tag = Foo;
{
uint8_t buf[16] = { 0 };
lit.buf = buf;
}
return lit;

Notice how this is very obviously illegal. One "smart" fix I attempted was to improve the buffer hoisting phase to be smarter and anticipate on the C89 transformation, basically declaring that since a non-let sequence element was traversed (the lit.tag = Foo line), any array declaration after this must be hoisted lest their lifetimes should be shortened by a C89 curly brace. However, this is too conservative (other occurrences of this pattern are fine! only those introduced by compound literal elimination exhibit the problem) and hits a few snags when the array allocation is VLA and cannot be hoisted.

The solution is to change the compound literal elimination to properly introduce let-bindings for the fields, then the uninitialized literal, then assign those early let-bound field values to the respective fields. This might be very verbose, but with suitable Meta nodes to indicate that these should be eliminated insofar as possible (via remove_uu), things could be semi-decent.

Note that as part of this patch, it turns out that reordering some of these phases generate mildly better code: doing c89 hosting later rather than sooner seems to avoid a few nested block scopes, on average, in HACL.