wfxl / wfxm

5 files changed, 27 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