Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32.

3 files changed, 253 insertions, 2 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index b67c3cc5..d136bf9b 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,7 +212,30 @@ Inductive instruction: Type :=
   | Pallocframe(sz: Z)(ofs_ra ofs_link: int)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
   | Pbuiltin(ef: external_function)(args: list preg)(res: list preg)
-  | Pannot(ef: external_function)(args: list (annot_arg preg)).
+  | Pannot(ef: external_function)(args: list (annot_arg preg))
+  | Padcl_ir (n: int) (r: ireg)
+  | Padcl_rr (r1: ireg) (r2: ireg)
+  | Paddl (r1: ireg) (r2: ireg)
+  | Pbsfl (r1: ireg) (r2: ireg)
+  | Pbslr (r1: ireg) (r2: ireg)
+  | Pbswap (r: ireg)
+  | Pfmadd132 (r1: freg) (r2: freg) (r3: freg)
+  | Pfmadd213 (r1: freg) (r2: freg) (r3: freg)
+  | Pfmadd231 (r1: freg) (r2: freg) (r3: freg)
+  | Pfmsub132 (r1: freg) (r2: freg) (r3: freg)
+  | Pfmsub213 (r1: freg) (r2: freg) (r3: freg)
+  | Pfmsub231 (r1: freg) (r2: freg) (r3: freg)
+  | Pfnmadd132 (r1: freg) (r2: freg) (r3: freg)
+  | Pfnmadd213 (r1: freg) (r2: freg) (r3: freg)
+  | Pfnmadd231 (r1: freg) (r2: freg) (r3: freg)
+  | Pfnmsub132 (r1: freg) (r2: freg) (r3: freg)
+  | Pfnmsub213 (r1: freg) (r2: freg) (r3: freg)
+  | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg)
+  | Pmaxsd (r1: freg) (r2: freg)
+  | Pminsd (r1: freg) (r2: freg)
+  | Prolw_8 (r: ireg)
+  | Psbbl (r1: ireg) (r2: ireg)
+  | Psqrtsd (r1: freg) (r2: freg).
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -748,7 +771,32 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pbuiltin ef args res =>
       Stuck                             (**r treated specially below *)
   | Pannot ef args =>
-      Stuck                             (**r treated specially below *)
+    Stuck                             (**r treated specially below *)
+  (** The following instructions and directives are not generated directly by Asmgen,
+      so we do not model them. *)
+  | Padcl_ir _ _
+  | Padcl_rr _ _
+  | Paddl _ _
+  | Pbswap _
+  | Pbsfl _ _
+  | Pbslr _ _
+  | Pfmadd132 _ _ _
+  | Pfmadd213 _ _ _
+  | Pfmadd231 _ _ _
+  | Pfmsub132 _ _ _
+  | Pfmsub213 _ _ _
+  | Pfmsub231 _ _ _
+  | Pfnmadd132 _ _ _
+  | Pfnmadd213 _ _ _
+  | Pfnmadd231 _ _ _
+  | Pfnmsub132 _ _ _
+  | Pfnmsub213 _ _ _
+  | Pfnmsub231 _ _ _
+  | Pmaxsd _ _
+  | Pminsd _ _
+  | Prolw_8 _
+  | Psbbl _ _
+  | Psqrtsd _ _ => Stuck 
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 9a458c37..e93de125 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -14,5 +14,162 @@
    of the IA32 assembly code.  Currently not done, this expansion
    is performed on the fly in PrintAsm. *)
 
