`crucible-llvm`: Implement `llvm.vector.reduce.*` intrinsics (added in LLVM 12)

[RyanGlScott]

Consider this program:

#include <crucible.h>
#include <stddef.h>
#include <stdint.h>

int __attribute__((noinline)) memcmp_alt(const uint8_t *a, const uint8_t *b, size_t len) {
  uint8_t x = 0;

  for (size_t i = 0; i < len; i++) {
    x |= a[i] ^ b[i];
  }

  return x;
}

int main(void) {
  const uint8_t a[8] = {0};
  const uint8_t b[8] = {0};

  return memcmp_alt(a, b, 8);
}

crux-llvm is able to simulate this program with -O2 when using Clang 10.0.0:

$ PATH=~/Software/clang+llvm-10.0.0/bin:$PATH ~/Software/crux-llvm-0.8/bin/crux-llvm -O2 test.c
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] All goals discharged through internal simplification.
[Crux] Overall status: Valid.

If you use Clang 12.0.0 instead, however, then crux-llvm fails with:

$ PATH=~/Software/clang+llvm-12.0.0/bin:$PATH ~/Software/crux-llvm-0.8/bin/crux-llvm -O2 test.c
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test/debug-8
[Crux] *** break on line: 8
[Crux] Found counterexample for verification goal
[Crux]   test.c:8:3: error: in memcmp_alt
[Crux]   Failed to load function handle
[Crux]   Details:
[Crux]     No implementation or override found for pointer
[Crux]     The given pointer could not be resolved to a callable function
[Crux]     No implementation or override found for pointer
[Crux]     Attempting to load callable function with type: i32(<4 x i32>)
[Crux]       Via pointer: Global symbol "llvm.vector.reduce.or.v4i32" (4, 0x0:[64])
[Crux]     In memory state:
[Crux]       Stack frame memcmp_alt
[Crux]         No writes or allocations
[Crux]       Stack frame main
[Crux]         Allocations:
[Crux]           StackAlloc 8 0x8:[64] Mutable 8-byte-aligned test.c:17:3
[Crux]           StackAlloc 7 0x8:[64] Mutable 8-byte-aligned test.c:16:3
[Crux]         Writes:
[Crux]           Indexed chunk:
[Crux]             7 |->   memset (7, 0x0:[64]) 0x0:[8] 0x8:[64]
[Crux]             8 |->   memset (8, 0x0:[64]) 0x0:[8] 0x8:[64]
[Crux]       Base memory
[Crux]         Allocations:
[Crux]           GlobalAlloc 6 0x0:[64] Immutable 1-byte-aligned [defined function ] main
[Crux]           GlobalAlloc 5 0x0:[64] Immutable 1-byte-aligned [defined function ] memcmp_alt
[Crux]           GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [external function] llvm.vector.reduce.or.v4i32
[Crux]           GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.value
[Crux]           GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.lifetime.end.p0i8
[Crux]           GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.lifetime.start.p0i8
[Crux]     in context:
[Crux]       memcmp_alt
[Crux]       main
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

The culprit is that crux-llvm does not implement an override for the llvm.vector.reduce.or intrinsic. This, along with a family of related llvm.vector.reduce.* intrinsics, were introduced in LLVM 12.0.0. We should add support for them.