configure

#!/bin/sh

#######################################################################
#                                                                     #
#              The Compcert verified compiler                         #
#                                                                     #
#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
#                                                                     #
#  Copyright Institut National de Recherche en Informatique et en     #
#  Automatique.  All rights reserved.  This file is distributed       #
#  under the terms of the INRIA Non-Commercial License Agreement.     #
#                                                                     #
#######################################################################

prefix='/usr/local'
bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
toolprefix=''
target=''
has_runtime_lib=true
has_standard_headers=true
clightgen=false
responsefile="gnu"
merlin=false
coqproject=false

usage='Usage: ./configure [options] target

Supported targets:
  ppc-eabi             (PowerPC, EABI with GNU/Unix tools)
  ppc-eabi-diab        (PowerPC, EABI with Diab tools)
  ppc-linux            (PowerPC, Linux)
  arm-eabi             (ARM, EABI, little endian)
  arm-linux            (ARM, EABI, little endian)
  arm-eabihf           (ARM, EABI using hardware FP registers, little endian)
  arm-hardfloat        (ARM, EABI using hardware FP registers, little endian)
  armeb-eabi           (ARM, EABI, big endian)
  armeb-linux          (ARM, EABI, big endian)
  armeb-eabihf         (ARM, EABI using hardware FP registers, big endian)
  armeb-hardfloat      (ARM, EABI using hardware FP registers, big endian)
  x86_32-linux         (x86 32 bits, Linux)
  x86_32-bsd           (x86 32 bits, BSD)
  x86_32-macosx        (x86 32 bits, MacOS X)
  x86_32-cygwin        (x86 32 bits, Cygwin environment under Windows)
  x86_64-linux         (x86 64 bits, Linux)
  x86_64-macosx        (x86 64 bits, MacOS X)
  manual               (edit configuration file by hand)

For x86 targets, the "x86_32-" prefix can also be written "ia32-".

For PowerPC targets, the "ppc-" prefix can be refined into:
  ppc64-               PowerPC 64 bits
  e5500-               Freescale e5500 core (PowerPC 64 bit, EREF extensions)

For ARM targets, the "arm-" or "armeb-" prefix can be refined into:
  armv6-               ARMv6   + VFPv2
  armv7a-              ARMv7-A + VFPv3-d16   (default for arm-)
  armv7r-              ARMv7-R + VFPv3-d16
  armv7m-              ARMv7-M + VFPv3-d16

  armebv6-             ARMv6   + VFPv2
  armebv7a-            ARMv7-A + VFPv3-d16   (default for armeb-)
  armebv7r-            ARMv7-R + VFPv3-d16
  armebv7m-            ARMv7-M + VFPv3-d16

Options:
  -prefix <dir>        Install in <dir>/bin and <dir>/lib/compcert
  -bindir <dir>        Install binaries in <dir>
  -libdir <dir>        Install libraries in <dir>
  -toolprefix <pref>   Prefix names of tools ("gcc", etc) with <pref>
  -no-runtime-lib      Do not compile nor install the runtime support library
  -no-standard-headers Do not install nor use the standard .h headers
  -clightgen           Also compile the clightgen tool
  -merlin              Generate .merlin file
  -coqproject          Generate a _CoqProject file for Proof General
'


#
# Parse Command-Line Arguments
#
while : ; do
  case "$1" in
    "")
        break;;
    -prefix|--prefix)
        prefix="$2"; shift;;
    -bindir|--bindir)
        bindir="$2"; shift;;
    -libdir|--libdir)
        libdir="$2"; shift;;
    -toolprefix|--toolprefix)
        toolprefix="$2"; shift;;
    -no-runtime-lib)
        has_runtime_lib=false;;
    -no-standard-headers)
        has_standard_headers=false;;
    -clightgen)
        clightgen=true;;
    -merlin)
        merlin=true;;
    -coqproject)
        coqproject=true;;
    *)
        if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
        target="$1";;
  esac
  shift
done


