aboutsummaryrefslogtreecommitdiffstats
path: root/arm
diff options
context:
space:
mode:
Diffstat (limited to 'arm')
-rw-r--r--arm/Asm.v27
-rw-r--r--arm/Asmexpand.ml174
-rw-r--r--arm/TargetPrinter.ml187
3 files changed, 229 insertions, 159 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index 85eb94c1..613f027b 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -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
generated by cgit (git 2.34.1) at 2024-06-30 21:52:37 +0000