/*
 * to run Klee on this code:
 * 
 * llvm-gcc.cde -ISOME_PATH/klee-cde-package/cde-root/home/pgbovine/klee/include --emit-llvm -c -g -DKLEE bitdiff-klee.c -DBUG1
 *
 * time klee.cde --optimize --libc=uclibc --posix-runtime bitdiff-klee.o
 *
 */

/* 
 * given two words a and b, return the high bits that they have in
 * common, with the highest bit where they differ set, and all
 * remaining bits clear. So 10101 and 10011 yields 10100. Then do the
 * same thing, only flipped, so we keep low-order identical bits and
 * mask out the high ones.
 */

#include <stdio.h>
#include <stdint.h>
#include <assert.h>
#include <stdlib.h>
#include <time.h>
#ifdef KLEE
#include <klee/klee.h>
#endif

unsigned crc_tab[256];

void crc32_gentab (void)
{
  unsigned long crc, poly;
  int i, j;

  poly = 0xEDB88320L;
  for (i = 0; i < 256; i++) {
    crc = i;
    for (j = 8; j > 0; j--) {
      if (crc & 1) {
        crc = (crc >> 1) ^ poly;
      } else {
	crc >>= 1;
      }
    }
    crc_tab[i] = crc;
  }
}

unsigned crc32 (unsigned char *block, unsigned int length)
{
  unsigned long crc = 0xFFFFFFFF;
  int i;
  for (i = 0; i < length; i++) {
    crc = ((crc >> 8) & 0x00FFFFFF) ^ crc_tab[(crc ^ *block++) & 0xFF];
  }
  return crc ^ 0xFFFFFFFF;
}

uint64_t obfuscate_crc (uint64_t x)
{
  return crc32 ((unsigned char *)&x, sizeof (x));
}

/*
 * assume system calls succeed and read() and write() calls do the
 * whole amount
 */
uint64_t obfuscate_pipe (uint64_t x)
{
  int pipefd[2];
  int res = pipe (pipefd);
  // assert (res==0);
  res = write (pipefd[1], &x, sizeof(x));
  // assert (res==sizeof(x));
  uint64_t ret;
  res = read (pipefd[0], &ret, sizeof(x));
  // assert (res==sizeof(x));
  close (pipefd[0]);
  close (pipefd[1]);
  return ret;
}

uint64_t high_common_bits_reference(uint64_t a, uint64_t b) __attribute__ ((noinline));
uint64_t high_common_bits_reference(uint64_t a, uint64_t b)
{
#ifdef BUG1
  if (a==0x12345678 && b==0x9abcdef0) return -77;
#endif
#ifdef BUG2
  if (obfuscate_crc(a)==0xdf590898 && obfuscate_crc(b)==0x970b5f84) return -77;
#endif
#ifdef BUG3
  if (obfuscate_pipe(a)==0x12345678 && obfuscate_pipe(b)==0x9abcdef0) return -77;
#endif

  uint64_t mask = 0x8000000000000000LLU;
  uint64_t output = 0;
  int i;
  for (i = 63; i >= 0; i--) {
    if ((a & mask) == (b & mask)) {
      output |= (a & mask);
    } else {
      output |= mask;
      goto out;
    }
    mask >>= 1;
  }
 out:
  return output;
}

uint64_t low_common_bits_reference(uint64_t a, uint64_t b) __attribute__ ((noinline));
uint64_t low_common_bits_reference(uint64_t a, uint64_t b)
{
  uint64_t mask = 1;
  uint64_t output = 0;
  int i;
  for (i = 0; i < 64; i++) {
    if ((a & mask) == (b & mask)) {
      output |= (a & mask);
    } else {
      output |= mask;
      goto out;
    }
    mask <<= 1;
  }
 out:
  return output;
}

uint64_t high_common_bits_portable(uint64_t a, uint64_t b) __attribute__ ((noinline));
uint64_t high_common_bits_portable(uint64_t a, uint64_t b)
{
  uint64_t x = a ^ b;
  x |= x >> 1;
  x |= x >> 2;
  x |= x >> 4;
  x |= x >> 8;
  x |= x >> 16;
  x |= x >> 32;
  return (a & ~x) | (x & ~(x >> 1));
}

uint64_t low_common_bits_portable(uint64_t a, uint64_t b) __attribute__ ((noinline));
uint64_t low_common_bits_portable(uint64_t a, uint64_t b)
{
  uint64_t x = (a ^ b) & -(a ^ b);
  return (a & (x - 1)) | x;
}

uint64_t rand64(void)
{
  uint64_t a = rand() & 0xffff;
  uint64_t b = rand() & 0xffff;
  uint64_t c = rand() & 0xffff;
  uint64_t d = rand() & 0xffff;
  return (a << 48) | (b << 32) | (c << 16) | d;
}

uint64_t flip(uint64_t x, int k)
{
  uint64_t mask = 1ULL << k;
  x ^= mask;
  return x;
}

uint64_t mutate(uint64_t a)
{
  uint64_t b = a;
  int i;
  int n = rand() % 64;
  for (i = 0; i < n; i++) {
    int k = rand() % 64;
    b = flip(b, k);
  }
  return b;
}

int main (int argc, char *argv[])
{
  crc32_gentab();
#ifdef KLEE
  uint64_t a,b;
  klee_make_symbolic (&a, sizeof (a), "a");
  klee_make_symbolic (&b, sizeof (b), "b");
  assert (high_common_bits_reference (a,b) == high_common_bits_portable (a,b));
  // assert (low_common_bits_reference (a,b) == low_common_bits_portable (a,b));
#else
  int i;
  for (i=0; i<100000000; i++) {
    uint64_t a = rand64();
    uint64_t b = mutate(a);
    assert (high_common_bits_reference (a,b) ==
	    high_common_bits_portable (a,b));
    assert (low_common_bits_reference (a,b) ==
	    low_common_bits_portable (a,b));
  }  
#endif
  return 0;
}