diff options
Diffstat (limited to 'verilog/Conventions1.v')
| -rw-r--r-- | verilog/Conventions1.v | 569 |
1 files changed, 269 insertions, 300 deletions
diff --git a/verilog/Conventions1.v b/verilog/Conventions1.v index b6fb2620..eeaae3c4 100644 --- a/verilog/Conventions1.v +++ b/verilog/Conventions1.v @@ -2,12 +2,17 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Prashanth Mundkur, SRI International *) (* *) (* 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. *) (* *) +(* The contributions by Prashanth Mundkur are reused and adapted *) +(* under the terms of a Contributor License Agreement between *) +(* SRI International and INRIA. *) +(* *) (* *********************************************************************) (** Function calling conventions and other conventions regarding the use of @@ -15,7 +20,6 @@ Require Import Coqlib Decidableplus. Require Import AST Machregs Locations. -Require Import Errors. (** * Classification of machine registers *) @@ -24,65 +28,67 @@ Require Import Errors. - 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 and x86-64 application binary interfaces (ABI) - in our choice of callee- and caller-save registers. + 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 - | AX | CX | DX => false - | BX | BP => true - | SI | DI => negb Archi.ptr64 || Archi.win64 (**r callee-save in ELF 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 => Archi.win64 - | FP0 => false + | R5 | R6 | R7 => false + | R8 | R9 => true + | R10 | R11 | R12 | R13 | R14 | R15 | R16 | R17 => false + | R18 | R19 | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 => true + | R28 | R29 | R30 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 => false + | F8 | F9 => true + | F10 | F11 | F12 | F13 | F14 | F15 | F16 | F17 => false + | F18 | F19 | F20 | F21 | F22 | F23 | F24 | F25 | F26 | F27 => true + | F28 | F29 | F30 | F31 => false end. Definition int_caller_save_regs := - if Archi.ptr64 - then if Archi.win64 - then AX :: CX :: DX :: R8 :: R9 :: R10 :: R11 :: nil - else AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil - else AX :: CX :: DX :: nil. + R5 :: R6 :: R7 :: + R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: + R28 :: R29 :: R30 :: + nil. Definition float_caller_save_regs := - if Archi.ptr64 - then if Archi.win64 - then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: nil - else 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. + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: + F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: + F28 :: F29 :: F30 :: F31 :: + nil. Definition int_callee_save_regs := - if Archi.ptr64 - then if Archi.win64 - then BX :: SI :: DI :: BP :: R12 :: R13 :: R14 :: R15 :: nil - else BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil - else BX :: SI :: DI :: BP :: nil. + R8 :: R9 :: + R18 :: R19 :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: + nil. Definition float_callee_save_regs := - if Archi.ptr64 && Archi.win64 - then X6 :: X7 :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil - else nil. + F8 :: F9 :: + F18 :: F19 :: F20 :: F21 :: F22 :: F23 :: F24 :: F25 :: F26 :: F27 :: + nil. Definition destroyed_at_call := List.filter (fun r => negb (is_callee_save r)) all_mregs. +Definition dummy_int_reg := R6. (**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) := 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 + | R5 | R6 | R7 | R8 | R9 | R10 | R11 + | R12 | R13 | R14 | R15 | R16 | R17 | R18 | R19 + | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 + | R28 | R29 | R30 => 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. -Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) -Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) - -Definition callee_save_type := mreg_type. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -99,43 +105,32 @@ Definition callee_save_type := mreg_type. 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-32 and x86-64 conventions. *) + implement the standard RISC-V conventions as found here: + https://github.com/riscv/riscv-elf-psabi-doc/blob/master/riscv-elf.md +*) (** ** Location of function 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_32 (s: signature) : rpair mreg := - match proj_sig_res s with - | Tint | Tany32 => One AX - | Tfloat | Tsingle => One FP0 - | Tany64 => One X0 - | 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]. *) +(** 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_64 (s: signature) : rpair mreg := +Definition loc_result (s: signature) : rpair mreg := match proj_sig_res s with - | Tint | Tlong | Tany32 | Tany64 => One AX - | Tfloat | Tsingle => One X0 + | Tint | Tany32 => One R10 + | Tfloat | Tsingle | Tany64 => One F10 + | Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10 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 loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (proj_sig_res sig); auto. + intros. unfold loc_result, mreg_type; + destruct (proj_sig_res sig); auto; destruct Archi.ptr64; auto. Qed. (** The result locations are caller-save registers *) @@ -144,8 +139,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, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. + intros. unfold loc_result, is_callee_save; + destruct (proj_sig_res s); simpl; auto; destruct Archi.ptr64; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -156,13 +151,13 @@ Lemma loc_result_pair: | One _ => True | Twolong r1 r2 => r1 <> r2 /\ proj_sig_res sg = Tlong - /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. - intros. - unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (proj_sig_res sg); auto. + intros. + unfold loc_result; destruct (proj_sig_res sg); auto. + unfold mreg_type; destruct Archi.ptr64; auto. split; auto. congruence. Qed. @@ -171,104 +166,146 @@ Qed. 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, proj_sig_res. - destruct Archi.ptr64; rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) -(** In the x86-32 ABI, all arguments are passed on stack. (Snif.) *) +(** The RISC-V ABI states the following conventions for passing arguments + to a function. First for non-variadic functions: -Fixpoint loc_arguments_32 - (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) := - match tyl with - | nil => nil - | ty :: tys => - match ty with - | Tlong => Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) - | _ => One (S Outgoing ofs ty) - end - :: loc_arguments_32 tys (ofs + typesize ty) - end. +- RV64: pass the first 8 integer arguments in integer registers + (a1...a8: int_param_regs), the first 8 FP arguments in FP registers + (fa1...fa8: float_param_regs) then in integer registers (a1...a8), + and the remaining arguments on the stack, in 8-byte slots. + +- RV32: same, but arguments of size 64 bits that must be passed in + integer registers are passed in two consecutive integer registers + (a(i), a(i+1)), or in a(8) and on a 32-bit word on the stack. + Stack-allocated arguments are aligned to their natural alignment. + +For variadic functions, the fixed arguments are passed as described +above, then the variadic arguments receive special treatment: -(** In the x86-64 ELF 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. +- RV64: FP registers are not used for passing variadic arguments. + All variadic arguments, including FP arguments, are passed in the + remaining integer registers (a1...a8), then on the stack, in 8-byte + slots. + +- RV32: likewise, but arguments of 64-bit types (integers as well + as floats) are passed in two consecutive aligned integer registers + (a(2i), a(2i+1)), or on the stack, in aligned 8-byte slots. + +The passing of FP arguments to variadic functions in integer registers +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 int_param_regs_elf64 := DI :: SI :: DX :: CX :: R8 :: R9 :: nil. -Definition float_param_regs_elf64 := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. +Definition int_param_regs := + R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. +Definition float_param_regs := + F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil. + +(** To evaluate FP arguments that must be passed in integer registers, + we can use any FP caller-save register that is not already used to pass + a fixed FP argument. Since there are 8 integer registers for argument + passing, we need at most 8 extra more FP registers for these FP + arguments. *) + +Definition float_extra_param_regs := + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. + +Definition int_arg (ri rf ofs: Z) (ty: typ) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match list_nth_z int_param_regs ri with + | Some r => + One(R r) :: rec (ri + 1) rf ofs + | None => + let ofs := align ofs (typesize ty) in + One(S Outgoing ofs ty) + :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) + end. -Fixpoint loc_arguments_elf64 - (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_elf64 ir with - | None => - One (S Outgoing ofs ty) :: loc_arguments_elf64 tys ir fr (ofs + 2) - | Some ireg => - One (R ireg) :: loc_arguments_elf64 tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle) as ty :: tys => - match list_nth_z float_param_regs_elf64 fr with +Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match list_nth_z (if va then nil else float_param_regs) rf with + | Some r => + One (R r) :: rec ri (rf + 1) ofs + | None => + (* We are out of FP registers, or cannot use them because vararg, + so try to put the argument in an extra FP register while + reserving an integer register or register pair into which + fixup code will move the extra FP register. *) + let regpair := negb Archi.ptr64 && zeq (typesize ty) 2 in + let ri' := if va && regpair then align ri 2 else ri in + match list_nth_z float_extra_param_regs ri' with + | Some r => + let ri'' := ri' + (if Archi.ptr64 then 1 else typesize ty) in + let ofs'' := if regpair && zeq ri' 7 then ofs + 1 else ofs in + One (R r) :: rec ri'' rf ofs'' | None => - One (S Outgoing ofs ty) :: loc_arguments_elf64 tys ir fr (ofs + 2) - | Some freg => - One (R freg) :: loc_arguments_elf64 tys ir (fr + 1) ofs + (* We are out of integer registers, pass argument on stack *) + let ofs := align ofs (typesize ty) in + One(S Outgoing ofs ty) + :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) end end. -(** In the x86-64 Win64 ABI: -- The first 4 arguments are passed in registers [RCX], [RDX], [R8], and [R9] - (for integer arguments) and [X0] to [X3] (for floating-point arguments). - Each argument "burns" both an integer register and a FP integer. -- 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. -- Four 8-byte words are always reserved at the bottom of the outgoing area - so that the callee can use them to save the registers containing the - first four arguments. This is handled in the Stacking phase. -*) - -Definition int_param_regs_win64 := CX :: DX :: R8 :: R9 :: nil. -Definition float_param_regs_win64 := X0 :: X1 :: X2 :: X3 :: nil. +Definition split_long_arg (va: bool) (ri rf ofs: Z) + (rec: Z -> Z -> Z -> list (rpair loc)) := + let ri := if va then align ri 2 else ri in + match list_nth_z int_param_regs ri, list_nth_z int_param_regs (ri + 1) with + | Some r1, Some r2 => + Twolong (R r2) (R r1) :: rec (ri + 2) rf ofs + | Some r1, None => + Twolong (S Outgoing ofs Tint) (R r1) :: rec (ri + 1) rf (ofs + 1) + | None, _ => + let ofs := align ofs 2 in + Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: + rec ri rf (ofs + 2) + end. -Fixpoint loc_arguments_win64 - (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) := +Fixpoint loc_arguments_rec + (tyl: list typ) (fixed ri rf 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_win64 r with - | None => - One (S Outgoing ofs ty) :: loc_arguments_win64 tys r (ofs + 2) - | Some ireg => - One (R ireg) :: loc_arguments_win64 tys (r + 1) ofs - end - | (Tfloat | Tsingle) as ty :: tys => - match list_nth_z float_param_regs_win64 r with - | None => - One (S Outgoing ofs ty) :: loc_arguments_win64 tys r (ofs + 2) - | Some freg => - One (R freg) :: loc_arguments_win64 tys (r + 1) ofs - end + | (Tint | Tany32) as ty :: tys => + (* pass in one integer register or on stack *) + int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) + | Tsingle as ty :: tys => + (* pass in one FP register or on stack. + If vararg, reserve 1 integer register. *) + float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) + | Tlong as ty :: tys => + if Archi.ptr64 then + (* pass in one integer register or on stack *) + int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) + else + (* pass in register pair or on stack; align register pair if vararg *) + split_long_arg (zle fixed 0) ri rf ofs(loc_arguments_rec tys (fixed - 1)) + | (Tfloat | Tany64) as ty :: tys => + (* pass in one FP register or on stack. + If vararg, reserve 1 or 2 integer registers. *) + float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) + end. + +(** Number of fixed arguments for a function with signature [s]. *) + +Definition fixed_arguments (s: signature) : Z := + match s.(sig_cc).(cc_vararg) with + | Some n => n + | None => list_length_z s.(sig_args) 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) := - if Archi.ptr64 - then if Archi.win64 - then loc_arguments_win64 s.(sig_args) 0 0 - else loc_arguments_elf64 s.(sig_args) 0 0 0 - else loc_arguments_32 s.(sig_args) 0. + loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0. -(** Argument locations are either caller-save registers or [Outgoing] +(** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) Definition loc_argument_acceptable (l: loc) : Prop := @@ -278,175 +315,107 @@ Definition loc_argument_acceptable (l: loc) : Prop := | _ => False end. -Definition loc_argument_32_charact (ofs: Z) (l: loc) : Prop := - match l with - | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 - | _ => False - end. - -Definition loc_argument_elf64_charact (ofs: Z) (l: loc) : Prop := - match l with - | R r => In r int_param_regs_elf64 \/ In r float_param_regs_elf64 - | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') - | _ => False - end. - -Definition loc_argument_win64_charact (ofs: Z) (l: loc) : Prop := - match l with - | R r => In r int_param_regs_win64 \/ In r float_param_regs_win64 - | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') - | _ => False - end. - -Remark loc_arguments_32_charact: - forall tyl 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_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } - induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros. -- contradiction. -- destruct H. -+ destruct ty; subst p; simpl; lia. -+ apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *. -* eapply X; eauto; lia. -* destruct H; split; eapply X; eauto; lia. -Qed. - -Remark loc_arguments_elf64_charact: - forall tyl ir fr ofs p, - In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p. +Lemma loc_arguments_rec_charact: + forall va tyl ri rf ofs p, + ofs >= 0 -> + In p (loc_arguments_rec va tyl ri rf ofs) -> forall_rpair loc_argument_acceptable p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_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_elf64; intros. - elim H. - assert (A: forall ty, In p - match list_nth_z int_param_regs_elf64 ir with - | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl (ir + 1) fr ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_elf64 tyl ir fr (ofs + 2) - end -> - forall_rpair (loc_argument_elf64_charact ofs) p). - { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1. - subst. left. eapply list_nth_z_in; eauto. - eapply IHtyl; eauto. - subst. split. lia. assumption. - eapply Y; eauto. lia. } - assert (B: forall ty, In p - match list_nth_z float_param_regs_elf64 fr with - | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_elf64 tyl ir fr (ofs + 2) - end -> - forall_rpair (loc_argument_elf64_charact ofs) p). - { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1. - subst. right. eapply list_nth_z_in; eauto. - eapply IHtyl; eauto. - subst. split. lia. assumption. - eapply Y; eauto. lia. } - destruct a; eauto. -Qed. - -Remark loc_arguments_win64_charact: - forall tyl r ofs p, - In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p. -Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_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_win64; intros. - elim H. - assert (A: forall ty, In p - match list_nth_z int_param_regs_win64 r with - | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_win64 tyl r (ofs + 2) - end -> - forall_rpair (loc_argument_win64_charact ofs) p). - { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1. - subst. left. eapply list_nth_z_in; eauto. - eapply IHtyl; eauto. - subst. split. lia. assumption. - eapply Y; eauto. lia. } - assert (B: forall ty, In p - match list_nth_z float_param_regs_win64 r with - | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_win64 tyl r (ofs + 2) - end -> - forall_rpair (loc_argument_win64_charact ofs) p). - { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1. - subst. right. eapply list_nth_z_in; eauto. - eapply IHtyl; eauto. - subst. split. lia. assumption. - eapply Y; eauto. lia. } - destruct a; eauto. + set (OK := fun (l: list (rpair loc)) => + forall p, In p l -> forall_rpair loc_argument_acceptable p). + set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) => + forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)). + assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false). + { decide_goal. } + assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false). + { decide_goal. } + assert (CSFX: forall r, In r float_extra_param_regs -> is_callee_save r = false). + { decide_goal. } + assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0). + { intros. + assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos). + lia. } + assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))). + { intros. eapply Z.divide_trans. apply typealign_typesize. + apply align_divides. apply typesize_pos. } + assert (SK: (if Archi.ptr64 then 2 else 1) > 0). + { destruct Archi.ptr64; lia. } + assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). + { intros. destruct Archi.ptr64. lia. apply typesize_pos. } + assert (A: forall ri rf ofs ty f, + OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)). + { intros until f; intros OF OO; red; unfold int_arg; intros. + destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; destruct H. + - subst p; simpl. apply CSI. 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); lia. + } + assert (B: forall va ri rf ofs ty f, + OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)). + { intros until f; intros OF OO; red; unfold float_arg; intros. + destruct (list_nth_z (if va then nil else float_param_regs) rf) as [r|] eqn:NTH. + - destruct H. + + subst p; simpl. apply CSF. destruct va. simpl in NTH; discriminate. eapply list_nth_z_in; eauto. + + eapply OF; eauto. + - set (regpair := negb Archi.ptr64 && zeq (typesize ty) 2) in *. + set (ri' := if va && regpair then align ri 2 else ri) in *. + destruct (list_nth_z float_extra_param_regs ri') as [r|] eqn:NTH'; destruct H. + + subst p; simpl. apply CSFX. eapply list_nth_z_in; eauto. + + eapply OF; [|eauto]. destruct (regpair && zeq ri' 7); lia. + + subst p; simpl. auto. + + eapply OF; [|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. + } + assert (C: forall va ri rf ofs f, + OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)). + { intros until f; intros OF OO; unfold split_long_arg. + set (ri' := if va then align ri 2 else ri). + set (ofs' := align ofs 2). + assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto). + destruct (list_nth_z int_param_regs ri') as [r1|] eqn:NTH1; + [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac]. + - red; simpl; intros; destruct H. + + subst p; split; apply CSI; eauto using list_nth_z_in. + + eapply OF; [idtac|eauto]. lia. + - red; simpl; intros; destruct H. + + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in. + + eapply OF; [idtac|eauto]. lia. + - red; simpl; intros; destruct H. + + subst p; repeat split; auto using Z.divide_1_l. lia. + + eapply OF; [idtac|eauto]. lia. + } + cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)). + unfold OK. eauto. + induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. +- red; simpl; tauto. +- destruct ty1. ++ (* int *) apply A; unfold OKF; auto. ++ (* float *) apply B; unfold OKF; auto. ++ (* long *) + destruct Archi.ptr64. + apply A; unfold OKF; auto. + apply C; unfold OKF; auto. ++ (* single *) apply B; unfold OKF; auto. ++ (* any32 *) apply A; unfold OKF; auto. ++ (* any64 *) apply B; unfold OKF; 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. destruct Archi.ptr64 eqn:SF; [destruct Archi.win64 eqn:W64|]. -- (* WIN 64 bits *) - assert (A: forall r, In r int_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). - assert (B: forall r, In r float_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; decide_goal). - assert (X: forall l, loc_argument_win64_charact 0 l -> loc_argument_acceptable l). - { unfold loc_argument_win64_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_win64_charact; eauto using Z.divide_0_r. - unfold forall_rpair; destruct p; intuition auto. -- (* ELF 64 bits *) - assert (A: forall r, In r int_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF, W64; decide_goal). - assert (B: forall r, In r float_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite W64; decide_goal). - assert (X: forall l, loc_argument_elf64_charact 0 l -> loc_argument_acceptable l). - { unfold loc_argument_elf64_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_elf64_charact; eauto using Z.divide_0_r. - 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. } - exploit loc_arguments_32_charact; eauto. - unfold forall_rpair; destruct p; intuition auto. + unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. lia. Qed. -Global Hint Resolve loc_arguments_acceptable: locs. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. - unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto. + reflexivity. Qed. (** ** Normalization of function results and parameters *) -(** In the x86 ABI, a return value of type "char" is returned in - register AL, leaving the top 24 bits of EAX unspecified. - Likewise, a return value of type "short" is returned in register - AH, leaving the top 16 bits of EAX unspecified. Hence, return - values of small integer types need re-normalization after calls. *) - -Definition return_value_needs_normalization (t: rettype) : bool := - match t with - | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true - | _ => false - end. - -(** Function parameters are passed in normalized form and do not need - to be re-normalized at function entry. *) +(** No normalization needed. *) +Definition return_value_needs_normalization (t: rettype) := false. Definition parameter_needs_normalization (t: rettype) := false. |