From 7cdd676d002e33015b496f609538a9e86d77c543 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 8 Aug 2019 11:18:38 +0200 Subject: AArch64 port This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. --- aarch64/Conventions1.v | 380 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 380 insertions(+) create mode 100644 aarch64/Conventions1.v (limited to 'aarch64/Conventions1.v') diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v new file mode 100644 index 00000000..5914e8f2 --- /dev/null +++ b/aarch64/Conventions1.v @@ -0,0 +1,380 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and INRIA Paris *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Function calling conventions and other conventions regarding the use of + machine registers and stack slots. *) + +Require Import Coqlib Decidableplus. +Require Import AST Events Locations. +Require Archi. + +(** * Classification of machine registers *) + +(** Machine registers (type [mreg] in module [Locations]) are divided in: +- 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 Procedure Call Standard for the ARM 64-bit Architecture + (AArch64) document: R19-R28 and F8-F15 are callee-save. *) + +Definition is_callee_save (r: mreg): bool := + match r with + | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 => false + | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => false + | R17 => false + | R19 | R20 | R21 | R22 | R23 => true + | R24 | R25 | R26 | R27 | R28 => true + | R29 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 => false + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 => true + | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 => false + | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => false + end. + +Definition int_caller_save_regs := + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 + :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 + :: R17 :: R29 :: nil. + +Definition float_caller_save_regs := + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 + :: F16 :: F17 :: F18 :: F19 :: F20 :: F21 :: F22 :: F23 + :: F24 :: F25 :: F26 :: F27 :: F28 :: F29 :: F30 :: F31 :: nil. + +Definition int_callee_save_regs := + R19 :: R20 :: R21 :: R22 :: R23 + :: R24 :: R25 :: R26 :: R27 :: R28 :: nil. + +Definition float_callee_save_regs := + F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil. + +Definition destroyed_at_call := + List.filter (fun r => negb (is_callee_save r)) all_mregs. + +Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) +Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) + +Definition callee_save_type := mreg_type. + +Definition is_float_reg (r: mreg): bool := + match r with + | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 + | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 + | R17 | R19 | R20 | R21 | R22 | R23 + | R24 | R25 | R26 | R27 | R28 + | R29 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 + | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 + | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true + end. + +(** * Function calling conventions *) + +(** The functions in this section determine the locations (machine registers + and stack slots) used to communicate arguments and results between the + caller and the callee during function calls. These locations are functions + of the signature of the function and of the call instruction. + Agreement between the caller and the callee on the locations to use + is guaranteed by our dynamic semantics for Cminor and RTL, which demand + that the signature of the call instruction is identical to that of the + called function. + + Calling conventions are largely arbitrary: they must respect the properties + proved in this section (such as no overlapping between the locations + of function arguments), but this leaves much liberty in choosing actual + locations. *) + +(** ** Location of function result *) + +(** The result value of a function is passed back to the caller in + registers [R0] or [F0], 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 := + match s.(sig_res) with + | None => One R0 + | Some (Tint | Tlong | Tany32 | Tany64) => One R0 + | Some (Tfloat | Tsingle) => One F0 + end. + +(** 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. +Qed. + +(** The result locations are caller-save registers *) + +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. +Qed. + +(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) + +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 + /\ Archi.ptr64 = false + end. +Proof. + intros; unfold loc_result; destruct (sig_res sg) as [[]|]; exact I. +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. rewrite H; auto. +Qed. + +(** ** Location of function arguments *) + +(** +- The first 8 integer arguments are passed in registers [R0...R7]. +- The first 8 FP arguments are passed in registers [F0...F7]. +- Extra arguments are passed on the stack, in [Outgoing] slots of size + 64 bits (2 words), consecutively assigned, starting at word offset 0. +**) + +Definition int_param_regs := + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: nil. + +Definition float_param_regs := + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. + +Fixpoint loc_arguments_rec + (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_rec tys ir fr (ofs + 2) + | Some ireg => + One (R ireg) :: loc_arguments_rec 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_rec tys ir fr (ofs + 2) + | Some freg => + One (R freg) :: loc_arguments_rec 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 0 0. + +(** [size_arguments s] returns the number of [Outgoing] slots used + to call a function with signature [s]. *) + +Fixpoint size_arguments_rec (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_rec tys ir fr (ofs + 2) + | Some ireg => size_arguments_rec tys (ir + 1) fr ofs + end + | (Tfloat | Tsingle) :: tys => + match list_nth_z float_param_regs fr with + | None => size_arguments_rec tys ir fr (ofs + 2) + | Some freg => size_arguments_rec tys ir (fr + 1) ofs + end + end. + +Definition size_arguments (s: signature) : Z := + size_arguments_rec s.(sig_args) 0 0 0. + +(** Argument locations are either caller-save registers or [Outgoing] + stack slots at nonnegative offsets. *) + +Definition loc_argument_acceptable (l: loc) : Prop := + match l with + | R r => is_callee_save r = false + | S Outgoing ofs ty => ofs >= 0 /\ (typealign ty | ofs) + | _ => False + end. + +Definition loc_argument_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_rec_charact: + forall tyl ir fr ofs p, + In p (loc_arguments_rec tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_charact ofs) p. +Proof. + assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l). + { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_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 Z.divide_refl. } +Opaque list_nth_z. + induction tyl; simpl loc_arguments_rec; intros. +- contradiction. +- assert (A: forall ty, In p + match list_nth_z int_param_regs ir with + | Some ireg => One (R ireg) :: loc_arguments_rec tyl (ir + 1) fr ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_rec tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_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_rec tyl ir (fr + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_rec tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_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. + assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by 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_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_charact, loc_argument_acceptable. + destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. + intros [C D]. split; auto. apply Z.divide_trans with 2; auto. + exists (2 / typealign ty); destruct ty; reflexivity. + } + exploit loc_arguments_rec_charact; eauto using Z.divide_0_r. + 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 ir fr ofs0, + ofs0 <= size_arguments_rec 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_rec tyl (ir + 1) fr ofs0 + | None => size_arguments_rec tyl ir fr (ofs0 + 2) + end). + { destruct (list_nth_z int_param_regs ir); eauto. + apply Z.le_trans with (ofs0 + 2); auto. omega. } + assert (B: ofs0 <= + match list_nth_z float_param_regs fr with + | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0 + | None => size_arguments_rec tyl ir fr (ofs0 + 2) + end). + { destruct (list_nth_z float_param_regs fr); eauto. + apply Z.le_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 Z.le_ge. apply size_arguments_rec_above. +Qed. + +Lemma loc_arguments_rec_bounded: + forall ofs ty tyl ir fr ofs0, + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) -> + ofs + typesize ty <= size_arguments_rec 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_rec tyl (ir + 1) fr ofs0 + | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2) + end) -> + ofs + typesize ty <= + match list_nth_z int_param_regs ir with + | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0 + | None => size_arguments_rec 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 Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_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_rec tyl ir (fr + 1) ofs0 + | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2) + end) -> + ofs + typesize ty <= + match list_nth_z float_param_regs fr with + | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0 + | None => size_arguments_rec 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 Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_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. + eauto using loc_arguments_rec_bounded. +Qed. + +Lemma loc_arguments_main: + loc_arguments signature_main = nil. +Proof. + unfold loc_arguments; reflexivity. +Qed. + -- cgit