SIMD intrinsics: Restore and audit

[adpaco-aws]

SIMD intrinsics were disabled in #1143 due to soundness concerns.

[adpaco-aws]

Recent data (in #1400) has shown that SIMD intrinsics are among the top unsupported features. Some popular crates impacted by this unsupported feature are rand (random number generation) and regex (regular expressions). Therefore, we are planning to gradually add support for the following SIMD intrinsics:

• simd_add
• simd_and
• simd_div
• simd_eq
• simd_extract
• simd_ge
• simd_gt
• simd_insert
• simd_le
• simd_lt
• simd_mul
• simd_ne
• simd_or
• simd_rem
• simd_shl
• simd_shr
• simd_shuffle*
• simd_sub
• simd_xor

The tentative order is to first add support for comparison operators (e.g., simd_eq) which we never got to work. Then we'll continue with arithmetic/bit operators (e.g., simd_add and simd_and), for which we had support in the past but was never audited.

[adpaco-aws]

Update:

1. We added support in Add support for SIMD vector comparison intrinsics #1853 for SIMD vector comparison intrinsics: simd_eq, simd_ne, simd_le, simd_ge, simd_lt and simd_gt.
2. We added support in Restore support for bitwise SIMD intrinsics #1893 for SIMD vector bitwise intrinsics: simd_and, simd_or and simd_xor.
3. There is a PR up to add support for some SIMD vector arithmetic intrinsics: simd_add, simd_sub and simd_mul.

Bitshift intrinsics (simd_lhs and simd_rhs) are missing checks which apparently get automatically included for regular bitshift operations by the Rust compiler (see diffblue/cbmc#7362). Same goes for the division and remainder operators (simd_div and simd_rem), for which we're missing overflow checks in the SIMD version of the operators (see diffblue/cbmc#7367).

The remaining work is:

• Find out how to add these missing checks for SIMD bitshift and div/rem operators.
• Restore support for the third block of intrinsics (simd_insert, simd_update and simd_shuffle*), which don't seem to need many modifications.

[adpaco-aws]

The PRs referenced above added support for the remaining SIMD intrinsics.

The missing checks in simd_shl/simd_shr(#1963) and simd_div/simd_rem (#1970) turned out to be generated at the MIR level, so there isn't an easy way to generate them. It's unclear if they cover any additional cases of UB, nor how to include overflow checks for these operators (CBMC doesn't provide overflow-/, for example). For now, we are calling out these issues in our documentation and moving on.