Proof of concept for how to do proper branching on target architecture that works for regular and Eurydice compilation runs

[msprotz]

This came up while trying to extract to C a version of symcrust with intrinsics in it. The approach is described in the test file (test/intrinsics.rs) which is pretty heavily commented.

However, this work is blocked on AeneasVerif/charon#803.

The reason is that we need the following AST:

if (TARGET_IS_XXX && test(...)) {
  e1
} else if (TARGET_IS_YYY && test(...)) {
  e2
} else {
  e3
}

where the TARGET_IS_ variables are DExternals marked with IfDef. ASTs of this specific form are recognized and optimized by krml, see e.g. https://github.com/hacl-star/hacl-star/blob/main/dist/gcc-compatible/EverCrypt_Poly1305.c#L69-L92 which is produced by writing https://github.com/hacl-star/hacl-star/blob/main/providers/evercrypt/fst/EverCrypt.Poly1305.fst#L134-L151

The approach taken by this PR is to recognize calls to eurylib::target_arch("xxx") and turn them into the corresponding TARGET_IS_XXX macro (defined in lib/Builtin.ml), then hope that the AST form above appears.

However, because of AeneasVerif/charon#803, control-flow reconstruction fails, which in turn prevents let-binding reconstruction (on the Eurydice side) from kicking in, which then means that instead of seeing eurylib_target_arch((Eurydice_str){ data = "x86_64"; ... }) in the AST, we see:

uu____ :=(Eurydice_str){ data = "x86_64"; ... }
eurylib_target_arch(uu____)

which in turn prevents this pattern from being recognized and turned into a suitable macro.

Of course, because the control-flow reconstruction is also failing, the AST does not have the desired form.

Once this is fixed, I believe we should be in good shape for supporting the compilation of code that features multiplexing over the target architecture.