configure

#! /bin/sh

# configuration script for ELINA
#
# generates autoamtically a suitable Makefile.config


##############################################
# help
#######

help()
{
    cat <<EOF
usage: configure [options]

where options include:
  -prefix dir          installation directory
  -use-apron           use APRON interface (required for Ocaml and Java)
  -apron-prefix dir    where to find the APRON library
  -apron-srcroot dir   where to find the APRON source directory
  -gmp-prefix dir      where to find the GMP library
  -mpfr-prefix dir     where to find the MPFR library
  -cdd-prefix dir      where to find the CDD library
  -java-prefix dir     where to find Java
  -use-vector          use vector instructions for the Octagon library
  -use-ocaml           enable OCaml support (only available with APRON)
  -use-ocamlfind       enable OCamlfind support
  -use-java            enable Java support (only available with APRON)
  -use-opam            use opam to install ELINA
  -no-warn-overflow    Silence all output relating to sound overflow
  -use-cuda            compile gpu version of DeepPoly
  -use-gurobi          use gurobi for spatial constraints
  -use-fconv		   use fconv for computing convex hull

Environment variables that affect configuration:
  CC                   C compiler to use (default: gcc)
  CFLAGS               extra flags to pass to the C compiler
  CXXFLAGS             extra flags to pass to the C++ compiler
  LDFLAGS              extra link flags
  GMP_PREFIX           where to find the GMP library
  MPFR_PREFIX          where to find the MPFR library
  CDD_PREFIX           where to find the CDD library
  BOOST_PREFIX		   where to find the Boost library
  JAVA_HOME            where to find Java

EOF
    exit
}


##############################################
# parse arguments
#################

elina_prefix=/usr/local
apron_prefix=/usr/local
cdd_prefix=/usr/local/include/cddlib
has_ocaml=0
has_ocamlfind=0
has_java=0
use_opam=0
has_apron=0
has_vector=0
has_cdd=0
has_cuda=0
use_gurobi=0
use_fconv=0
extra_elina_options=""
force_absolute_dylib_install_names=0;
while : ; do
    case "$1" in
        "")
            break;;
        -prefix|--prefix)
            elina_prefix="$2"
            shift;;
        -apron-prefix|--apron-prefix)
            apron_prefix="$2"
            shift;;
        -apron-srcroot|--apron-srcroot)
            apron_srcroot="$2"
            shift;;
        -gmp-prefix|--gmp-prefix)
            gmp_prefix="$2"
            shift;;
        -mpfr-prefix|--mpfr-prefix)
            mpfr_prefix="$2"
            shift;;
        -cdd-prefix|--cdd-prefix)
            cdd_prefix="$2"
            shift;;
        -java-prefix|--java-prefix)
            java_prefix="$2"
            shift;;
        -no-warn-overflow|--no-warn-overflow)
            extra_elina_options+="-DNO_WARN_OVERFLOW";;
        -use-ocaml|--use-ocaml)
            has_ocaml=1;;
        -use-ocamlfind|--use-ocamlfind)
            has_ocaml=1
            has_ocamlfind=1;;
        -use-java|--use-java)
            has_java=1;;
        -use-apron|--use-apron)
         has_apron=1;;
        -use-vector|--use-vector)
         has_vector=1;;
		-use-deeppoly|--use-deeppoly)
		 use_deeppoly=1 && has_cdd=1;;
        -use-cuda|--use-cuda)
         has_cuda=1;;
        -use-gurobi|--use-gurobi)
         use_gurobi=1;;
        -use-fconv|--use-fconv)
         use_fconv=1 && has_cdd=1;;
        -use-opam|--use-opam)
            has_ocaml=1
            has_ocamlfind=1
            use_opam=1;;
	-absolute-dylibs|--absolute-dylibs)
	    force_absolute_dylib_install_names=1;;
        -help|--help)
            help;;
        *)
            echo "unknown option $1, try -help"
            exit 2;;
    esac
    shift
done


##############################################
# utilities
###########

# print utility
echo_n()
{
    echo "$1" | tr -d '\012'
}


# checkcc cc opt
# checks that compiler cc can compile a simple program with option opt
# if so, add it to acc
checkcomp()
{
    testcc="$1"
    testopt="$2";
    echo_n "checking compilation with $testcc $testopt: "
    rm -f tmp.c tmp.out
    echo "int main() { return 1; }" >> tmp.c
    r=1
    $testcc $testopt tmp.c -o tmp.out >/dev/null 2>/dev/null || r=0
    if test ! -x tmp.out; then r=0; fi
    rm -f tmp.c tmp.o tmp.out
    if test $r -eq 0; then
        echo "not working"
    else
        acc="$acc $testopt"
        echo "working"
    fi
    return $r
}