#
# Extract Architecture, Model and Default Endianness
#
case "$target" in
  arm-*|armv7a-*)
      arch="arm"; model="armv7a"; endianness="little"; bitsize=32;;
  armv6-*)
      arch="arm"; model="armv6"; endianness="little"; bitsize=32;;
  armv7r-*)
      arch="arm"; model="armv7r"; endianness="little"; bitsize=32;;
  armv7m-*)
      arch="arm"; model="armv7m"; endianness="little"; bitsize=32;;
  armeb-*|armebv7a-*)
      arch="arm"; model="armv7a"; endianness="big"; bitsize=32;;
  armebv6-*)
      arch="arm"; model="armv6"; endianness="big"; bitsize=32;;
  armebv7r-*)
      arch="arm"; model="armv7r"; endianness="big"; bitsize=32;;
  armebv7m-*)
      arch="arm"; model="armv7m"; endianness="big"; bitsize=32;;
  x86_32-*|ia32-*)
      arch="x86"; model="32sse2"; endianness="little"; bitsize=32;;
  x86_64-*)
      arch="x86"; model="64"; endianness="little"; bitsize=64;;
  powerpc-*|ppc-*)
      arch="powerpc"; model="ppc32"; endianness="big"; bitsize=32;;
  powerpc64-*|ppc64-*)
      arch="powerpc"; model="ppc64"; endianness="big"; bitsize=32;;
  e5500-*)
      arch="powerpc"; model="e5500"; endianness="big"; bitsize=32;;
  manual)
      ;;
  "")
      echo "Error: no target architecture specified." 1>&2
      echo "$usage" 1>&2
      exit 2
      ;;
  *)
      echo "Error: unknown target architecture: '$target'." 1>&2
      echo "$usage" 1>&2
      exit 2
      ;;
esac

target=${target#[a-zA-Z0-9]*-}


# Per-target configuration
asm_supports_cfi=""
casm_options=""
casmruntime=""
clinker_options=""
cprepro_options=""
struct_passing=""
struct_return=""


#
# ARM Target Configuration
#
if test "$arch" = "arm"; then

  case "$target" in
    eabi|linux)
        abi="eabi"
        ;;
    eabihf|hf|hardfloat)
        abi="hardfloat"
        ;;
    *)
        echo "Error: invalid eabi/system '$target' for architecture ARM." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac

  casm="${toolprefix}gcc"
  casm_options="-c"
  cc="${toolprefix}gcc"
  clinker="${toolprefix}gcc"
  cprepro="${toolprefix}gcc"
  cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
  libmath="-lm"
  struct_passing="ints"
  struct_return="int1-4"
  system="linux"
fi


#
# PowerPC Target Configuration
#
if test "$arch" = "powerpc"; then

  case "$target" in
    eabi|eabi-diab|linux)
        ;;
    *)
        echo "Error: invalid eabi/system '$target' for architecture PowerPC." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac

  case "$target" in
    linux)
        struct_return="ref"
        ;;
    *)
        struct_return="int1-8"
        ;;
  esac

  case "$target" in
    eabi-diab)
        abi="eabi"
        asm_supports_cfi=false
        casm="${toolprefix}das"
        casm_options="-Xalign-value"
        cc="${toolprefix}dcc"
        clinker="${toolprefix}dcc"
        cprepro="${toolprefix}dcc"
        cprepro_options="-E -D__GNUC__"
        libmath="-lm"
        struct_passing="ref-caller"
        system="diab"
        responsefile="diab"
        ;;
    *)
        abi="eabi"
        casm="${toolprefix}gcc"
        casm_options="-c"
        casmruntime="${toolprefix}gcc -c -Wa,-mregnames"
        cc="${toolprefix}gcc"
        clinker="${toolprefix}gcc"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -U__GNUC__ -E"
        libmath="-lm"
        struct_passing="ref-caller"
        system="linux"
        ;;
  esac
fi


