https://github.com/eth-srl/ELINA
Tip revision: 9c2b0f640dafb3759e4093f964aedd0a25a241ce authored by Gagandeep Singh on 08 April 2020, 14:07:30 UTC
Update opt_pk_resize.c
Update opt_pk_resize.c
Tip revision: 9c2b0f6
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
-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
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
PPL_PREFIX where to find tye PPL library
JAVA_HOME where to find Java
EOF
exit
}
##############################################
# parse arguments
#################
elina_prefix=/usr/local
apron_prefix=/usr/local
has_ocaml=0
has_ocamlfind=0
has_java=0
use_opam=0
has_apron=0
has_vector=0
has_cuda=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;;
-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-cuda|--use-cuda)
has_cuda=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"
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"
# 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
##############################################
# 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
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
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
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_cuda" -eq 0; then is_cuda=; else is_cuda=-DCUDA; 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 VECTOR, compile GPUPoly (the GPU version of DeepPoly)
IS_CUDA = $is_cuda
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 -march=native -ffp-contract=off
DFLAGS = -g -DNUM_LONGLONGRAT -DNUM_DOUBLE -DTHRESHOLD=0.75 -DTIMING \$(AFLAGS) \$(IS_APRON) \$(IS_VECTOR)
# 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