diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 55 |
1 files changed, 53 insertions, 2 deletions
@@ -55,6 +55,8 @@ Supported targets: x86_64-macosx (x86 64 bits, MacOS X) rv32-linux (RISC-V 32 bits, Linux) 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) @@ -177,6 +179,8 @@ case "$target" in arch="riscV"; model="32"; endianness="little"; bitsize=32;; rv64-*) 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) @@ -433,6 +437,40 @@ if test "$arch" = "riscV"; then fi # +# K1c Target Configuration +# +if test "$arch" = "mppa_k1c"; 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 K1c backend" + exit 1 + fi + osupper=`echo $os|tr a-z A-Z` + k1base="k1-$os" + casm="k1-elf-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 __K1C_${osupper}__ -std=c99 -E -include ccomp_k1c_fixes.h" + libmath="-lm" + system="linux" +fi + +# # AArch64 (ARMv8 64 bits) Target Configuration # if test "$arch" = "aarch64"; then @@ -800,6 +838,21 @@ RESPONSEFILE="none" EOF 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 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\\ + ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v +EOF +fi + # # Clean up target-dependent files to force their recompilation # @@ -853,6 +906,4 @@ cat <<EOF Coq development will not be installed EOF fi - fi - |