diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | mppa_k1c/CBuiltins.ml | 10 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | 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); +} |