#
# x86 (32 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "32"; then

  case "$target" in
    bsd)
        abi="standard"
        casm="${toolprefix}gcc"
        casm_options="-m32 -c"
        cc="${toolprefix}gcc -m32"
        clinker="${toolprefix}gcc"
        clinker_options="-m32"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
        libmath="-lm"
        struct_passing="ints"
        struct_return="int1248"    # to check!
        system="bsd"
        ;;
    cygwin)
        abi="standard"
        casm="${toolprefix}gcc"
        casm_options="-m32 -c"
        cc="${toolprefix}gcc -m32"
        clinker="${toolprefix}gcc"
        clinker_options="-m32"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
        libmath="-lm"
        struct_passing="ints"
        struct_return="ref"
        system="cygwin"
        ;;
    linux)
        abi="standard"
        casm="${toolprefix}gcc"
        casm_options="-m32 -c"
        cc="${toolprefix}gcc -m32"
        clinker="${toolprefix}gcc"
        clinker_options="-m32"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
        libmath="-lm"
        struct_passing="ints"
        struct_return="ref"
        system="linux"
        ;;
    macosx)
        # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11
        kernel_major=`uname -r | cut -d "." -f 1`

        abi="macosx"
        casm="${toolprefix}gcc"
        casm_options="-arch i386 -c"
        cc="${toolprefix}gcc -arch i386"
        clinker="${toolprefix}gcc"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E"
        libmath=""
        struct_passing="ints"
        struct_return="int1248"
        system="macosx"

        if [[ $kernel_major -gt 11 ]]; then
          # OSX >= 10.8
          clinker_options="-arch i386 -Wl,-no_pie"
        else
          # OSX <= 10.7
          clinker_options="-arch i386"
        fi
        ;;
    *)
        echo "Error: invalid eabi/system '$target' for architecture IA32/X86_32." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac
fi

#
# IA32 (64 bits) Target Configuration
#
if test "$arch" = "x86" -a "$bitsize" = "64"; then

  case "$target" in
    linux)
        abi="standard"
        casm="${toolprefix}gcc"
        casm_options="-m64 -c"
        cc="${toolprefix}gcc -m64"
        clinker="${toolprefix}gcc"
        clinker_options="-m64"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
        libmath="-lm"
        struct_passing="ref-callee"   # wrong!
        struct_return="ref"           # to check!
        system="linux"
        ;;
    macosx)
        # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11
        kernel_major=`uname -r | cut -d "." -f 1`

        abi="macosx"
        casm="${toolprefix}gcc"
        casm_options="-arch x86_64 -c"
        cc="${toolprefix}gcc -arch x86_64"
        clinker="${toolprefix}gcc"
        cprepro="${toolprefix}gcc"
        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E"
        libmath=""
        struct_passing="ref-callee"   # wrong!
        struct_return="ref"           # to check!
        system="macosx"
        ;;
    *)
        echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac
fi

#
# Finalize Target Configuration
#
if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi


#
# Test Assembler Support for CFI Directives
#
if test "$target" != "manual" && test -z "$asm_supports_cfi"; then
  echo "Testing assembler support for CFI directives... " | tr -d '\n'
  f=/tmp/compcert-configure-$$.s
  rm -f $f
  cat >> $f <<EOF
testfun:
  .file 1 "testfun.c"
  .loc 1 1
  .cfi_startproc
  .cfi_adjust_cfa_offset 16
  .cfi_endproc
EOF
  if $casm $casm_options -o /dev/null $f 2>/dev/null
  then echo "yes"; asm_supports_cfi=true
  else echo "no";  asm_supports_cfi=false
  fi
  rm -f $f
fi


#
# Test Availability of Required Tools
#
missingtools=false

echo "Testing Coq... " | tr -d '\n'
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
  8.6)
        echo "version $coq_ver -- good!";;
  ?.*)
        echo "version $coq_ver -- UNSUPPORTED"
        echo "Error: CompCert requires Coq version 8.6."
        missingtools=true;;
  *)
        echo "NOT FOUND"
        echo "Error: make sure Coq version 8.6 is installed."
        missingtools=true;;
esac

echo "Testing OCaml... " | tr -d '\n'
ocaml_ver=`ocamlopt -version 2>/dev/null`
case "$ocaml_ver" in
  4.00.*|4.01.*)
        echo "version $ocaml_ver -- UNSUPPORTED"
        echo "Error: CompCert requires OCaml version 4.02 or later."
        missingtools=true;;
  4.0*)
        echo "version $ocaml_ver -- good!";;
  ?.*)
        echo "version $ocaml_ver -- UNSUPPORTED"
        echo "Error: CompCert requires OCaml version 4.02 or later."
        missingtools=true;;
  *)
        echo "NOT FOUND"
        echo "Error: make sure OCaml version 4.02 or later is installed."
        missingtools=true;;
