diff options
Diffstat (limited to 'ia32/Conventions1.v')
-rw-r--r-- | ia32/Conventions1.v | 331 |
1 files changed, 282 insertions, 49 deletions
diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v index 08a86815..dbc8b064 100644 --- a/ia32/Conventions1.v +++ b/ia32/Conventions1.v @@ -2,7 +2,7 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -13,11 +13,8 @@ (** Function calling conventions and other conventions regarding the use of machine registers and stack slots. *) -Require Import Coqlib. -Require Import Decidableplus. -Require Import AST. -Require Import Events. -Require Import Locations. +Require Import Coqlib Decidableplus. +Require Import AST Machregs Locations. (** * Classification of machine registers *) @@ -26,23 +23,37 @@ Require Import Locations. - Callee-save registers, whose value is preserved across a function call. - Caller-save registers that can be modified during a function call. - We follow the x86-32 application binary interface (ABI) in our choice - of callee- and caller-save registers. + We follow the x86-32 and x86-64 application binary interfaces (ABI) + in our choice of callee- and caller-save registers. *) Definition is_callee_save (r: mreg) : bool := match r with | AX | CX | DX => false - | BX | SI | DI | BP => true + | BX | BP => true + | SI | DI => negb Archi.ptr64 (**r callee-save in 32 bits but not in 64 bits *) + | R8 | R9 | R10 | R11 => false + | R12 | R13 | R14 | R15 => true | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => false | FP0 => false end. -Definition int_caller_save_regs := AX :: CX :: DX :: nil. +Definition int_caller_save_regs := + if Archi.ptr64 + then AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil + else AX :: CX :: DX :: nil. -Definition float_caller_save_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. +Definition float_caller_save_regs := + if Archi.ptr64 + then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: + X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil + else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. -Definition int_callee_save_regs := BX :: SI :: DI :: BP :: nil. +Definition int_callee_save_regs := + if Archi.ptr64 + then BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil + else BX :: SI :: DI :: BP :: nil. Definition float_callee_save_regs : list mreg := nil. @@ -52,6 +63,14 @@ Definition destroyed_at_call := Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) +Definition is_float_reg (r: mreg) := + match r with + | AX | BX | CX | DX | SI | DI | BP + | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => false + | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | FP0 => true + end. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -68,15 +87,16 @@ Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) of function arguments), but this leaves much liberty in choosing actual locations. To ensure binary interoperability of code generated by our compiler with libraries compiled by another compiler, we - implement the standard x86 conventions. *) + implement the standard x86-32 and x86-64 conventions. *) (** ** Location of function result *) -(** The result value of a function is passed back to the caller in - registers [AX] or [DX:AX] or [FP0], depending on the type of the returned value. - We treat a function without result as a function with one integer result. *) +(** In 32 bit mode, the result value of a function is passed back to the + caller in registers [AX] or [DX:AX] or [FP0], depending on the type + of the returned value. We treat a function without result as a + function with one integer result. *) -Definition loc_result (s: signature) : rpair mreg := +Definition loc_result_32 (s: signature) : rpair mreg := match s.(sig_res) with | None => One AX | Some (Tint | Tany32) => One AX @@ -85,13 +105,27 @@ Definition loc_result (s: signature) : rpair mreg := | Some Tlong => Twolong DX AX end. +(** In 64 bit mode, he result value of a function is passed back to + the caller in registers [AX] or [X0]. *) + +Definition loc_result_64 (s: signature) : rpair mreg := + match s.(sig_res) with + | None => One AX + | Some (Tint | Tlong | Tany32 | Tany64) => One AX + | Some (Tfloat | Tsingle) => One X0 + end. + +Definition loc_result := + if Archi.ptr64 then loc_result_64 else loc_result_32. + (** The result registers have types compatible with that given in the signature. *) Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto. + intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type; + destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto. Qed. (** The result locations are caller-save registers *) @@ -100,8 +134,8 @@ Lemma loc_result_caller_save: forall (s: signature), forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. - intros. - unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; + destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -110,17 +144,32 @@ Lemma loc_result_pair: forall sg, match loc_result sg with | One _ => True - | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + | Twolong r1 r2 => + r1 <> r2 /\ sg.(sig_res) = Some Tlong + /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + /\ Archi.splitlong = true end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence. + intros. change Archi.splitlong with (negb Archi.ptr64). + unfold loc_result, loc_result_32, loc_result_64, mreg_type; + destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto. + split; auto. congruence. +Qed. + +(** The location of the result depends only on the result part of the signature *) + +Lemma loc_result_exten: + forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. +Proof. + intros. unfold loc_result, loc_result_32, loc_result_64. + destruct Archi.ptr64; rewrite H; auto. Qed. (** ** Location of function arguments *) -(** All arguments are passed on stack. (Snif.) *) +(** In the x86-32 ABI, all arguments are passed on stack. (Snif.) *) -Fixpoint loc_arguments_rec +Fixpoint loc_arguments_32 (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil @@ -129,27 +178,77 @@ Fixpoint loc_arguments_rec | Tlong => Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) | _ => One (S Outgoing ofs ty) end - :: loc_arguments_rec tys (ofs + typesize ty) + :: loc_arguments_32 tys (ofs + typesize ty) + end. + +(** In the x86-64 ABI: +- The first 6 integer arguments are passed in registers [DI], [SI], [DX], [CX], [R8], [R9]. +- The first 8 floating-point arguments are passed in registers [X0] to [X7]. +- Extra arguments are passed on the stack, in [Outgoing] slots. + Consecutive stack slots are separated by 8 bytes, even if only 4 bytes + of data is used in a slot. +*) + +Definition int_param_regs := DI :: SI :: DX :: CX :: R8 :: R9 :: nil. +Definition float_param_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. + +Fixpoint loc_arguments_64 + (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) := + match tyl with + | nil => nil + | (Tint | Tlong | Tany32 | Tany64) as ty :: tys => + match list_nth_z int_param_regs ir with + | None => + One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2) + | Some ireg => + One (R ireg) :: loc_arguments_64 tys (ir + 1) fr ofs + end + | (Tfloat | Tsingle) as ty :: tys => + match list_nth_z float_param_regs fr with + | None => + One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2) + | Some freg => + One (R freg) :: loc_arguments_64 tys ir (fr + 1) ofs + end end. (** [loc_arguments s] returns the list of locations where to store arguments when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list (rpair loc) := - loc_arguments_rec s.(sig_args) 0. + if Archi.ptr64 + then loc_arguments_64 s.(sig_args) 0 0 0 + else loc_arguments_32 s.(sig_args) 0. (** [size_arguments s] returns the number of [Outgoing] slots used to call a function with signature [s]. *) -Fixpoint size_arguments_rec +Fixpoint size_arguments_32 (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs - | ty :: tys => size_arguments_rec tys (ofs + typesize ty) + | ty :: tys => size_arguments_32 tys (ofs + typesize ty) + end. + +Fixpoint size_arguments_64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := + match tyl with + | nil => ofs + | (Tint | Tlong | Tany32 | Tany64) :: tys => + match list_nth_z int_param_regs ir with + | None => size_arguments_64 tys ir fr (ofs + 2) + | Some ireg => size_arguments_64 tys (ir + 1) fr ofs + end + | (Tfloat | Tsingle) :: tys => + match list_nth_z float_param_regs fr with + | None => size_arguments_64 tys ir fr (ofs + 2) + | Some freg => size_arguments_64 tys ir (fr + 1) ofs + end end. Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args) 0. + if Archi.ptr64 + then size_arguments_64 s.(sig_args) 0 0 0 + else size_arguments_32 s.(sig_args) 0. (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -161,19 +260,26 @@ Definition loc_argument_acceptable (l: loc) : Prop := | _ => False end. -Definition loc_argument_charact (ofs: Z) (l: loc) : Prop := +Definition loc_argument_32_charact (ofs: Z) (l: loc) : Prop := match l with | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 | _ => False end. -Remark loc_arguments_rec_charact: +Definition loc_argument_64_charact (ofs: Z) (l: loc) : Prop := + match l with + | R r => In r int_param_regs \/ In r float_param_regs + | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') + | _ => False + end. + +Remark loc_arguments_32_charact: forall tyl ofs p, - In p (loc_arguments_rec tyl ofs) -> forall_rpair (loc_argument_charact ofs) p. + In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l). + assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l). { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } - induction tyl as [ | ty tyl]; simpl loc_arguments_rec; intros. + induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros. - contradiction. - destruct H. + destruct ty; subst p; simpl; omega. @@ -182,23 +288,73 @@ Proof. * destruct H; split; eapply X; eauto; omega. Qed. +Remark loc_arguments_64_charact: + forall tyl ir fr ofs p, + In p (loc_arguments_64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_64_charact ofs) p. +Proof. + assert (X: forall ofs1 ofs2 l, loc_argument_64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_64_charact ofs1 l). + { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). + { destruct p; simpl; intuition eauto. } + assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). + { intros. apply Z.divide_add_r; auto. apply Zdivide_refl. } +Opaque list_nth_z. + induction tyl; simpl loc_arguments_64; intros. + elim H. + assert (A: forall ty, In p + match list_nth_z int_param_regs ir with + | Some ireg => One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_64_charact ofs) p). + { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1. + subst. left. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. omega. assumption. + eapply Y; eauto. omega. } + assert (B: forall ty, In p + match list_nth_z float_param_regs fr with + | Some ireg => One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_64_charact ofs) p). + { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1. + subst. right. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. omega. assumption. + eapply Y; eauto. omega. } + destruct a; eauto. +Qed. + Lemma loc_arguments_acceptable: forall (s: signature) (p: rpair loc), In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. - unfold loc_arguments; intros. - exploit loc_arguments_rec_charact; eauto. - assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l). + unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF. +- (* 64 bits *) + assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). + assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. + assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_64_charact, loc_argument_acceptable. + destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. + intros [C D]. split; auto. apply Zdivide_trans with 2; auto. + exists (2 / typealign ty); destruct ty; reflexivity. + } + exploit loc_arguments_64_charact; eauto using Zdivide_0. + unfold forall_rpair; destruct p; intuition auto. +- (* 32 bits *) + assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. } - destruct p; simpl; intuition auto. + exploit loc_arguments_32_charact; eauto. + unfold forall_rpair; destruct p; intuition auto. Qed. Hint Resolve loc_arguments_acceptable: locs. (** The offsets of [Outgoing] arguments are below [size_arguments s]. *) -Remark size_arguments_rec_above: - forall tyl ofs0, ofs0 <= size_arguments_rec tyl ofs0. +Remark size_arguments_32_above: + forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0. Proof. induction tyl; simpl; intros. omega. @@ -206,23 +362,45 @@ Proof. generalize (typesize_pos a); omega. Qed. +Remark size_arguments_64_above: + forall tyl ir fr ofs0, + ofs0 <= size_arguments_64 tyl ir fr ofs0. +Proof. + induction tyl; simpl; intros. + omega. + assert (A: ofs0 <= + match list_nth_z int_param_regs ir with + | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 + | None => size_arguments_64 tyl ir fr (ofs0 + 2) + end). + { destruct (list_nth_z int_param_regs ir); eauto. + apply Zle_trans with (ofs0 + 2); auto. omega. } + assert (B: ofs0 <= + match list_nth_z float_param_regs fr with + | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 + | None => size_arguments_64 tyl ir fr (ofs0 + 2) + end). + { destruct (list_nth_z float_param_regs fr); eauto. + apply Zle_trans with (ofs0 + 2); auto. omega. } + destruct a; auto. +Qed. + Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. intros; unfold size_arguments. apply Zle_ge. - apply size_arguments_rec_above. + destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above]. Qed. -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> - ofs + typesize ty <= size_arguments s. +Lemma loc_arguments_32_bounded: + forall ofs ty tyl ofs0, + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) -> + ofs + typesize ty <= size_arguments_32 tyl ofs0. Proof. - intros until ty. unfold loc_arguments, size_arguments. generalize (sig_args s) 0. - induction l as [ | t l]; simpl; intros x IN. + induction tyl as [ | t l]; simpl; intros x IN. - contradiction. - rewrite in_app_iff in IN; destruct IN as [IN|IN]. -+ apply Zle_trans with (x + typesize t); [|apply size_arguments_rec_above]. ++ apply Zle_trans with (x + typesize t); [|apply size_arguments_32_above]. Ltac decomp := match goal with | [ H: _ \/ _ |- _ ] => destruct H; decomp @@ -233,8 +411,63 @@ Proof. + apply IHl; auto. Qed. +Lemma loc_arguments_64_bounded: + forall ofs ty tyl ir fr ofs0, + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) -> + ofs + typesize ty <= size_arguments_64 tyl ir fr ofs0. +Proof. + induction tyl; simpl; intros. + contradiction. + assert (T: forall ty0, typesize ty0 <= 2). + { destruct ty0; simpl; omega. } + assert (A: forall ty0, + In (S Outgoing ofs ty) (regs_of_rpairs + match list_nth_z int_param_regs ir with + | Some ireg => + One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs0 + | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) + end) -> + ofs + typesize ty <= + match list_nth_z int_param_regs ir with + | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 + | None => size_arguments_64 tyl ir fr (ofs0 + 2) + end). + { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. + - discriminate. + - eapply IHtyl; eauto. + - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - eapply IHtyl; eauto. } + assert (B: forall ty0, + In (S Outgoing ofs ty) (regs_of_rpairs + match list_nth_z float_param_regs fr with + | Some ireg => + One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs0 + | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) + end) -> + ofs + typesize ty <= + match list_nth_z float_param_regs fr with + | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 + | None => size_arguments_64 tyl ir fr (ofs0 + 2) + end). + { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. + - discriminate. + - eapply IHtyl; eauto. + - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - eapply IHtyl; eauto. } + destruct a; eauto. +Qed. + +Lemma loc_arguments_bounded: + forall (s: signature) (ofs: Z) (ty: typ), + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> + ofs + typesize ty <= size_arguments s. +Proof. + unfold loc_arguments, size_arguments; intros. + destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded. +Qed. + Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. - reflexivity. + unfold loc_arguments; destruct Archi.ptr64; reflexivity. Qed. |