+open Asm
+open Asmexpandaux
+open AST
+open Camlcoq
+
+(* Useful constants and helper functions *)
+
+let _0 = Integers.Int.zero
+
+(* Handling of compiler-inlined builtins *)
+
+let emit_builtin_inline oc name args res =
+  match name, args, res with
+  (* Integer arithmetic *)
+  | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] ->
+     if a1 <> res then
+       emit (Pmov_rr (res,a1));
+     emit (Pbswap res)
+  | "__builtin_bswap16", [IR a1], [IR res] ->
+     if a1 <> res then
+       emit (Pmov_rr (res,a1));
+     emit (Prolw_8 res)
+  | "__builtin_clz", [IR a1], [IR res] ->
+     emit (Pbslr (a1,res));
+     emit (Pxor_ri(res,coqint_of_camlint 31l))
+  | "__builtin_ctz", [IR a1], [IR res] ->
+     emit (Pbsfl (a1,res))
+  (* Float arithmetic *)
+  | "__builtin_fabs", [FR a1], [FR res] ->
+     if a1 <> res then
+       emit (Pmovsd_ff (a1,res));
+     emit (Pabsd res) (* This ensures that need_masks is set to true *)
+  | "__builtin_fsqrt", [FR a1], [FR res] ->
+     emit (Psqrtsd (a1,res))
+  | "__builtin_fmax", [FR a1; FR a2], [FR res] ->
+     if res = a1 then
+       emit (Pmaxsd (a2,res))
+     else if res = a2 then
+       emit (Pmaxsd (a1,res))
+     else begin
+	 emit (Pmovsd_ff (a1,res));
+	 emit (Pmaxsd (a2,res))
+       end
+  | "__builtin_fmin", [FR a1; FR a2], [FR res] ->
+     if res = a1 then
+       emit (Pminsd (a2,res))
+     else if res = a2 then
+       emit (Pminsd (a1,res))
+     else begin
+	 emit (Pmovsd_ff (a1,res));
+	 emit (Pminsd (a2,res))
+       end
+  | "__builtin_fmadd",  [FR a1; FR a2; FR a3], [FR res] ->
+     if res = a1 then
+       emit (Pfmadd132 (a2,a3,res))
+     else if res = a2 then
+       emit (Pfmadd213 (a2,a3,res))
+     else if res = a3 then
+       emit (Pfmadd231 (a2,a3,res))
+     else begin
+	 emit (Pmovsd_ff (a2,res));
+	 emit (Pfmadd231 (a1,a2,res))
+       end
+  |"__builtin_fmsub",  [FR a1; FR a2; FR a3], [FR res] ->
+     if res = a1 then
+       emit (Pfmsub132 (a2,a3,res))
+     else if res = a2 then
+       emit (Pfmsub213 (a2,a3,res))
+     else if res = a3 then
+       emit (Pfmsub231 (a2,a3,res))
+     else begin
+	 emit (Pmovsd_ff (a2,res));
+	 emit (Pfmsub231 (a1,a2,res))
+       end
+  | "__builtin_fnmadd",  [FR a1; FR a2; FR a3], [FR res] ->
+     if res = a1 then
+       emit (Pfnmadd132 (a2,a3,res))
+     else if res = a2 then
+       emit (Pfnmadd213 (a2,a3,res))
+     else if res = a3 then
+       emit (Pfnmadd231 (a2,a3,res))
+     else begin
+	 emit (Pmovsd_ff (a2,res));
+	 emit (Pfnmadd231 (a1,a2,res))
+       end
+  |"__builtin_fnmsub",  [FR a1; FR a2; FR a3], [FR res] ->
+     if res = a1 then
+       emit (Pfnmsub132 (a2,a3,res))
+     else if res = a2 then
+       emit (Pfnmsub213 (a2,a3,res))
+     else if res = a3 then
+       emit (Pfnmsub231 (a2,a3,res))
+     else begin
+	 emit (Pmovsd_ff (a2,res));
+	 emit (Pfnmsub231 (a1,a2,res))
+       end
+  (* 64-bit integer arithmetic *)
+  | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
+     assert (ah = EDX && al = EAX && rh = EDX && rl = EAX);
+     emit (Pneg EAX);
+     emit (Padcl_ir (_0,EDX));
+     emit (Pneg EDX)
+  | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+     assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
+     emit (Paddl (EBX,EAX));
+     emit (Padcl_rr (ECX,EDX))
+  | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+     assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
+     emit (Psub_rr (EBX,EAX));
+     emit (Psbbl (ECX,EDX))
+  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+     assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
+     emit (Pmul_r EDX)
+  (* Memory accesses *)
+ (* | "__builtin_read16_reversed", [IR a1], [IR res] ->
+     fprintf oc "	movzwl	0(%a), %a\n" ireg a1 ireg res;
+     fprintf oc "	rolw	$8, %a\n" ireg16 res
+  | "__builtin_read32_reversed", [IR a1], [IR res] ->
+     fprintf oc "	movl	0(%a), %a\n" ireg a1 ireg res;
+     fprintf oc "	bswap	%a\n" ireg res
+  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
+     let tmp = if a1 = ECX then EDX else ECX in
+     if a2 <> tmp then
+       emit (Pmov_rr (a2,tmp));
+     fprintf oc "	xchg	%a, %a\n" ireg8 tmp high_ireg8 tmp;
+     fprintf oc "	movw	%a, 0(%a)\n" ireg16 tmp ireg a1
+  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
+     let tmp = if a1 = ECX then EDX else ECX in
+     if a2 <> tmp then
+       emit (Pmov_rr (a2,tmp));
+     emit (Pbswap res);
+     fprintf oc "	movl	%a, 0(%a)\n" ireg tmp ireg a1
+  (* Synchronization *)
+  | "__builtin_membar", [], _ ->
+     ()
+  (* Vararg stuff *)
+  | "__builtin_va_start", [IR a], _ ->
+     print_builtin_va_start oc a
+		       (* Catch-all *)  *)
+  | _ ->
+     invalid_arg ("unrecognized builtin " ^ name)
+       
+let expand_instruction instr =
+  match instr with
+  | _ -> emit instr
+       
 let expand_program p = p
 
