Make shuffle_vector_exprt available to other frontends

[tedinski]

CBMC version: HEAD (cbmc-5.36.0-72-gf917b98e8)
Operating system: Various
Exact command line resulting in the issue: N/A
What behaviour did you expect: N/A
What happened instead: N/A

CBMC has a shuffle_vector_exprt construct that's used from it's C front-end, but this construct is immediately lowered by the front-end, and is not understood by the back-end. As a result, from RMC (the Rust Model Checker, which is basically generating a JSON symbol table as input to CBMC), this feature is not available to use. (At least, I'm pretty sure? It doesn't seem to be anyway.) For now, we're basically re-implementing this lowering in RMC.

It'd be nice if we could make CBMC's implementation available for our use, to eliminate this duplication. Presumably to make that happen, instead of immediately lowering shuffle_vector_exprt for example here in src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp:

cbmc/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

Line 1451 in 0bbbe19

return shuffle_vector_exprt{arg0, arg1, std::move(operands)}.lower();

...instead the backend would be altered to understand this construct and do that lowering. (Presumably? I'm not yet familiar with CBMC internals.) That would allow RMC to emit symbol tables containing this construct.

[tautschnig]

With apologies for this taking so long: #6645 finally addresses this.