diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 10 | ||||
| -rw-r--r-- | mppa_k1c/CBuiltins.ml | 10 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 10 | ||||
| -rw-r--r-- | test/monniaux/k1_builtins/test_k1_builtins.c | 8 |
5 files changed, 38 insertions, 5 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 26c6cc02..55138a3f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -80,6 +80,11 @@ Inductive instruction : Type := | Pwfxl (n: int) (src: ireg)
| Pwfxm (n: int) (src: ireg)
| Pldu (dst: ireg) (addr: ireg)
+ | Pawait
+ | Psleep
+ | Pstop
+ | Pbarrier
+ | Pfence
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index bcc2d28f..e09492e9 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -381,6 +381,16 @@ let expand_builtin_inline name args res = let open Asmvliw in else emit (Pwfxm(n, src))) | "__builtin_k1_ldu", [BA(IR addr)], BR(IR res) -> emit (Pldu(res, addr)) + | "__builtin_k1_await", [], _ -> + emit Pawait + | "__builtin_k1_sleep", [], _ -> + emit Psleep + | "__builtin_k1_stop", [], _ -> + emit Pstop + | "__builtin_k1_barrier", [], _ -> + emit Pbarrier + | "__builtin_k1_fence", [], _ -> + emit Pfence (* Byte swaps *) (*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index 0de6d0c7..e4652d77 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -24,8 +24,8 @@ let builtins = { (* The builtin list is inspired from the GCC file builtin_k1.h *) Builtins.functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *) (* BCU Instructions *) - "__builtin_k1_await", (TVoid [], [], false); - "__builtin_k1_barrier", (TVoid [], [], false); + "__builtin_k1_await", (TVoid [], [], false); (* DONE *) + "__builtin_k1_barrier", (TVoid [], [], false); (* DONE *) "__builtin_k1_doze", (TVoid [], [], false); "__builtin_k1_wfxl", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) "__builtin_k1_wfxm", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) @@ -33,8 +33,8 @@ let builtins = { "__builtin_k1_invalitlb", (TVoid [], [], false); "__builtin_k1_probetlb", (TVoid [], [], false); "__builtin_k1_readtlb", (TVoid [], [], false); - "__builtin_k1_sleep", (TVoid [], [], false); - "__builtin_k1_stop", (TVoid [], [], false); + "__builtin_k1_sleep", (TVoid [], [], false); (* DONE *) + "__builtin_k1_stop", (TVoid [], [], false); (* DONE *) "__builtin_k1_syncgroup", (TVoid [], [TInt(IUInt, [])], false); "__builtin_k1_tlbwrite", (TVoid [], [], false); @@ -49,7 +49,7 @@ let builtins = { "__builtin_k1_dinvall", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_dtouchl", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_dzerol", (TVoid [], [TPtr(TVoid [], [])], false); - "__builtin_k1_fence", (TVoid [], [], false); + "__builtin_k1_fence", (TVoid [], [], false); (* DONE *) "__builtin_k1_iinval", (TVoid [], [], false); "__builtin_k1_iinvals", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_itouchl", (TVoid [], [TPtr(TVoid [], [])], false); diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index b2a9e827..c67792e7 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -288,6 +288,16 @@ module Target (*: TARGET*) = fprintf oc " wfxm $s%ld = %a\n" (camlint_of_coqint n) ireg dst | Pldu(dst, addr) -> fprintf oc " ld.u %a = 0[%a]\n" ireg dst ireg addr + | Pawait -> + fprintf oc " await\n" + | Psleep -> + fprintf oc " sleep\n" + | Pstop -> + fprintf oc " stop\n" + | Pbarrier -> + fprintf oc " barrier\n" + | Pfence -> + fprintf oc " fence\n" | 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 261eedc2..db90d4ea 100644 --- a/test/monniaux/k1_builtins/test_k1_builtins.c +++ b/test/monniaux/k1_builtins/test_k1_builtins.c @@ -10,3 +10,11 @@ void test_system_regs(void) { void test_loads(void *addr) { __builtin_k1_ldu(addr); } + +void test_stops(void) { + __builtin_k1_await(); + __builtin_k1_sleep(); + __builtin_k1_stop(); + __builtin_k1_barrier(); + __builtin_k1_fence(); +} |