esac

echo "Testing OCaml .opt compilers... " | tr -d '\n'
ocaml_opt_ver=`ocamlopt.opt -version 2>/dev/null`
if test "$ocaml_opt_ver" = "$ocaml_ver"; then
  echo "yes"
  ocaml_opt_comp=true
else
  echo "no, will do without"
  ocaml_opt_comp=false
fi

MENHIR_REQUIRED=20161201
echo "Testing Menhir... " | tr -d '\n'
menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
case "$menhir_ver" in
  20[0-9][0-9][0-9][0-9][0-9][0-9])
      if test "$menhir_ver" -ge $MENHIR_REQUIRED; then
          echo "version $menhir_ver -- good!"
          menhir_includes="-I `menhir --suggest-menhirLib`"
        else
          echo "version $menhir_ver -- UNSUPPORTED"
          echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later."
          missingtools=true
        fi;;
  *)
        echo "NOT FOUND"
        echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed."
        missingtools=true;;
esac

echo "Testing GNU make... " | tr -d '\n'
make=''
for mk in make gmake gnumake; do
  make_ver=`$mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p'`
  case "$make_ver" in
    3.8*|3.9*|[4-9].*)
        echo "version $make_ver (command '$mk') -- good!"
        make="$mk"
        break;;
  esac
done
if test -z "$make"; then
  echo "NOT FOUND"
  echo "Error: make sure GNU Make version 3.80 or later is installed."
  missingtools=true
fi

if $missingtools; then
  echo "One or several required tools are missing or too old.  Aborting."
  exit 2
fi

if $merlin; then
    cat > .merlin <<EOF
S lib
S common
S $arch
S backend
S cfrontend
S driver
S debug
S exportclight
S cparser
S extraction

B lib
B common
B $arch
B backend
B cfrontend
B driver
B debug
B exportclight
B cparser
B extraction

EOF
fi

if $coqproject; then
    echo "-R lib compcert.lib \
-R common compcert.common \
-R ${arch} compcert.${arch} \
-R backend compcert.backend \
-R cfrontend compcert.cfrontend \
-R driver compcert.driver \
-R flocq compcert.flocq \
-R exportclight compcert.exportclight \
-R cparser compcert.cparser" > _CoqProject
    case $arch in
        x86)
            echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject
            ;;
    esac
fi

#
# Generate Makefile.config
#
sharedir="$(dirname "$bindir")"/share

rm -f Makefile.config
cat > Makefile.config <<EOF
PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
MANDIR=$sharedir/man
SHAREDIR=$sharedir
OCAML_OPT_COMP=$ocaml_opt_comp
MENHIR_INCLUDES=$menhir_includes
EOF
if $merlin; then
    cat >> Makefile.config <<EOF
COMPFLAGS=-bin-annot
EOF
fi

if test "$target" != "manual"; then
cat >> Makefile.config <<EOF
ABI=$abi
ARCH=$arch
ASM_SUPPORTS_CFI=$asm_supports_cfi
BITSIZE=$bitsize
CASM=$casm
CASM_OPTIONS=$casm_options
CASMRUNTIME=$casmruntime
CC=$cc
CLIGHTGEN=$clightgen
CLINKER=$clinker
CLINKER_OPTIONS=$clinker_options
CPREPRO=$cprepro
CPREPRO_OPTIONS=$cprepro_options
ENDIANNESS=$endianness
HAS_RUNTIME_LIB=$has_runtime_lib
HAS_STANDARD_HEADERS=$has_standard_headers
LIBMATH=$libmath
MODEL=$model
STRUCT_PASSING=$struct_passing
STRUCT_RETURN=$struct_return
SYSTEM=$system
RESPONSEFILE=$responsefile
EOF
else
cat >> Makefile.config <<'EOF'

