WIP - Trying to add builtins support. They are not detected for now :(

4 files changed, 34 insertions, 38 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 008e6c67..df394ecf 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -166,6 +166,9 @@ Inductive ex_instruction : Type :=
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
               -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
+  (* Instructions not generated by Asmgen (most likely result of AsmExpand) *)
+  | Pclzll (rd rs: ireg)
+  | Pstsud (rd rs1 rs2: ireg)
 .
 
 (** The pseudo-instructions are the following:
@@ -1053,28 +1056,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 
   (** The following instructions and directives are not generated directly by Asmgen,
       so we do not model them. *)
-(*| Pfence
-
-  | Pfmvxs _ _
-  | Pfmvxd _ _
-
-  | Pfmins _ _ _
-  | Pfmaxs _ _ _
-  | Pfsqrts _ _
-  | Pfmadds _ _ _ _
-  | Pfmsubs _ _ _ _
-  | Pfnmadds _ _ _ _
-  | Pfnmsubs _ _ _ _
-
-  | Pfmind _ _ _
-  | Pfmaxd _ _ _
-  | Pfsqrtd _ _
-  | Pfmaddd _ _ _ _
-  | Pfmsubd _ _ _ _
-  | Pfnmaddd _ _ _ _
-  | Pfnmsubd _ _ _ _
+  | Pclzll _ _
+  | Pstsud _ _ _
     => Stuck
-*)end.
+  end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers to
   the RISC-V view.  Note that no LTL register maps to [X31].  This
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index f0a9404c..282fa476 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -565,11 +565,11 @@ let expand_instruction instr =
   | Pj_s(symb, sg) ->
       fixup_call sg; emit instr
 
-  | Pbuiltin (ef,args,res) ->
+*)| PExpand Pbuiltin (ef,args,res) ->
      begin match ef with
      | EF_builtin (name,sg) ->
         expand_builtin_inline (camlstring_of_coqstring name) args res
-     | EF_vload chunk ->
+   (*| EF_vload chunk ->
         expand_builtin_vload chunk args res
      | EF_vstore chunk ->
         expand_builtin_vstore chunk args
@@ -579,10 +579,10 @@ let expand_instruction instr =
         expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
      | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
         emit instr
-     | _ ->
+   *)| _ ->
         assert false
      end
-*)| _ ->
+  | _ ->
      emit instr
 
 (* NOTE: Dwarf register maps for RV32G are not yet specified
diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml
index 0c981d11..b478f9b3 100644
--- a/mppa_k1c/CBuiltins.ml
+++ b/mppa_k1c/CBuiltins.ml
@@ -22,34 +22,39 @@ let builtins = {
     "__builtin_va_list", TPtr(TVoid [], [])
   ];
   Builtins.functions = [
+    "__builtin_clzll",
+      (TInt(IInt, []), 
+      [TInt(IULongLong, [])], false);
+    "__builtin_k1_stsud",
+      (TInt(IULongLong, []), 
+      [TInt(IULongLong, []); TInt(IULongLong, [])], false);
     (* Synchronization *)
-    "__builtin_fence",
+(*  "__builtin_fence",
       (TVoid [], [], false);
     (* Integer arithmetic *)
     "__builtin_bswap64",
-      (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
+      (TInt(IULongLong, []), 
+       [TInt(IULongLong, [])], false);
     (* Float arithmetic *)
     "__builtin_fmadd",
       (TFloat(FDouble, []),
-       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
-       false);
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmsub",
       (TFloat(FDouble, []),
-       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
-       false);
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fnmadd",
       (TFloat(FDouble, []),
-       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
-       false);
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fnmsub",
       (TFloat(FDouble, []),
-       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
-       false);
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmax",
-      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+      (TFloat(FDouble, []),
+       [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmin",
-      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
-  ]
+      (TFloat(FDouble, []),
+       [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+*)]
 }
 
 let va_list_type = TPtr(TVoid [], [])  (* to check! *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 8e3cce5a..ad06500e 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -222,6 +222,12 @@ module Target : TARGET =
               assert false
          end
 
+      (* Pseudo-instructions not generated by Asmgen *)
+      | Pclzll(rd, rs) ->
+         fprintf oc "	clzll	%a = %a\n;;\n" ireg rd ireg rs
+      | Pstsud(rd, rs1, rs2) ->
+         fprintf oc "	stsud	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+
       let print_cf_instruction oc = function
       | Pget (rd, rs) ->
          fprintf oc "	get	%a = %a\n;;\n" ireg rd preg rs