From e93ef3ef5f0925ce6b99208157a49a99032c1f87 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 11 Apr 2019 11:57:09 +0200 Subject: __builtin_k1_ldu --- mppa_k1c/Asm.v | 6 ++++-- mppa_k1c/Asmexpand.ml | 4 +++- mppa_k1c/CBuiltins.ml | 10 +++++----- mppa_k1c/TargetPrinter.ml | 5 ++++- test/monniaux/k1_builtins/test_k1_builtins.c | 4 ++++ 5 files changed, 20 insertions(+), 9 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 9517099c..26c6cc02 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -72,13 +72,15 @@ Inductive instruction : Type := | Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *) | Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *) | Pjumptable (r: ireg) (labels: list label) - + + (* For builtins *) | Ploopdo (count: ireg) (loopend: label) | Pgetn (n: int) (dst: ireg) | Psetn (n: int) (src: ireg) | Pwfxl (n: int) (src: ireg) | Pwfxm (n: int) (src: ireg) - + | Pldu (dst: ireg) (addr: ireg) + (** Loads **) | Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *) | Plbu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *) diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 1bf99768..bcc2d28f 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -379,7 +379,9 @@ let expand_builtin_inline name args res = let open Asmvliw in (if not_system_register cn then failwith (Printf.sprintf "__builtin_k1_wfxm(n, val): n must be between 0 and %ld, was %ld" last_system_register cn) else emit (Pwfxm(n, src))) - + | "__builtin_k1_ldu", [BA(IR addr)], BR(IR res) -> + emit (Pldu(res, addr)) + (* Byte swaps *) (*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> expand_bswap16 res a1 diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index f9eec191..0de6d0c7 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -27,8 +27,8 @@ let builtins = { "__builtin_k1_await", (TVoid [], [], false); "__builtin_k1_barrier", (TVoid [], [], false); "__builtin_k1_doze", (TVoid [], [], false); - "__builtin_k1_wfxl", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); - "__builtin_k1_wfxm", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); + "__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); "__builtin_k1_invalitlb", (TVoid [], [], false); "__builtin_k1_probetlb", (TVoid [], [], false); @@ -38,8 +38,8 @@ let builtins = { "__builtin_k1_syncgroup", (TVoid [], [TInt(IUInt, [])], false); "__builtin_k1_tlbwrite", (TVoid [], [], false); - "__builtin_k1_get", (TInt(IULongLong, []), [TInt(IInt, [])], false); - "__builtin_k1_set", (TVoid [], [TInt(IInt, []); TInt(IULongLong, [])], false); + "__builtin_k1_get", (TInt(IULongLong, []), [TInt(IInt, [])], false); (* DONE *) + "__builtin_k1_set", (TVoid [], [TInt(IInt, []); TInt(IULongLong, [])], false); (* DONE *) (* LSU Instructions *) (* No ACWS - __int128 *) @@ -55,7 +55,7 @@ let builtins = { "__builtin_k1_itouchl", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_lbsu", (TInt(IChar, []), [TPtr(TVoid [], [])], false); "__builtin_k1_lbzu", (TInt(IUChar, []), [TPtr(TVoid [], [])], false); - "__builtin_k1_ldu", (TInt(IULongLong, []), [TPtr(TVoid [], [])], false); + "__builtin_k1_ldu", (TInt(IULongLong, []), [TPtr(TVoid [], [])], false); (* DONE *) "__builtin_k1_lhsu", (TInt(IShort, []), [TPtr(TVoid [], [])], false); "__builtin_k1_lhzu", (TInt(IUShort, []), [TPtr(TVoid [], [])], false); "__builtin_k1_lwzu", (TInt(IUInt, []), [TPtr(TVoid [], [])], false); diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index af1c5581..b2a9e827 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -275,6 +275,7 @@ module Target (*: TARGET*) = | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) -> fprintf oc " cb.%a %a? %a\n" bcond bt ireg r print_label lbl + (* For builtins *) | Ploopdo (r, lbl) -> fprintf oc " loopdo %a, %a\n" ireg r print_label lbl | Pgetn(n, dst) -> @@ -285,7 +286,9 @@ module Target (*: TARGET*) = fprintf oc " wfxl $s%ld = %a\n" (camlint_of_coqint n) ireg dst | Pwfxm(n, dst) -> 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 + | Pjumptable (idx_reg, tbl) -> let lbl = new_label() in (* jumptables := (lbl, tbl) :: !jumptables; *) diff --git a/test/monniaux/k1_builtins/test_k1_builtins.c b/test/monniaux/k1_builtins/test_k1_builtins.c index 9aa6873b..261eedc2 100644 --- a/test/monniaux/k1_builtins/test_k1_builtins.c +++ b/test/monniaux/k1_builtins/test_k1_builtins.c @@ -6,3 +6,7 @@ void test_system_regs(void) { __builtin_k1_get(K1_SFR_EV4); __builtin_k1_set(K1_SFR_EV4, 0x4000ULL); } + +void test_loads(void *addr) { + __builtin_k1_ldu(addr); +} -- cgit