# Target architecture
# ARCH=powerpc
# ARCH=arm
# ARCH=x86
ARCH=

# Hardware variant
# MODEL=ppc32       # for plain PowerPC
# MODEL=ppc64       # for PowerPC with 64-bit instructions
# MODEL=e5500       # for Freescale e5500 PowerPC variant
# MODEL=armv6       # for ARM
# MODEL=armv7a      # for ARM
# MODEL=armv7r      # for ARM
# MODEL=armv7m      # for ARM
# MODEL=32sse2      # for x86 in 32-bit mode
# MODEL=64          # for x86 in 64-bit mode
MODEL=

# Target ABI
# ABI=eabi          # for PowerPC / Linux and other SVR4 or EABI platforms
# ABI=eabi          # for ARM
# ABI=hardfloat     # for ARM
# ABI=standard      # for x86
ABI=

# Target bit width
# BITSIZE=64        # for x86 in 64-bit mode
# BITSIZE=32        # otherwise
BITSIZE=

# Target endianness
# ENDIANNESS=big     # for ARM or PowerPC
# ENDIANNESS=little  # for ARM or x86
ENDIANNESS=

# Default calling conventions for passing structs and unions by value
# See options -fstruct-passing=<style> and -fstruct-return=<style>
# in the CompCert user's manual
#
STRUCT_PASSING=ref_callee
# STRUCT_PASSING=ref_caller
# STRUCT_PASSING=ints
#
STRUCT_RETURN=ref
# STRUCT_RETURN=int1248
# STRUCT_RETURN=int1-4
# STRUCT_RETURN=int1-8

# Target operating system and development environment
#
# Possible choices for PowerPC:
# SYSTEM=linux
# SYSTEM=diab
#
# Possible choices for ARM:
# SYSTEM=linux
#
# Possible choices for x86:
# SYSTEM=linux
# SYSTEM=bsd
# SYSTEM=macosx
# SYSTEM=cygwin
SYSTEM=

# C compiler for compiling runtime library files and some tests
CC=gcc

# Preprocessor for .c files
CPREPRO=gcc -U__GNUC__ -E

# Assembler for assembling .s files
CASM=gcc -c

# Assembler for assembling runtime library files
CASMRUNTIME=gcc -c

# Linker
CLINKER=gcc

# Math library. Set to empty under MacOS X
LIBMATH=-lm

# Turn on/off the installation and use of the runtime support library
HAS_RUNTIME_LIB=true

# Turn on/off the installation and use of the standard header files
HAS_STANDARD_HEADERS=true

# Whether the assembler $(CASM) supports .cfi debug directives
ASM_SUPPORTS_CFI=false
#ASM_SUPPORTS_CFI=true

# Turn on/off compilation of clightgen
CLIGHTGEN=false

# Whether the other tools support responsefiles in gnu syntax
RESPONSEFILE="none"

EOF
fi

#
# Clean up target-dependent files to force their recompilation
#
rm -f .depend $arch/Archi.vo ${arch}_${bitsize}/Archi.vo runtime/*.o

#
# Summarize Configuration
#
if test "$target" = "manual"; then
cat <<EOF

Please finish the configuration by editing file ./Makefile.config.

EOF
else

bindirexp=`echo "$bindir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
libdirexp=`echo "$libdir" | sed -e "s|\\\$(PREFIX)|$prefix|"`

cat <<EOF

CompCert configuration:
    Target architecture........... $arch
    Hardware model................ $model
    Application binary interface.. $abi
    Endianness.................... $endianness
    Composite passing conventions. arguments: $struct_passing, return values: $struct_return
    OS and development env........ $system
    C compiler.................... $cc
    C preprocessor................ $cprepro
    Assembler..................... $casm
    Assembler supports CFI........ $asm_supports_cfi
    Assembler for runtime lib..... $casmruntime
    Linker........................ $clinker
    Math library.................. $libmath
    Binaries installed in......... $bindirexp
    Runtime library provided...... $has_runtime_lib
    Library files installed in.... $libdirexp
    Standard headers provided..... $has_standard_headers
    Standard headers installed in. $libdirexp/include
    Build command to use.......... $make

EOF
fi