File tree Expand file tree Collapse file tree 1 file changed +8
-3
lines changed
Expand file tree Collapse file tree 1 file changed +8
-3
lines changed Original file line number Diff line number Diff line change @@ -91,7 +91,9 @@ Definition is_float_reg (r: mreg) :=
9191
9292(** How to use registers for register allocation.
9393 We favor the use of caller-save registers, using callee-save registers
94- only when no caller-save is available. *)
94+ only when no caller-save is available.
95+ We favor the use of registers x8 to x15, as they enable more compact
96+ encodings of instructions (with the C extension of the ISA). *)
9597
9698Record alloc_regs := mk_alloc_regs {
9799 preferred_int_regs: list mreg;
@@ -101,8 +103,11 @@ Record alloc_regs := mk_alloc_regs {
101103}.
102104
103105Definition allocatable_registers (_: unit) :=
104- {| preferred_int_regs := int_caller_save_regs;
105- remaining_int_regs := int_callee_save_regs;
106+ {| preferred_int_regs :=
107+ R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: nil;
108+ remaining_int_regs :=
109+ R5 :: R6 :: R7 :: R16 :: R17 :: R28 :: R29 :: R30 ::
110+ int_callee_save_regs;
106111 preferred_float_regs := float_caller_save_regs;
107112 remaining_float_regs := float_callee_save_regs |}.
108113
You can’t perform that action at this time.
0 commit comments