+let expand_function fn =
+  set_current_function fn;
+  List.iter expand_instruction fn.fn_code;
+  get_current_function ()
+
+let expand_fundef = function
+  | Internal f -> Internal (expand_function f)
+  | External ef -> External ef
+
+let expand_program (p: Asm.program) : Asm.program =
+  AST.transform_program expand_fundef p
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index a53a8fbd..a7aa9e90 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -841,6 +841,52 @@ module Target(System: SYSTEM):TARGET =
             fprintf oc "	ret\n"
           end
       (** Pseudo-instructions *)
+      | Padcl_ir (n,res) ->
+	 fprintf oc "  	adcl	$%ld, %a\n" (camlint_of_coqint n) ireg res;
+      | Padcl_rr (a1,res) ->
+	 fprintf oc "  	adcl	%a, %a\n" ireg a1 ireg res;
+      | Paddl (a1,res) ->
+	 fprintf oc "	addl	%a, %a\n" ireg a1 ireg res;
+      | Pbsfl (a1,res) ->
+	 fprintf oc "	bsfl	%a, %a\n" ireg a1 ireg res
+      | Pbslr (a1,res) ->
+	 fprintf oc "	bsrl	%a, %a\n" ireg a1 ireg res;
+      | Pbswap res ->
+	 fprintf oc "	bswap	%a\n" ireg res
+      | Pfmadd132 (a1,a2,res) ->
+	 fprintf oc "	vfmadd132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmadd213 (a1,a2,res) ->
+	 fprintf oc "	vfmadd213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmadd231 (a1,a2,res) ->
+	 fprintf oc "	vfmadd231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmsub132 (a1,a2,res) ->
+	 fprintf oc "	vfmsub132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmsub213 (a1,a2,res) ->
+	 fprintf oc "	vfmsub213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmsub231 (a1,a2,res) ->
+	 fprintf oc "	vfmsub231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmadd132 (a1,a2,res) ->
+	 fprintf oc "	vfnmadd132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmadd213 (a1,a2,res) ->
+	 fprintf oc "	vfnmadd213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmadd231 (a1,a2,res) ->
+	 fprintf oc "	vfnmadd231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmsub132 (a1,a2,res) ->
+	 fprintf oc "	vfnmsub132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmsub213 (a1,a2,res) ->
+	 fprintf oc "	vfnmsub213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmsub231 (a1,a2,res) ->
+	 fprintf oc "	vfnmsub231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pmaxsd (a1,res) ->
+	 fprintf oc "	maxsd	%a, %a\n" freg a1 freg res
+      | Pminsd (a1,res) ->
+	 fprintf oc "	minsd	%a, %a\n" freg a1 freg res
+      | Prolw_8 res ->
+	 fprintf oc "	rolw	$8, %a\n" ireg16 res
+      | Psbbl (a1,res) ->
+	 fprintf oc "	sbbl	%a, %a\n" ireg a1 ireg res
+      | Psqrtsd (a1,res) ->
+	 fprintf oc "	sqrtsd	%a, %a\n" freg a1 freg res
       | Plabel(l) ->
           fprintf oc "%a:\n" label (transl_label l)
       | Pallocframe(sz, ofs_ra, ofs_link) ->