diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 75 |
1 files changed, 74 insertions, 1 deletions
@@ -57,6 +57,8 @@ 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 KVX, bare runtime) + kvx-cos (Kalray KVX, 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) @@ -189,6 +191,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) @@ -401,6 +405,40 @@ 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" + bindir="$HOME/.usr/bin" + libdir="$HOME/.usr/lib" + 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 @@ -758,6 +796,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 OptionMonad.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 # @@ -844,5 +918,4 @@ cat <<EOF Coq development will not be installed EOF fi - fi |