From d6d8cbb001e04d17b096c604850a7973507bbb5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Gourdin?= Date: Wed, 22 Jun 2022 16:52:44 +0200 Subject: [PATCH 1/2] proposed bugfix for issue #436 --- riscV/Asm.v | 7 ++-- riscV/Asmexpand.ml | 76 +++++++++++++++++++++--------------------- riscV/Asmgenproof.v | 3 +- riscV/Conventions1.v | 8 ++--- riscV/Machregs.v | 60 ++++++++++++++++----------------- riscV/TargetPrinter.ml | 2 +- 6 files changed, 80 insertions(+), 76 deletions(-) diff --git a/riscV/Asm.v b/riscV/Asm.v index a47573a2bd..35f1486673 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -751,7 +751,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pj_l l => goto_label f l rs m | Pj_s s sg => - Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m + Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) + #X6 <- Vundef + ) m | Pj_r r sg => Next (rs#PC <- (rs#r)) m | Pjal_s s sg => @@ -1001,7 +1003,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Definition preg_of (r: mreg) : preg := match r with - | R5 => X5 | R6 => X6 | R7 => X7 + | R5 => X5 | R7 => X7 | R8 => X8 | R9 => X9 | R10 => X10 | R11 => X11 | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15 | R16 => X16 | R17 => X17 | R18 => X18 | R19 => X19 @@ -1180,6 +1182,7 @@ Qed. Definition data_preg (r: preg) : bool := match r with | IR RA => false + | IR X6 => false | IR X31 => false | IR _ => true | FR _ => true diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index ab0e6fee0c..e59487e019 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -469,85 +469,85 @@ let expand_bswap64 d s = re-rolled as a loop to produce more compact code. *) let expand_clz ~sixtyfour ~splitlong = - (* Input: X in X5 or (X5, X6) if splitlong - Result: N in X7 - Temporaries: S in X8, Y in X9 *) + (* Input: X in X5 or (X5, X7) if splitlong + Result: N in X8 + Temporaries: S in X6, Y in X9 *) let lbl1 = new_label() in let lbl2 = new_label() in (* N := bitsize of X's type (32 or 64) *) - expand_loadimm32 X7 (coqint_of_camlint + expand_loadimm32 X8 (coqint_of_camlint (if sixtyfour || splitlong then 64l else 32l)); (* S := initial shift amount (16 or 32) *) - expand_loadimm32 X8 (coqint_of_camlint (if sixtyfour then 32l else 16l)); + expand_loadimm32 X6 (coqint_of_camlint (if sixtyfour then 32l else 16l)); if splitlong then begin (* if (Xhigh == 0) goto lbl1 *) - emit (Pbeqw(X X6, X0, lbl1)); + emit (Pbeqw(X X7, X0, lbl1)); (* N := 32 *) - expand_loadimm32 X7 (coqint_of_camlint 32l); + expand_loadimm32 X8 (coqint_of_camlint 32l); (* X := Xhigh *) - emit (Pmv(X5, X6)) + emit (Pmv(X5, X7)) end; (* lbl1: *) emit (Plabel lbl1); (* Y := X >> S *) - emit (if sixtyfour then Psrll(X9, X X5, X X8) else Psrlw(X9, X X5, X X8)); + emit (if sixtyfour then Psrll(X9, X X5, X X6) else Psrlw(X9, X X5, X X6)); (* if (Y == 0) goto lbl2 *) emit (if sixtyfour then Pbeql(X X9, X0, lbl2) else Pbeqw(X X9, X0, lbl2)); (* N := N - S *) - emit (Psubw(X7, X X7, X X8)); + emit (Psubw(X8, X X8, X X6)); (* X := Y *) emit (Pmv(X5, X9)); (* lbl2: *) emit (Plabel lbl2); (* S := S / 2 *) - emit (Psrliw(X8, X X8, _1)); + emit (Psrliw(X6, X X6, _1)); (* if (S != 0) goto lbl1; *) - emit (Pbnew(X X8, X0, lbl1)); + emit (Pbnew(X X6, X0, lbl1)); (* N := N - X *) - emit (Psubw(X7, X X7, X X5)) + emit (Psubw(X8, X X8, X X5)) (* Count trailing zeros. Algorithm 5-14 from Hacker's Delight, re-rolled as a loop to produce more compact code. *) let expand_ctz ~sixtyfour ~splitlong = - (* Input: X in X6 or (X5, X6) if splitlong - Result: N in X7 - Temporaries: S in X8, Y in X9 *) + (* Input: X in X7 or (X5, X7) if splitlong + Result: N in X8 + Temporaries: S in X6, Y in X9 *) let lbl1 = new_label() in let lbl2 = new_label() in (* N := bitsize of X's type (32 or 64) *) - expand_loadimm32 X7 (coqint_of_camlint + expand_loadimm32 X8 (coqint_of_camlint (if sixtyfour || splitlong then 64l else 32l)); (* S := initial shift amount (16 or 32) *) - expand_loadimm32 X8 (coqint_of_camlint (if sixtyfour then 32l else 16l)); + expand_loadimm32 X6 (coqint_of_camlint (if sixtyfour then 32l else 16l)); if splitlong then begin (* if (Xlow == 0) goto lbl1 *) emit (Pbeqw(X X5, X0, lbl1)); (* N := 32 *) - expand_loadimm32 X7 (coqint_of_camlint 32l); + expand_loadimm32 X8 (coqint_of_camlint 32l); (* X := Xlow *) - emit (Pmv(X6, X5)) + emit (Pmv(X7, X5)) end; (* lbl1: *) emit (Plabel lbl1); (* Y := X >> S *) - emit (if sixtyfour then Pslll(X9, X X6, X X8) else Psllw(X9, X X6, X X8)); + emit (if sixtyfour then Pslll(X9, X X7, X X6) else Psllw(X9, X X7, X X6)); (* if (Y == 0) goto lbl2 *) emit (if sixtyfour then Pbeql(X X9, X0, lbl2) else Pbeqw(X X9, X0, lbl2)); (* N := N - S *) - emit (Psubw(X7, X X7, X X8)); + emit (Psubw(X8, X X8, X X6)); (* X := Y *) - emit (Pmv(X6, X9)); + emit (Pmv(X7, X9)); (* lbl2: *) emit (Plabel lbl2); (* S := S / 2 *) - emit (Psrliw(X8, X X8, _1)); + emit (Psrliw(X6, X X6, _1)); (* if (S != 0) goto lbl1; *) - emit (Pbnew(X X8, X0, lbl1)); + emit (Pbnew(X X6, X0, lbl1)); (* N := N - most significant bit of X *) - emit (if sixtyfour then Psrlil(X6, X X6, coqint_of_camlint 63l) - else Psrliw(X6, X X6, coqint_of_camlint 31l)); - emit (Psubw(X7, X X7, X X6)) + emit (if sixtyfour then Psrlil(X7, X X7, coqint_of_camlint 63l) + else Psrliw(X7, X X7, coqint_of_camlint 31l)); + emit (Psubw(X8, X X8, X X7)) (* Handling of compiler-inlined builtins *) @@ -570,33 +570,33 @@ let expand_builtin_inline name args res = expand_bswap64 res a1 | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))], BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (ah = X6 && al = X5 && rh = X5 && rl = X6); + assert (ah = X7 && al = X5 && rh = X5 && rl = X7); expand_bswap32 X5 X5; - expand_bswap32 X6 X6 + expand_bswap32 X7 X7 (* Count zeros *) | "__builtin_clz", [BA(IR a)], BR(IR res) -> - assert (a = X5 && res = X7); + assert (a = X5 && res = X8); expand_clz ~sixtyfour:false ~splitlong:false | "__builtin_clzl", [BA(IR a)], BR(IR res) -> - assert (a = X5 && res = X7); + assert (a = X5 && res = X8); expand_clz ~sixtyfour:Archi.ptr64 ~splitlong:false | "__builtin_clzll", [BA(IR a)], BR(IR res) -> - assert (a = X5 && res = X7); + assert (a = X5 && res = X8); expand_clz ~sixtyfour:true ~splitlong:false | "__builtin_clzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> - assert (al = X5 && ah = X6 && res = X7); + assert (al = X5 && ah = X7 && res = X8); expand_clz ~sixtyfour:false ~splitlong:true | "__builtin_ctz", [BA(IR a)], BR(IR res) -> - assert (a = X6 && res = X7); + assert (a = X7 && res = X8); expand_ctz ~sixtyfour:false ~splitlong:false | "__builtin_ctzl", [BA(IR a)], BR(IR res) -> - assert (a = X6 && res = X7); + assert (a = X7 && res = X8); expand_ctz ~sixtyfour:Archi.ptr64 ~splitlong:false | "__builtin_ctzll", [BA(IR a)], BR(IR res) -> - assert (a = X6 && res = X7); + assert (a = X7 && res = X8); expand_ctz ~sixtyfour:true ~splitlong:false | "__builtin_ctzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> - assert (al = X5 && ah = X6 && res = X7); + assert (al = X5 && ah = X7 && res = X8); expand_ctz ~sixtyfour:false ~splitlong:true (* Float arithmetic *) | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 798dad9f6d..520341324a 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -815,7 +815,8 @@ Local Transparent destroyed_by_op. traceEq. (* match states *) econstructor; eauto. - apply agree_set_other; auto with asmgen. + eapply agree_exten; eauto. intros. + Simpl. Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* Mbuiltin *) diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index eeaae3c45e..4035e0636e 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -34,7 +34,7 @@ Require Import AST Machregs Locations. Definition is_callee_save (r: mreg) : bool := match r with - | R5 | R6 | R7 => false + | R5 | 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 @@ -47,7 +47,7 @@ Definition is_callee_save (r: mreg) : bool := end. Definition int_caller_save_regs := - R5 :: R6 :: R7 :: + R5 :: R7 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: R28 :: R29 :: R30 :: nil. @@ -71,14 +71,14 @@ Definition float_callee_save_regs := 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_int_reg := R5. (**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 - | R5 | R6 | R7 | R8 | R9 | R10 | R11 + | R5 | 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 diff --git a/riscV/Machregs.v b/riscV/Machregs.v index 89fa37b025..a9679095f8 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -40,7 +40,7 @@ Require Import Op. Inductive mreg: Type := (** Allocatable integer regs. *) - | R5: mreg | R6: mreg | R7: mreg + | R5: mreg | R7: mreg | R8: mreg | R9: mreg | R10: mreg | R11: mreg | R12: mreg | R13: mreg | R14: mreg | R15: mreg | R16: mreg | R17: mreg | R18: mreg | R19: mreg @@ -62,7 +62,7 @@ Proof. decide equality. Defined. Global Opaque mreg_eq. Definition all_mregs := - R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 + R5 :: R7 :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 @@ -87,7 +87,7 @@ Global Instance Finite_mreg : Finite mreg := { Definition mreg_type (r: mreg): typ := match r with - | R5 | R6 | R7 | R8 | R9 | R10 | R11 + | R5 | R7 | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 => if Archi.ptr64 then Tany64 else Tany32 @@ -105,22 +105,22 @@ Module IndexedMreg <: INDEXED_TYPE. Definition eq := mreg_eq. Definition index (r: mreg): positive := match r with - | R5 => 1 | R6 => 2 | R7 => 3 - | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7 - | R12 => 8 | R13 => 9 | R14 => 10 | R15 => 11 - | R16 => 12 | R17 => 13 | R18 => 14 | R19 => 15 - | R20 => 16 | R21 => 17 | R22 => 18 | R23 => 19 - | R24 => 20 | R25 => 21 | R26 => 22 | R27 => 23 - | R28 => 24 | R29 => 25 | R30 => 26 - - | F0 => 28 | F1 => 29 | F2 => 30 | F3 => 31 - | F4 => 32 | F5 => 33 | F6 => 34 | F7 => 35 - | F8 => 36 | F9 => 37 | F10 => 38 | F11 => 39 - | F12 => 40 | F13 => 41 | F14 => 42 | F15 => 43 - | F16 => 44 | F17 => 45 | F18 => 46 | F19 => 47 - | F20 => 48 | F21 => 49 | F22 => 50 | F23 => 51 - | F24 => 52 | F25 => 53 | F26 => 54 | F27 => 55 - | F28 => 56 | F29 => 57 | F30 => 58 | F31 => 59 + | R5 => 5 | R7 => 7 + | R8 => 8 | R9 => 9 | R10 => 10 | R11 => 11 + | R12 => 12 | R13 => 13 | R14 => 14 | R15 => 15 + | R16 => 16 | R17 => 17 | R18 => 18 | R19 => 19 + | R20 => 20 | R21 => 21 | R22 => 22 | R23 => 23 + | R24 => 24 | R25 => 25 | R26 => 26 | R27 => 27 + | R28 => 28 | R29 => 29 | R30 => 30 + + | F0 => 32 | F1 => 33 | F2 => 34 | F3 => 35 + | F4 => 36 | F5 => 37 | F6 => 38 | F7 => 39 + | F8 => 40 | F9 => 41 | F10 => 42 | F11 => 43 + | F12 => 44 | F13 => 45 | F14 => 46 | F15 => 47 + | F16 => 48 | F17 => 49 | F18 => 50 | F19 => 51 + | F20 => 52 | F21 => 53 | F22 => 54 | F23 => 55 + | F24 => 56 | F25 => 57 | F26 => 58 | F27 => 59 + | F28 => 60 | F29 => 61 | F30 => 62 | F31 => 63 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. @@ -136,7 +136,7 @@ Definition is_stack_reg (r: mreg) : bool := false. Local Open Scope string_scope. Definition register_names := - ("X5", R5) :: ("X6", R6) :: ("X7", R7) :: + ("X5", R5) :: ("X7", R7) :: ("X8", R8) :: ("X9", R9) :: ("X10", R10) :: ("X11", R11) :: ("X12", R12) :: ("X13", R13) :: ("X14", R14) :: ("X15", R15) :: ("X16", R16) :: ("X17", R17) :: ("X18", R18) :: ("X19", R19) :: @@ -193,16 +193,16 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_inline_asm txt sg clob => destroyed_by_clobber clob - | EF_memcpy sz al => R5 :: R6 :: R7 :: F0 :: nil + | EF_memcpy sz al => R5 :: R7 :: F0 :: nil | EF_builtin name sg => if string_dec name "__builtin_clz" || string_dec name "__builtin_clzl" || string_dec name "__builtin_clzll" then - R5 :: R8 :: R9 :: nil + R5 :: R9 :: nil else if string_dec name "__builtin_ctz" || string_dec name "__builtin_ctzl" || string_dec name "__builtin_ctzll" then - R6 :: R8 :: R9 :: nil + R7 :: R9 :: nil else nil | _ => nil @@ -223,21 +223,21 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list( match ef with | EF_builtin name sg => if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then - (Some R6 :: Some R5 :: nil, Some R5 :: Some R6 :: nil) + (Some R7 :: Some R5 :: nil, Some R5 :: Some R7 :: nil) else if string_dec name "__builtin_clz" || string_dec name "__builtin_clzl" then - (Some R5 :: nil, Some R7 :: nil) + (Some R5 :: nil, Some R8 :: nil) else if string_dec name "__builtin_clzll" then if Archi.ptr64 - then (Some R5 :: nil, Some R7 :: nil) - else (Some R6 :: Some R5 :: nil, Some R7 :: nil) + then (Some R5 :: nil, Some R8 :: nil) + else (Some R7 :: Some R5 :: nil, Some R8 :: nil) else if string_dec name "__builtin_ctz" || string_dec name "__builtin_ctzl" then - (Some R6 :: nil, Some R7 :: nil) + (Some R7 :: nil, Some R8 :: nil) else if string_dec name "__builtin_ctzll" then if Archi.ptr64 - then (Some R6 :: nil, Some R7 :: nil) - else (Some R6 :: Some R5 :: nil, Some R7 :: nil) + then (Some R7 :: nil, Some R8 :: nil) + else (Some R7 :: Some R5 :: nil, Some R8 :: nil) else (nil, nil) | _ => diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index d8137f84dc..5980ee8a9d 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -320,7 +320,7 @@ module Target : TARGET = | Pj_l(l) -> fprintf oc " j %a\n" print_label l | Pj_s(s, sg) -> - fprintf oc " j %a\n" symbol s + fprintf oc " tail %a\n" symbol s | Pj_r(r, sg) -> fprintf oc " jr %a\n" ireg r | Pjal_s(s, sg) -> From b14d831ec89f5451fd72f338369e54873045cc34 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Gourdin?= Date: Thu, 23 Jun 2022 11:01:02 +0200 Subject: [PATCH 2/2] new proposition using a jump macro this time --- riscV/Asm.v | 5 ++- riscV/Asmexpand.ml | 76 +++++++++++++++++++++--------------------- riscV/Conventions1.v | 8 ++--- riscV/Machregs.v | 60 ++++++++++++++++----------------- riscV/TargetPrinter.ml | 2 +- 5 files changed, 75 insertions(+), 76 deletions(-) diff --git a/riscV/Asm.v b/riscV/Asm.v index 35f1486673..2346e7aac0 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -752,7 +752,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out goto_label f l rs m | Pj_s s sg => Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) - #X6 <- Vundef + #X31 <- Vundef ) m | Pj_r r sg => Next (rs#PC <- (rs#r)) m @@ -1003,7 +1003,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Definition preg_of (r: mreg) : preg := match r with - | R5 => X5 | R7 => X7 + | R5 => X5 | R6 => X6 | R7 => X7 | R8 => X8 | R9 => X9 | R10 => X10 | R11 => X11 | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15 | R16 => X16 | R17 => X17 | R18 => X18 | R19 => X19 @@ -1182,7 +1182,6 @@ Qed. Definition data_preg (r: preg) : bool := match r with | IR RA => false - | IR X6 => false | IR X31 => false | IR _ => true | FR _ => true diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index e59487e019..ab0e6fee0c 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -469,85 +469,85 @@ let expand_bswap64 d s = re-rolled as a loop to produce more compact code. *) let expand_clz ~sixtyfour ~splitlong = - (* Input: X in X5 or (X5, X7) if splitlong - Result: N in X8 - Temporaries: S in X6, Y in X9 *) + (* Input: X in X5 or (X5, X6) if splitlong + Result: N in X7 + Temporaries: S in X8, Y in X9 *) let lbl1 = new_label() in let lbl2 = new_label() in (* N := bitsize of X's type (32 or 64) *) - expand_loadimm32 X8 (coqint_of_camlint + expand_loadimm32 X7 (coqint_of_camlint (if sixtyfour || splitlong then 64l else 32l)); (* S := initial shift amount (16 or 32) *) - expand_loadimm32 X6 (coqint_of_camlint (if sixtyfour then 32l else 16l)); + expand_loadimm32 X8 (coqint_of_camlint (if sixtyfour then 32l else 16l)); if splitlong then begin (* if (Xhigh == 0) goto lbl1 *) - emit (Pbeqw(X X7, X0, lbl1)); + emit (Pbeqw(X X6, X0, lbl1)); (* N := 32 *) - expand_loadimm32 X8 (coqint_of_camlint 32l); + expand_loadimm32 X7 (coqint_of_camlint 32l); (* X := Xhigh *) - emit (Pmv(X5, X7)) + emit (Pmv(X5, X6)) end; (* lbl1: *) emit (Plabel lbl1); (* Y := X >> S *) - emit (if sixtyfour then Psrll(X9, X X5, X X6) else Psrlw(X9, X X5, X X6)); + emit (if sixtyfour then Psrll(X9, X X5, X X8) else Psrlw(X9, X X5, X X8)); (* if (Y == 0) goto lbl2 *) emit (if sixtyfour then Pbeql(X X9, X0, lbl2) else Pbeqw(X X9, X0, lbl2)); (* N := N - S *) - emit (Psubw(X8, X X8, X X6)); + emit (Psubw(X7, X X7, X X8)); (* X := Y *) emit (Pmv(X5, X9)); (* lbl2: *) emit (Plabel lbl2); (* S := S / 2 *) - emit (Psrliw(X6, X X6, _1)); + emit (Psrliw(X8, X X8, _1)); (* if (S != 0) goto lbl1; *) - emit (Pbnew(X X6, X0, lbl1)); + emit (Pbnew(X X8, X0, lbl1)); (* N := N - X *) - emit (Psubw(X8, X X8, X X5)) + emit (Psubw(X7, X X7, X X5)) (* Count trailing zeros. Algorithm 5-14 from Hacker's Delight, re-rolled as a loop to produce more compact code. *) let expand_ctz ~sixtyfour ~splitlong = - (* Input: X in X7 or (X5, X7) if splitlong - Result: N in X8 - Temporaries: S in X6, Y in X9 *) + (* Input: X in X6 or (X5, X6) if splitlong + Result: N in X7 + Temporaries: S in X8, Y in X9 *) let lbl1 = new_label() in let lbl2 = new_label() in (* N := bitsize of X's type (32 or 64) *) - expand_loadimm32 X8 (coqint_of_camlint + expand_loadimm32 X7 (coqint_of_camlint (if sixtyfour || splitlong then 64l else 32l)); (* S := initial shift amount (16 or 32) *) - expand_loadimm32 X6 (coqint_of_camlint (if sixtyfour then 32l else 16l)); + expand_loadimm32 X8 (coqint_of_camlint (if sixtyfour then 32l else 16l)); if splitlong then begin (* if (Xlow == 0) goto lbl1 *) emit (Pbeqw(X X5, X0, lbl1)); (* N := 32 *) - expand_loadimm32 X8 (coqint_of_camlint 32l); + expand_loadimm32 X7 (coqint_of_camlint 32l); (* X := Xlow *) - emit (Pmv(X7, X5)) + emit (Pmv(X6, X5)) end; (* lbl1: *) emit (Plabel lbl1); (* Y := X >> S *) - emit (if sixtyfour then Pslll(X9, X X7, X X6) else Psllw(X9, X X7, X X6)); + emit (if sixtyfour then Pslll(X9, X X6, X X8) else Psllw(X9, X X6, X X8)); (* if (Y == 0) goto lbl2 *) emit (if sixtyfour then Pbeql(X X9, X0, lbl2) else Pbeqw(X X9, X0, lbl2)); (* N := N - S *) - emit (Psubw(X8, X X8, X X6)); + emit (Psubw(X7, X X7, X X8)); (* X := Y *) - emit (Pmv(X7, X9)); + emit (Pmv(X6, X9)); (* lbl2: *) emit (Plabel lbl2); (* S := S / 2 *) - emit (Psrliw(X6, X X6, _1)); + emit (Psrliw(X8, X X8, _1)); (* if (S != 0) goto lbl1; *) - emit (Pbnew(X X6, X0, lbl1)); + emit (Pbnew(X X8, X0, lbl1)); (* N := N - most significant bit of X *) - emit (if sixtyfour then Psrlil(X7, X X7, coqint_of_camlint 63l) - else Psrliw(X7, X X7, coqint_of_camlint 31l)); - emit (Psubw(X8, X X8, X X7)) + emit (if sixtyfour then Psrlil(X6, X X6, coqint_of_camlint 63l) + else Psrliw(X6, X X6, coqint_of_camlint 31l)); + emit (Psubw(X7, X X7, X X6)) (* Handling of compiler-inlined builtins *) @@ -570,33 +570,33 @@ let expand_builtin_inline name args res = expand_bswap64 res a1 | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))], BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (ah = X7 && al = X5 && rh = X5 && rl = X7); + assert (ah = X6 && al = X5 && rh = X5 && rl = X6); expand_bswap32 X5 X5; - expand_bswap32 X7 X7 + expand_bswap32 X6 X6 (* Count zeros *) | "__builtin_clz", [BA(IR a)], BR(IR res) -> - assert (a = X5 && res = X8); + assert (a = X5 && res = X7); expand_clz ~sixtyfour:false ~splitlong:false | "__builtin_clzl", [BA(IR a)], BR(IR res) -> - assert (a = X5 && res = X8); + assert (a = X5 && res = X7); expand_clz ~sixtyfour:Archi.ptr64 ~splitlong:false | "__builtin_clzll", [BA(IR a)], BR(IR res) -> - assert (a = X5 && res = X8); + assert (a = X5 && res = X7); expand_clz ~sixtyfour:true ~splitlong:false | "__builtin_clzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> - assert (al = X5 && ah = X7 && res = X8); + assert (al = X5 && ah = X6 && res = X7); expand_clz ~sixtyfour:false ~splitlong:true | "__builtin_ctz", [BA(IR a)], BR(IR res) -> - assert (a = X7 && res = X8); + assert (a = X6 && res = X7); expand_ctz ~sixtyfour:false ~splitlong:false | "__builtin_ctzl", [BA(IR a)], BR(IR res) -> - assert (a = X7 && res = X8); + assert (a = X6 && res = X7); expand_ctz ~sixtyfour:Archi.ptr64 ~splitlong:false | "__builtin_ctzll", [BA(IR a)], BR(IR res) -> - assert (a = X7 && res = X8); + assert (a = X6 && res = X7); expand_ctz ~sixtyfour:true ~splitlong:false | "__builtin_ctzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> - assert (al = X5 && ah = X7 && res = X8); + assert (al = X5 && ah = X6 && res = X7); expand_ctz ~sixtyfour:false ~splitlong:true (* Float arithmetic *) | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 4035e0636e..eeaae3c45e 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -34,7 +34,7 @@ Require Import AST Machregs Locations. Definition is_callee_save (r: mreg) : bool := match r with - | R5 | R7 => 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 @@ -47,7 +47,7 @@ Definition is_callee_save (r: mreg) : bool := end. Definition int_caller_save_regs := - R5 :: R7 :: + R5 :: R6 :: R7 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: R28 :: R29 :: R30 :: nil. @@ -71,14 +71,14 @@ Definition float_callee_save_regs := Definition destroyed_at_call := List.filter (fun r => negb (is_callee_save r)) all_mregs. -Definition dummy_int_reg := R5. (**r Used in [Coloring]. *) +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 - | R5 | R7 | R8 | R9 | R10 | R11 + | 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 diff --git a/riscV/Machregs.v b/riscV/Machregs.v index a9679095f8..89fa37b025 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -40,7 +40,7 @@ Require Import Op. Inductive mreg: Type := (** Allocatable integer regs. *) - | R5: mreg | R7: mreg + | R5: mreg | R6: mreg | R7: mreg | R8: mreg | R9: mreg | R10: mreg | R11: mreg | R12: mreg | R13: mreg | R14: mreg | R15: mreg | R16: mreg | R17: mreg | R18: mreg | R19: mreg @@ -62,7 +62,7 @@ Proof. decide equality. Defined. Global Opaque mreg_eq. Definition all_mregs := - R5 :: R7 :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 + 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 :: F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 @@ -87,7 +87,7 @@ Global Instance Finite_mreg : Finite mreg := { Definition mreg_type (r: mreg): typ := match r with - | R5 | R7 | R8 | R9 | R10 | R11 + | 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 => if Archi.ptr64 then Tany64 else Tany32 @@ -105,22 +105,22 @@ Module IndexedMreg <: INDEXED_TYPE. Definition eq := mreg_eq. Definition index (r: mreg): positive := match r with - | R5 => 5 | R7 => 7 - | R8 => 8 | R9 => 9 | R10 => 10 | R11 => 11 - | R12 => 12 | R13 => 13 | R14 => 14 | R15 => 15 - | R16 => 16 | R17 => 17 | R18 => 18 | R19 => 19 - | R20 => 20 | R21 => 21 | R22 => 22 | R23 => 23 - | R24 => 24 | R25 => 25 | R26 => 26 | R27 => 27 - | R28 => 28 | R29 => 29 | R30 => 30 - - | F0 => 32 | F1 => 33 | F2 => 34 | F3 => 35 - | F4 => 36 | F5 => 37 | F6 => 38 | F7 => 39 - | F8 => 40 | F9 => 41 | F10 => 42 | F11 => 43 - | F12 => 44 | F13 => 45 | F14 => 46 | F15 => 47 - | F16 => 48 | F17 => 49 | F18 => 50 | F19 => 51 - | F20 => 52 | F21 => 53 | F22 => 54 | F23 => 55 - | F24 => 56 | F25 => 57 | F26 => 58 | F27 => 59 - | F28 => 60 | F29 => 61 | F30 => 62 | F31 => 63 + | R5 => 1 | R6 => 2 | R7 => 3 + | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7 + | R12 => 8 | R13 => 9 | R14 => 10 | R15 => 11 + | R16 => 12 | R17 => 13 | R18 => 14 | R19 => 15 + | R20 => 16 | R21 => 17 | R22 => 18 | R23 => 19 + | R24 => 20 | R25 => 21 | R26 => 22 | R27 => 23 + | R28 => 24 | R29 => 25 | R30 => 26 + + | F0 => 28 | F1 => 29 | F2 => 30 | F3 => 31 + | F4 => 32 | F5 => 33 | F6 => 34 | F7 => 35 + | F8 => 36 | F9 => 37 | F10 => 38 | F11 => 39 + | F12 => 40 | F13 => 41 | F14 => 42 | F15 => 43 + | F16 => 44 | F17 => 45 | F18 => 46 | F19 => 47 + | F20 => 48 | F21 => 49 | F22 => 50 | F23 => 51 + | F24 => 52 | F25 => 53 | F26 => 54 | F27 => 55 + | F28 => 56 | F29 => 57 | F30 => 58 | F31 => 59 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. @@ -136,7 +136,7 @@ Definition is_stack_reg (r: mreg) : bool := false. Local Open Scope string_scope. Definition register_names := - ("X5", R5) :: ("X7", R7) :: + ("X5", R5) :: ("X6", R6) :: ("X7", R7) :: ("X8", R8) :: ("X9", R9) :: ("X10", R10) :: ("X11", R11) :: ("X12", R12) :: ("X13", R13) :: ("X14", R14) :: ("X15", R15) :: ("X16", R16) :: ("X17", R17) :: ("X18", R18) :: ("X19", R19) :: @@ -193,16 +193,16 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_inline_asm txt sg clob => destroyed_by_clobber clob - | EF_memcpy sz al => R5 :: R7 :: F0 :: nil + | EF_memcpy sz al => R5 :: R6 :: R7 :: F0 :: nil | EF_builtin name sg => if string_dec name "__builtin_clz" || string_dec name "__builtin_clzl" || string_dec name "__builtin_clzll" then - R5 :: R9 :: nil + R5 :: R8 :: R9 :: nil else if string_dec name "__builtin_ctz" || string_dec name "__builtin_ctzl" || string_dec name "__builtin_ctzll" then - R7 :: R9 :: nil + R6 :: R8 :: R9 :: nil else nil | _ => nil @@ -223,21 +223,21 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list( match ef with | EF_builtin name sg => if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then - (Some R7 :: Some R5 :: nil, Some R5 :: Some R7 :: nil) + (Some R6 :: Some R5 :: nil, Some R5 :: Some R6 :: nil) else if string_dec name "__builtin_clz" || string_dec name "__builtin_clzl" then - (Some R5 :: nil, Some R8 :: nil) + (Some R5 :: nil, Some R7 :: nil) else if string_dec name "__builtin_clzll" then if Archi.ptr64 - then (Some R5 :: nil, Some R8 :: nil) - else (Some R7 :: Some R5 :: nil, Some R8 :: nil) + then (Some R5 :: nil, Some R7 :: nil) + else (Some R6 :: Some R5 :: nil, Some R7 :: nil) else if string_dec name "__builtin_ctz" || string_dec name "__builtin_ctzl" then - (Some R7 :: nil, Some R8 :: nil) + (Some R6 :: nil, Some R7 :: nil) else if string_dec name "__builtin_ctzll" then if Archi.ptr64 - then (Some R7 :: nil, Some R8 :: nil) - else (Some R7 :: Some R5 :: nil, Some R8 :: nil) + then (Some R6 :: nil, Some R7 :: nil) + else (Some R6 :: Some R5 :: nil, Some R7 :: nil) else (nil, nil) | _ => diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 5980ee8a9d..0bb45d99aa 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -320,7 +320,7 @@ module Target : TARGET = | Pj_l(l) -> fprintf oc " j %a\n" print_label l | Pj_s(s, sg) -> - fprintf oc " tail %a\n" symbol s + fprintf oc " jump %a, x31\n" symbol s | Pj_r(r, sg) -> fprintf oc " jr %a\n" ireg r | Pjal_s(s, sg) ->