diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 98 |
1 files changed, 62 insertions, 36 deletions
@@ -57,10 +57,12 @@ Supported targets: rv64-linux (RISC-V 64 bits, Linux) k1c-mbr (Kalray K1c, bare runtime) k1c-cos (Kalray K1c, ClusterOS) + aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux) manual (edit configuration file by hand) For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-". For x86 targets, the "x86_64-" prefix can also be written "amd64-". +For AArch64 targets, the "aarch64-" prefix can also be written "arm64-". For PowerPC targets, the "ppc-" prefix can be refined into: ppc64- PowerPC 64 bits @@ -179,6 +181,8 @@ case "$target" in arch="riscV"; model="64"; endianness="little"; bitsize=64;; k1c-*) arch="mppa_k1c"; model="64"; endianness="little"; bitsize=64;; + aarch64-*|arm64-*) + arch="aarch64"; model="default"; endianness="little"; bitsize=64;; manual) ;; "") @@ -453,8 +457,8 @@ if test "$arch" = "mppa_k1c"; then fi osupper=`echo $os|tr a-z A-Z` k1base="k1-$os" - casm="$k1base-gcc" - casm_options="$model_options -c" + casm="k1-elf-as" + casm_options="$model_options" cc="$k1base-gcc $model_options" clinker="$k1base-gcc" bindir="$HOME/.usr/bin" @@ -466,6 +470,29 @@ if test "$arch" = "mppa_k1c"; then system="linux" fi +# +# AArch64 (ARMv8 64 bits) Target Configuration +# +if test "$arch" = "aarch64"; then + case "$target" in + linux) + abi="standard" + casm="${toolprefix}gcc" + casm_options="-c" + cc="${toolprefix}gcc" + clinker="${toolprefix}gcc" + clinker_options="" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -U__GNUC__ -E" + libmath="-lm" + system="linux";; + *) + echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2 + echo "$usage" 1>&2 + exit 2;; + esac +fi + # # Finalize Target Configuration @@ -541,43 +568,38 @@ 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.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1" + echo "Error: CompCert requires one of the following Coq versions: 8.11.1, 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.9.0 is installed." + echo "Error: make sure Coq version 8.9.1 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.*) + 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.02 or later." + echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; - 4.02.*|4.03.*|4.04.*) - echo "version $ocaml_ver -- good!" - echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations" - echo "have a hardware bug that can be triggered by this version of OCaml." - echo "To avoid this risk, it is recommended to use OCaml 4.05 or later.";; - 4.0*) + 4.*) echo "version $ocaml_ver -- good!";; ?.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.02 or later." + echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure OCaml version 4.02 or later is installed." + echo "Error: make sure OCaml version 4.05 or later is installed." missingtools=true;; esac @@ -591,23 +613,23 @@ else ocaml_opt_comp=false fi -MENHIR_REQUIRED=20161201 -MENHIR_NEW_API=20180530 -MENHIR_MAX=20181113 -menhir_flags='' +MENHIR_REQUIRED=20190626 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 -a "$menhir_ver" -le $MENHIR_MAX; then + if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" - menhir_includes="-I `menhir --suggest-menhirLib`" - if test "$menhir_ver" -ge $MENHIR_NEW_API; then - menhir_flags="--coq-lib-path compcert.cparser.MenhirLib" + menhir_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') + if test -z "$menhir_dir"; then + echo "Error: cannot determine the location of the Menhir API library." + echo "This can be due to an incorrect Menhir package." + echo "Consider using the OPAM package for Menhir." + missingtools=true fi else echo "version $menhir_ver -- UNSUPPORTED" - echo "Error: CompCert requires a version of Menhir between $MENHIR_REQUIRED and $MENHIR_MAX, included." + echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." missingtools=true fi;; *) @@ -671,7 +693,8 @@ echo "-R lib compcert.lib \ -R driver compcert.driver \ -R flocq compcert.flocq \ -R exportclight compcert.exportclight \ --R cparser compcert.cparser" > _CoqProject +-R cparser compcert.cparser \ +-R MenhirLib compcert.MenhirLib" > _CoqProject case $arch in x86) echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject @@ -692,8 +715,7 @@ MANDIR=$sharedir/man SHAREDIR=$sharedir COQDEVDIR=$coqdevdir OCAML_OPT_COMP=$ocaml_opt_comp -MENHIR_INCLUDES=$menhir_includes -MENHIR_FLAGS=$menhir_flags +MENHIR_DIR=$menhir_dir COMPFLAGS=-bin-annot EOF @@ -728,6 +750,8 @@ cat >> Makefile.config <<'EOF' # ARCH=powerpc # ARCH=arm # ARCH=x86 +# ARCH=riscV +# ARCH=aarch6 ARCH= # Hardware variant @@ -741,23 +765,24 @@ ARCH= # MODEL=armv7m # for ARM # MODEL=32sse2 # for x86 in 32-bit mode # MODEL=64 # for x86 in 64-bit mode +# MODEL=default # for others 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=standard # for others ABI= # Target bit width -# BITSIZE=64 # for x86 in 64-bit mode +# BITSIZE=64 # for x86 in 64-bit mode, RiscV in 64-bit mode, AArch64 # BITSIZE=32 # otherwise BITSIZE= # Target endianness # ENDIANNESS=big # for ARM or PowerPC -# ENDIANNESS=little # for ARM or x86 +# ENDIANNESS=little # for ARM or x86 or RiscV or AArch64 ENDIANNESS= # Target operating system and development environment @@ -766,7 +791,7 @@ ENDIANNESS= # SYSTEM=linux # SYSTEM=diab # -# Possible choices for ARM: +# Possible choices for ARM, AArch64, RiscV: # SYSTEM=linux # # Possible choices for x86: @@ -816,11 +841,14 @@ fi if [ "$arch" = "mppa_k1c" ]; then cat >> Makefile.config <<EOF ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure +EXECUTE=k1-cluster --syscall=libstd_scalls.so -- +CFLAGS= -D __K1C_COS__ +SIMU=k1-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ - Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v\\ - AbstractBasicBlocksDef.v DepTreeTheory.v ImpDep.v Parallelizability.v\\ + Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ + AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v EOF fi @@ -878,6 +906,4 @@ cat <<EOF Coq development will not be installed EOF fi - fi - |