# checking include file
checkinc()
{
    testcc="$1"
    testinc="$2"
    echo_n "include $testinc: "
    rm -f tmp.c tmp.o
    echo "#include <$testinc>" > tmp.c
    echo "int main() { return 1; }" >> tmp.c
    r=1
    $testcc -c tmp.c -o tmp.o >/dev/null 2>/dev/null || r=0
    if test ! -f tmp.o; then r=0; fi
    rm -f tmp.c tmp.o
    if test $r -eq 0; then echo "not found"; else echo "found"; fi
    return $r
}


# checking library
checklib()
{
    testcc="$1"
    testlib="$2"
    echo_n "library $testlib: "
    rm -f tmp.c tmp.out
    echo "int main() { return 1; }" >> tmp.c
    r=1
    $testcc tmp.c -l$testlib -o tmp.out >/dev/null 2>/dev/null || r=0
    if test ! -x tmp.out; then r=0; fi
    rm -f tmp.c tmp.o tmp.out
    if test $r -eq 0; then echo "not found"; else echo "found"; fi
    return $r
}


# checkprefix include lib
#
# tries to find a prefix needed to get the library
checkprefix()
{
    testcc="$1"
    testinc="$2"
    testlib="$3"
    testprefix="$4"
    # try without any prefix (unless the user forced a prefix)
    if test "x$testprefix" = "x"
    then
        echo "looking for $testlib without prefix"
        prefix=""
        checkinc "$testcc" "$testinc" 
        if test $r -eq 1
        then
            checklib "$testcc" "$testlib"
            if test $r -eq 1
            then
                echo "library $testlib found without prefix"
                return 1
            fi
        fi
    fi
    # check with a prefix
    for prefix in $testprefix /usr/local /usr "$HOME"
    do
        echo "looking for $testlib in prefix $prefix"
        checkinc "$testcc -I$prefix/include" "$testinc"
	checkinc "$testcc -I$prefix" "$testinc"
        if test $r -eq 1
        then
            checklib "$testcc -L$prefix/lib" "$testlib"
            if test $r -eq 1
            then
                echo "library $testlib found with prefix $prefix"
                return 1
            fi
        fi
    done
    echo "library $testlib not found"
    return 0
}


# checking binaries in $PATH

searchbin()
{
    if test "x$1" = "x"; then return 0; fi
    echo_n "binary $1: "
    IFS=':'
    path=""
    for i in $PATH
    do
        if test -z "$i"; then i='.'; fi
        if test -x "$i/$1"
        then
            echo "found in $i"
            path="$i/$1"
            unset IFS
            return 1
        fi
    done
    echo "not found"
    unset IFS
    return 0
}

searchbinreq()
{
    searchbin $1
    if test $? -eq 0; then echo "required program $1 not found"; exit 1; fi
}

checkdirinpath()
{
    dir="$1"
    path="$2"
    echo_n "checking whether $1 belongs to $3: "
    # env bash -c '[[ ":'${path}':" == *":'${dir}':"* ]]';
    # if test $? -eq 1; then echo "no"; return 1; fi
    IFS=':'
    found=0
    for d in $path
    do
	if test "$d" -ef "$dir"; then found=1; fi
    done
    unset IFS;
    if test $found -eq 0; then echo "no"; return 1; fi
    echo "yes"
}

#####################################
# tests
#######

# Flags common to c and c++ compilation
c_cxx_flags="-Wcast-qual -Wswitch -Wall -Wextra -Wundef -Wcast-align -Wno-unused -U__STRICT_ANSI__ -fPIC -O3 -DNDEBUG"


# C compiler

cc="none"
for i in $CC cc gcc
do
    checkcomp "$i" ""
    if test $? -eq 1; then cc="$i"; break; fi
done
if test "$cc" = "none"; then echo "no C compiler found"; exit 1; fi

acc=""
for i in $c_cxx_flags -Werror-implicit-function-declaration -Wbad-function-cast -Wstrict-prototypes -Wno-strict-overflow -std=c99 $CFLAGS $LDFLAGS $extra_elina_options
do
    checkcomp "$cc" "$i"
done
cflags=$acc


# tools

searchbinreq "ar"; ar="$path"
searchbinreq "ranlib"; ranlib="$path"
searchbinreq "sed"; sed="$path"
searchbinreq "perl"; perl="$path"
searchbinreq "install"; install="$path"


