diff options
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 33 |
1 files changed, 16 insertions, 17 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index bed3c040..41ea0979 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -38,13 +38,12 @@ Require Import Op. assembly-code generator [Asmgen]. *) -(* FIXME - no R31 *) Inductive mreg: Type := (* Allocatable General Purpose regs. *) - | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R9 - | R10 (* R11 to R14 res *) | R15 | R16 | R17 | R18 | R19 + | R0 | R1 | R2 | R3 | R4 | 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 | R32 | R33 | R34 | R35 | R36 | R37 | R38 | R39 + | R30 | R31 (* | 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. @@ -54,10 +53,10 @@ Proof. decide equality. Defined. Global Opaque mreg_eq. Definition all_mregs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9 - :: R10 :: R15 :: R16 :: R17 :: R18 :: R19 + R0 :: R1 :: R2 :: R3 :: R4 :: 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 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 + :: R30 :: R31 (* :: 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. @@ -86,12 +85,12 @@ Module IndexedMreg <: INDEXED_TYPE. Definition index (r: mreg): positive := match r with | R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5 - | R5 => 6 | R6 => 7 | R7 => 8 | R9 => 10 - | R10 => 11 - | R15 => 16 | R16 => 17 | R17 => 18 | R18 => 19 | R19 => 20 + | R5 => 6 | R6 => 7 | R7 => 8 | R8 => 9 | R9 => 10 + | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 *) | R14 => 15 + | R15 => 16 (* | R16 => 17 *) | R17 => 18 | R18 => 19 | R19 => 20 | R20 => 21 | R21 => 22 | R22 => 23 | R23 => 24 | R24 => 25 | R25 => 26 | R26 => 27 | R27 => 28 | R28 => 29 | R29 => 30 - | R30 => 31 | R32 => 33 | R33 => 34 | R34 => 35 + | R30 => 31 | R31 => 32 (* | R32 => 33 *) | R33 => 34 | R34 => 35 | R35 => 36 | R36 => 37 | R37 => 38 | R38 => 39 | R39 => 40 | R40 => 41 | R41 => 42 | R42 => 43 | R43 => 44 | R44 => 45 | R45 => 46 | R46 => 47 | R47 => 48 | R48 => 49 | R49 => 50 @@ -115,12 +114,12 @@ Local Open Scope string_scope. Definition register_names := ("R0" , R0) :: ("R1" , R1) :: ("R2" , R2) :: ("R3" , R3) :: ("R4" , R4) - :: ("R5" , R5) :: ("R6" , R6) :: ("R7" , R7) :: ("R9" , R9) - :: ("R10", R10) - :: ("R15", R15) :: ("R16", R16) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19) + :: ("R5" , R5) :: ("R6" , R6) :: ("R7" , R7) :: ("R8" , R8) :: ("R9" , R9) + :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) *) :: ("R14", R14) + :: ("R15", R15) (* :: ("R16", R16) *) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) :: ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) :: ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: ("R29", R29) - :: ("R30", R30) :: ("R32", R32) :: ("R33", R33) :: ("R34", R34) + :: ("R30", R30) :: ("R31", R31) (* :: ("R32", R32) *) :: ("R33", R33) :: ("R34", R34) :: ("R35", R35) :: ("R36", R36) :: ("R37", R37) :: ("R38", R38) :: ("R39", R39) :: ("R40", R40) :: ("R41", R41) :: ("R42", R42) :: ("R43", R43) :: ("R44", R44) :: ("R45", R45) :: ("R46", R46) :: ("R47", R47) :: ("R48", R48) :: ("R49", R49) @@ -175,9 +174,9 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := Definition destroyed_by_setstack (ty: typ): list mreg := nil. -Definition destroyed_at_function_entry: list mreg := R10 :: nil. +Definition destroyed_at_function_entry: list mreg := R14 :: nil. -Definition temp_for_parent_frame: mreg := R10. (* FIXME - and R8 ?? *) +Definition temp_for_parent_frame: mreg := R14. (* FIXME - ?? *) Definition destroyed_at_indirect_call: list mreg := nil. (* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *) |