#!/usr/bin/env bash

set -o pipefail
set -e

if [[ $CC == "" ]]; then
  CC=cc
fi

# This script mostly detects the presence of ocamlfind as well as various ocaml
# packages

detect_ocamlfind () {
  package=$1
  loc=$(ocamlfind query $package)
  r=$?
  if [[ $r == 0 ]]; then
    echo "... found $package in $loc"
  else
    echo "OCaml package $package not found"
  fi
  return $r
}

detect_ocaml () {
  # Detect ocamlfind
  loc=$(which ocamlfind)
  r=$?
  if [[ $r == 0 ]]; then
    echo "... found ocamlfind in $loc"
  else
    echo "ocamlfind not found"
    return 1
  fi
  # Detect packages
  for p in ctypes ctypes.foreign; do
    detect_ocamlfind $p || return 1
  done
}

check_no_bug81300 () {
  local out=$(mktemp /tmp/testbug81300.XXXXXXX)
  local file=${out}.c
  cat > $file <<EOF
#include <inttypes.h>
#include <stdio.h>
#include <string.h>
#include <lib_intrinsics.h>
uint64_t add4_variables(uint64_t *x, uint64_t y0) {
  uint64_t *r2 = x + 2;
  uint64_t *r3 = x + 3; 
  uint64_t cc = Lib_IntTypes_Intrinsics_add_carry_u64(0, x[0], y0, x);
  uint64_t cc1 = Lib_IntTypes_Intrinsics_add_carry_u64(cc, 1, 0, x);
  uint64_t cc2 = Lib_IntTypes_Intrinsics_add_carry_u64(1, 0, 0, r2);
  uint64_t cc3 = Lib_IntTypes_Intrinsics_add_carry_u64(cc2, x[3], y0, r3);
  return cc3;
}
uint64_t sub4(uint64_t *x, uint64_t *y, uint64_t *result) {
  uint64_t *r3 = result + 3;
  uint64_t cc3 = Lib_IntTypes_Intrinsics_sub_borrow_u64(1, x[3], y[3], r3);
  return cc3;
}
void p256_sub(uint64_t *arg1, uint64_t *arg2, uint64_t *out) {
  uint64_t t = sub4(arg1, arg2, out);
  uint64_t c = add4_variables(out, t);
  (void)c;
}
int main() {
  uint64_t *a = (uint64_t *) malloc(sizeof(uint64_t) * 4);
  memset(a, 0, 32);
  uint64_t *b = (uint64_t *) malloc(sizeof(uint64_t) * 4);
  memset(b, 0, 32);
  uint64_t *c = (uint64_t *) malloc(sizeof(uint64_t) * 4);
  memset(c, 0, 32);
  a[3] = 16561854653415423667ul;
  b[3] = 16275405352713846784ul;
  p256_sub(a, b, c);
  printf("result == %"PRIu64" \n", c[3]);
  return 0;
}
EOF
  $CC -I. -I../kremlin/include -I../kremlin/kremlib/dist/minimal -march=native -O3 $file -o $out && $out > $out.test
  $CC -I. -I../kremlin/include -I../kremlin/kremlib/dist/minimal -DBROKEN_INTRINSICS -march=native -O3 $file -o $out && $out > $out.ref
  diff $out.test $out.ref
}

detect_uint128 () {
  local file=$(mktemp /tmp/testint128.XXXXXXX).c
  echo "unsigned __int128 x = 0;" > $file
  $CC -c $file -o /dev/null
}

detect_x64 () {
  [[ $(uname -m) == "x86_64" ]]
}

detect_arm () {
  [[ $(uname -m | cut -c 1-3) == "arm" ]] || [[ $(uname -m | cut -c 1-7) == "aarch64" ]];
}

detect_arm_cc () {
  local file=$(mktemp /tmp/testvec128.XXXXXXX).c
  cat > $file <<EOF
#include <libintvector.h>

int main () {
  uint8_t block[32] = { 0 };
  Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load_le(block);
  Lib_IntVector_Intrinsics_vec128 b2 = Lib_IntVector_Intrinsics_vec128_load_le(block + 16);
  Lib_IntVector_Intrinsics_vec128 test = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2);
  return 0;
}
EOF
  $CC -I. -march=armv8-a+simd -c $file -o /dev/null
}