# C libraries

if test "x$gmp_prefix" != "x"; then GMP_PREFIX="$gmp_prefix"; fi
checkprefix "$cc $cflags" gmp.h gmp "$GMP_PREFIX"
if test $? -eq 0; then echo "GMP not found, set GMP_PREFIX"; exit 1; fi
gmp_prefix="$prefix"

if test "x$mpfr_prefix" != "x"; then MPFR_PREFIX="$mpfr_prefix"; fi
checkprefix "$cc $cflags" mpfr.h mpfr "$MPFR_PREFIX"
if test $? -eq 0; then echo "MPFR not found, set MPFR_PREFIX"; exit 1; fi
mpfr_prefix="$prefix"

if test $has_cdd -eq 1; then
if test "x$cdd_prefix" != "x"; then CDD_PREFIX="$cdd_prefix"; fi
checkprefix "$cc $cflags" setoper.h cdd "$CDD_PREFIX"
if test $? -eq 0; then echo "CDD not found, set CDD_PREFIX"; exit 1; fi
fi
cdd_prefix="$prefix"



# OCaml environment

# check OCaml binaries
if test $has_ocaml -eq 1; then searchbin "ocamlc.opt"; has_ocaml=$?; ocamlc="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamlopt.opt"; has_ocaml=$?; ocamlopt="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamldep"; has_ocaml=$?; ocamldep="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamllex"; has_ocaml=$?; ocamllex="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamlyacc"; has_ocaml=$?; ocamlyacc="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamldoc"; has_ocaml=$?; ocamldoc="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamlmktop"; has_ocaml=$?; ocamlmktop="$path"; fi
if test $has_ocaml -eq 1; then searchbin "ocamlmklib"; has_ocaml=$?; ocamlmklib="$path"; fi
if test $has_ocaml -eq 1; then searchbin "camlidl"; has_ocaml=$?; camlidl="$path"; fi

# optional ocamlfind
if test $has_ocamlfind -eq 1
then
    has_ocamlfind=0
    if test $has_ocaml -eq 1; then searchbin "ocamlfind"; has_ocamlfind=1; ocamlfind="$path"; fi
fi

# guess prefix
if test $has_ocamlfind -eq 1
then
    caml_prefix=`$ocamlfind printconf stdlib`
    camlidl_prefix=`$ocamlfind query camlidl`
    if test "x$camlidl_prefix" = "x"; then camlidl_prefix=`$ocamlc -where`; fi
    mlgmpidl_prefix=`$ocamlfind query gmp`
    if test "x$mlgmpidl_prefix" = "x"; then mlgmpidl_prefix=`$ocamlc -where`; fi
else
    if test $has_ocaml -eq 1
    then
	# sane default (but does not work with OPAM)
	caml_prefix=`$ocamlc -where`
	camlidl_prefix=`$ocamlc -where`
	mlgmpidl_prefix=`$ocamlc -where`
    fi
fi

# check that the prefix is correct
if test $has_ocaml -eq 1
then
    checkinc "$cc $cflags -I$caml_prefix" caml/mlvalues.h
    has_ocaml=$?
fi
if test $has_ocaml -eq 1
then
    checkinc "$cc $cflags -I$caml_prefix -I$camlidl_prefix" caml/camlidlruntime.h
    has_ocaml=$?
fi
if test $has_ocaml -eq 1
then
    cc_cmd="$cc $cflags -I$caml_prefix -I$mlgmpidl_prefix";
    if test "x$gmp_prefix" != "x"; then cc_cmd="$cc_cmd  -I$gmp_prefix/include"; fi
    checkinc "$cc_cmd" gmp_caml.h
    has_ocaml=$?
fi

# Java environment

# check Java binaries
if test "x$java_prefix" != "x"; then JAVA_HOME="$java_prefix"; fi
if test "x$JAVA_HOME" != "x"; then PATH=$JAVA_HOME/bin:$PATH; fi
if test $has_java -eq 1; then searchbin "java"; has_java=$?; java="$path"; fi
if test $has_java -eq 1; then searchbin "javac"; has_java=$?; javac="$path"; fi
if test $has_java -eq 1; then searchbin "javah"; has_java=$?; javah="$path"; fi
if test $has_java -eq 1; then searchbin "javadoc"; has_java=$?; javadoc="$path"; fi
if test $has_java -eq 1; then searchbin "jar"; has_java=$?; jar="$path"; fi

# check jni includes
if test $has_java -eq 1
then
    checkinc "$cc $cflags -I$JAVA_HOME/include" jni.h
    if test $? -eq 0; then echo "JNI not found, please set JAVA_HOME"; has_java=0; fi
