Commit b4a08d08 authored by David Monniaux's avatar David Monniaux
Browse files

k1c -> kvx changes

parent 490a6cae
......@@ -47,9 +47,9 @@
/riscV/ConstpropOp.v
/riscV/SelectOp.v
/riscV/SelectLong.v
/mppa_k1c/ConstpropOp.v
/mppa_k1c/SelectOp.v
/mppa_k1c/SelectLong.v
/kvx/ConstpropOp.v
/kvx/SelectOp.v
/kvx/SelectLong.v
/aarch64/ConstpropOp.v
/aarch64/SelectOp.v
/aarch64/SelectLong.v
......@@ -79,11 +79,11 @@
/doc/html/
# MacOS metadata
.DS_Store
runtime/mppa_k1c/i64_sdiv.s
runtime/mppa_k1c/i64_smod.s
runtime/mppa_k1c/i64_udiv.s
runtime/mppa_k1c/i64_udivmod.s
runtime/mppa_k1c/i64_umod.s
runtime/kvx/i64_sdiv.s
runtime/kvx/i64_smod.s
runtime/kvx/i64_udiv.s
runtime/kvx/i64_udivmod.s
runtime/kvx/i64_umod.s
# Test generated data
/test/clightgen/*.v
# Coq caches
......
......@@ -14,7 +14,7 @@ check-admitted:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -35,7 +35,7 @@ build_x86_64:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -58,7 +58,7 @@ build_ia32:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -81,7 +81,7 @@ build_aarch64:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -104,7 +104,7 @@ build_arm:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -128,7 +128,7 @@ build_armhf:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -149,7 +149,7 @@ build_ppc:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -170,7 +170,7 @@ build_ppc64:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -193,7 +193,7 @@ build_rv64:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......@@ -214,13 +214,13 @@ build_rv32:
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
- when: manual
build_k1c:
build_kvx:
stage: build
image: "coqorg/coq"
before_script:
......@@ -228,12 +228,12 @@ build_k1c:
- eval `opam config env`
- opam install -y menhir
script:
- ./config_k1c.sh -no-runtime-lib
- ./config_kvx.sh -no-runtime-lib
- make -j "$NJOBS"
rules:
- if: '$CI_COMMIT_BRANCH == "mppa-work"'
when: always
- if: '$CI_COMMIT_BRANCH == "mppa-k1c"'
- if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
when: always
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
......
......@@ -36,7 +36,7 @@ opam install coq menhir
## Compilation
Pre-compilation configure replace the placeholder with your desired platform
(for Kalray Coolidge it is `k1c-cos`)
(for Kalray Coolidge it is `kvx-cos`)
```
./configure <platform>
```
......@@ -57,7 +57,7 @@ ccomp -O3 test.c -o test.bin
```
## Changing platform
If you decide to change the platform, for instance from k1c-cos to k1c-mbr, you
If you decide to change the platform, for instance from kvx-cos to kvx-mbr, you
should change the `compcert.ini` file with the respective tools and then run
```
make install
......
......@@ -43,7 +43,7 @@ cparser/pre_parser_messages.ml:
DIRS=extraction \
lib common $(ARCH) backend cfrontend cparser driver \
exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml
exportclight debug kvx/unittest kvx/abstractbb/Impure/ocaml
INCLUDES=$(patsubst %,-I %, $(DIRS))
......
......@@ -22,13 +22,13 @@ Depending on the platform, this logging system is or is not thread-safe and is o
| AArch64 | Yes | Yes | No |
| ARM | Yes | No | No |
| IA32 | Yes | No | No |
| K1c | Yes | Yes | No |
| KVX | Yes | Yes | No |
| PowerPC | No | | |
| PowerPC 64 | No | | |
| Risc-V 32 | No | | |
| Risc-V 64 | No | | |
| x86-64 | Yes | Yes | Yes |
For recompiling the program using profiling information, use `-fprofile-use= compcert_profiling.dat -ftracelinearize` (substitute the appropriate filename for `compcert_profiling.dat` if needed). Experiments show performance improvement on K1c, not on other platforms.
For recompiling the program using profiling information, use `-fprofile-use= compcert_profiling.dat -ftracelinearize` (substitute the appropriate filename for `compcert_profiling.dat` if needed). Experiments show performance improvement on KVX, not on other platforms.
The same options (except for `-fprofile-use=` and `-fprofile-arcs`) should be used to compile the logging and optimized versions of the program: only functions that are exactly the same in the intermediate representation will be optimized according to profiling information.
......@@ -4,8 +4,8 @@ The verified C compiler ported to Kalray.
## Features
This delivery contains (in addition to features from CompCert master branch):
- A fully functional port of CompCert to Coolidge k1c VLIW core
- Postpass scheduling optimization, only for k1c. Activated by default, it can be deactivated with the compiler flag `-fno-postpass`
- A fully functional port of CompCert to Coolidge kvx VLIW core
- Postpass scheduling optimization, only for kvx. Activated by default, it can be deactivated with the compiler flag `-fno-postpass`
- Some experimental features that are work in progress:
- Slightly better subexpression eliminations, called CSE2 and CSE3. Both go through loops and feature a small alias analysis.
- `-fduplicate 0` to activate static branch prediction information. The branch prediction is basic, it annotates each `Icond` node by an `option bool`. A `Some true` annotation indicates we predict the branch will be taken. `Some false` indicates the fallthrough case is predicted. `None` indicates we could not predict anything, and are not sure about which control will be preferred.
......
......@@ -79,7 +79,7 @@ let fast_cmove ty =
| "riscV", _ -> false
| "x86", _ ->
(match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
| "mppa_k1c", _ -> true
| "kvx", _ -> true
| a, m -> failwith (Printf.sprintf "fast_cmove: unknown arch %s %s" a m)
(* The if-conversion heuristic depend on the
......
exec ./config_simple.sh k1c-cos "$@"
exec ./config_simple.sh kvx-cos "$@"
......@@ -55,8 +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)
kvx-mbr (Kalray KVX, bare runtime)
kvx-cos (Kalray KVX, ClusterOS)
aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux)
manual (edit configuration file by hand)
......@@ -179,8 +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;;
kvx-*)
arch="kvx"; model="64"; endianness="little"; bitsize=64;;
aarch64-*|arm64-*)
arch="aarch64"; model="default"; endianness="little"; bitsize=64;;
manual)
......@@ -437,9 +437,9 @@ if test "$arch" = "riscV"; then
fi
#
# K1c Target Configuration
# KVX Target Configuration
#
if test "$arch" = "mppa_k1c"; then
if test "$arch" = "kvx"; then
#model_options="-march=rv64imafd -mabi=lp64d"
# FIXME - maybe later add it for NodeOS & cie
#model_options=-m64
......@@ -452,12 +452,12 @@ if test "$arch" = "mppa_k1c"; then
elif test "$target" = "elf";
then os="elf";
else
echo "Unknown K1c backend"
echo "Unknown KVX backend"
exit 1
fi
osupper=`echo $os|tr a-z A-Z`
k1base="k1-$os"
casm="k1-elf-as"
k1base="kvx-$os"
casm="kvx-elf-as"
casm_options="$model_options"
cc="$k1base-gcc $model_options"
clinker="$k1base-gcc"
......@@ -465,7 +465,7 @@ if test "$arch" = "mppa_k1c"; then
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"
cprepro_options="$model_options -D __KVX_${osupper}__ -std=c99 -E -include ccomp_kvx_fixes.h"
libmath="-lm"
system="linux"
fi
......@@ -838,12 +838,12 @@ RESPONSEFILE="none"
EOF
fi
if [ "$arch" = "mppa_k1c" ]; then
if [ "$arch" = "kvx" ]; 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 --
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\\
......
......@@ -238,8 +238,8 @@ let rv64 =
struct_passing_style = SP_ref_callee; (* Wrong *)
struct_return_style = SR_ref } (* to check *)
let mppa_k1c =
{ name = "k1c";
let kvx =
{ name = "kvx";
char_signed = true;
wchar_signed = true;
sizeof_ptr = 8;
......
......@@ -87,7 +87,7 @@ val arm_littleendian : t
val arm_bigendian : t
val rv32 : t
val rv64 : t
val mppa_k1c : t
val kvx : t
val aarch64 : t
val gcc_extensions : t -> t
......
......@@ -25,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }
<font color=gray><H1 align="center">The CompCert verified compiler</H1>
<H2 align="center">Commented Coq development</H2>
<H3 align="center">Version 3.7, 2020-03-31</H3></font>
<H3 align="center">PATCHED for the Kalray MPPA-K1C VLIW CORE</H3>
<H3 align="center">PATCHED for the Kalray MPPA-KVX VLIW CORE</H3>
<H2>Introduction</H2>
......@@ -54,11 +54,11 @@ inequations by fixpoint iteration.
<LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph.
</UL></font>
<H4>The <tt>abstractbb</tt> library, introduced for MPPA-K1C</H4>
<H4>The <tt>abstractbb</tt> library, introduced for MPPA-KVX</H4>
<UL>
<LI> <A HREF="html/compcert.mppa_k1c.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks.
<LI> <A HREF="html/compcert.mppa_k1c.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
<LI> <A HREF="html/compcert.mppa_k1c.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.mppa_k1c.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing.
<LI> <A HREF="html/compcert.kvx.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks.
<LI> <A HREF="html/compcert.kvx.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
<LI> <A HREF="html/compcert.kvx.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.kvx.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing.
</UL>
<font color=gray>
......@@ -77,7 +77,7 @@ See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory rep
<LI> <A HREF="html/compcert.common.Smallstep.html">Smallstep</A>: tools for small-step semantics.
<LI> <A HREF="html/compcert.common.Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
<LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics.
<LI> <A HREF="html/compcert.mppa_k1c.Op.html"><I>Op</I></A>: operators, addressing modes and their
<LI> <A HREF="html/compcert.kvx.Op.html"><I>Op</I></A>: operators, addressing modes and their
semantics.
<LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints.
</UL>
......@@ -108,21 +108,21 @@ pseudo-registers).
code, control-flow graph of basic blocks, finitely many physical registers, infinitely
many stack slots). <BR>
See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of
locations) and <A HREF="html/compcert.mppa_k1c.Machregs.html"><I>Machregs</I></A> (description of processor registers).
locations) and <A HREF="html/compcert.kvx.Machregs.html"><I>Machregs</I></A> (description of processor registers).
<LI> <A HREF="html/compcert.backend.Linear.html">Linear</A>: like LTL, but the CFG is
replaced by a linear list of instructions with explicit branches and labels.
<LI> <A HREF="html/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete
view of the activation record.
</UL>
</font>
<H4>Languages introduced for MPPA-K1C</H4>
<H4>Languages introduced for MPPA-KVX</H4>
<UL>
<LI> <A HREF="html/compcert.mppa_k1c.lib.Machblock.html">Machblock</A>: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step).
This IR is generic over the processor, even if currently, only used for MPPA_K1C.
<LI> <A HREF="html/compcert.mppa_k1c.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for Mppa_K1c VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles.
<LI> <A HREF="html/compcert.mppa_k1c.Asmblock.html"><I>Asmblock</I></A>: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks.
<LI> <A HREF="html/compcert.kvx.lib.Machblock.html">Machblock</A>: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step).
This IR is generic over the processor, even if currently, only used for MPPA_KVX.
<LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for Mppa_KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles.
<LI> <A HREF="html/compcert.kvx.Asmblock.html"><I>Asmblock</I></A>: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks.
This IR is an intermediate step between Machblock and Asmvliw.
<LI> <A HREF="html/compcert.mppa_k1c.Asm.html"><I>Asm</I></A>: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of <I>Asmvliw</I> for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax).
<LI> <A HREF="html/compcert.kvx.Asm.html"><I>Asm</I></A>: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of <I>Asmvliw</I> for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax).
</UL>
<font color=gray><H3>Compiler passes</H3></font>
......@@ -169,13 +169,13 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
<TD>Recognition of operators<br>and addressing modes</TD>
<TD>Cminor to CminorSel</TD>
<TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br>
<A HREF="html/compcert.mppa_k1c.SelectOp.html"><I>SelectOp</I></A><br>
<A HREF="html/compcert.mppa_k1c.SelectLong.html"><I>SelectLong</I></A><br>
<A HREF="html/compcert.kvx.SelectOp.html"><I>SelectOp</I></A><br>
<A HREF="html/compcert.kvx.SelectLong.html"><I>SelectLong</I></A><br>
<A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br>
<A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD>
<TD><A HREF="html/compcert.backend.Selectionproof.html">Selectionproof</A><br>
<A HREF="html/compcert.mppa_k1c.SelectOpproof.html"><I>SelectOpproof</I></A><br>
<A HREF="html/compcert.mppa_k1c.SelectLongproof.html"><I>SelectLongproof</I></A><br>
<A HREF="html/compcert.kvx.SelectOpproof.html"><I>SelectOpproof</I></A><br>
<A HREF="html/compcert.kvx.SelectLongproof.html"><I>SelectLongproof</I></A><br>
<A HREF="html/compcert.backend.SelectDivproof.html">SelectDivproof</A><br>
<A HREF="html/compcert.backend.SplitLongproof.html">SplitLongproof</A></TD>
</TR>
......@@ -214,18 +214,18 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
<TD>Constant propagation</TD>
<TD>RTL to RTL</TD>
<TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br>
<A HREF="html/compcert.mppa_k1c.ConstpropOp.html"><I>ConstpropOp</I></A></TD>
<A HREF="html/compcert.kvx.ConstpropOp.html"><I>ConstpropOp</I></A></TD>
<TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br>
<A HREF="html/compcert.mppa_k1c.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
<A HREF="html/compcert.kvx.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
</TR>
<TR valign="top">
<TD>Common subexpression elimination</TD>
<TD>RTL to RTL</TD>
<TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR>
<A HREF="html/compcert.mppa_k1c.CombineOp.html"><I>CombineOp</I></A></TD>
<A HREF="html/compcert.kvx.CombineOp.html"><I>CombineOp</I></A></TD>
<TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
<A HREF="html/compcert.mppa_k1c.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
<A HREF="html/compcert.kvx.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
</TR>
<TR valign="top">
......@@ -282,44 +282,44 @@ This IR is generic over the processor, even if currently, only used for MPPA_K1C
<TD>Linear to Mach</TD>
<TD><A HREF="html/compcert.backend.Stacking.html">Stacking</A><BR>
<A HREF="html/compcert.backend.Bounds.html">Bounds</A><BR>
<A HREF="html/compcert.mppa_k1c.Stacklayout.html"><I>Stacklayout</I></A></TD>
<A HREF="html/compcert.kvx.Stacklayout.html"><I>Stacklayout</I></A></TD>
<TD><A HREF="html/compcert.backend.Stackingproof.html">Stackingproof</A><br>
<A HREF="html/compcert.common.Separation.html">Separation</A></TD>
</TR>
</TABLE>
<H4>Compilation passes introduced for MPPA-K1C</H4>
<H4>Compilation passes introduced for MPPA-KVX</H4>
<TABLE cellpadding="5%">
<TR valign="top">
<TD>Reconstruction of basic-blocks at Mach level</TD>
<TD>Mach to Machblock</TD>
<TD><A HREF="html/compcert.mppa_k1c.lib.Machblockgen.html">Machblockgen</A></TD>
<TD><A HREF="html/compcert.mppa_k1c.lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR>
<A HREF="html/compcert.mppa_k1c.lib.Machblockgenproof.html">Machblockgenproof</A></TD>
<TD><A HREF="html/compcert.kvx.lib.Machblockgen.html">Machblockgen</A></TD>
<TD><A HREF="html/compcert.kvx.lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR>
<A HREF="html/compcert.kvx.lib.Machblockgenproof.html">Machblockgenproof</A></TD>
</TR>
<TR valign="top">
<TD>Emission of purely sequential assembly code</TD>
<TD>Machblock to Asmblock</TD>
<TD><A HREF="html/compcert.mppa_k1c.Asmblockgen.html"><I>Asmblockgen</I></A></TD>
<TD><A HREF="html/compcert.mppa_k1c.lib.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR>
<A HREF="html/compcert.mppa_k1c.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR>
<A HREF="html/compcert.mppa_k1c.Asmblockgenproof.html"><I>Asmblockgenproof</I></A></TD>
<TD><A HREF="html/compcert.kvx.Asmblockgen.html"><I>Asmblockgen</I></A></TD>
<TD><A HREF="html/compcert.kvx.lib.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR>
<A HREF="html/compcert.kvx.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR>
<A HREF="html/compcert.kvx.Asmblockgenproof.html"><I>Asmblockgenproof</I></A></TD>
</TR>
<TR valign="top">
<TD>Bundling (and basic-block scheduling)</TD>
<TD>Asmblock to Asmvliw</TD>
<TD><A HREF="html/compcert.mppa_k1c.PostpassScheduling.html"><I>PostpassScheduling</I></A> using<BR>
<A HREF="html/compcert.mppa_k1c.Asmblockdeps.html"><I>Asmblockdeps</I></A> and the <tt>abstractbb</tt> library</TD>
<TD><A HREF="html/compcert.mppa_k1c.PostpassSchedulingproof.html"><I>PostpassSchedulingproof</I></A></TD>
<TD><A HREF="html/compcert.kvx.PostpassScheduling.html"><I>PostpassScheduling</I></A> using<BR>
<A HREF="html/compcert.kvx.Asmblockdeps.html"><I>Asmblockdeps</I></A> and the <tt>abstractbb</tt> library</TD>
<TD><A HREF="html/compcert.kvx.PostpassSchedulingproof.html"><I>PostpassSchedulingproof</I></A></TD>
</TR>
<TR valign="top">
<TD>Flattening bundles (only a bureaucratic operation)</TD>
<TD>Asmvliw to Asm</TD>
<TD><A HREF="html/compcert.mppa_k1c.Asmgen.html"><I>Asmgen</I></A></TD>
<TD><A HREF="html/compcert.mppa_k1c.Asmgenproof.html"><I>Asmgenproof</I></A></TD>
<TD><A HREF="html/compcert.kvx.Asmgen.html"><I>Asmgen</I></A></TD>
<TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A></TD>
</TR>
</TABLE>
......@@ -341,10 +341,10 @@ CSE, and dead code elimination.
<LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>.
<LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
See also: <A HREF="html/compcert.mppa_k1c.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
See also: <A HREF="html/compcert.kvx.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
<LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
See also: <A HREF="html/compcert.mppa_k1c.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
See also: <A HREF="html/compcert.kvx.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
</UL>
<H3>Type systems</H3>
......
......@@ -15,7 +15,7 @@
let prepro_options = ref ([]: string list)
let linker_options = ref ([]: string list)
let assembler_options = ref ([]: string list)
let option_flongdouble = ref (Configuration.arch = "mppa_k1c")
let option_flongdouble = ref (Configuration.arch = "kvx")
let option_fstruct_passing = ref false
let option_fbitfields = ref false
let option_fvararg_calls = ref true
......
......@@ -123,7 +123,7 @@ let get_bool_config key =
let arch =
match get_config_string "arch" with
| "powerpc"|"arm"|"x86"|"riscV"|"mppa_k1c"|"aarch64" as a -> a
| "powerpc"|"arm"|"x86"|"riscV"|"kvx"|"aarch64" as a -> a
| v -> bad_config "arch" [v]
let model = get_config_string "model"
let abi = get_config_string "abi"
......
......@@ -116,7 +116,7 @@ let init () =
| "riscV" -> if Configuration.model = "64"
then Machine.rv64
else Machine.rv32
| "mppa_k1c" -> Machine.mppa_k1c
| "kvx" -> Machine.kvx
| "aarch64" -> Machine.aarch64
| _ -> assert false
end;
......
......@@ -13,7 +13,7 @@
(* *)
(* *************************************************************)
(** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *)
(** Architecture-dependent parameters for MPPA KVX. Mostly copied from the Risc-V backend *)
Require Import ZArith List.
Require Import Binary Bits.
......
......@@ -13,7 +13,7 @@
(* *)
(* *************************************************************)
(** * Abstract syntax for K1c textual assembly language.
(** * Abstract syntax for KVX textual assembly language.
Each emittable instruction is defined here. ';;' is also defined as an instruction.
The goal of this representation is to stay compatible with the rest of the generic backend of CompCert
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment