diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 17 | ||||
| -rw-r--r-- | mppa_k1c/CBuiltins.ml | 1 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 9 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | test/monniaux/k1_builtins/test_k1_builtins.c | 8 |
6 files changed, 35 insertions, 6 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 7c6bd013..9517099c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -76,6 +76,8 @@ Inductive instruction : Type := | 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)
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 2997bc8b..1bf99768 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -345,7 +345,8 @@ let expand_bswap64 d s = assert false (* Handling of compiler-inlined builtins *) let last_system_register = 511l - +let not_system_register cn =cn<0l || cn>last_system_register + let expand_builtin_inline name args res = let open Asmvliw in match name, args, res with (* Synchronization *) @@ -360,14 +361,24 @@ let expand_builtin_inline name args res = let open Asmvliw in emit (Pstsud(res, a1, a2)) | "__builtin_k1_get", [BA_int(n)], BR(IR res) -> let cn = camlint_of_coqint n in - (if cn<0l || cn>last_system_register + (if not_system_register cn then failwith (Printf.sprintf "__builtin_k1_get(n): n must be between 0 and %ld, was %ld" last_system_register cn) else emit (Pgetn(n, res))) | "__builtin_k1_set", [BA_int(n); BA(IR src)], _ -> let cn = camlint_of_coqint n in - (if cn<0l || cn>last_system_register + (if not_system_register cn then failwith (Printf.sprintf "__builtin_k1_set(n, val): n must be between 0 and %ld, was %ld" last_system_register cn) else emit (Psetn(n, src))) + | "__builtin_k1_wfxl", [BA_int(n); BA(IR src)], _ -> + let cn = camlint_of_coqint n in + (if not_system_register cn + then failwith (Printf.sprintf "__builtin_k1_wfxl(n, val): n must be between 0 and %ld, was %ld" last_system_register cn) + else emit (Pwfxl(n, src))) + | "__builtin_k1_wfxm", [BA_int(n); BA(IR src)], _ -> + let cn = camlint_of_coqint n 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))) (* Byte swaps *) (*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index e5cdcd01..f9eec191 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -27,7 +27,6 @@ let builtins = { "__builtin_k1_await", (TVoid [], [], false); "__builtin_k1_barrier", (TVoid [], [], false); "__builtin_k1_doze", (TVoid [], [], false); - (* No __builtin_k1_get - not compatible with the Asm model *) "__builtin_k1_wfxl", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); "__builtin_k1_wfxm", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); "__builtin_k1_invaldtlb", (TVoid [], [], false); diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index f9712428..61f9089f 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -220,8 +220,13 @@ Definition builtin_constraints (ef: external_function) : match ef with | EF_builtin id sg => if string_dec id "__builtin_k1_get" then OK_const :: nil - else if string_dec id "__builtin_k1_set" then OK_const :: OK_default :: nil - else nil + else if string_dec id "__builtin_k1_set" + then OK_const :: OK_default :: nil + else if string_dec id "__builtin_k1_wfxl" + then OK_const :: OK_default :: nil + else if string_dec id "__builtin_k1_wfxm" + then OK_const :: OK_default :: nil + else nil | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index beac8cfe..af1c5581 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -281,6 +281,10 @@ module Target (*: TARGET*) = fprintf oc " get %a = $s%ld\n" ireg dst (camlint_of_coqint n) | Psetn(n, dst) -> fprintf oc " set $s%ld = %a\n" (camlint_of_coqint n) ireg dst + | Pwfxl(n, dst) -> + 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 | 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 new file mode 100644 index 00000000..9aa6873b --- /dev/null +++ b/test/monniaux/k1_builtins/test_k1_builtins.c @@ -0,0 +1,8 @@ +#include <mppa_bare_runtime/k1c/registers.h> + +void test_system_regs(void) { + __builtin_k1_wfxl(K1_SFR_EV4, 0x1000ULL); + __builtin_k1_wfxm(K1_SFR_EV4, 0x2000ULL); + __builtin_k1_get(K1_SFR_EV4); + __builtin_k1_set(K1_SFR_EV4, 0x4000ULL); +} |