fi

# Set apron source root
if test $has_apron -eq 1 
then
    if test $has_ocaml -eq 1
    then
       if test "x$apron_srcroot" = "x"; then
           if test $use_opam -eq 1; then
	      apron_srcroot=`ocamlfind query apron`
           else
	      echo "Apron source not found, set APRON_SRCROOT"; exit 1
           fi
       fi
    fi
fi


# GPUPoly environment
if test $has_cuda -eq 1
then
    searchbin "cmake"
    if test $? -eq 1
    then
        echo "Configuring GPUPoly (using CMake)"
        cd gpupoly
        cmake -DCMAKE_INSTALL_PREFIX:PATH=$elina_prefix .
        if test $? -ne 0; then echo "Failed to configure GPUPoly"; has_cuda=0; fi
        cd ..
    else
        echo "GPUPoly requires CMake."
        has_cuda=0
    fi
fi


##############################################
# Custom tests
##############

# Use abolute dynamic library names under OSX when explicitly asked,
# or when the installation prefix does not belong to DYLD_LIBRARY_PATH
# nor DYLD_FALLBACK_LIBRARY_PATH or
# '$(HOME)/lib:/usr/local/lib:/lib:/usr/lib' (the default fallback).
absolute_dylib_install_names=;
if test "x$(uname -s)" = "xDarwin"
then
    has_timing=0
    has_native=0
    if test $force_absolute_dylib_install_names -eq 1
    then
	echo "using absolute dynamic library install names as requested"
	absolute_dylib_install_names=1
    else
	libdir="${elina_prefix}/lib"
	if test "x$DYLD_FALLBACK_LIBRARY_PATH" != "x"
	then
	    fldpath="$DYLD_FALLBACK_LIBRARY_PATH"
	else
	    fldpath="$HOME/lib:/usr/local/lib:/lib:/usr/lib"
	fi
	checkdirinpath "${libdir}" "$DYLD_LIBRARY_PATH" "DYLD_LIBRARY_PATH" || \
	    checkdirinpath "${libdir}" "${fldpath}" "DYLD_FALLBACK_LIBRARY_PATH"
	if test $? -eq 1
	then
	    echo "forcing absolute dynamic library install names"
	    absolute_dylib_install_names=1
	fi
    fi
else
    has_timing=1
    has_native=1
    if test $force_absolute_dylib_install_names -eq 1
    then
	echo "ignoring option \`-absolute-dylibs', only meaningful under OSX";
    fi
fi


##############################################
# log
#####

cat <<EOF

detected configuration:

   optional OCaml support       $has_ocaml
   optional OCamlFind support   $has_ocamlfind
   optional Java support        $has_java
   optional CUDA support        $has_cuda

   installation path            $elina_prefix

EOF

test "x$absolute_dylib_install_names" = "x1" && cat <<EOF
   dynamic libraries shall use absolute install names

EOF

##############################################
# generation
############

if test "$has_ocaml" -eq 0; then has_ocaml=; fi
if test "$has_java" -eq 0; then has_java=; fi
if test "$has_apron" -eq 0; then has_apron=; else has_apron=-DHAS_APRON; fi
if test "$has_vector" -eq 0; then is_vector=; else is_vector=-DVECTOR; fi
if test "$has_timing" -eq 0; then has_timing=; else has_timing=-DTIMING; fi
if test "$has_native" -eq 0; then has_native=; else has_native=-march=native; fi
if test "$has_cuda" -eq 0; then is_cuda=; else is_cuda=-DCUDA; fi
if test "$use_gurobi" -eq 0; then use_gurobi=; fi
if test "$use_fconv" -eq 0; then use_fconv=; fi
if test "$use_opam" -eq 0; then use_opam=; fi


cat > Makefile.config <<EOF
# generated by ./configure

# If defined to non-empty value, compiles the OCaml interface (bytecode)
HAS_OCAML = $has_ocaml

# If defined to non-empty value, compiles the OCaml interface (native code)
HAS_OCAMLOPT = $has_ocaml

# If defined to non-empty value, compiles the Java interface
HAS_JAVA = $has_java

# If defined to HAS_APRON, uses the apron interface
IS_APRON = $has_apron

# if defined to VECTOR, uses SIMD instructions for the Octagon library
IS_VECTOR = $is_vector

# if defined to TIMING, uses the rdtsc timer for measuring clock times
HAS_TIMING = $has_timing

# if defined to NATIVE, uses the -march=native compilation option
HAS_NATIVE = $has_native

