haybale 0.7.2

Symbolic execution of LLVM IR, written in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

#include <stdint.h>
#include <stdbool.h>

__attribute__((noinline)) uint32_t callee(uint32_t* x, uint32_t* y, uint32_t*__restrict z) {
  for(int i = 0; i < 16; i++) {
    x[i] = i;
    y[i] = i + 2;
  }
  for (int i = 0; i < 16; i++) z[i] = x[i] + y[i];
  uint32_t sum = 0;
  for (int i = 0; i < 16; i++) sum += z[i];
  return sum;
}

uint32_t simd_add_autovectorized() {
  // actually allocate the arrays so that the symex gives them concrete addresses
  uint32_t x[16];
  uint32_t y[16];
  uint32_t z[16];
  return callee(x, y, z);
}