diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 79 |
1 files changed, 76 insertions, 3 deletions
@@ -58,6 +58,9 @@ Supported targets: x86_64-cygwin (x86 64 bits, Cygwin environment under Windows) rv32-linux (RISC-V 32 bits, Linux) rv64-linux (RISC-V 64 bits, Linux) + kvx-mbr (Kalray KV3, bare runtime) + kvx-elf (Kalray KV3, ELF) + kvx-cos (Kalray KV3, ClusterOS) aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux) aarch64-macos (AArch64, i.e. Apple silicon, MacOS) manual (edit configuration file by hand) @@ -190,6 +193,8 @@ case "$target" in arch="riscV"; model="32"; endianness="little"; bitsize=32;; rv64-*) arch="riscV"; model="64"; endianness="little"; bitsize=64;; + kvx-*) + arch="kvx"; model="64"; endianness="little"; bitsize=64;; aarch64-*|arm64-*) arch="aarch64"; model="default"; endianness="little"; bitsize=64;; manual) @@ -402,6 +407,38 @@ if test "$arch" = "riscV"; then fi # +# KVX Target Configuration +# +if test "$arch" = "kvx"; then + #model_options="-march=rv64imafd -mabi=lp64d" + # FIXME - maybe later add it for NodeOS & cie + #model_options=-m64 + model_options= + abi="standard" + if test "$target" = "mbr"; + then os="mbr"; + elif test "$target" = "cos"; + then os="cos"; + elif test "$target" = "elf"; + then os="elf"; + else + echo "Unknown KVX backend" + exit 1 + fi + osupper=`echo $os|tr a-z A-Z` + k1base="kvx-$os" + casm="$k1base-as" + casm_options="$model_options" + cc="$k1base-gcc $model_options" + clinker="$k1base-gcc" + clinker_options="$model_options -L$libdir -Wl,-rpath=$libdir" + cprepro="$k1base-gcc" + cprepro_options="$model_options -D __KVX_${osupper}__ -std=c99 -E -include ccomp_kvx_fixes.h" + libmath="-lm" + system="linux" +fi + +# # AArch64 (ARMv8 64 bits) Target Configuration # if test "$arch" = "aarch64"; then @@ -523,9 +560,9 @@ esac echo "Testing OCaml... " | tr -d '\n' ocaml_ver=`ocamlc -version 2>/dev/null` case "$ocaml_ver" in - 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*) + 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*|4.05.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.05 or later." + echo "Error: CompCert requires OCaml version 4.06 or later." missingtools=true;; 4.*) echo "version $ocaml_ver -- good!";; @@ -650,6 +687,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers INSTALL_COQDEV=$install_coqdev LIBMATH=$libmath MODEL=$model +OS=${os:-unspecified} SYSTEM=$system RESPONSEFILE=$responsefile LIBRARY_FLOCQ=$library_Flocq @@ -759,6 +797,42 @@ LIBRARY_MENHIRLIB=local # external EOF fi +if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling +cat >> Makefile.config <<EOF +ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v IterList.v \\ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asm.v Asmblockprops.v\\ + ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ + Asmblockdeps.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 + # TODO: UPDATE THIS + # DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v +EXTRA_EXTRACTION= Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 Asmgen.Asmgen_expand.storeptr +EOF +fi + +if [ "$arch" = "kvx" ]; then +cat >> Makefile.config <<EOF +ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib +EXECUTE=kvx-cluster --syscall=libstd_scalls.so -- +CFLAGS= -D __KVX_COS__ +SIMU=kvx-cluster -- +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.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 ExtFloats.v\\ + AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v +EOF +fi + +if [ "$arch" = "riscV" ] ; then +cat >> Makefile.config <<EOF +EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq +BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v +EOF +fi + # # Generate Merlin and CoqProject files to simplify development # @@ -845,5 +919,4 @@ cat <<EOF Coq development will not be installed EOF fi - fi |