# if define to USE_DEEPPOLY, compile DeepPoly
USE_DEEPPOLY = $use_deeppoly


# if define to USE_FCONV, compile Fconv
USE_FCONV = $use_fconv
CDD_PREFIX = $cdd_prefix

ifneq (\$(CDD_PREFIX),)
  ifneq (,\$(findstring /include/cddlib, \$(CDD_PREFIX)))
    CDD_INCLUDE_FLAG = -I\$(CDD_PREFIX)
  else
    CDD_INCLUDE_FLAG = -I\$(CDD_PREFIX)/include
  endif
  ifneq (,\$(findstring /include/cddlib, \$(CDD_PREFIX)))
    CDD_LIB_FLAG = -L\$(CDD_PREFIX)/../../lib
  else
    CDD_LIB_FLAG = -L\$(CDD_PREFIX)/lib
  endif
else
  CDD_INCLUDE_FLAG =
  CDD_LIB_FLAG =
endif

# if defined to VECTOR, compile GPUPoly (a GPU version of DeepPoly)
IS_CUDA = $is_cuda

# if defined, compile with Gurobi library
USE_GUROBI = $use_gurobi

ELINA_PREFIX = $elina_prefix
APRON_PREFIX = $apron_prefix

# Install location of Java .jar files
JAVA_PREFIX = $elina_prefix/lib

# Only if you do not use FINDLIB
MLGMPIDL_PREFIX = $mlgmpidl_prefix

GMP_PREFIX = $gmp_prefix

ifneq (\$(GMP_PREFIX),)
  GMP_INCLUDE_FLAG = -I\$(GMP_PREFIX)/include
  GMP_LIB_FLAG = -L\$(GMP_PREFIX)/lib
else
  GMP_INCLUDE_FLAG =
  GMP_LIB_FLAG =
endif

MPFR_PREFIX = $mpfr_prefix

ifneq (\$(MPFR_PREFIX),)
  MPFR_INCLUDE_FLAG = -I\$(MPFR_PREFIX)/include
  MPFR_LIB_FLAG = -L\$(MPFR_PREFIX)/lib
else
  MPFR_INCLUDE_FLAG =
  MPFR_LIB_FLAG =
endif

# Install location of OCAML
CAML_PREFIX = $caml_prefix

# Install location of CAMLIDL
CAMLIDL_PREFIX = $camlidl_prefix

PERL = $perl

# If defined to non-empty value, assumed to be the right executable,
# use FINDLIB/ocamlfind package system
OCAMLFIND = $ocamlfind

CAMLIDL = $camlidl

OCAMLC = $ocamlc

OCAMLOPT = $ocamlopt

OCAMLMKLIB = $ocamlmklib

INSTALL = $install

INSTALLd = $install -d

# Java launcher
JAVA = $java

# Java compiler
JAVAC = $javac -Xlint:unchecked

# Java header compiler
JAVAH = $javah

# Java documentation generator
JAVADOC = $javadoc

# Java archive tool
JAR = $jar

# Preprocessing directives to find JNI headers
JNIINC = -I$java_home/include/

# C compilation flags
CFLAGS = $cflags

# Architecture specific flags
AFLAGS = -D_GNU_SOURCE -pthread -fno-tree-vectorize -m64 -ffp-contract=off \$(HAS_NATIVE)
DFLAGS = -g  -DNUM_LONGLONGRAT -DNUM_DOUBLE -DTHRESHOLD=0.75 \$(AFLAGS) \$(IS_APRON) \$(IS_VECTOR) \$(HAS_TIMING)


# ocamlc compilation flags
OCAMLFLAGS = -g

# ocamlopt compilation flags
OCAMLOPTFLAGS = -inline 20

# Location of APRON source code
APRON_SRCROOT = $apron_srcroot

USE_OPAM = $use_opam

# OSX only:
ABSOLUTE_DYLIB_INSTALL_NAMES = $absolute_dylib_install_names

ifneq (\$(ABSOLUTE_DYLIB_INSTALL_NAMES),)
  CC_ELINA_DYLIB += -install_name \$(ELINA_PREFIX)/lib/\$@
  CXX_ELINA_DYLIB += -install_name \$(ELINA_PREFIX)/lib/\$@
else
ifneq (\$(USE_OPAM),)
  CC_ELINA_DYLIB += -Wl,-rpath=\$(ELINA_PREFIX)/lib
  CXX_ELINA_DYLIB += -Wl,-rpath=\$(ELINA_PREFIX)/lib
endif
endif


EOF