diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 13:11:13 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 13:11:13 +0200 |
| commit | 9ff90aa440d195076a30fe4d8a055d050d84f726 (patch) | |
| tree | 415d9145ff9414b47370ac86c7c221fda694d628 | |
| parent | 71bfa128316019b0199db87acdf31deb9f9e7405 (diff) | |
| download | compcert-kvx-9ff90aa440d195076a30fe4d8a055d050d84f726.tar.gz compcert-kvx-9ff90aa440d195076a30fe4d8a055d050d84f726.zip | |
data cache builtins
| -rw-r--r-- | mppa_k1c/Asm.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 8 | ||||
| -rw-r--r-- | mppa_k1c/CBuiltins.ml | 10 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 8 | ||||
| -rw-r--r-- | test/monniaux/k1_builtins/test_k1_builtins.c | 3 |
5 files changed, 28 insertions, 5 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 55138a3f..bb78eda1 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -85,6 +85,10 @@ Inductive instruction : Type := | Pstop
| Pbarrier
| Pfence
+ | Pdinval
+ | Pdinvall (addr: ireg)
+ | Pdtouchl (addr: ireg)
+ | Pdzerol (addr: ireg)
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index e09492e9..97a85881 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -391,6 +391,14 @@ let expand_builtin_inline name args res = let open Asmvliw in emit Pbarrier | "__builtin_k1_fence", [], _ -> emit Pfence + | "__builtin_k1_dinval", [], _ -> + emit Pdinval + | "__builtin_k1_dinvall", [BA(IR addr)], _ -> + emit (Pdinvall addr) + | "__builtin_k1_dtouchl", [BA(IR addr)], _ -> + emit (Pdtouchl addr) + | "__builtin_k1_dzerol", [BA(IR addr)], _ -> + emit (Pdzerol addr) (* Byte swaps *) (*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index e4652d77..56412d71 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -26,7 +26,7 @@ let builtins = { (* BCU Instructions *) "__builtin_k1_await", (TVoid [], [], false); (* DONE *) "__builtin_k1_barrier", (TVoid [], [], false); (* DONE *) - "__builtin_k1_doze", (TVoid [], [], false); + "__builtin_k1_doze", (TVoid [], [], false); (* opcode not supported in assembly, not in documentation *) "__builtin_k1_wfxl", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) "__builtin_k1_wfxm", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) "__builtin_k1_invaldtlb", (TVoid [], [], false); @@ -45,10 +45,10 @@ let builtins = { (* No ACWS - __int128 *) "__builtin_k1_afda", (TInt(IULongLong, []), [TPtr(TVoid [], []); TInt(ILongLong, [])], false); "__builtin_k1_aldc", (TInt(IULongLong, []), [TPtr(TVoid [], [])], false); - "__builtin_k1_dinval", (TVoid [], [], false); - "__builtin_k1_dinvall", (TVoid [], [TPtr(TVoid [], [])], false); - "__builtin_k1_dtouchl", (TVoid [], [TPtr(TVoid [], [])], false); - "__builtin_k1_dzerol", (TVoid [], [TPtr(TVoid [], [])], false); + "__builtin_k1_dinval", (TVoid [], [], false); (* DONE *) + "__builtin_k1_dinvall", (TVoid [], [TPtr(TVoid [], [])], false); (* DONE *) + "__builtin_k1_dtouchl", (TVoid [], [TPtr(TVoid [], [])], false); (* DONE *) + "__builtin_k1_dzerol", (TVoid [], [TPtr(TVoid [], [])], false); (* DONE *) "__builtin_k1_fence", (TVoid [], [], false); (* DONE *) "__builtin_k1_iinval", (TVoid [], [], false); "__builtin_k1_iinvals", (TVoid [], [TPtr(TVoid [], [])], false); diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index c67792e7..fc4d6ba6 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -298,6 +298,14 @@ module Target (*: TARGET*) = fprintf oc " barrier\n" | Pfence -> fprintf oc " fence\n" + | Pdinval -> + fprintf oc " dinval\n" + | Pdinvall addr -> + fprintf oc " dinvall 0[%a]\n" ireg addr + | Pdtouchl addr -> + fprintf oc " dtouchl 0[%a]\n" ireg addr + | Pdzerol addr -> + fprintf oc " dzerol 0[%a]\n" ireg addr | Pjumptable (idx_reg, tbl) -> let lbl = new_label() in diff --git a/test/monniaux/k1_builtins/test_k1_builtins.c b/test/monniaux/k1_builtins/test_k1_builtins.c index db90d4ea..e9ee6727 100644 --- a/test/monniaux/k1_builtins/test_k1_builtins.c +++ b/test/monniaux/k1_builtins/test_k1_builtins.c @@ -9,6 +9,9 @@ void test_system_regs(void) { void test_loads(void *addr) { __builtin_k1_ldu(addr); + __builtin_k1_dinvall(addr); + __builtin_k1_dtouchl(addr); + __builtin_k1_dzerol(addr); } void test_stops(void) { |