aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--arm/Asm.v39
-rw-r--r--arm/Asmexpand.ml332
-rw-r--r--arm/TargetPrinter.ml321
-rw-r--r--backend/Asmexpandaux.ml57
-rw-r--r--ia32/Asm.v76
-rw-r--r--ia32/Asmexpand.ml373
-rw-r--r--ia32/TargetPrinter.ml359
-rw-r--r--powerpc/Asmexpand.ml55
8 files changed, 615 insertions, 997 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index dd434c02..2a120dd4 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -148,7 +148,6 @@ Inductive instruction : Type :=
| Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *)
| Pmvn: ireg -> shift_op -> instruction (**r integer complement *)
| Porr: ireg -> ireg -> shift_op -> instruction (**r bitwise or *)
- | Ppush: list ireg -> instruction (** push registers on the stack instruction *)
| Prsb: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction *)
| Psbfx: ireg -> ireg -> int -> int -> instruction (**r signed bitfield extract *)
| Pstr: ireg -> ireg -> shift_op -> instruction (**r int32 store *)
@@ -205,24 +204,7 @@ Inductive instruction : Type :=
| Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
| Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *)
| Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *)
- | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *)
- | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *)
- | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *)
- | Pclz: preg -> preg -> instruction (**r count leading zeros. *)
- | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *)
- | Prev: preg -> preg -> instruction (**r reverse bytes and reverse bits. *)
- | Prev16: preg -> preg -> instruction (**r reverse bytes and reverse bits. *)
- | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *)
- | Psbc: ireg -> ireg -> shift_op -> instruction (**r add with carry *)
- (* Add, sub, rsb versions with s suffix *)
- | Padds: ireg -> ireg -> shift_op -> instruction (**r integer addition with update of condition flags *)
- | Psubs: ireg -> ireg -> shift_op -> instruction (**r integer subtraction with update of condition flags *)
- | Prsbs: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction with update of condition flags *)
- | Pdmb: instruction (**r data memory barrier *)
- | Pdsb: instruction (**r data synchronization barrier *)
- | Pisb: instruction (**r instruction synchronization barrier *)
- | Pbne: label -> instruction. (**r branch if negative macro *)
-
+ | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *)
(** The pseudo-instructions are the following:
@@ -741,25 +723,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
end
| Pbuiltin ef args res => Stuck (**r treated specially below *)
| Pannot ef args => Stuck (**r treated specially below *)
- (** The following instructions and directives are not generated directly by Asmgen,
- so we do not model them. *)
- | Ppush _
- | Padc _ _ _
- | Pcfi_adjust _
- | Pclz _ _
- | Prev _ _
- | Prev16 _ _
- | Pfsqrt _ _
- | Prsc _ _ _
- | Psbc _ _ _
- | Padds _ _ _
- | Psubs _ _ _
- | Prsbs _ _ _
- | Pdmb
- | Pdsb
- | Pisb
- | Pbne _ =>
- Stuck
end.
(** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 95f35f37..4baaac3d 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -11,334 +11,8 @@
(* *********************************************************************)
(* Expanding built-ins and some pseudo-instructions by rewriting
- of the ARM assembly code. Currently not everything done, this
- expansion is performed on the fly in PrintAsm. *)
+ of the ARM assembly code. Currently not done, this expansion
+ is performed on the fly in PrintAsm. *)
-open Asm
-open Asmexpandaux
-open Asmgen
-open AST
-open Camlcoq
-open Integers
+let expand_program p = p
-(* Useful constants and helper functions *)
-
-let _0 = Integers.Int.zero
-let _1 = Integers.Int.one
-let _2 = coqint_of_camlint 2l
-let _4 = coqint_of_camlint 4l
-let _8 = coqint_of_camlint 8l
-let _16 = coqint_of_camlint 16l
-
-(* Emit instruction sequences that set or offset a register by a constant. *)
-(* No S suffix because they are applied to SP most of the time. *)
-
-let expand_movimm dst n =
- match Asmgen.decompose_int n with
- | [] -> assert false
- | hd::tl->
- emit (Pmov (dst,SOimm hd));
- List.iter
- (fun n -> emit (Porr (dst,dst, SOimm n))) tl
-
-let expand_subimm dst src n =
- match Asmgen.decompose_int n with
- | [] -> assert false
- | hd::tl ->
- emit (Psub(dst,src,SOimm hd));
- List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl
-
-let expand_addimm dst src n =
- match Asmgen.decompose_int n with
- | [] -> assert false
- | hd::tl ->
- emit (Padd (dst,src,SOimm hd));
- List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl
-
-let expand_int64_arith conflict rl fn =
- if conflict then
- begin
- fn IR14;
- emit (Pmov (rl,SOreg IR14))
- end else
- fn rl
-
-
-(* Built-ins. They come in two flavors:
- - annotation statements: take their arguments in registers or stack
- locations; generate no code;
- - inlined by the compiler: take their arguments in arbitrary
- registers.
-*)
-
-(* Handling of annotations *)
-
-let expand_annot_val txt targ args res =
- emit (Pannot (EF_annot(txt,[targ]), List.map (fun r -> AA_base r) args));
- match args, res with
- | [IR src], [IR dst] ->
- if dst <> src then emit (Pmov (dst,SOreg src))
- | [FR src], [FR dst] ->
- if dst <> src then emit (Pfcpyd (dst,src))
- | _, _ -> assert false
-
-
-(* Handling of memcpy *)
-
-(* The ARM has strict alignment constraints for 2 and 4 byte accesses.
- 8-byte accesses must be 4-aligned. *)
-
-let expand_builtin_memcpy_small sz al src dst =
- let rec copy ofs sz =
- if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
- emit (Pfldd (FR7,src,ofs));
- emit (Pfstd (FR7,dst,ofs));
- copy (Int.add ofs _8) (sz - 8)
- end else if sz >= 4 && al >= 4 then begin
- emit (Pldr (IR14,src,SOimm ofs));
- emit (Pstr (IR14,dst,SOimm ofs));
- copy (Int.add ofs _4) (sz - 4)
- end else if sz >= 2 && al >= 2 then begin
- emit (Pldrh (IR14,src,SOimm ofs));
- emit (Pstrh (IR14,dst,SOimm ofs));
- copy (Int.add ofs _2) (sz - 2)
- end else if sz >= 1 then begin
- emit (Pldrb (IR14,src,SOimm ofs));
- emit (Pstrb (IR14,dst,SOimm ofs));
- copy (Int.add ofs _1) (sz - 1)
- end else
- () in
- copy _0 sz
-
-let expand_builtin_memcpy_big sz al src dst =
- assert (sz >= al);
- assert (sz mod al = 0);
- assert (src = IR2);
- assert (dst = IR3);
- let (load, store, chunksize) =
- if al >= 4 then (Pldr (IR12,src,SOimm _4), Pstr (IR12,dst,SOimm _4) , 4)
- else if al = 2 then (Pldrh (IR12,src,SOimm _2), Pstrh (IR12,dst,SOimm _2), 2)
- else (Pldrb (IR12,src,SOimm _1), Pstrb (IR12,dst,SOimm _1), 1) in
- expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize)));
- let lbl = new_label () in
- emit (Plabel lbl);
- emit load;
- emit (Psubs (IR14,IR14,SOimm _1));
- emit store;
- emit (Pbne lbl)
-
-let expand_builtin_memcpy sz al args =
- let (dst, src) =
- match args with [IR d; IR s] -> (d, s) | _ -> assert false in
- if sz <= 32
- then expand_builtin_memcpy_small sz al src dst
- else expand_builtin_memcpy_big sz al src dst
-
-(* Handling of volatile reads and writes *)
-
-let expand_builtin_vload_common chunk args res =
- match chunk, args, res with
- | Mint8unsigned, [IR addr], [IR res] ->
- emit (Pldrb (res, addr,SOimm _0))
- | Mint8signed, [IR addr], [IR res] ->
- emit (Pldrsb (res, addr,SOimm _0))
- | Mint16unsigned, [IR addr], [IR res] ->
- emit (Pldrh (res, addr, SOimm _0))
- | Mint16signed, [IR addr], [IR res] ->
- emit (Pldrsh (res, addr, SOimm _0))
- | Mint32, [IR addr], [IR res] ->
- emit (Pldr (res,addr, SOimm _0))
- | Mint64, [IR addr], [IR res1; IR res2] ->
- if addr <> res2 then begin
- emit (Pldr (res2, addr, SOimm _0));
- emit (Pldr (res1, addr, SOimm _4))
- end else begin
- emit (Pldr (res1,addr, SOimm _4));
- emit (Pldr (res2,addr, SOimm _0))
- end
- | Mfloat32, [IR addr], [FR res] ->
- emit (Pflds (res, addr, _0))
- | Mfloat64, [IR addr], [FR res] ->
- emit (Pfldd (res,addr, _0))
- | _ ->
- assert false
-
-let expand_builtin_vload chunk args res =
- expand_builtin_vload_common chunk args res
-
-let expand_builtin_vload_global chunk id ofs args res =
- emit (Ploadsymbol (IR14,id,ofs));
- expand_builtin_vload_common chunk args res
-
-let expand_builtin_vstore_common chunk args =
- match chunk, args with
- | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
- emit (Pstrb (src,addr, SOimm _0))
- | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
- emit (Pstrh (src,addr, SOimm _0))
- | Mint32, [IR addr; IR src] ->
- emit (Pstr (src,addr, SOimm _0))
- | Mint64, [IR addr; IR src1; IR src2] ->
- emit (Pstr (src2,addr,SOimm _0));
- emit (Pstr (src1,addr,SOimm _0))
- | Mfloat32, [IR addr; FR src] ->
- emit (Pfstd (src,addr,_0))
- | Mfloat64, [IR addr; FR src] ->
- emit (Pfsts (src,addr,_0));
- | _ ->
- assert false
-
-let expand_builtin_vstore chunk args =
- expand_builtin_vstore_common chunk args
-
-let expand_builtin_vstore_global chunk id ofs args =
- emit (Ploadsymbol (IR14,id,ofs));
- expand_builtin_vstore_common chunk args
-
-(* Handling of varargs *)
-
-let align n a = (n + a - 1) land (-a)
-
-let rec next_arg_location ir ofs = function
- | [] ->
- Int32.of_int (ir * 4 + ofs)
- | (Tint | Tsingle | Tany32) :: l ->
- if ir < 4
- then next_arg_location (ir + 1) ofs l
- else next_arg_location ir (ofs + 4) l
- | (Tfloat | Tlong | Tany64) :: l ->
- if ir < 3
- then next_arg_location (align ir 2 + 2) ofs l
- else next_arg_location ir (align ofs 8 + 8) l
-
-let expand_builtin_va_start r =
- if not !current_function.fn_sig.sig_cc.cc_vararg then
- invalid_arg "Fatal error: va_start used in non-vararg function";
- let ofs =
- Int32.add
- (next_arg_location 0 0 !current_function.fn_sig.sig_args)
- !PrintAsmaux.current_function_stacksize in
- expand_addimm IR14 IR13 (coqint_of_camlint ofs);
- emit (Pstr (IR14,r,SOimm _0))
-
-
-(* Handling of compiler-inlined builtins *)
-let expand_builtin_inline name args res =
- match name, args, res with
- (* Integer arithmetic *)
- | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
- emit (Prev (IR res,IR a1))
- | "__builtin_bswap16", [IR a1], [IR res] ->
- emit (Prev16 (IR res,IR a1))
- | "__builtin_clz", [IR a1], [IR res] ->
- emit (Pclz (IR res, IR a1))
- (* Float arithmetic *)
- | "__builtin_fabs", [FR a1], [FR res] ->
- emit (Pfabsd (res,a1))
- | "__builtin_fsqrt", [FR a1], [FR res] ->
- emit (Pfsqrt (res,a1))
- (* 64-bit integer arithmetic *)
- | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] ->
- emit (Prsbs (rl,al,SOimm _0));
- if !Clflags.option_mthumb then begin
- emit (Pmvn (rh,SOreg ah));
- emit (Padc (rh,rh,SOimm _0))
- end else
- begin
- emit (Prsc (rh,ah,SOimm _0))
- end
- | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
- expand_int64_arith (rl = ah || rl = bh) rl
- (fun rl ->
- emit (Padds (rl,al,SOreg bl));
- emit (Padc (rh,ah,SOreg bh)))
- | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
- expand_int64_arith (rl = ah || rl = bh) rl
- (fun rl ->
- emit (Psubs (rl,al,SOreg bl));
- emit (Psbc (rh,ah,SOreg bh)))
- | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
- emit (Pumull (rl,rh,a,b))
- (* Memory accesses *)
- | "__builtin_read16_reversed", [IR a1], [IR res] ->
- emit (Pldrh (res,a1,SOimm _0));
- emit (Prev16 (IR res,IR res));
- | "__builtin_read32_reversed", [IR a1], [IR res] ->
- emit (Pldr (res,a1,SOimm _0));
- emit (Prev (IR res,IR res));
- | "__builtin_write16_reverse", [IR a1; IR a2], _ ->
- emit (Prev16 (IR IR14, IR a2));
- emit (Pstrh (IR14, a1, SOimm _0))
- | "__builtin_write32_reverse", [IR a1; IR a2], _ ->
- emit (Prev (IR IR14, IR a2));
- emit (Pstr (IR14, a1, SOimm _0))
- (* Synchronization *)
- | "__builtin_membar",[], _ ->
- ()
- | "__builtin_dmb", [], _ ->
- emit Pdmb
- | "__builtin_dsb", [], _ ->
- emit Pdsb
- | "__builtin_isb", [], _ ->
- emit Pisb
- (* Vararg stuff *)
- | "__builtin_va_start", [IR a], _ ->
- expand_builtin_va_start a
- (* Catch-all *)
- | _ ->
- invalid_arg ("unrecognized builtin " ^ name)
-
-let expand_instruction instr =
- match instr with
- | Pallocframe (sz, ofs) ->
- emit (Pmov (IR12,SOreg IR13));
- if (!current_function).fn_sig.sig_cc.cc_vararg then begin
- emit (Ppush [IR0;IR1;IR2;IR3]);
- emit (Pcfi_adjust _16);
- end;
- expand_subimm IR13 IR13 sz;
- emit (Pcfi_adjust sz);
- emit (Pstr (IR12,IR13,SOimm ofs))
- | Pfreeframe (sz, ofs) ->
- let sz =
- if (!current_function).fn_sig.sig_cc.cc_vararg
- then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz))
- else sz in
- if Asmgen.is_immed_arith sz
- then emit (Padd (IR13,IR13,SOimm sz))
- else emit (Pldr (IR13,IR13,SOimm sz))
- | Pbuiltin (ef,args,res) ->
- begin match ef with
- | EF_builtin (name,sg) ->
- expand_builtin_inline (extern_atom name) args res
- | EF_vload chunk ->
- expand_builtin_vload chunk args res
- | EF_vstore chunk ->
- expand_builtin_vstore chunk args
- | EF_vload_global(chunk, id, ofs) ->
- expand_builtin_vload_global chunk id ofs args res
- | EF_vstore_global(chunk, id, ofs) ->
- expand_builtin_vstore_global chunk id ofs args
- | EF_annot_val (txt,targ) ->
- expand_annot_val txt targ args res
- | EF_memcpy(sz, al) ->
- expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
- (Int32.to_int (camlint_of_coqint al)) args
- | EF_inline_asm(txt, sg, clob) ->
- emit instr
- | _ -> assert false
- end
- | _ ->
- emit instr
-
-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/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 88261940..505c3265 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -304,6 +304,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
let print_location oc loc =
if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
+
+(* Built-ins. They come in two flavors:
+ - annotation statements: take their arguments in registers or stack
+ locations; generate no code;
+ - inlined by the compiler: take their arguments in arbitrary
+ registers.
+*)
(* Handling of annotations *)
@@ -315,6 +322,167 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
fprintf oc "%s annotation: " comment;
print_annot_stmt preg "sp" oc txt targs args
end
+
+ let print_annot_val oc txt args res =
+ fprintf oc "%s annotation: " comment;
+ print_annot_val preg oc txt args;
+ match args, res with
+ | [IR src], [IR dst] ->
+ if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1)
+ | [FR src], [FR dst] ->
+ if dst = src then 0 else (fprintf oc " vmov.f64 %a, %a\n" freg dst freg src; 1)
+ | _, _ -> assert false
+
+(* Handling of memcpy *)
+
+(* The ARM has strict alignment constraints for 2 and 4 byte accesses.
+ 8-byte accesses must be 4-aligned. *)
+
+ let print_builtin_memcpy_small oc sz al src dst =
+ let rec copy ofs sz ninstr =
+ if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
+ fprintf oc " vldr %a, [%a, #%d]\n" freg FR7 ireg src ofs;
+ fprintf oc " vstr %a, [%a, #%d]\n" freg FR7 ireg dst ofs;
+ copy (ofs + 8) (sz - 8) (ninstr + 2)
+ end else if sz >= 4 && al >= 4 then begin
+ fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs;
+ fprintf oc " str %a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
+ copy (ofs + 4) (sz - 4) (ninstr + 2)
+ end else if sz >= 2 && al >= 2 then begin
+ fprintf oc " ldrh %a, [%a, #%d]\n" ireg IR14 ireg src ofs;
+ fprintf oc " strh %a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
+ copy (ofs + 2) (sz - 2) (ninstr + 2)
+ end else if sz >= 1 then begin
+ fprintf oc " ldrb %a, [%a, #%d]\n" ireg IR14 ireg src ofs;
+ fprintf oc " strb %a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
+ copy (ofs + 1) (sz - 1) (ninstr + 2)
+ end else
+ ninstr in
+ copy 0 sz 0
+
+ let print_builtin_memcpy_big oc sz al src dst =
+ assert (sz >= al);
+ assert (sz mod al = 0);
+ assert (src = IR2);
+ assert (dst = IR3);
+ let (load, store, chunksize) =
+ if al >= 4 then ("ldr", "str", 4)
+ else if al = 2 then ("ldrh", "strh", 2)
+ else ("ldrb", "strb", 1) in
+ let n = movimm oc "r14" (coqint_of_camlint (Int32.of_int (sz / chunksize))) in
+ let lbl = new_label() in
+ fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize;
+ fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14;
+ fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize;
+ fprintf oc " bne .L%d\n" lbl;
+ n + 4
+
+ let print_builtin_memcpy oc sz al args =
+ let (dst, src) =
+ match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+ fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
+ comment sz al;
+ let n =
+ if sz <= 32
+ then print_builtin_memcpy_small oc sz al src dst
+ else print_builtin_memcpy_big oc sz al src dst in
+ fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n
+
+(* Handling of volatile reads and writes *)
+
+ let print_builtin_vload_common oc chunk args res =
+ match chunk, args, res with
+ | Mint8unsigned, [IR addr], [IR res] ->
+ fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint8signed, [IR addr], [IR res] ->
+ fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint16unsigned, [IR addr], [IR res] ->
+ fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint16signed, [IR addr], [IR res] ->
+ fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint32, [IR addr], [IR res] ->
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint64, [IR addr], [IR res1; IR res2] ->
+ if addr <> res2 then begin
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr;
+ fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr
+ end else begin
+ fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr;
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr
+ end; 2
+ | Mfloat32, [IR addr], [FR res] ->
+ fprintf oc " vldr %a, [%a, #0]\n" freg_single res ireg addr; 1
+ | Mfloat64, [IR addr], [FR res] ->
+ fprintf oc " vldr %a, [%a, #0]\n" freg res ireg addr; 1
+ | _ ->
+ assert false
+
+ let print_builtin_vload oc chunk args res =
+ fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+ let n = print_builtin_vload_common oc chunk args res in
+ fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n
+
+ let print_builtin_vload_global oc chunk id ofs args res =
+ fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+ let n1 = loadsymbol oc IR14 id ofs in
+ let n2 = print_builtin_vload_common oc chunk [IR IR14] res in
+ fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n1 + n2
+
+ let print_builtin_vstore_common oc chunk args =
+ match chunk, args with
+ | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
+ fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1
+ | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
+ fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1
+ | Mint32, [IR addr; IR src] ->
+ fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1
+ | Mint64, [IR addr; IR src1; IR src2] ->
+ fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr;
+ fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2
+ | Mfloat32, [IR addr; FR src] ->
+ fprintf oc " vstr %a, [%a, #0]\n" freg_single src ireg addr; 1
+ | Mfloat64, [IR addr; FR src] ->
+ fprintf oc " vstr %a, [%a, #0]\n" freg src ireg addr; 1
+ | _ ->
+ assert false
+
+ let print_builtin_vstore oc chunk args =
+ fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+ let n = print_builtin_vstore_common oc chunk args in
+ fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
+
+ let print_builtin_vstore_global oc chunk id ofs args =
+ fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+ let n1 = loadsymbol oc IR14 id ofs in
+ let n2 = print_builtin_vstore_common oc chunk (IR IR14 :: args) in
+ fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n1 + n2
+
+(* Handling of varargs *)
+
+ let align n a = (n + a - 1) land (-a)
+
+ let rec next_arg_location ir ofs = function
+ | [] ->
+ Int32.of_int (ir * 4 + ofs)
+ | (Tint | Tsingle | Tany32) :: l ->
+ if ir < 4
+ then next_arg_location (ir + 1) ofs l
+ else next_arg_location ir (ofs + 4) l
+ | (Tfloat | Tlong | Tany64) :: l ->
+ if ir < 3
+ then next_arg_location (align ir 2 + 2) ofs l
+ else next_arg_location ir (align ofs 8 + 8) l
+
+ let print_builtin_va_start oc r =
+ if not (!current_function_sig).sig_cc.cc_vararg then
+ invalid_arg "Fatal error: va_start used in non-vararg function";
+ let ofs =
+ Int32.add
+ (next_arg_location 0 0 (!current_function_sig).sig_args)
+ !current_function_stacksize in
+ let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in
+ fprintf oc " str r14, [%a, #0]\n" ireg r;
+ n + 1
(* Auxiliary for 64-bit integer arithmetic built-ins. They expand to
two instructions, one computing the low 32 bits of the result,
@@ -331,6 +499,79 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
end else
fn rl
+(* Handling of compiler-inlined builtins *)
+
+ let print_builtin_inline oc name args res =
+ fprintf oc "%s begin %s\n" comment name;
+ let n = match name, args, res with
+ (* Integer arithmetic *)
+ | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
+ fprintf oc " rev %a, %a\n" ireg res ireg a1; 1
+ | "__builtin_bswap16", [IR a1], [IR res] ->
+ fprintf oc " rev16 %a, %a\n" ireg res ireg a1; 1
+ | "__builtin_clz", [IR a1], [IR res] ->
+ fprintf oc " clz %a, %a\n" ireg res ireg a1; 1
+ (* Float arithmetic *)
+ | "__builtin_fabs", [FR a1], [FR res] ->
+ fprintf oc " vabs.f64 %a, %a\n" freg res freg a1; 1
+ | "__builtin_fsqrt", [FR a1], [FR res] ->
+ fprintf oc " vsqrt.f64 %a, %a\n" freg res freg a1; 1
+ (* 64-bit integer arithmetic *)
+ | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
+ print_int64_arith oc (rl = ah) rl (fun rl ->
+ fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al;
+ (* No "rsc" instruction in Thumb2. Emulate based on
+ rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry)
+ == mvn a, b; adc a, a, #0 *)
+ if !Clflags.option_mthumb then begin
+ fprintf oc " mvn %a, %a\n" ireg rh ireg ah;
+ fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3
+ end else begin
+ fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2
+ end)
+ | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+ print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
+ fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl;
+ fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
+ | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+ print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
+ fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl;
+ fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
+ | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+ fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
+ (* Memory accesses *)
+ | "__builtin_read16_reversed", [IR a1], [IR res] ->
+ fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1;
+ fprintf oc " rev16 %a, %a\n" ireg res ireg res; 2
+ | "__builtin_read32_reversed", [IR a1], [IR res] ->
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1;
+ fprintf oc " rev %a, %a\n" ireg res ireg res; 2
+ | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
+ fprintf oc " rev16 %a, %a\n" ireg IR14 ireg a2;
+ fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 2
+ | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
+ fprintf oc " rev %a, %a\n" ireg IR14 ireg a2;
+ fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2
+ (* Synchronization *)
+ | "__builtin_membar", [], _ ->
+ 0
+ | "__builtin_dmb", [], _ ->
+ fprintf oc " dmb\n"; 1
+ | "__builtin_dsb", [], _ ->
+ fprintf oc " dsb\n"; 1
+ | "__builtin_isb", [], _ ->
+ fprintf oc " isb\n"; 1
+
+ (* Vararg stuff *)
+ | "__builtin_va_start", [IR a], _ ->
+ print_builtin_va_start oc a
+ (* Catch-all *)
+ | _ ->
+ invalid_arg ("unrecognized builtin " ^ name)
+ in
+ fprintf oc "%s end %s\n" comment name;
+ n
+
(* Fixing up calling conventions *)
type direction = Incoming | Outgoing
@@ -475,15 +716,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n
let print_instruction oc = function
- (* Core instructions *)
- | Padc (r1,r2,so) ->
- fprintf oc " adc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
+ (* Core instructions *)
| Padd(r1, r2, so) ->
fprintf oc " add%s %a, %a, %a\n"
(if !Clflags.option_mthumb && r2 <> IR14 then "s" else "")
ireg r1 ireg r2 shift_op so; 1
- | Padds (r1,r2,so) ->
- fprintf oc " adds %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
| Pand(r1, r2, so) ->
fprintf oc " and%t %a, %a, %a\n"
thumbS ireg r1 ireg r2 shift_op so; 1
@@ -494,8 +731,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
fprintf oc " b %a\n" print_label lbl; 1
| Pbc(bit, lbl) ->
fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1
- | Pbne lbl ->
- fprintf oc " bne %a\n" print_label lbl; 1
| Pbsymb(id, sg) ->
let n = fixup_arguments oc Outgoing sg in
fprintf oc " b %a\n" symbol id;
@@ -520,19 +755,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| Pbic(r1, r2, so) ->
fprintf oc " bic%t %a, %a, %a\n"
thumbS ireg r1 ireg r2 shift_op so; 1
- | Pclz (r1,r2) ->
- fprintf oc " clz %a, %a\n" preg r1 preg r2; 1
| Pcmp(r1, so) ->
fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1
- | Pdmb ->
- fprintf oc " dmb\n"; 1
- | Pdsb ->
- fprintf oc " dsb\n"; 1
- | Peor(r1, r2, so) ->
+ | Peor(r1, r2, so) ->
fprintf oc " eor%t %a, %a, %a\n"
thumbS ireg r1 ireg r2 shift_op so; 1
- | Pisb ->
- fprintf oc " isb\n"; 1
| Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) ->
fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
| Pldrb(r1, r2, sa) ->
@@ -564,22 +791,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| Porr(r1, r2, so) ->
fprintf oc " orr%t %a, %a, %a\n"
thumbS ireg r1 ireg r2 shift_op so; 1
- | Prev (r1,r2) ->
- fprintf oc " rev %a, %a\n" preg r1 preg r2; 1
- | Prev16 (r1,r2) ->
- fprintf oc " rev16 %a, %a\n" preg r1 preg r2; 1
| Prsb(r1, r2, so) ->
- fprintf oc " rsb%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | Prsbs(r1, r2, so) ->
- fprintf oc " rsbs %a, %a, %a\n"
- ireg r1 ireg r2 shift_op so; 1
- | Prsc (r1,r2,so) ->
- fprintf oc " rsc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
- | Pfsqrt (f1,f2) ->
- fprintf oc " vsqrt.f64 %a, %a\n" freg f1 freg f2; 1
- | Psbc (r1,r2,sa) ->
- fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 1
+ fprintf oc " rsb%t %a, %a, %a\n"
+ thumbS ireg r1 ireg r2 shift_op so; 1
| Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) ->
fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa;
begin match r1, r2, sa with
@@ -604,9 +818,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| Psub(r1, r2, so) ->
fprintf oc " sub%t %a, %a, %a\n"
thumbS ireg r1 ireg r2 shift_op so; 1
- | Psubs(r1, r2, so) ->
- fprintf oc " subs %a, %a, %a\n"
- ireg r1 ireg r2 shift_op so; 1
| Pudiv ->
if Opt.hardware_idiv then begin
fprintf oc " udiv r0, r0, r1\n"; 1
@@ -675,11 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| Pfdivs(r1, r2, r3) ->
fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
| Pfmuls(r1, r2, r3) ->
- fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
- | Ppush rl ->
- let first = ref true in
- let sep () = if !first then first := false else output_string oc ", " in
- fprintf oc " push {%a}\n" (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl; ;1
+ fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
| Pfsubs(r1, r2, r3) ->
fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
| Pflis(r1, f) ->
@@ -731,9 +938,25 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
(* Pseudo-instructions *)
| Pallocframe(sz, ofs) ->
- assert false
+ fprintf oc " mov r12, sp\n";
+ if (!current_function_sig).sig_cc.cc_vararg then begin
+ fprintf oc " push {r0, r1, r2, r3}\n";
+ cfi_adjust oc 16l
+ end;
+ let sz' = camlint_of_coqint sz in
+ let ninstr = subimm oc "sp" "sp" sz in
+ cfi_adjust oc sz';
+ fprintf oc " str r12, [sp, #%a]\n" coqint ofs;
+ current_function_stacksize := sz';
+ ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2)
| Pfreeframe(sz, ofs) ->
- assert false
+ let sz =
+ if (!current_function_sig).sig_cc.cc_vararg
+ then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz))
+ else sz in
+ if Asmgen.is_immed_arith sz
+ then fprintf oc " add sp, sp, #%a\n" coqint sz
+ else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1
| Plabel lbl ->
fprintf oc "%a:\n" print_label lbl; 0
| Ploadsymbol(r1, id, ofs) ->
@@ -765,6 +988,21 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
end
| Pbuiltin(ef, args, res) ->
begin match ef with
+ | EF_builtin(name, sg) ->
+ print_builtin_inline oc (extern_atom name) args res
+ | EF_vload chunk ->
+ print_builtin_vload oc chunk args res
+ | EF_vstore chunk ->
+ print_builtin_vstore oc chunk args
+ | EF_vload_global(chunk, id, ofs) ->
+ print_builtin_vload_global oc chunk id ofs args res
+ | EF_vstore_global(chunk, id, ofs) ->
+ print_builtin_vstore_global oc chunk id ofs args
+ | EF_memcpy(sz, al) ->
+ print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
+ (Int32.to_int (camlint_of_coqint al)) args
+ | EF_annot_val(txt, targ) ->
+ print_annot_val oc (extern_atom txt) args res
| EF_inline_asm(txt, sg, clob) ->
fprintf oc "%s begin inline assembly\n\t" comment;
print_inline_asm preg oc (extern_atom txt) sg args res;
@@ -780,7 +1018,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| _ ->
assert false
end
- | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0
let no_fallthrough = function
| Pb _ -> true
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
deleted file mode 100644
index 6ce6c005..00000000
--- a/backend/Asmexpandaux.ml
+++ /dev/null
@@ -1,57 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(* Util functions used for the expansion of built-ins and some
- pseudo-instructions *)
-
-open Asm
-open AST
-open Camlcoq
-
-(* Buffering the expanded code *)
-
-let current_code = ref ([]: instruction list)
-
-let emit i = current_code := i :: !current_code
-
-(* Generation of fresh labels *)
-
-let dummy_function = { fn_code = []; fn_sig = signature_main }
-let current_function = ref dummy_function
-let next_label = ref (None: label option)
-
-let new_label () =
- let lbl =
- match !next_label with
- | Some l -> l
- | None ->
- (* on-demand computation of the next available label *)
- List.fold_left
- (fun next instr ->
- match instr with
- | Plabel l -> if P.lt l next then next else P.succ l
- | _ -> next)
- P.one (!current_function).fn_code
- in
- next_label := Some (P.succ lbl);
- lbl
-
-
-let set_current_function f =
- current_function := f; next_label := None; current_code := []
-
-let get_current_function () =
- let c = List.rev !current_code in
- let fn = !current_function in
- set_current_function dummy_function;
- {fn with fn_code = c}
diff --git a/ia32/Asm.v b/ia32/Asm.v
index b423b4fc..b67c3cc5 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,42 +212,7 @@ 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))
- | Padcl_ir (n: int) (r: ireg)
- | Padcl_rr (r1: ireg) (r2: ireg)
- | Paddl (r1: ireg) (r2: ireg)
- | Paddl_mi (a: addrmode) (n: int)
- | Paddl_ri (r1: ireg) (n: int)
- | Pbsfl (r1: ireg) (r2: ireg)
- | Pbslr (r1: ireg) (r2: ireg)
- | Pbswap (r: ireg)
- | Pcfi_adjust (n: int)
- | 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)
- | Pmovb_rm (rs: ireg) (a: addrmode)
- | Pmovq_rm (rs: freg) (a: addrmode)
- | Pmovq_mr (a: addrmode) (rs: freg)
- | Pmovsb
- | Pmovsw
- | Pmovw_rm (rs: ireg) (ad: addrmode)
- | Prep_movsl
- | Prolw_8 (r: ireg)
- | Psbbl (r1: ireg) (r2: ireg)
- | Psqrtsd (r1: freg) (r2: freg)
- | Psubl_ri (r1: ireg) (n: int)
- | Pxchg (r1: ireg) (r2: ireg).
+ | Pannot(ef: external_function)(args: list (annot_arg preg)).
Definition code := list instruction.
Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -783,44 +748,7 @@ 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 *)
- (** The following instructions and directives are not generated directly by Asmgen,
- so we do not model them. *)
- | Padcl_ir _ _
- | Padcl_rr _ _
- | Paddl _ _
- | Paddl_mi _ _
- | Paddl_ri _ _
- | Pbswap _
- | Pbsfl _ _
- | Pbslr _ _
- | Pcfi_adjust _
- | Pfmadd132 _ _ _
- | Pfmadd213 _ _ _
- | Pfmadd231 _ _ _
- | Pfmsub132 _ _ _
- | Pfmsub213 _ _ _
- | Pfmsub231 _ _ _
- | Pfnmadd132 _ _ _
- | Pfnmadd213 _ _ _
- | Pfnmadd231 _ _ _
- | Pfnmsub132 _ _ _
- | Pfnmsub213 _ _ _
- | Pfnmsub231 _ _ _
- | Pmaxsd _ _
- | Pminsd _ _
- | Pmovb_rm _ _
- | Pmovq_rm _ _
- | Pmovq_mr _ _
- | Pmovsb
- | Pmovsw
- | Pmovw_rm _ _
- | Prep_movsl
- | Prolw_8 _
- | Psbbl _ _
- | Psqrtsd _ _
- | Psubl_ri _ _
- | Pxchg _ _ => Stuck
+ Stuck (**r treated specially below *)
end.
(** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index e07672a6..9a458c37 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -14,378 +14,5 @@
of the IA32 assembly code. Currently not done, this expansion
is performed on the fly in PrintAsm. *)
-open Asm
-open Asmexpandaux
-open Asmgen
-open AST
-open Camlcoq
-open Datatypes
-open Integers
-
-(* Useful constants and helper functions *)
-
-let _0 = Int.zero
-let _1 = Int.one
-let _2 = coqint_of_camlint 2l
-let _4 = coqint_of_camlint 4l
-let _8 = coqint_of_camlint 8l
-
-let stack_alignment () =
- if Configuration.system = "macoxs" then 16
- else 8
-
-(* SP adjustment to allocate or free a stack frame *)
-
-let int32_align n a =
- if n >= 0l
- then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
- else Int32.logand n (Int32.of_int (-a))
-
-let sp_adjustment sz =
- let sz = camlint_of_coqint sz in
- (* Preserve proper alignment of the stack *)
- let sz = int32_align sz (stack_alignment ()) in
- (* The top 4 bytes have already been allocated by the "call" instruction. *)
- let sz = Int32.sub sz 4l in
- sz
-
-
-(* Built-ins. They come in two flavors:
- - annotation statements: take their arguments in registers or stack
- locations; generate no code;
- - inlined by the compiler: take their arguments in arbitrary
- registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *)
-
-(* Handling of annotations *)
-
-let expand_annot_val txt targ args res =
- emit (Pannot (EF_annot(txt,[targ]), List.map (fun r -> AA_base r) args));
- match args, res with
- | [IR src], [IR dst] ->
- if dst <> src then emit (Pmov_rr (dst,src))
- | [FR src], [FR dst] ->
- if dst <> src then emit (Pmovsd_ff (dst,src))
- | _, _ -> assert false
-
-
-(* Handling of memcpy *)
-
-(* Unaligned memory accesses are quite fast on IA32, so use large
- memory accesses regardless of alignment. *)
-
-let expand_builtin_memcpy_small sz al src dst =
- assert (src = EDX && dst = EAX);
- let rec copy ofs sz =
- if sz >= 8 && !Clflags.option_ffpu then begin
- emit (Pmovq_rm (XMM7,Addrmode (Some src, None, Coq_inl ofs)));
- emit (Pmovq_mr (Addrmode (Some src, None, Coq_inl ofs),XMM7));
- copy (Int.add ofs _8) (sz - 8)
- end else if sz >= 4 then begin
- emit (Pmov_rm (ECX,Addrmode (Some src, None, Coq_inl ofs)));
- emit (Pmov_mr (Addrmode (Some src, None, Coq_inl ofs),ECX));
- copy (Int.add ofs _4) (sz - 4)
- end else if sz >= 2 then begin
- emit (Pmovw_rm (ECX,Addrmode (Some src, None, Coq_inl ofs)));
- emit (Pmovw_mr (Addrmode (Some src, None, Coq_inl ofs),ECX));
- copy (Int.add ofs _2) (sz - 2)
- end else if sz >= 1 then begin
- emit (Pmovb_rm (ECX,Addrmode (Some src, None, Coq_inl ofs)));
- emit (Pmovb_mr (Addrmode (Some src, None, Coq_inl ofs),ECX));
- copy (Int.add ofs _1) (sz - 1)
- end in
- copy _0 sz
-
-let expand_builtin_memcpy_big sz al src dst =
- assert (src = ESI && dst = EDI);
- emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4))));
- emit Prep_movsl;
- if sz mod 4 >= 2 then emit Pmovsw;
- if sz mod 2 >= 1 then emit Pmovsb
-
-let expand_builtin_memcpy sz al args =
- let (dst, src) =
- match args with [IR d; IR s] -> (d, s) | _ -> assert false in
- if sz <= 32
- then expand_builtin_memcpy_small sz al src dst
- else expand_builtin_memcpy_big sz al src dst
-
-(* Handling of volatile reads and writes *)
-
-let offset_addressing (Addrmode(base, ofs, cst)) delta =
- Addrmode(base, ofs,
- match cst with
- | Coq_inl n -> Coq_inl(Integers.Int.add n delta)
- | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta))
-
-let expand_builtin_vload_common chunk addr res =
- match chunk, res with
- | Mint8unsigned, [IR res] ->
- emit (Pmovzb_rm (res,addr))
- | Mint8signed, [IR res] ->
- emit (Pmovsb_rm (res,addr))
- | Mint16unsigned, [IR res] ->
- emit (Pmovzw_rm (res,addr))
- | Mint16signed, [IR res] ->
- emit (Pmovsw_rm (res,addr))
- | Mint32, [IR res] ->
- emit (Pmov_rm (res,addr))
- | Mint64, [IR res1; IR res2] ->
- let addr' = offset_addressing addr (coqint_of_camlint 4l) in
- if not (Asmgen.addressing_mentions addr res2) then begin
- emit (Pmov_rm (res2,addr));
- emit (Pmov_rm (res1,addr'))
- end else begin
- emit (Pmov_rm (res1,addr'));
- emit (Pmov_rm (res2,addr))
- end
- | Mfloat32, [FR res] ->
- emit (Pmovss_fm (res,addr))
- | Mfloat64, [FR res] ->
- emit (Pmovsd_fm (res,addr))
- | _ ->
- assert false
-
-let expand_builtin_vload chunk args res =
- match args with
- | [IR addr] ->
- expand_builtin_vload_common chunk (Addrmode (Some addr,None, Coq_inl _0)) res
- | _ ->
- assert false
-
-let expand_builtin_vload_global chunk id ofs args res =
- expand_builtin_vload_common chunk (Addrmode(None, None, Coq_inr(id,ofs))) res
-
-let expand_builtin_vstore_common chunk addr src tmp =
- match chunk, src with
- | (Mint8signed | Mint8unsigned), [IR src] ->
- if Asmgen.low_ireg src then
- emit (Pmovb_mr (addr,src))
- else begin
- emit (Pmov_rr (tmp,src));
- emit (Pmovb_mr (addr,tmp))
- end
- | (Mint16signed | Mint16unsigned), [IR src] ->
- emit (Pmovw_mr (addr,src))
- | Mint32, [IR src] ->
- emit (Pmov_mr (addr,src))
- | Mint64, [IR src1; IR src2] ->
- let addr' = offset_addressing addr (coqint_of_camlint 4l) in
- emit (Pmov_mr (addr,src2));
- emit (Pmov_mr (addr',src1))
- | Mfloat32, [FR src] ->
- emit (Pmovss_mf (addr,src))
- | Mfloat64, [FR src] ->
- emit (Pmovsd_mf (addr,src))
- | _ ->
- assert false
-
-let expand_builtin_vstore chunk args =
- match args with
- | IR addr :: src ->
- expand_builtin_vstore_common chunk
- (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src
- (if addr = EAX then ECX else EAX)
- | _ -> assert false
-
-
-let expand_builtin_vstore_global chunk id ofs args =
- expand_builtin_vstore_common chunk
- (Addrmode(None, None, Coq_inr(id,ofs))) args EAX
-
-
-(* Handling of varargs *)
-
-let expand_builtin_va_start r =
- if not !current_function.fn_sig.sig_cc.cc_vararg then
- invalid_arg "Fatal error: va_start used in non-vararg function";
- let ofs = coqint_of_camlint
- Int32.(add (add !PrintAsmaux.current_function_stacksize 4l)
- (mul 4l (Z.to_int32 (Conventions1.size_arguments
- !current_function.fn_sig)))) in
- emit (Pmov_mr (Addrmode (Some r, None, Coq_inl _0),ESP));
- emit (Paddl_mi (Addrmode (Some r,None,Coq_inl _0),ofs))
-
-(* Handling of compiler-inlined builtins *)
-
-let expand_builtin_inline 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] ->
- let addr = Addrmode(Some a1,None,Coq_inl _0) in
- emit (Pmovzw_rm (res,addr));
- emit (Prolw_8 res)
- | "__builtin_read32_reversed", [IR a1], [IR res] ->
- let addr = Addrmode(Some a1,None,Coq_inl _0) in
- emit (Pmov_rm (res,addr));
- emit (Pbswap res)
- | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
- let tmp = if a1 = ECX then EDX else ECX in
- let addr = Addrmode(Some a1,None,Coq_inl _0) in
- if a2 <> tmp then
- emit (Pmov_rr (a2,tmp));
- emit (Pxchg (tmp,tmp));
- emit (Pmovw_mr (addr,tmp))
- (* Vararg stuff *)
- | "__builtin_va_start", [IR a], _ ->
- expand_builtin_va_start a
- (* Synchronization *)
- | "__builtin_membar", [], _ ->
- ()
- (* Catch-all *)
- | _ ->
- invalid_arg ("unrecognized builtin " ^ name)
-
-
-
-let expand_instruction instr =
- match instr with
- | Pallocframe (sz, ofs_ra, ofs_link) ->
- let sz = sp_adjustment sz in
- let addr = Addrmode(Some ESP,None,Coq_inl (coqint_of_camlint (Int32.add sz 4l))) in
- let addr' = Addrmode (Some ESP, None, Coq_inl ofs_link) in
- let sz' = coqint_of_camlint sz in
- emit (Psubl_ri (ESP,sz'));
- emit (Pcfi_adjust sz');
- emit (Plea (EDX,addr));
- emit (Pmov_mr (addr',EDX));
- PrintAsmaux.current_function_stacksize := sz
- | Pfreeframe(sz, ofs_ra, ofs_link) ->
- let sz = sp_adjustment sz in
- emit (Paddl_ri (ESP,coqint_of_camlint sz))
- | Pbuiltin (ef,args, res) ->
- begin
- match ef with
- | EF_builtin(name, sg) ->
- expand_builtin_inline (extern_atom name) args res
- | EF_vload chunk ->
- expand_builtin_vload chunk args res
- | EF_vstore chunk ->
- expand_builtin_vstore chunk args
- | EF_vload_global(chunk, id, ofs) ->
- expand_builtin_vload_global chunk id ofs args res
- | EF_vstore_global(chunk, id, ofs) ->
- expand_builtin_vstore_global chunk id ofs args
- | EF_memcpy(sz, al) ->
- expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
- (Int32.to_int (camlint_of_coqint al)) args
- | EF_annot_val(txt, targ) ->
- expand_annot_val txt targ args res
- | EF_inline_asm(txt, sg, clob) ->
- emit instr
- | _ -> assert false
- end
- | _ -> 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 18aacebf..a53a8fbd 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -348,7 +348,156 @@ module Target(System: SYSTEM):TARGET =
print_annot_stmt preg "%esp" oc txt targs args
end
- (* Handling of varargs *)
+ let print_annot_val oc txt args res =
+ fprintf oc "%s annotation: " comment;
+ print_annot_val preg oc txt args;
+ match args, res with
+ | [IR src], [IR dst] ->
+ if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst
+ | [FR src], [FR dst] ->
+ if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst
+ | _, _ -> assert false
+
+(* Handling of memcpy *)
+
+(* Unaligned memory accesses are quite fast on IA32, so use large
+ memory accesses regardless of alignment. *)
+
+ let print_builtin_memcpy_small oc sz al src dst =
+ assert (src = EDX && dst = EAX);
+ let rec copy ofs sz =
+ if sz >= 8 && !Clflags.option_ffpu then begin
+ fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7;
+ fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst;
+ copy (ofs + 8) (sz - 8)
+ end else if sz >= 4 then begin
+ fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX;
+ fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst;
+ copy (ofs + 4) (sz - 4)
+ end else if sz >= 2 then begin
+ fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX;
+ fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst;
+ copy (ofs + 2) (sz - 2)
+ end else if sz >= 1 then begin
+ fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX;
+ fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst;
+ copy (ofs + 1) (sz - 1)
+ end in
+ copy 0 sz
+
+ let print_builtin_memcpy_big oc sz al src dst =
+ assert (src = ESI && dst = EDI);
+ fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX;
+ fprintf oc " rep movsl\n";
+ if sz mod 4 >= 2 then fprintf oc " movsw\n";
+ if sz mod 2 >= 1 then fprintf oc " movsb\n"
+
+ let print_builtin_memcpy oc sz al args =
+ let (dst, src) =
+ match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+ fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
+ comment sz al;
+ if sz <= 32
+ then print_builtin_memcpy_small oc sz al src dst
+ else print_builtin_memcpy_big oc sz al src dst;
+ fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment
+
+(* Handling of volatile reads and writes *)
+
+ let offset_addressing (Addrmode(base, ofs, cst)) delta =
+ Addrmode(base, ofs,
+ match cst with
+ | Coq_inl n -> Coq_inl(Integers.Int.add n delta)
+ | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta))
+
+ let print_builtin_vload_common oc chunk addr res =
+ match chunk, res with
+ | Mint8unsigned, [IR res] ->
+ fprintf oc " movzbl %a, %a\n" addressing addr ireg res
+ | Mint8signed, [IR res] ->
+ fprintf oc " movsbl %a, %a\n" addressing addr ireg res
+ | Mint16unsigned, [IR res] ->
+ fprintf oc " movzwl %a, %a\n" addressing addr ireg res
+ | Mint16signed, [IR res] ->
+ fprintf oc " movswl %a, %a\n" addressing addr ireg res
+ | Mint32, [IR res] ->
+ fprintf oc " movl %a, %a\n" addressing addr ireg res
+ | Mint64, [IR res1; IR res2] ->
+ let addr' = offset_addressing addr (coqint_of_camlint 4l) in
+ if not (Asmgen.addressing_mentions addr res2) then begin
+ fprintf oc " movl %a, %a\n" addressing addr ireg res2;
+ fprintf oc " movl %a, %a\n" addressing addr' ireg res1
+ end else begin
+ fprintf oc " movl %a, %a\n" addressing addr' ireg res1;
+ fprintf oc " movl %a, %a\n" addressing addr ireg res2
+ end
+ | Mfloat32, [FR res] ->
+ fprintf oc " movss %a, %a\n" addressing addr freg res
+ | Mfloat64, [FR res] ->
+ fprintf oc " movsd %a, %a\n" addressing addr freg res
+ | _ ->
+ assert false
+
+ let print_builtin_vload oc chunk args res =
+ fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+ begin match args with
+ | [IR addr] ->
+ print_builtin_vload_common oc chunk
+ (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res
+ | _ ->
+ assert false
+ end;
+ fprintf oc "%s end builtin __builtin_volatile_read\n" comment
+
+ let print_builtin_vload_global oc chunk id ofs args res =
+ fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+ print_builtin_vload_common oc chunk
+ (Addrmode(None, None, Coq_inr(id,ofs))) res;
+ fprintf oc "%s end builtin __builtin_volatile_read\n" comment
+
+ let print_builtin_vstore_common oc chunk addr src tmp =
+ match chunk, src with
+ | (Mint8signed | Mint8unsigned), [IR src] ->
+ if Asmgen.low_ireg src then
+ fprintf oc " movb %a, %a\n" ireg8 src addressing addr
+ else begin
+ fprintf oc " movl %a, %a\n" ireg src ireg tmp;
+ fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr
+ end
+ | (Mint16signed | Mint16unsigned), [IR src] ->
+ fprintf oc " movw %a, %a\n" ireg16 src addressing addr
+ | Mint32, [IR src] ->
+ fprintf oc " movl %a, %a\n" ireg src addressing addr
+ | Mint64, [IR src1; IR src2] ->
+ let addr' = offset_addressing addr (coqint_of_camlint 4l) in
+ fprintf oc " movl %a, %a\n" ireg src2 addressing addr;
+ fprintf oc " movl %a, %a\n" ireg src1 addressing addr'
+ | Mfloat32, [FR src] ->
+ fprintf oc " movss %a, %a\n" freg src addressing addr
+ | Mfloat64, [FR src] ->
+ fprintf oc " movsd %a, %a\n" freg src addressing addr
+ | _ ->
+ assert false
+
+ let print_builtin_vstore oc chunk args =
+ fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+ begin match args with
+ | IR addr :: src ->
+ print_builtin_vstore_common oc chunk
+ (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src
+ (if addr = EAX then ECX else EAX)
+ | _ ->
+ assert false
+ end;
+ fprintf oc "%s end builtin __builtin_volatile_write\n" comment
+
+ let print_builtin_vstore_global oc chunk id ofs args =
+ fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+ print_builtin_vstore_common oc chunk
+ (Addrmode(None, None, Coq_inr(id,ofs))) args EAX;
+ fprintf oc "%s end builtin __builtin_volatile_write\n" comment
+
+(* Handling of varargs *)
let print_builtin_va_start oc r =
if not (!current_function_sig).sig_cc.cc_vararg then
@@ -360,6 +509,117 @@ module Target(System: SYSTEM):TARGET =
fprintf oc " movl %%esp, 0(%a)\n" ireg r;
fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r
+(* Handling of compiler-inlined builtins *)
+
+ let print_builtin_inline oc name args res =
+ fprintf oc "%s begin builtin %s\n" comment name;
+ begin match name, args, res with
+ (* Integer arithmetic *)
+ | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] ->
+ if a1 <> res then
+ fprintf oc " movl %a, %a\n" ireg a1 ireg res;
+ fprintf oc " bswap %a\n" ireg res
+ | "__builtin_bswap16", [IR a1], [IR res] ->
+ if a1 <> res then
+ fprintf oc " movl %a, %a\n" ireg a1 ireg res;
+ fprintf oc " rolw $8, %a\n" ireg16 res
+ | "__builtin_clz", [IR a1], [IR res] ->
+ fprintf oc " bsrl %a, %a\n" ireg a1 ireg res;
+ fprintf oc " xorl $31, %a\n" ireg res
+ | "__builtin_ctz", [IR a1], [IR res] ->
+ fprintf oc " bsfl %a, %a\n" ireg a1 ireg res
+ (* Float arithmetic *)
+ | "__builtin_fabs", [FR a1], [FR res] ->
+ need_masks := true;
+ if a1 <> res then
+ fprintf oc " movapd %a, %a\n" freg a1 freg res;
+ fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res
+ | "__builtin_fsqrt", [FR a1], [FR res] ->
+ fprintf oc " sqrtsd %a, %a\n" freg a1 freg res
+ | "__builtin_fmax", [FR a1; FR a2], [FR res] ->
+ if res = a1 then
+ fprintf oc " maxsd %a, %a\n" freg a2 freg res
+ else if res = a2 then
+ fprintf oc " maxsd %a, %a\n" freg a1 freg res
+ else begin
+ fprintf oc " movapd %a, %a\n" freg a1 freg res;
+ fprintf oc " maxsd %a, %a\n" freg a2 freg res
+ end
+ | "__builtin_fmin", [FR a1; FR a2], [FR res] ->
+ if res = a1 then
+ fprintf oc " minsd %a, %a\n" freg a2 freg res
+ else if res = a2 then
+ fprintf oc " minsd %a, %a\n" freg a1 freg res
+ else begin
+ fprintf oc " movapd %a, %a\n" freg a1 freg res;
+ fprintf oc " minsd %a, %a\n" freg a2 freg res
+ end
+ | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"),
+ [FR a1; FR a2; FR a3], [FR res] ->
+ let opcode =
+ match name with
+ | "__builtin_fmadd" -> "vfmadd"
+ | "__builtin_fmsub" -> "vfmsub"
+ | "__builtin_fnmadd" -> "vfnmadd"
+ | "__builtin_fnmsub" -> "vfnmsub"
+ | _ -> assert false in
+ if res = a1 then
+ fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res
+ else if res = a2 then
+ fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res
+ else if res = a3 then
+ fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res
+ else begin
+ fprintf oc " movapd %a, %a\n" freg a3 freg res;
+ fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg 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);
+ fprintf oc " negl %a\n" ireg EAX;
+ fprintf oc " adcl $0, %a\n" ireg EDX;
+ fprintf oc " negl %a\n" ireg 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);
+ fprintf oc " addl %a, %a\n" ireg EBX ireg EAX;
+ fprintf oc " adcl %a, %a\n" ireg ECX ireg 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);
+ fprintf oc " subl %a, %a\n" ireg EBX ireg EAX;
+ fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX
+ | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+ assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
+ fprintf oc " mull %a\n" ireg 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
+ fprintf oc " movl %a, %a\n" ireg a2 ireg 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
+ fprintf oc " movl %a, %a\n" ireg a2 ireg tmp;
+ fprintf oc " bswap %a\n" ireg tmp;
+ 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)
+ end;
+ fprintf oc "%s end builtin %s\n" comment name
(* Printing of instructions *)
@@ -581,83 +841,36 @@ 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;
- | Paddl_mi (addr,n) ->
- fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) addressing addr
- | Paddl_ri (res,n) ->
- fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) 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
- | Pcfi_adjust sz ->
- cfi_adjust oc (camlint_of_coqint sz)
- | 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
- | Pmovb_rm (r1,a) ->
- fprintf oc " movb %a, %a\n" addressing a ireg8 r1
- | Pmovq_rm(rd, a) ->
- fprintf oc " movq %a, %a\n" addressing a freg rd
- | Pmovq_mr(a, r1) ->
- fprintf oc " movq %a, %a\n" freg r1 addressing a
- | Pmovsb ->
- fprintf oc " movsb\n";
- | Pmovsw ->
- fprintf oc " movsw\n";
- | Pmovw_rm (r1, a) ->
- fprintf oc " movw %a, %a\n" addressing a ireg16 r1
- | Prep_movsl ->
- fprintf oc " rep movsl\n"
- | 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
- | Psubl_ri (res,n) ->
- fprintf oc " subl $%ld, %a\n" (camlint_of_coqint n) ireg res;
- | Pxchg (a1,a2) ->
- fprintf oc " xchg %a, %a\n" ireg8 a1 high_ireg8 a2;
| Plabel(l) ->
fprintf oc "%a:\n" label (transl_label l)
- | Pallocframe(sz, ofs_ra, ofs_link)
+ | Pallocframe(sz, ofs_ra, ofs_link) ->
+ let sz = sp_adjustment sz in
+ let ofs_link = camlint_of_coqint ofs_link in
+ fprintf oc " subl $%ld, %%esp\n" sz;
+ cfi_adjust oc sz;
+ fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l);
+ fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link;
+ current_function_stacksize := sz
| Pfreeframe(sz, ofs_ra, ofs_link) ->
- assert false
+ let sz = sp_adjustment sz in
+ fprintf oc " addl $%ld, %%esp\n" sz
| Pbuiltin(ef, args, res) ->
begin match ef with
+ | EF_builtin(name, sg) ->
+ print_builtin_inline oc (extern_atom name) args res
+ | EF_vload chunk ->
+ print_builtin_vload oc chunk args res
+ | EF_vstore chunk ->
+ print_builtin_vstore oc chunk args
+ | EF_vload_global(chunk, id, ofs) ->
+ print_builtin_vload_global oc chunk id ofs args res
+ | EF_vstore_global(chunk, id, ofs) ->
+ print_builtin_vstore_global oc chunk id ofs args
+ | EF_memcpy(sz, al) ->
+ print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
+ (Int32.to_int (camlint_of_coqint al)) args
+ | EF_annot_val(txt, targ) ->
+ print_annot_val oc (extern_atom txt) args res
| EF_inline_asm(txt, sg, clob) ->
fprintf oc "%s begin inline assembly\n\t" comment;
print_inline_asm preg oc (extern_atom txt) sg args res;
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index ec5a767f..699c841f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -19,10 +19,48 @@ open Integers
open AST
open Memdata
open Asm
-open Asmexpandaux
+(* Buffering the expanded code *)
-(* Useful constants and helper functions *)
+let current_code = ref ([]: instruction list)
+
+let emit i = current_code := i :: !current_code
+
+let emit_loadimm r n =
+ List.iter emit (Asmgen.loadimm r n [])
+
+let emit_addimm rd rs n =
+ List.iter emit (Asmgen.addimm rd rs n [])
+
+let get_code () =
+ let c = List.rev !current_code in current_code := []; c
+
+(* Generation of fresh labels *)
+
+let dummy_function = { fn_code = []; fn_sig = signature_main }
+let current_function = ref dummy_function
+let next_label = ref (None : label option)
+
+let new_label () =
+ let lbl =
+ match !next_label with
+ | Some l -> l
+ | None ->
+ (* on-demand computation of the next available label *)
+ List.fold_left
+ (fun next instr ->
+ match instr with
+ | Plabel l -> if P.lt l next then next else P.succ l
+ | _ -> next)
+ P.one (!current_function).fn_code
+ in
+ next_label := Some (P.succ lbl);
+ lbl
+
+let set_current_function f =
+ current_function := f; next_label := None
+
+(* Useful constants *)
let _0 = Integers.Int.zero
let _1 = Integers.Int.one
@@ -33,14 +71,6 @@ let _8 = coqint_of_camlint 8l
let _m4 = coqint_of_camlint (-4l)
let _m8 = coqint_of_camlint (-8l)
-let emit_loadimm r n =
- List.iter emit (Asmgen.loadimm r n [])
-
-let emit_addimm rd rs n =
- List.iter emit (Asmgen.addimm rd rs n [])
-
-
-
(* Handling of annotations *)
let expand_annot_val txt targ args res =
@@ -503,8 +533,11 @@ let expand_instruction instr =
let expand_function fn =
set_current_function fn;
+ current_code := [];
List.iter expand_instruction fn.fn_code;
- get_current_function ()
+ let c = get_code() in
+ set_current_function dummy_function;
+ { fn with fn_code = c }
let expand_fundef = function
| Internal f -> Internal (expand_function f)