diff options
Diffstat (limited to 'mppa_k1c/Conventions1.v')
| -rw-r--r-- | mppa_k1c/Conventions1.v | 418 |
1 files changed, 0 insertions, 418 deletions
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v deleted file mode 100644 index ab30ded9..00000000 --- a/mppa_k1c/Conventions1.v +++ /dev/null @@ -1,418 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* Xavier Leroy INRIA Paris-Rocquencourt *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. 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 Machregs Locations. - -(** * Classification of machine registers *) - -(** Machine registers (type [mreg] in module [Locations]) are divided in - the following groups: -- 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 RISC-V application binary interface (ABI) in our choice - of callee- and caller-save registers. -*) - -Definition is_callee_save (r: mreg) : bool := - match r with - (* | R15 | R16 | R17 *) | R18 | R19 | R20 | R21 | R22 - | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 | R31 => true - | _ => false - end. - -Definition int_caller_save_regs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 - :: R10 :: R11 :: R15 (* :: R16 *) :: R17 - (* :: R32 *) :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 :: R40 :: R41 - :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49 :: R50 :: R51 - :: R52 :: R53 :: R54 :: R55 :: R56 :: R57 :: R58 :: R59 :: R60 :: R61 - :: R62 :: R63 :: nil. - -Definition float_caller_save_regs : list mreg := nil. - -Definition int_callee_save_regs := - (* R15 :: R16 :: R17 :: *)R18 :: R19 :: R20 :: R21 :: R22 - :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R31 :: nil. - -Definition float_callee_save_regs : list mreg := nil. - -Definition destroyed_at_call := - List.filter (fun r => negb (is_callee_save r)) all_mregs. - -Definition dummy_int_reg := R63. (**r Used in [Coloring]. *) -Definition dummy_float_reg := R62. (**r Used in [Coloring]. *) - -Definition callee_save_type := mreg_type. - -Definition is_float_reg (r: mreg) := false. - -(** * 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. To ensure binary interoperability of code generated by our - compiler with libraries compiled by another compiler, we - implement the standard RISC-V conventions. *) - -(** ** Location of function result *) - -(** The result value of a function is passed back to the caller in - registers [R10] or [F10] or [R10,R11], 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 - | Tvoid => One R0 - | Tint8signed => One R0 - | Tint8unsigned => One R0 - | Tint16signed => One R0 - | Tint16unsigned => One R0 - | Tint | Tany32 => One R0 - | Tfloat | Tsingle | Tany64 => One R0 - | Tlong => if Archi.ptr64 then One R0 else One R0 - 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, mreg_type. - destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial. -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, is_callee_save; - destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; 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 /\ proj_sig_res sg = 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); auto; - unfold mreg_type; try destruct Archi.ptr64; auto; - destruct t; auto. -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 RISC-V ABI states the following convention for passing arguments - to a function: - -- Arguments are passed in registers when possible. - -- Up to eight integer registers (ai: int_param_regs) and up to eight - floating-point registers (fai: float_param_regs) are used for this - purpose. - -- If the arguments to a function are conceptualized as fields of a C - struct, each with pointer alignment, the argument registers are a - shadow of the first eight pointer-words of that struct. If argument - i < 8 is a floating-point type, it is passed in floating-point - register fa_i; otherwise, it is passed in integer register a_i. - -- When primitive arguments twice the size of a pointer-word are passed - on the stack, they are naturally aligned. When they are passed in the - integer registers, they reside in an aligned even-odd register pair, - with the even register holding the least-significant bits. - -- Floating-point arguments to variadic functions (except those that - are explicitly named in the parameter list) are passed in integer - registers. - -- The portion of the conceptual struct that is not passed in argument - registers is passed on the stack. The stack pointer sp points to the - first argument not passed in a register. - -The bit about variadic functions doesn't quite fit CompCert's model. -We do our best by passing the FP arguments in registers, as usual, -and reserving the corresponding integer registers, so that fixup -code can be introduced in the Asmexpand pass. -*) - -Definition param_regs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: nil. - -Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ) - (rec: Z -> Z -> list (rpair loc)) := - match list_nth_z regs rn with - | Some r => - One(R r) :: rec (rn + 1) ofs - | None => - let ofs := align ofs (typealign ty) in - One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty)) - end. - -Definition two_args (regs: list mreg) (rn: Z) (ofs: Z) - (rec: Z -> Z -> list (rpair loc)) := - let rn := align rn 2 in - match list_nth_z regs rn, list_nth_z regs (rn + 1) with - | Some r1, Some r2 => - Twolong (R r2) (R r1) :: rec (rn + 2) ofs - | _, _ => - let ofs := align ofs 2 in - Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: - rec rn (ofs + 2) - end. - -Definition hybrid_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ) - (rec: Z -> Z -> list (rpair loc)) := - let rn := align rn 2 in - match list_nth_z regs rn with - | Some r => - One (R r) :: rec (rn + 2) ofs - | None => - let ofs := align ofs 2 in - One (S Outgoing ofs ty) :: rec rn (ofs + 2) - end. - -Fixpoint loc_arguments_rec (va: bool) - (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) := - match tyl with - | nil => nil - | ty :: tys => one_arg param_regs r ofs ty (loc_arguments_rec va tys) -(* - | (Tint | Tany32) as ty :: tys => - one_arg int_param_regs r ofs ty (loc_arguments_rec va tys) - | Tsingle as ty :: tys => - one_arg float_param_regs r ofs ty (loc_arguments_rec va tys) - | Tlong as ty :: tys => - if Archi.ptr64 - then one_arg int_param_regs r ofs ty (loc_arguments_rec va tys) - else two_args int_param_regs r ofs (loc_arguments_rec va tys) - | (Tfloat | Tany64) as ty :: tys => - if va && negb Archi.ptr64 - then hybrid_arg float_param_regs r ofs ty (loc_arguments_rec va tys) - else one_arg float_param_regs r ofs ty (loc_arguments_rec va tys) -*) - 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_cc).(cc_vararg) s.(sig_args) 0 0. - -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Definition max_outgoing_1 (accu: Z) (l: loc) : Z := - match l with - | S Outgoing ofs ty => Z.max accu (ofs + typesize ty) - | _ => accu - end. - -Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z := - match rl with - | One l => max_outgoing_1 accu l - | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2 - end. - -Definition size_arguments (s: signature) : Z := - List.fold_left max_outgoing_2 (loc_arguments s) 0. - -(** Argument locations are either non-temporary 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. - -Lemma loc_arguments_rec_charact: - forall va tyl rn ofs p, - ofs >= 0 -> - In p (loc_arguments_rec va tyl rn ofs) -> forall_rpair loc_argument_acceptable p. -Proof. - set (OK := fun (l: list (rpair loc)) => - forall p, In p l -> forall_rpair loc_argument_acceptable p). - set (OKF := fun (f: Z -> Z -> list (rpair loc)) => - forall rn ofs, ofs >= 0 -> OK (f rn ofs)). - set (OKREGS := fun (l: list mreg) => forall r, In r l -> is_callee_save r = false). - assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0). - { intros. - assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos). - omega. } - assert (SK: (if Archi.ptr64 then 2 else 1) > 0). - { destruct Archi.ptr64; omega. } - assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). - { intros. destruct Archi.ptr64. omega. apply typesize_pos. } - assert (A: forall regs rn ofs ty f, - OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). - { intros until f; intros OR OF OO; red; unfold one_arg; intros. - destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. - - eapply OF; eauto. - - subst p; simpl. auto using align_divides, typealign_pos. - - eapply OF; [idtac|eauto]. - generalize (AL ofs ty OO) (SKK ty); omega. - } - assert (B: forall regs rn ofs f, - OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)). - { intros until f; intros OR OF OO; unfold two_args. - set (rn' := align rn 2). - set (ofs' := align ofs 2). - assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto). - assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint) - :: f rn' (ofs' + 2))). - { red; simpl; intros. destruct H. - - subst p; simpl. - repeat split; auto using Z.divide_1_l. omega. - - eapply OF; [idtac|eauto]. omega. - } - destruct (list_nth_z regs rn') as [r1|] eqn:NTH1; - destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2; - try apply DFL. - red; simpl; intros; destruct H. - - subst p; simpl. split; apply OR; eauto using list_nth_z_in. - - eapply OF; [idtac|eauto]. auto. - } - assert (C: forall regs rn ofs ty f, - OKREGS regs -> OKF f -> ofs >= 0 -> typealign ty = 1 -> OK (hybrid_arg regs rn ofs ty f)). - { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros. - set (rn' := align rn 2) in *. - destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. - - eapply OF; eauto. - - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. - - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega. - } - assert (D: OKREGS param_regs). - { red. decide_goal. } - assert (E: OKREGS param_regs). - { red. decide_goal. } - - cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)). - unfold OK. eauto. - induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. - - red; simpl; tauto. - - destruct ty1. -+ (* int *) apply A; auto. -+ (* float *) - apply A; auto. -+ (* long *) - apply A; auto. -+ (* single *) - apply A; auto. -+ (* any32 *) - apply A; auto. -+ (* any64 *) - apply A; auto. -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. eapply loc_arguments_rec_charact; eauto. omega. -Qed. - -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark fold_max_outgoing_above: - forall l n, fold_left max_outgoing_2 l n >= n. -Proof. - assert (A: forall n l, max_outgoing_1 n l >= n). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } - induction l; simpl; intros. - - omega. - - eapply Zge_trans. eauto. - destruct a; simpl. apply A. eapply Zge_trans; eauto. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros. apply fold_max_outgoing_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. -Proof. - intros until ty. - assert (A: forall n l, n <= max_outgoing_1 n l). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } - assert (B: forall p n, - In (S Outgoing ofs ty) (regs_of_rpair p) -> - ofs + typesize ty <= max_outgoing_2 n p). - { intros. destruct p; simpl in H; intuition; subst; simpl. - - xomega. - - eapply Z.le_trans. 2: apply A. xomega. - - xomega. } - assert (C: forall l n, - In (S Outgoing ofs ty) (regs_of_rpairs l) -> - ofs + typesize ty <= fold_left max_outgoing_2 l n). - { induction l; simpl; intros. - - contradiction. - - rewrite in_app_iff in H. destruct H. - + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. - + apply IHl; auto. - } - apply C. -Qed. - -Lemma loc_arguments_main: - loc_arguments signature_main = nil. -Proof. - reflexivity. -Qed. - - -Definition return_value_needs_normalization (t: rettype) : bool := false. |