diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asm.v | 27 | ||||
-rw-r--r-- | arm/Asmexpand.ml | 174 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 187 |
3 files changed, 229 insertions, 159 deletions
@@ -43,6 +43,16 @@ Inductive freg: Type := | FR8: freg | FR9: freg | FR10: freg | FR11: freg | FR12: freg | FR13: freg | FR14: freg | FR15: freg. +Inductive sreg: Type := + | SR0: sreg | SR1: sreg | SR2: sreg | SR3: sreg + | SR4: sreg | SR5: sreg | SR6: sreg | SR7: sreg + | SR8: sreg | SR9: sreg | SR10: sreg | SR11: sreg + | SR12: sreg | SR13: sreg | SR14: sreg | SR15: sreg + | SR16: sreg | SR17: sreg | SR18: sreg | SR19: sreg + | SR20: sreg | SR21: sreg | SR22: sreg | SR23: sreg + | SR24: sreg | SR25: sreg | SR26: sreg | SR27: sreg + | SR28: sreg | SR29: sreg | SR30: sreg | SR31: sreg. + Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. @@ -228,8 +238,15 @@ Inductive instruction : Type := | Pldrh_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int16 load with post increment *) | Pstr_p: ireg -> ireg -> shift_op -> instruction (**r int32 store with post increment *) | Pstrb_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int8 store with post increment *) - | Pstrh_p: ireg -> ireg -> shift_op -> instruction. (**r unsigned int16 store with post increment *) + | Pstrh_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int16 store with post increment *) + (* Instructions for fixup of calling conventions *) + | Pfcpy_fs: freg -> sreg -> instruction (**r single precision float move for incoming arguments *) + | Pfcpy_sf: sreg -> freg -> instruction (**r single precision float move for outgoing arguments *) + | Pfcpy_fii: freg -> ireg -> ireg -> instruction (**r copy integer register pair to double fp-register *) + | Pfcpy_fi: freg -> ireg -> instruction (**r copy integer register to single fp-register *) + | Pfcpy_iif: ireg -> ireg -> freg -> instruction (**r copy double fp-register to integer register pair *) + | Pfcpy_if: ireg -> freg -> instruction. (**r copy single fp-register to integer register *) (** The pseudo-instructions are the following: @@ -784,7 +801,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pldrh_p _ _ _ | Pstr_p _ _ _ | Pstrb_p _ _ _ - | Pstrh_p _ _ _ => + | Pstrh_p _ _ _ + | Pfcpy_fs _ _ + | Pfcpy_sf _ _ + | Pfcpy_fii _ _ _ + | Pfcpy_fi _ _ + | Pfcpy_iif _ _ _ + | Pfcpy_if _ _ => Stuck end. diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index b65007df..dd960484 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -409,6 +409,161 @@ let expand_builtin_inline name args res = | _ -> raise (Error ("unrecognized builtin " ^ name)) + +(* Handling of calling conventions *) + +type direction = Incoming | Outgoing + +module FixupEABI = struct + + let ireg_param = function + | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false + + let freg_param = function + | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false + + let fixup_double dir f i1 i2 = + match dir with + | Incoming -> (* f <- (i1, i2) *) + emit (Pfcpy_fii (f, i1, i2)) + | Outgoing -> (* (i1, i2) <- f *) + emit (Pfcpy_iif (i1, i2, f)) + + let fixup_single dir f i = + match dir with + | Incoming -> (* f <- i *) + emit (Pfcpy_fi (f, i)) + | Outgoing -> (* i <- f *) + emit (Pfcpy_if (i, f)) + + let fixup_conventions dir tyl = + let rec fixup i tyl = + if i < 4 then + match tyl with + | [] -> () + | (Tint | Tany32) :: tyl' -> + fixup (i+1) tyl' + | Tlong :: tyl' -> + fixup (((i + 1) land (-2)) + 2) tyl' + | (Tfloat | Tany64) :: tyl' -> + let i = (i + 1) land (-2) in + if i < 4 then begin + if Archi.big_endian + then fixup_double dir (freg_param i) (ireg_param (i+1)) (ireg_param i) + else fixup_double dir (freg_param i) (ireg_param i) (ireg_param (i+1)); + fixup (i+2) tyl' + end + | Tsingle :: tyl' -> + fixup_single dir (freg_param i) (ireg_param i); + fixup (i+1) tyl' + in fixup 0 tyl + + let fixup_arguments dir sg = + fixup_conventions dir sg.sig_args + + let fixup_result dir sg = + fixup_conventions dir (proj_sig_res sg :: []) +end + +module FixupHF = struct + + type fsize = Single | Double + + let rec find_single used pos = + if pos >= Array.length used then pos + else if used.(pos) then find_single used (pos + 1) + else begin used.(pos) <- true; pos end + + let rec find_double used pos = + if pos + 1 >= Array.length used then pos + else if used.(pos) || used.(pos + 1) then find_double used (pos + 2) + else begin used.(pos) <- true; used.(pos + 1) <- true; pos / 2 end + + let freg_param = function + | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 + | 4 -> FR4 | 5 -> FR5 | 6 -> FR6 | 7 -> FR7 + | _ -> assert false + + let sreg_param = function + | 0 -> SR0 | 1 -> SR1 | 2 -> SR2 | 3 -> SR3 + | 4 -> SR4 | 5 -> SR5 | 6 -> SR6 | 7 -> SR7 + | 8 -> SR8 | 9 -> SR9 | 10 -> SR10 | 11 -> SR11 + | 12 -> SR12 | 13 -> SR13 | 14 -> SR14 | 15 -> SR15 + | _ -> assert false + + let rec fixup_actions used fr tyl = + match tyl with + | [] -> [] + | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl' + | (Tfloat | Tany64) :: tyl' -> + if fr >= 8 then [] else begin + let dr = find_double used 0 in + assert (dr < 8); + (fr, Double, dr) :: fixup_actions used (fr + 1) tyl' + end + | Tsingle :: tyl' -> + if fr >= 8 then [] else begin + let sr = find_single used 0 in + assert (sr < 16); + (fr, Single, sr) :: fixup_actions used (fr + 1) tyl' + end + + let rec fixup_outgoing = function + | [] -> () + | (fr, Double, dr) :: act -> + if fr <> dr then begin + let fr = freg_param fr + and dr = freg_param dr in + emit (Pfcpyd (dr, fr)) + end; + fixup_outgoing act + | (fr, Single, sr) :: act -> + let fr = freg_param fr + and sr = sreg_param sr in + emit (Pfcpy_sf (sr, fr)); + fixup_outgoing act + + let rec fixup_incoming = function + | [] -> () + | (fr, Double, dr) :: act -> + fixup_incoming act; + if fr <> dr then begin + let fr = freg_param fr + and dr = freg_param dr in + emit (Pfcpyd (fr, dr)) + end + | (fr, Single, sr) :: act -> + fixup_incoming act; + if (2 * fr) <> sr then begin + let fr = freg_param fr + and sr = sreg_param sr in + emit (Pfcpy_fs (fr, sr)) + end + + let fixup_arguments dir sg = + if sg.sig_cc.cc_vararg then + FixupEABI.fixup_arguments dir sg + else begin + let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in + match dir with + | Outgoing -> fixup_outgoing act + | Incoming -> fixup_incoming act + end + + let fixup_result dir sg = + if sg.sig_cc.cc_vararg then + FixupEABI.fixup_result dir sg +end + +let (fixup_arguments, fixup_result) = + match Configuration.abi with + | "eabi" -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result) + | "hardfloat" -> (FixupHF.fixup_arguments, FixupHF.fixup_result) + | _ -> assert false + + +(* Instruction expansion *) + let expand_instruction instr = match instr with | Pallocframe (sz, ofs) -> @@ -463,6 +618,24 @@ let expand_instruction instr = | _ -> assert false end + (* Fixup for calling conventions *) + | Pbsymb(id, sg) -> + fixup_arguments Outgoing sg; + emit instr + | Pbreg(r, sg) -> + if r = IR14 then + fixup_result Outgoing sg + else + fixup_arguments Outgoing sg; + emit instr + | Pblsymb(_, sg) -> + fixup_arguments Outgoing sg; + emit instr; + fixup_result Incoming sg + | Pblreg(_, sg) -> + fixup_arguments Outgoing sg; + emit instr; + fixup_result Incoming sg | _ -> emit instr @@ -492,6 +665,7 @@ let preg_to_dwarf = function let expand_function id fn = try set_current_function fn; + fixup_arguments Incoming fn.fn_sig; if !Clflags.option_g then expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code else diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 0cd3c908..cb66a9a1 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -71,9 +71,20 @@ struct | FR8 -> "s16" | FR9 -> "s18" | FR10 -> "s20" | FR11 -> "s22" | FR12 -> "s24" | FR13 -> "s26" | FR14 -> "s28" | FR15 -> "s30" + let single_param_reg_name = function + | SR0 -> "s0" | SR1 -> "s1" | SR2 -> "s2" | SR3 -> "s3" + | SR4 -> "s4" | SR5 -> "s5" | SR6 -> "s6" | SR7 -> "s7" + | SR8 -> "s8" | SR9 -> "s9" | SR10 -> "s10" | SR11 -> "s11" + | SR12 -> "s12" | SR13 -> "s13" | SR14 -> "s14" | SR15 -> "s15" + | SR16 -> "s16" | SR17 -> "s1" | SR18 -> "s18" | SR19 -> "s19" + | SR20 -> "s20" | SR21 -> "s21" | SR22 -> "s22" | SR23 -> "s23" + | SR24 -> "s24" | SR25 -> "s25" | SR26 -> "s26" | SR27 -> "s27" + | SR28 -> "s28" | SR29 -> "s29" | SR30 -> "s30" | SR31 -> "s31" + let ireg oc r = output_string oc (int_reg_name r) let freg oc r = output_string oc (float_reg_name r) let freg_single oc r = output_string oc (single_float_reg_name r) + let freg_param_single oc r = output_string oc (single_param_reg_name r) let preg oc = function | IR r -> ireg oc r @@ -278,141 +289,6 @@ struct print_file_line oc comment file line - (* Fixing up calling conventions *) - - type direction = Incoming | Outgoing - - module FixupEABI = struct - - let ireg_param = function - | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false - - let freg_param = function - | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false - - let fixup_double oc dir f i1 i2 = - match dir with - | Incoming -> (* f <- (i1, i2) *) - fprintf oc " vmov %a, %a, %a\n" freg f ireg i1 ireg i2 - | Outgoing -> (* (i1, i2) <- f *) - fprintf oc " vmov %a, %a, %a\n" ireg i1 ireg i2 freg f - - let fixup_single oc dir f i = - match dir with - | Incoming -> (* f <- i *) - fprintf oc " vmov %a, %a\n" freg_single f ireg i - | Outgoing -> (* i <- f *) - fprintf oc " vmov %a, %a\n" ireg i freg_single f - - let fixup_conventions oc dir tyl = - let rec fixup i tyl = - if i >= 4 then 0 else - match tyl with - | [] -> 0 - | (Tint | Tany32) :: tyl' -> - fixup (i+1) tyl' - | Tlong :: tyl' -> - fixup (((i + 1) land (-2)) + 2) tyl' - | (Tfloat | Tany64) :: tyl' -> - let i = (i + 1) land (-2) in - if i >= 4 then 0 else begin - if Archi.big_endian - then fixup_double oc dir (freg_param i) (ireg_param (i+1)) (ireg_param i) - else fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1)); - 1 + fixup (i+2) tyl' - end - | Tsingle :: tyl' -> - fixup_single oc dir (freg_param i) (ireg_param i); - 1 + fixup (i+1) tyl' - in fixup 0 tyl - - let fixup_arguments oc dir sg = - fixup_conventions oc dir sg.sig_args - - let fixup_result oc dir sg = - fixup_conventions oc dir (proj_sig_res sg :: []) - - end - - module FixupHF = struct - - type fsize = Single | Double - - let rec find_single used pos = - if pos >= Array.length used then pos - else if used.(pos) then find_single used (pos + 1) - else begin used.(pos) <- true; pos end - - let rec find_double used pos = - if pos + 1 >= Array.length used then pos - else if used.(pos) || used.(pos + 1) then find_double used (pos + 2) - else begin used.(pos) <- true; used.(pos + 1) <- true; pos / 2 end - - let rec fixup_actions used fr tyl = - match tyl with - | [] -> [] - | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl' - | (Tfloat | Tany64) :: tyl' -> - if fr >= 8 then [] else begin - let dr = find_double used 0 in - assert (dr < 8); - (fr, Double, dr) :: fixup_actions used (fr + 1) tyl' - end - | Tsingle :: tyl' -> - if fr >= 8 then [] else begin - let sr = find_single used 0 in - assert (sr < 16); - (fr, Single, sr) :: fixup_actions used (fr + 1) tyl' - end - - let rec fixup_outgoing oc = function - | [] -> 0 - | (fr, Double, dr) :: act -> - if fr = dr then fixup_outgoing oc act else begin - fprintf oc " vmov.f64 d%d, d%d\n" dr fr; - 1 + fixup_outgoing oc act - end - | (fr, Single, sr) :: act -> - fprintf oc " vmov.f32 s%d, s%d\n" sr (2*fr); - 1 + fixup_outgoing oc act - - let rec fixup_incoming oc = function - | [] -> 0 - | (fr, Double, dr) :: act -> - let n = fixup_incoming oc act in - if fr = dr then n else begin - fprintf oc " vmov.f64 d%d, d%d\n" fr dr; - 1 + n - end - | (fr, Single, sr) :: act -> - let n = fixup_incoming oc act in - if (2*fr) = sr then n else begin - fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; - 1 + n - end - - let fixup_arguments oc dir sg = - if sg.sig_cc.cc_vararg then - FixupEABI.fixup_arguments oc dir sg - else begin - let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in - match dir with - | Outgoing -> fixup_outgoing oc act - | Incoming -> fixup_incoming oc act - end - - let fixup_result oc dir sg = - if sg.sig_cc.cc_vararg then - FixupEABI.fixup_result oc dir sg - else - 0 - end - - let (fixup_arguments, fixup_result) = - match Opt.float_abi with - | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result) - | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result) - (* Printing of instructions *) let shift_op oc = function @@ -446,26 +322,13 @@ struct | 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; - n + 1 + fprintf oc " b %a\n" symbol id; 1 | Pbreg(r, sg) -> - let n = - if r = IR14 - then fixup_result oc Outgoing sg - else fixup_arguments oc Outgoing sg in - fprintf oc " bx %a\n" ireg r; - n + 1 + fprintf oc " bx %a\n" ireg r; 1 | Pblsymb(id, sg) -> - let n1 = fixup_arguments oc Outgoing sg in - fprintf oc " bl %a\n" symbol id; - let n2 = fixup_result oc Incoming sg in - n1 + 1 + n2 + fprintf oc " bl %a\n" symbol id; 1 | Pblreg(r, sg) -> - let n1 = fixup_arguments oc Outgoing sg in - fprintf oc " blx %a\n" ireg r; - let n2 = fixup_result oc Incoming sg in - n1 + 1 + n2 + fprintf oc " blx %a\n" ireg r; 1 | Pbic(r1, r2, so) -> fprintf oc " bic%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 @@ -747,6 +610,20 @@ struct end | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 | Pcfi_rel_offset ofs -> cfi_rel_offset oc "lr" (camlint_of_coqint ofs); 0 + (* Fixup instructions for calling conventions *) + | Pfcpy_fs(r1, r2) -> + fprintf oc " vmov.f32 %a, %a\n" freg_single r1 freg_param_single r2; 1 + | Pfcpy_sf(r1, r2) -> + fprintf oc " vmov.f32 %a, %a\n" freg_param_single r1 freg_single r2; 1 + | Pfcpy_fii (r1, r2, r3) -> + fprintf oc " vmov %a, %a, %a\n" freg r1 ireg r2 ireg r3; 1 + | Pfcpy_fi (r1, r2) -> + fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; 1 + | Pfcpy_iif (r1, r2, r3) -> + fprintf oc " vmov %a, %a, %a\n" ireg r1 ireg r2 freg r3; 1 + | Pfcpy_if (r1, r2) -> + fprintf oc " vmov %a, %a\n" ireg r1 freg_single r2; 1 + let no_fallthrough = function | Pb _ -> true @@ -762,10 +639,7 @@ struct else 2 in (len + add) * 4 - | Pbuiltin (EF_inline_asm _,_,_) -> 1024 (* Better be safe than sorry *) - | Pbreg _ - | Pblsymb _ - | Pblreg _ -> 72 (* 4 for branch, 4 for fixup result 4 * 16 for fixup args *) + | Pbuiltin (EF_inline_asm _,_,_) -> 1024 (* Better be safe than sorry *) | _ -> 12 @@ -824,7 +698,6 @@ struct let print_instructions oc fn = current_function_sig := fn.fn_sig; - ignore (fixup_arguments oc Incoming fn.fn_sig); print_instructions oc false fn.fn_code; if !literals_in_code then emit_constants oc |