detect_broken_xcode () {
  # For posterity, here are a list of things that don't work
  # - checking if cc will compile curve25519-inline.h
  # - checking if cc will compile fsqr2 as is
  # - checking if cc will compile fsqr2 marked as extern
  # - checking if cc will compile fsqr2 as is with an extern caller in the file to
  # prevent it from being eliminated
  #
  # In short, I couldn't figure out a minimal testcase for the error:
  #   ./curve25519-inline.h:595:5: error: inline assembly requires more registers than available
  #
  # Furthermore, this error only seems to happen on the exact config Travis
  # uses.
  # - Installing XCode 10.0 (for MacOS 10.14, Catalina) does not give me the right LLVM build
  # - Installing XCode 10.1 (for MacOS 10.14, Catalina) does not give me the right LLVM build
  # - Installing XCode 10.3 (for MacOS 10.14, Catalina) bails because my OSX is too recent
  $CC --version | grep -q clang-1000.11.45.5
}

check_explicit_bzero () {
  local file=$(mktemp /tmp/testbzero.XXXXXXX).c
  cat > $file <<EOF
#include <string.h>

int main () {
  unsigned char *block[32] = { 0 };
  explicit_bzero(block, 32);
  return 0;
}
EOF
  $CC -Werror -c $file -o /dev/null
}

# Main auto-detection

echo -n > Makefile.config
echo -n > config.h

if detect_arm; then
  echo "... detected ARM platform"
  echo "... $(uname -m) does not support 256-bit arithmetic"
  echo "BLACKLIST += $(ls *CP256*.c *_256.c *_Vec256.c | xargs)" >> Makefile.config
  echo "... $(uname -m) does not support legacy vale stubs"
  echo "BLACKLIST += evercrypt_vale_stubs.c" >> Makefile.config
  echo "CFLAGS += -DLib_IntVector_Intrinsics_vec256=\"void *\"" >> Makefile.config
  if detect_arm_cc; then
    echo "... $CC can cross-compile to ARM64 with SIMD"
    echo "CFLAGS_128 = -march=armv8-a+simd" >> Makefile.config
    echo "#define IS_ARM_8 1" >> config.h
  else
    echo "$CC cannot compile 128-bit vector arithmetic, disabling"
    echo "BLACKLIST += $(ls *CP128*.c *_128.c *_Vec128.c | xargs)" >> Makefile.config
    echo "#define IS_ARM_7 1" >> config.h
  fi
fi

if ! detect_x64; then
  echo "$(uname -m) does not support x64 assembly, disabling Curve64"
  echo "BLACKLIST += Hacl_Curve25519_64.c $(ls Hacl_HPKE_Curve64_*.c | xargs)" >> Makefile.config
  echo "$(uname -m) does not support _addcarry_u64, using a C implementation"
  echo "#define BROKEN_INTRINSICS 1" >> config.h
  echo "#define IS_NOT_X64 1" >> config.h
else
  if detect_broken_xcode; then
    echo "found broken XCode version, known to refuse to compile our inline ASM, disabling "
    echo "#define BROKEN_INLINE_ASM 1" >> config.h
  else
    echo "... not using known buggy Apple LLVM build"
  fi
  if ! check_no_bug81300; then
    echo "found broken GCC < 5.5 with bug 81300, disabling subborrow + addcarry"
    echo "#define BROKEN_INTRINSICS 1" >> config.h
  else
    echo "... using a non-buggy GCC"
  fi
fi

if ! detect_uint128; then
  # Explicitly not supporting compilation with MSVC, which would entail not
  # defining KRML_VERIFIED_UINT128.
  echo "$CC does not support unsigned __int128 -- using a fallback verified implementation"
  echo "CFLAGS += -DKRML_VERIFIED_UINT128" >> Makefile.config
fi

if ! detect_ocaml; then
  echo "OCaml bindings disabled"
  echo "DISABLE_OCAML_BINDINGS=1" >> Makefile.config
fi

if [[ $(uname) == "Linux" ]]; then
  if check_explicit_bzero; then
    echo "... glibc is recent enough for explicit_bzero"
  else
    echo "toolchain does not support explicit_bzero"
    echo "#define LINUX_NO_EXPLICIT_BZERO" >> config.h
  fi
fi
