From f642817f0dc761e51c3bd362f75b0068a8d4b0c8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 28 Apr 2017 15:56:59 +0200 Subject: RISC-V port and assorted changes This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress. --- riscV/Conventions1.v | 436 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 436 insertions(+) create mode 100644 riscV/Conventions1.v (limited to 'riscV/Conventions1.v') diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v new file mode 100644 index 00000000..922f878a --- /dev/null +++ b/riscV/Conventions1.v @@ -0,0 +1,436 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* 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 + 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 + | 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 := + R5 :: R6 :: R7 :: + R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: + R28 :: R29 :: R30 :: + nil. + +Definition float_caller_save_regs := + 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 := + R8 :: R9 :: + R18 :: R19 :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: + nil. + +Definition float_callee_save_regs := + 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 is_float_reg (r: mreg) := + match r with + | 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. + +(** * 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 + | None => One R10 + | Some (Tint | Tany32) => One R10 + | Some (Tfloat | Tsingle | Tany64) => One F10 + | Some Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10 + 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) as [[]|]; auto; destruct Archi.ptr64; 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, is_callee_save; + destruct (sig_res s) as [[]|]; 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. *) + +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.splitlong = true + end. +Proof. + intros. change Archi.splitlong with (negb Archi.ptr64). + unfold loc_result; destruct (sig_res sg) as [[]|]; auto. + unfold mreg_type; destruct Archi.ptr64; 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. 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 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. + +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 1)) + 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 + | (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 (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); 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 int_param_regs). + { red. decide_goal. } + assert (E: OKREGS float_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 *) + destruct (va && negb Archi.ptr64). + apply C; auto. + apply A; auto. ++ (* long *) + destruct Archi.ptr64. + apply A; auto. + apply B; auto. ++ (* single *) + apply A; auto. ++ (* any32 *) + apply A; auto. ++ (* any64 *) + destruct (va && negb Archi.ptr64). + apply C; auto. + 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 Zle_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 Zle_trans. eapply B; eauto. apply Zge_le. apply fold_max_outgoing_above. + + apply IHl; auto. + } + apply C. +Qed. + +Lemma loc_arguments_main: + loc_arguments signature_main = nil. +Proof. + reflexivity. +Qed. -- cgit